| Imports | Exports |
|---|---|
Name: module_info/2 Module: module_information Name: ajoin/2 Module: tools Name: flatten/2 Module: tools |
adapt_for_eventb(Term,Term) :- atomic(Term).
adapt_for_eventb(Term,Result) :-
Term=..[F|Args],
replace_functor(F,NewFunctor),
maplist(adapt_for_eventb,Args,NewArgs),
Result=..[NewFunctor|NewArgs].
Calls:
Name: =../2 |
|
Name: maplist/3 |
Module: foo_error |
Name: replace_functor/2 |
Module: sequent_prover |
Name: atomic/1 |
Called:
Name: parse_input/2 |
Module: sequent_prover |
add_hyp(Hyp,Hyps0,NewHyps) :- append(Hyps0,[Hyp],Hyps1), without_duplicates(Hyps1,NewHyps).
Calls:
Name: without_duplicates/2 |
Module: sequent_prover |
Name: append/3 |
Called:
Name: trans1/3 |
Module: sequent_prover |
Name: trans2/3 |
Module: sequent_prover |
Name: extract_disjuncts/5 |
Module: sequent_prover |
Name: symb_trans/4 |
Module: sequent_prover |
add_hyps(NewHyps,Hyps,SHyps) :- append(Hyps,NewHyps,All), without_duplicates(All,SHyps).
Calls:
Name: without_duplicates/2 |
Module: sequent_prover |
Name: append/3 |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
add_hyps(Hyp1,Hyp2,Hyps0,NewHyps) :- append(Hyps0,[Hyp1,Hyp2],Hyps1), without_duplicates(Hyps1,NewHyps).
Calls:
Name: without_duplicates/2 |
Module: sequent_prover |
Name: append/3 |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
add_meta_info(Key,Info,Value,Info1) :-
get_meta_info(Key,Info,Content),
Content \= [], !,
Old=..[Key,Content],
New=..[Key,[Value|Content]],
select(Old,Info,New,Info1).
add_meta_info(Key,Info,Value,[El|Info]) :- El=..[Key,[Value]].
Calls:
Name: =../2 |
|
Name: select/4 |
Module: foo_error |
Name: ! |
|
Name: \=/2 |
|
Name: get_meta_info/3 |
Module: sequent_prover |
Called:
Name: trans/4 |
Module: sequent_prover |
add_pos(_,Sequent,Sequent,[]) :- !.
add_pos(Hyps,InnerSequent,NewSequent,[PO|R]) :- add_pos(Hyps,sequent(Hyps,PO,InnerSequent),NewSequent,R).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: ! |
Called:
Name: add_wd_pos/4 |
Module: sequent_prover |
add_wd_pos(Hyps,POs,Sequent,NewSequent) :-
reverse(POs,List),
add_pos(Hyps,Sequent,NewSequent,List).
Calls:
Name: add_pos/4 |
Module: sequent_prover |
Name: reverse/2 |
Module: foo_error |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
all_in_set([E],S,Hyps) :- member_hyps(member(E,S),Hyps).
all_in_set([E|R],S,Hyps) :- member_hyps(member(E,S),Hyps), all_in_set(R,S,Hyps).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: member_hyps/2 |
Module: sequent_prover |
Called:
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
all_map_to([couple(_,F)],E) :- equal_terms(E,F), !.
all_map_to([couple(_,F)|T],E) :- equal_terms(E,F), all_map_to(T,E).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: equal_terms/2 |
Module: sequent_prover |
Name: ! |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
all_pairs(L,Pairs) :- findall([X,Y], (combination(L,[X,Y])), Pairs).
Calls:
Name: findall/3 |
and_empty(C,Conj,Op) :- C=..[Op,A,B], and_empty(A,ConjA,Op), and_empty(B,ConjB,Op), !, Conj = conjunct(ConjA,ConjB).
and_empty(A,equal(A,empty_set),_).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
and_equal_type(intersection(A,B),Ty,Conj) :- and_equal_type(A,Ty,L), and_equal_type(B,Ty,R), !, Conj = conjunct(L,R).
and_equal_type(A,Ty,equal(A,Ty)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule_with_info/4 |
Module: sequent_prover |
and_imp(C,R,Conj,Op) :- C=..[Op,A,B], and_imp(A,R,ConjA,Op), and_imp(B,R,ConjB,Op), !, Conj = conjunct(ConjA,ConjB).
and_imp(A,R,implication(R,A),conjunct).
and_imp(A,R,implication(A,R),disjunct).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
animation_function_result(state(success,_),[((1,1),'Proof succeeded.')]).
animation_function_result(state(Sequent,_),Matrix) :-
Sequent = sequent(_,_,Cont),
cont_length(Cont,LCont),
findall(((RowNr,ColNr),Cell), (cell_content(RowNr,ColNr,Sequent,Cell,LCont)), Matrix).
Calls:
Name: findall/3 |
|
Name: cont_length/2 |
Module: sequent_prover |
Name: =/2 |
animation_image_right_click_transition(Row,1,mon_deselect(Row)).
animation_image_right_click_transition(Row,1,Trans,state(sequent(Hyps,Goal,Cont),Info)) :- nth1(Row,Hyps,Hyp),
find_transitions(sequent([Hyp],Goal,Cont),Info,Transitions),
find_transitions(sequent([],Goal,Cont),Info,TransitionsG),
member(Trans,Transitions),
Trans \= mon_deselect(_),
\+ member(Trans,TransitionsG).
animation_image_right_click_transition(Row,1,Trans,state(sequent(Hyps,Goal,Cont),Info)) :-
length(Hyps,LHyps),
Row is LHyps + 2,
find_transitions(sequent([],Goal,Cont),Info,Transitions),
member(Trans,Transitions).
Calls:
Name: member/2 |
|
Name: find_transitions/3 |
Module: sequent_prover |
Name: is/2 |
|
Name: length/2 |
|
Name: not/1 |
|
Name: \=/2 |
|
Name: nth1/3 |
Module: foo_error |
append_sequents(sequent(Hyps,Goal,Cont),InnerCont,sequent(Hyps,Goal,InnerCont)) :-
cont_length(Cont,0).
append_sequents(sequent(Hyps,Goal,Cont),InnerCont,sequent(Hyps,Goal,Sequent)) :-
append_sequents(Cont,InnerCont,Sequent).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: cont_length/2 |
Module: sequent_prover |
Called:
Name: extract_disjuncts/5 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
append_to_op(C,R,Res,Op) :-
C=..[Op,A,B],
Inner=..[Op,R,A],!,
append_to_op(B,Inner,Res,Op).
append_to_op(B,R,C,Op) :- C=..[Op,R,B].
Calls:
Name: =../2 |
|
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: ! |
Called:
Name: reorder/3 |
Module: sequent_prover |
atom_int_concat(X,I,XI) :-
atom_codes(X,CX),
number_codes(I,CI),
append(CX,CI,COut),
atom_codes(XI,COut).
Calls:
Name: atom_codes/2 |
|
Name: append/3 |
|
Name: number_codes/2 |
Called:
Name: range/4 |
Module: sequent_prover |
axiom(hyp,Hyps,Goal) :- member_hyps(Goal,Hyps).
axiom(hyp_or,Hyps,Goal) :- member_of(disjunct,P,Goal), member_hyps(P,Hyps).
axiom(false_hyp,Hyps,_Goal) :- member_hyps(falsity,Hyps).
axiom(true_goal,_,truth).
axiom(Rule,_Hyps,Goal) :- axiom_wo_hyps(Goal,Rule).
axiom(cntr,Hyps,_) :-
member(P,Hyps),
(NotP = negation(P) ; negate(P,NotP)),
select(P,Hyps,Hyps0),
member_hyps(NotP,Hyps0).
axiom(fin_rel,Hyps,finite(Fun)) :-
member_hyps(member(Fun,FunType),Hyps),
is_rel(FunType,_,Dom,Ran),
member_hyps(finite(Dom),Hyps),
member_hyps(finite(Ran),Hyps).
axiom(fin_l_lower_bound,Hyps,exists([N],forall([X],member(X,S),LessEq))) :-
member_hyps(finite(S),Hyps),
is_less_eq(LessEq,N,X).
axiom(fin_l_upper_bound,Hyps,exists([N],forall([X],member(X,S),LessEq))) :-
member_hyps(finite(S),Hyps),
is_less_eq(LessEq,X,N).
axiom(derive_goal,Hyps,Goal) :- derive_goal(Hyps,Goal), \+ axiom(hyp,Hyps,Goal).
axiom(p2,Hyps,member(Add,Nat)) :-
is_natural_set(Nat),
member(member(N,Nat),Hyps),
equal_terms(Add,add(N,1)).
axiom(p2_,Hyps,member(Sub,Nat)) :-
is_natural_set(Nat),
member(L,Hyps),
is_less(L,0,N),
equal_terms(Sub,minus(N,1)).
axiom(inc,Hyps,Goal) :-
member(L,Hyps),
is_less(L,N,M),
equal_terms(Goal,less_equal(add(N,1),M)).
axiom(dec,Hyps,Goal) :-
member(L,Hyps),
is_less_eq(L,N,M),
equal_terms(Goal,less(minus(N,1),M)).
Calls:
Name: equal_terms/2 |
Module: sequent_prover |
Name: is_less_eq/3 |
Module: sequent_prover |
Name: member/2 |
|
Name: is_less/3 |
Module: sequent_prover |
Name: is_natural_set/1 |
Module: sequent_prover |
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: not/1 |
|
Name: derive_goal/2 |
Module: sequent_prover |
Name: member_hyps/2 |
Module: sequent_prover |
Name: is_rel/4 |
Module: sequent_prover |
Name: select/3 |
Module: foo_error |
Name: negate/2 |
Module: sequent_prover |
Name: =/2 |
|
Name: axiom_wo_hyps/2 |
Module: sequent_prover |
Name: member_of/3 |
Module: sequent_prover |
Called:
Name: trans1/3 |
Module: sequent_prover |
axiom2(fun_goal(member(F,FType)),Hyps,member(F,PFType)) :-
is_fun(PFType,partial,_,_),
member_hyps(member(F,FType),Hyps),
is_fun(FType,_,_,_).
Calls:
Name: is_fun/4 |
Module: sequent_prover |
Name: member_hyps/2 |
Module: sequent_prover |
Called:
Name: trans/4 |
Module: sequent_prover |
axiom_wo_hyps(true,true_goal).
axiom_wo_hyps(eq(E,E),eql).
Called:
Name: axiom/3 |
Module: sequent_prover |
bwd_to_fwd_comp(ring(R,S),Res) :-
bwd_to_fwd_comp(R,R2),
bwd_to_fwd_comp(S,S2),
Res = composition(S2,R2).
bwd_to_fwd_comp(X,X) :- X \= ring(_,_).
Calls:
Name: \=/2 |
|
Name: =/2 |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Called:
Name: simp_rule/4 |
Module: sequent_prover |
cell_content(Row,1,sequent(Hyps,_,_),Cell,_) :- nth1(Row,Hyps,RowHyp), translate_term(RowHyp,Cell).
cell_content(Row,1,sequent(Hyps,_,_),'---------------------',_) :- length(Hyps,LHyps), Row is LHyps + 1.
cell_content(Row,1,sequent(Hyps,Goal,_),Cell,_) :- length(Hyps,LHyps), Row is LHyps + 2, translate_term(Goal,Cell).
cell_content(Row,Col,Sequent,Cell,LCont) :-
extract_continuations(Sequent,LCont,Cont,Col),
cell_content(Row,1,Cont,Cell,LCont).
Calls:
Name: RECURSIVE_CALL/5 |
Module: sequent_prover |
Name: extract_continuations/4 |
Module: sequent_prover |
Name: translate_term/2 |
Module: sequent_prover |
Name: is/2 |
|
Name: length/2 |
|
Name: nth1/3 |
Module: foo_error |
change_sign(L,NL,Nr) :- remove_minus(L,NL,Nr), Nr > 0.
Calls:
Name: >/2 |
|
Name: remove_minus/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
collect_component('$'(X),OList,NList,_) :- !,
append(OList,[X],NList).
collect_component(X,OList,NList,_) :-
atomic(X),!,
append(OList,[X],NList).
collect_component(C,OList,NList,T) :-
C=..[T,A,B],!,
collect_components(A,B,OList,NList,T).
collect_component(X,OList,NList,_) :-
list_representation(X,[],L1),
append(OList,L1,NList).
Calls:
Name: append/3 |
|
Name: list_representation/3 |
Module: sequent_prover |
Name: collect_components/5 |
Module: sequent_prover |
Name: ! |
|
Name: =../2 |
|
Name: atomic/1 |
Called:
Name: collect_components/5 |
Module: sequent_prover |
collect_components(A,B,OList,NList,T) :-
collect_component(A,OList,L1,T),
collect_component(B,L1,NList,T).
Calls:
Name: collect_component/4 |
Module: sequent_prover |
Called:
Name: list_representation/3 |
Module: sequent_prover |
Name: collect_component/4 |
Module: sequent_prover |
collect_divisor(div(A, B), [LA, Div]) :-
A \= div(_,_), !,
list_representation(A,[LA]),
(B = 1 -> Div = [] ;
list_representation(B,[LB]), Div = [LB]).
collect_divisor(div(A, B), [Divident, NDivisors]) :-
collect_divisor(A, [Divident, Divisors]),
list_representation(B,LB),
append(Divisors, LB, NDivisors).
Calls:
Name: append/3 |
|
Name: list_representation/2 |
Module: sequent_prover |
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: =/2 |
|
Name: ->/3 |
|
Name: ! |
|
Name: \=/2 |
Called:
Name: list_representation/3 |
Module: sequent_prover |
collect_subtrahend(minus(A, B), [LA, Sub]) :-
A \= minus(_,_), !,
list_representation(A,[LA]),
(B = 0 -> Sub = [] ;
list_representation(B,[LB]), Sub = [LB]).
collect_subtrahend(minus(A, B), [Minuend, NSubtrahends]) :-
collect_subtrahend(A, [Minuend, Subtrahends]),
list_representation(B,LB),
append(Subtrahends, LB, NSubtrahends).
Calls:
Name: append/3 |
|
Name: list_representation/2 |
Module: sequent_prover |
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: =/2 |
|
Name: ->/3 |
|
Name: ! |
|
Name: \=/2 |
Called:
Name: list_representation/3 |
Module: sequent_prover |
combination(_,[]).
combination([X|T],[X|C]) :- combination(T,C).
combination([_|T],[X|C]) :- combination(T,[X|C]).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
comparable(G1,G2) :- G1=..[T1,_,_], G2=..[T2,_,_], comparison(T1), comparison(T2).
comparable(G1,G2) :- G1=..[F,P], G2=..[F,Q], !, comparable(P,Q).
comparable(G1,G2) :- functor(G1,F,_), functor(G2,F,_).
Calls:
Name: functor/3 |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
|
Name: =../2 |
|
Name: comparison/1 |
Module: sequent_prover |
Called:
Name: member_hyps/2 |
Module: sequent_prover |
comparison(equal).
comparison(greater).
comparison(greater_equal).
comparison(less).
comparison(less_equal).
comparison(not_equal).
Called:
Name: simp_rule/3 |
Module: sequent_prover |
Name: is_transitive/2 |
Module: sequent_prover |
Name: comparable/2 |
Module: sequent_prover |
compute(Expr,Res) :- evaluate(Expr,Res), Expr \= Res.
Calls:
Name: \=/2 |
|
Name: evaluate/2 |
Module: sequent_prover |
Called:
Name: simp_rule/6 |
Module: sequent_prover |
conjoin(truth,X,R) :- !, R=X.
conjoin(X,truth,R) :- !, R=X.
conjoin(X,Y,conjunct(X,Y)).
Calls:
Name: =/2 |
|
Name: ! |
Called:
Name: select_conjunct/3 |
Module: sequent_prover |
conjoin(E,X,R,Op) :- neutral_element(Op,E), !, R=X.
conjoin(X,E,R,Op) :- neutral_element(Op,E), !, R=X.
conjoin(X,Y,C,Op) :- C=..[Op,X,Y].
Calls:
Name: =../2 |
|
Name: =/2 |
|
Name: ! |
|
Name: neutral_element/2 |
Module: sequent_prover |
Called:
Name: select_conjunct/3 |
Module: sequent_prover |
cont_length(sequent(_,_,C),R) :- !, cont_length(C,R1), R is R1+1.
cont_length(_,0).
Calls:
Name: is/2 |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
Called:
Name: append_sequents/3 |
Module: sequent_prover |
Name: prop/2 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
| Module: sequent_prover | |
Name: extract_continuations/4 |
Module: sequent_prover |
convert_map_to([couple(X,Y)],[couple(Y,X)]) :- !.
convert_map_to([couple(X,Y)|T],[couple(Y,X)|R]) :- convert_map_to(T,R).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
create_descr(Rule,T,Descr) :- translate_term(T,TS),
ajoin([Rule,' (',TS,')'],Descr).
Calls:
Name: ajoin/2 |
Module: tools |
Name: translate_term/2 |
Module: sequent_prover |
Called:
Name: trans/4 |
Module: sequent_prover |
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
Name: simp_rule/6 |
Module: sequent_prover |
create_descr(Rule,S,T,Descr) :- translate_term(T,TS),
ajoin([Rule,' (',S,',',TS,')'],Descr).
Calls:
Name: ajoin/2 |
Module: tools |
Name: translate_term/2 |
Module: sequent_prover |
Called:
Name: trans/4 |
Module: sequent_prover |
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
Name: simp_rule/6 |
Module: sequent_prover |
derive_goal(Hyps,Goal) :-
is_less(Goal,A,B),
lower_bound(Hyps,Bound1,B),
upper_bound(Hyps,A,Bound2),
Bound1 > Bound2, !.
derive_goal(Hyps,Goal) :-
is_less_eq(Goal,A,B),
lower_bound(Hyps,Bound1,B),
upper_bound(Hyps,A,Bound2),
Bound1 >= Bound2, !.
derive_goal(Hyps,not_equal(A,B)) :- derive_goal(Hyps,greater(A,B)).
derive_goal(Hyps,not_equal(A,B)) :- derive_goal(Hyps,less(A,B)).
derive_goal(Hyps,Goal) :- is_transitive(Hyps,Goal).
Calls:
Name: is_transitive/2 |
Module: sequent_prover |
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
|
Name: >=/2 |
|
Name: upper_bound/3 |
Module: sequent_prover |
Name: lower_bound/3 |
Module: sequent_prover |
Name: is_less_eq/3 |
Module: sequent_prover |
Name: >/2 |
|
Name: is_less/3 |
Module: sequent_prover |
Called:
Name: axiom/3 |
Module: sequent_prover |
distri(C,Res,Op1,Op2) :-
C=..[Op1,A,B],
(X = A ; X = B),
functor(X,Op2,2),
distribute_op(C,X,Op1,Op2,Res).
Calls:
Name: distribute_op/5 |
Module: sequent_prover |
Name: functor/3 |
|
Name: =/2 |
|
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distri_l(C,Res,Op1,Op2) :-
C=..[Op1,X,_],
functor(X,Op2,2),
distribute_op(C,X,Op1,Op2,Res).
Calls:
Name: distribute_op/5 |
Module: sequent_prover |
Name: functor/3 |
|
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distri_l(C,Res,Op1,Op2,Op3) :-
C=..[Op1,X,_],
functor(X,Op2,2),
op_to_list(X,L,Op2),
distribute(C,X,L,CN,Op1),
list_to_op(CN,Res,Op3).
Calls:
Name: list_to_op/3 |
Module: sequent_prover |
Name: distribute/5 |
Module: sequent_prover |
Name: op_to_list/3 |
Module: sequent_prover |
Name: functor/3 |
|
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distri_r(C,Res,Op1,Op2) :-
C=..[Op1,_,X],
functor(X,Op2,2),
distribute_op(C,X,Op1,Op2,Res).
Calls:
Name: distribute_op/5 |
Module: sequent_prover |
Name: functor/3 |
|
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distri_reverse(C,U,Op) :- C=..[Op,A,B], distri_reverse(A,UA,Op), distri_reverse(B,UB,Op), !, U=..[Op,UA,UB].
distri_reverse(A,reverse(A),_).
Calls:
Name: =../2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distri_reverse_reverse(C,U,Op) :- C=..[Op,A,B], distri_reverse_reverse(A,UA,Op), distri_reverse_reverse(B,UB,Op), !, U=..[Op,UB,UA].
distri_reverse_reverse(A,reverse(A),_).
Calls:
Name: =../2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distri_setminus(C,Res) :-
C = set_subtraction(_,X),
X = union(_,_),
select_op(X,C,NewC,set_subtraction),
op_to_list(NewC,CL,set_subtraction),
op_to_list(X,L,union),
append(CL,L,L2),
list_to_op(L2,Res,set_subtraction).
Calls:
Name: list_to_op/3 |
Module: sequent_prover |
Name: append/3 |
|
Name: op_to_list/3 |
Module: sequent_prover |
Name: select_op/4 |
Module: sequent_prover |
Name: =/2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distri_union(union(A,B),Union,Op) :- distri_union(A,L,Op), distri_union(B,R,Op), !, Union = union(L,R).
distri_union(A,C,Op) :- C=..[Op,A].
Calls:
Name: =../2 |
|
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distribute(_,_,[],[],_).
distribute(C,X,[D|T],[N|R],Op) :- select_op(X,C,D,N,Op), distribute(C,X,T,R,Op).
Calls:
Name: RECURSIVE_CALL/5 |
Module: sequent_prover |
Name: select_op/5 |
Module: sequent_prover |
Called:
Name: distri_l/5 |
Module: sequent_prover |
Name: distribute_op/5 |
Module: sequent_prover |
distribute_exists(X,disjunct(A,B),Disj) :- distribute_exists(X,A,DisjA), distribute_exists(X,B,DisjB), !, Disj = disjunct(DisjA,DisjB).
distribute_exists(X,P,exists(X,P)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distribute_forall(X,P,conjunct(A,B),Conj) :-
distribute_forall(X,P,A,ConjA),
distribute_forall(X,P,B,ConjB),!,
Conj = conjunct(ConjA,ConjB).
distribute_forall(X,P,A,forall(X,P,A)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
distribute_op(C,X,Op1,Op2,Res) :-
op_to_list(X,L,Op2),
distribute(C,X,L,CN,Op1),
list_to_op(CN,Res,Op2).
Calls:
Name: list_to_op/3 |
Module: sequent_prover |
Name: distribute/5 |
Module: sequent_prover |
Name: op_to_list/3 |
Module: sequent_prover |
Called:
Name: distri_r/4 |
Module: sequent_prover |
Name: distri_l/4 |
Module: sequent_prover |
Name: distri/4 |
Module: sequent_prover |
el_of_op(Term,X,Op) :- Term=..[Op,A,B], !, (el_of_op(A,X,Op) ; el_of_op(B,X,Op)).
el_of_op(P,P,_).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: ! |
|
Name: =../2 |
Called:
Name: member_of/3 |
Module: sequent_prover |
equal_length(L1,L2) :- L1 = [c(A1,_)], L2 = [c(A2,_)], !, same_length(A1, A2).
equal_length([_],[_]).
Calls:
Name: same_length/2 |
Module: foo_error |
Name: ! |
|
Name: =/2 |
Called:
Name: equal_terms/2 |
Module: sequent_prover |
Name: member_hyps/2 |
Module: sequent_prover |
equal_lists(L1,L2) :- sort_list(L1,SL1), sort_list(L2,SL2), SL1 = SL2.
Calls:
Name: =/2 |
|
Name: sort_list/2 |
Module: sequent_prover |
Called:
Name: equal_terms/2 |
Module: sequent_prover |
equal_op(L1,L2) :- L1 = [c(_,T1)], L2 = [c(_,T2)], !, T1 = T2.
equal_op([E1],[E2]) :- E1 \= [c(_,_)], E2 \= [c(_,_)].
Calls:
Name: \=/2 |
|
Name: =/2 |
|
Name: ! |
Called:
Name: equal_terms/2 |
Module: sequent_prover |
equal_terms(X,X) :- !.
equal_terms(X,Y) :-
ground(X),
ground(Y),
list_representation(X,LX),
list_representation(Y,LY),
equal_op(LX,LY),
equal_length(LX,LY),
equal_lists(LX,LY).
Calls:
Name: equal_lists/2 |
Module: sequent_prover |
Name: equal_length/2 |
Module: sequent_prover |
Name: equal_op/2 |
Module: sequent_prover |
Name: list_representation/2 |
Module: sequent_prover |
Name: ground/1 |
|
Name: ! |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
Name: select_op/5 |
Module: sequent_prover |
Name: all_map_to/2 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
Name: without_duplicates/3 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
Name: trans2/3 |
Module: sequent_prover |
Name: is_negation/2 |
Module: sequent_prover |
Name: is_true/1 |
Module: sequent_prover |
Name: select_op/4 |
Module: sequent_prover |
Name: rewrite/4 |
Module: sequent_prover |
equiv(equal(A,B),equal(B,A)).
equiv(not_equal(A,B),not_equal(B,A)).
equiv(greater(A,B),less(B,A)).
equiv(less(A,B),greater(B,A)).
equiv(greater_equal(A,B),less_equal(B,A)).
equiv(less_equal(A,B),greater_equal(B,A)).
Called:
Name: is_transitive_aux/5 |
Module: sequent_prover |
Name: member_hyps/2 |
Module: sequent_prover |
evaluate(I,I) :- number(I).
evaluate(add(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI + NewJ.
evaluate(minus(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI - NewJ.
evaluate(multiplication(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI * NewJ.
evaluate(div(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), J =\= 0, Res is NewI // NewJ.
evaluate(modulo(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), J =\= 0, Res is NewI mod NewJ.
evaluate(power_of(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI ^ NewJ.
Calls:
Name: is/2 |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: =\=/2 |
|
Name: number/1 |
Called:
Name: compute/2 |
Module: sequent_prover |
extract_continuations(sequent(_,_,Cont),LCont,Cont,ColNr) :-
cont_length(Cont,ActualLCont),
ColNr is LCont - ActualLCont + 2.
extract_continuations(sequent(_,_,Cont),LCont,FoundCont,ColNr) :-
extract_continuations(Cont,LCont,FoundCont,ColNr).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: is/2 |
|
Name: cont_length/2 |
Module: sequent_prover |
Called:
Name: cell_content/5 |
Module: sequent_prover |
extract_disjuncts(Q,Hyps0,Goal,Cont,sequent(Hyps,Goal,Cont)) :- Q \= disjunct(_,_), add_hyp(Q,Hyps0,Hyps).
extract_disjuncts(disjunct(L,R),Hyps0,Goal,Cont,LRSequent) :-
extract_disjuncts(L,Hyps0,Goal,success,LSequent),
extract_disjuncts(R,Hyps0,Goal,Cont,RSequent),
append_sequents(LSequent,RSequent,LRSequent).
Calls:
Name: append_sequents/3 |
Module: sequent_prover |
Name: RECURSIVE_CALL/5 |
Module: sequent_prover |
Name: add_hyp/3 |
Module: sequent_prover |
Name: \=/2 |
Called:
Name: trans2/3 |
Module: sequent_prover |
find_transitions(Sequent,Info,Trans) :-
findall(T,(trans(T,state(Sequent,Info),_) ; trans(T,state(Sequent,Info),_,_)),TransL),
remove_dups(TransL,Trans).
Calls:
Name: remove_dups/2 |
Module: foo_error |
Name: findall/3 |
Called:
| Module: sequent_prover |
finite_intersection(intersection(A,B),Disj) :- finite_intersection(A,DisjA), finite_intersection(B,DisjB), !, Disj = disjunct(DisjA,DisjB).
finite_intersection(S,finite(S)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Called:
Name: trans1/3 |
Module: sequent_prover |
finite_union(union(A,B),Conj) :- finite_union(A,ConjA), finite_union(B,ConjB), !, Conj = conjunct(ConjA,ConjB).
finite_union(S,finite(S)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
free_identifiers(exists(Ids,P),Res) :- !, free_identifiers(P,Free), list_subtract(Free,Ids,Res).
free_identifiers(Term,Res) :-
(Term = forall(Ids,P,E)
; Term = event_b_comprehension_set(Ids,E,P)
; Term = quantified_intersection(Ids,P,E)
; Term = quantified_union(Ids,P,E)), !,
free_identifiers(implication(P,E),FreeImp), list_subtract(FreeImp,Ids,Res).
free_identifiers(Term,[]) :- atomic(Term), !.
free_identifiers(Term,[Term]) :- Term = '$'(E), atomic(E), !.
free_identifiers(C,Res) :-
C =.. [_|Args],
maplist(free_identifiers,Args,L),
append(L,Res).
Calls:
Name: append/2 |
Module: foo_error |
Name: maplist/3 |
Module: foo_error |
Name: =../2 |
|
Name: ! |
|
Name: atomic/1 |
|
Name: =/2 |
|
Name: list_subtract/3 |
Module: sequent_prover |
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
func_id(f).
func_id(g).
func_id(h).
Called:
Name: possible_function/1 |
Module: sequent_prover |
get_hyp(Hyps,Index,Hyp) :-
atom_codes(Index,C),
number_codes(Nr,C),
nth1(Nr,Hyps,Hyp).
Calls:
Name: nth1/3 |
Module: foo_error |
Name: number_codes/2 |
|
Name: atom_codes/2 |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
get_meta_info(Key,Info,Content) :- El=..[Key,Content], memberchk(El,Info), !.
get_meta_info(_,_,[]).
Calls:
Name: ! |
|
Name: memberchk/2 |
|
Name: =../2 |
Called:
Name: type_expression/2 |
Module: sequent_prover |
Name: get_scope/3 |
Module: sequent_prover |
Name: add_meta_info/4 |
Module: sequent_prover |
Name: remove_meta_info/4 |
Module: sequent_prover |
get_normalised_bexpr(Expr,NormExpr) :-
translate:transform_raw(Expr,TExpr),
well_def_hyps:normalize_predicate(TExpr,NormExpr).
Calls:
Name: normalize_predicate/2 |
Module: well_def_hyps |
Name: transform_raw/2 |
Module: translate |
Called:
Name: load_from_po_file/5 |
Module: sequent_prover |
get_scope(Hyps,Info,Scope) :-
get_meta_info(des_hyps,Info,DHyps),
maplist(get_typed_identifiers,DHyps,L1),
maplist(get_typed_identifiers,Hyps,L2),
append(L1,L2,IdsTypes),
flatten(IdsTypes,FIdsTypes),
select_types(FIdsTypes,SList),
Scope = [identifier(SList)].
Calls:
Name: =/2 |
|
Name: select_types/2 |
Module: sequent_prover |
Name: flatten/2 |
Module: tools |
Name: append/3 |
|
Name: maplist/3 |
Module: foo_error |
Name: get_meta_info/3 |
Module: sequent_prover |
Called:
Name: get_wd_pos/4 |
Module: sequent_prover |
Name: of_integer_type/3 |
Module: sequent_prover |
Name: get_wd_pos_of_expr/4 |
Module: sequent_prover |
get_typed_ast(NormExpr,TExpr) :-
well_def_hyps:convert_norm_expr_to_raw(NormExpr,RawExpr),
translate:transform_raw(RawExpr,TExpr).
Calls:
Name: transform_raw/2 |
Module: translate |
| Module: well_def_hyps |
Called:
Name: prove_predicate/2 |
Module: sequent_prover |
Name: symb_trans/4 |
Module: sequent_prover |
get_typed_identifiers(NormExpr,[]) :- with_ids(NormExpr,_), !.
get_typed_identifiers(NormExpr,List) :-
well_def_hyps:convert_norm_expr_to_raw(NormExpr,ParsedRaw),
bmachine:b_type_open_predicate(_,ParsedRaw,[],TypedPred,[]), TypedPred = b(forall(List,_,_),_,_), !.
get_typed_identifiers(NormExpr,List) :-
used_identifiers(NormExpr,Ids),
maplist(any_type,Ids,List).
Calls:
Name: maplist/3 |
Module: foo_error |
Name: used_identifiers/2 |
Module: sequent_prover |
Name: ! |
|
Name: =/2 |
|
Name: b_type_open_predicate/5 |
Module: bmachine |
| Module: well_def_hyps | |
Name: with_ids/2 |
Module: sequent_prover |
get_wd_pos(NormExpr,Scope,POs) :-
well_def_hyps:convert_norm_expr_to_raw(NormExpr,ParsedRaw),
bmachine:b_type_check_raw_expr(ParsedRaw,Scope,TypedPred,open(_)),
well_def_hyps:empty_hyps(H),
well_def_analyser:compute_all_wd_pos(TypedPred,H,[],TPOs),
maplist(well_def_hyps:normalize_predicate,TPOs,POs).
Calls:
Name: maplist/3 |
Module: foo_error |
Name: compute_all_wd_pos/4 |
Module: well_def_analyser |
Name: empty_hyps/1 |
Module: well_def_hyps |
Name: b_type_check_raw_expr/4 |
Module: bmachine |
| Module: well_def_hyps |
Called:
Name: get_wd_pos/4 |
Module: sequent_prover |
Name: get_wd_pos_of_expr/4 |
Module: sequent_prover |
get_wd_pos(NormExpr,Hyps,Info,POs) :-
get_scope(Hyps,Info,Scope),
get_wd_pos(NormExpr,Scope,POs).
Calls:
Name: get_wd_pos/3 |
Module: sequent_prover |
Name: get_scope/3 |
Module: sequent_prover |
Called:
Name: get_wd_pos/4 |
Module: sequent_prover |
Name: get_wd_pos_of_expr/4 |
Module: sequent_prover |
get_wd_pos_of_expr(NormExpr,Hyps,Info,POs) :-
get_scope(Hyps,Info,Scope),
possible_identifier(Y),
\+ in_scope(Y,Scope), !,
get_wd_pos(equal('$'(Y),NormExpr),Scope,POs).
Calls:
Name: get_wd_pos/3 |
Module: sequent_prover |
Name: ! |
|
Name: in_scope/2 |
Module: sequent_prover |
Name: not/1 |
|
Name: possible_identifier/1 |
Module: sequent_prover |
Name: get_scope/3 |
Module: sequent_prover |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
identifier(x).
identifier(y).
identifier(z).
Called:
Name: possible_identifier/1 |
Module: sequent_prover |
image_union(F,union(A,B),Union) :- image_union(F,A,L), image_union(F,B,R), !, Union = union(L,R).
image_union(F,A,image(F,A)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
implies(X,X).
implies(c(L,equal),c(L,greater_equal)).
implies(c(L,equal),c(RL,greater_equal)) :- reverse(L,RL).
implies(c(L,greater),c(L,greater_equal)).
implies(c(L,greater),c(L,not_equal)).
Calls:
Name: reverse/2 |
Module: foo_error |
Called:
Name: list_implies/2 |
Module: sequent_prover |
in_scope(Id,[identifier(List)]) :- memberchk(b(identifier(Id),_,[]),List).
Calls:
Name: memberchk/2 |
Called:
Name: get_wd_pos_of_expr/4 |
Module: sequent_prover |
is_empty(Expr,Term) :- is_equality(Expr,Term,empty_set).
is_empty(Expr,Term) :- Expr = subset(Term,empty_set).
Calls:
Name: =/2 |
|
Name: is_equality/3 |
Module: sequent_prover |
Called:
Name: simp_rule_with_info/4 |
Module: sequent_prover |
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
is_equality(equal(A,B),A,B).
is_equality(equal(B,A),A,B).
Called:
Name: lower_bound/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: is_empty/2 |
Module: sequent_prover |
Name: simp_rule_with_info/4 |
Module: sequent_prover |
Name: upper_bound/3 |
Module: sequent_prover |
is_equivalence(equivalence(A,B),A,B).
is_equivalence(equivalence(B,A),A,B).
Called:
Name: simp_rule/3 |
Module: sequent_prover |
is_fun(partial_function(DOM,RAN),partial,DOM,RAN).
is_fun(partial_injection(DOM,RAN),partial,DOM,RAN).
is_fun(partial_surjection(DOM,RAN),partial,DOM,RAN).
is_fun(partial_bijection(DOM,RAN),partial,DOM,RAN).
is_fun(total_function(DOM,RAN),total,DOM,RAN).
is_fun(total_injection(DOM,RAN),total,DOM,RAN).
is_fun(total_surjection(DOM,RAN),total,DOM,RAN).
is_fun(total_bijection(DOM,RAN),total,DOM,RAN).
Called:
Name: axiom2/3 |
Module: sequent_prover |
Name: is_rel/4 |
Module: sequent_prover |
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
is_inj(partial_injection(DOM,RAN),DOM,RAN).
is_inj(partial_bijection(DOM,RAN),DOM,RAN).
is_inj(total_injection(DOM,RAN),DOM,RAN).
is_inj(total_bijection(DOM,RAN),DOM,RAN).
Called:
Name: trans1/3 |
Module: sequent_prover |
Name: simp_rule_with_info/4 |
Module: sequent_prover |
is_integer_set(integer_set).
is_integer_set('INTEGER').
Called:
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
Name: type_expression/2 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
is_inter(intersection(A,B),A,B). % TODO: extend to nested inter
is_inter(intersection(B,A),A,B).
Called:
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
is_less(less(P,Q),P,Q).
is_less(greater(Q,P),P,Q).
Called:
Name: derive_goal/2 |
Module: sequent_prover |
Name: lower_bound/3 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: upper_bound/3 |
Module: sequent_prover |
is_less_eq(less_equal(P,Q),P,Q).
is_less_eq(greater_equal(Q,P),P,Q).
Called:
Name: simp_rule/3 |
Module: sequent_prover |
Name: upper_bound/3 |
Module: sequent_prover |
Name: derive_goal/2 |
Module: sequent_prover |
Name: lower_bound/3 |
Module: sequent_prover |
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
Name: is_true/1 |
Module: sequent_prover |
is_minus(NE,E) :- number(NE), NE < 0, E is abs(NE) ; NE = unary_minus(E).
Calls:
Name: =/2 |
|
Name: is/2 |
|
Name: </2 |
|
Name: number/1 |
Called:
Name: remove_minus/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
is_natural1_set(natural1_set).
is_natural1_set('NATURAL1').
Called:
Name: is_true/1 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
is_natural_set(natural_set).
is_natural_set('NATURAL').
Called:
Name: simp_rule/3 |
Module: sequent_prover |
Name: is_true/1 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
is_negation(Q,negation(P)) :- equal_terms(P,Q).
Calls:
Name: equal_terms/2 |
Module: sequent_prover |
Called:
Name: simp_rule/4 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
is_no_equality(negation(equal(A,B)),A,B).
is_no_equality(negation(equal(B,A)),A,B).
is_no_equality(not_equal(A,B),A,B).
is_no_equality(not_equal(B,A),A,B).
Called:
Name: trans1/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: simp_rule_with_hyps/5 |
Module: sequent_prover |
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
is_rel(F,Type,DOM,RAN) :- is_fun(F,Type,DOM,RAN).
is_rel(relations(DOM,RAN),partial,DOM,RAN).
is_rel(total_relation(DOM,RAN),total,DOM,RAN).
is_rel(surjection_relation(DOM,RAN),partial,DOM,RAN).
is_rel(total_surjection_relation(DOM,RAN),total,DOM,RAN).
Calls:
Name: is_fun/4 |
Module: sequent_prover |
Called:
Name: simp_rule_with_info/4 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
is_surj(total_bijection(DOM,RAN),DOM,RAN).
is_surj(total_surjection(DOM,RAN),DOM,RAN).
is_surj(partial_surjection(DOM,RAN),DOM,RAN).
is_surj(surjection_relation(DOM,RAN),DOM,RAN).
is_surj(total_surjection_relation(DOM,RAN),DOM,RAN).
Called:
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
is_transitive(Hyps,Goal) :-
Goal=..[F,L,R],
comparison(F),
F \= not_equal,
is_transitive_aux(Hyps,F,L,R,[]).
Calls:
Name: is_transitive_aux/5 |
Module: sequent_prover |
Name: \=/2 |
|
Name: comparison/1 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: derive_goal/2 |
Module: sequent_prover |
is_transitive_aux(Hyps,F,L,R,_) :-
Ex=..[F,L,R],
(member(Ex,Hyps) ; equiv(Ex,G2), member(G2,Hyps)).
is_transitive_aux(Hyps,F,L,R,Visited) :-
Ex=..[F,L,M],
(member(Ex,Hyps) ; equiv(Ex,G2), member(G2,Hyps)),
\+ member(M,Visited),
is_transitive_aux(Hyps,F,M,R,[L|Visited]).
Calls:
Name: RECURSIVE_CALL/5 |
Module: sequent_prover |
Name: member/2 |
|
Name: not/1 |
|
Name: equiv/2 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: is_transitive/2 |
Module: sequent_prover |
is_true(equal(X,Y)) :- equal_terms(X,Y).
is_true(less_equal(X,Y)) :- equal_terms(X,Y).
is_true(greater_equal(X,Y)) :- equal_terms(X,Y).
is_true(negation(falsity)).
is_true(subset(empty_set,_)).
is_true(subset(S,T)) :- equal_terms(S,T).
is_true(implication(_P,truth)).
is_true(implication(falsity,_P)).
is_true(implication(P,Q)) :- equal_terms(P,Q).
is_true(equivalence(P,Q)) :- equal_terms(P,Q).
is_true(member(card(_S),Nat)) :- is_natural_set(Nat).
is_true(P) :- is_less_eq(P,0,card(_S)).
is_true(member(min(S),T)) :- equal_terms(S,T).
is_true(member(max(S),T)) :- equal_terms(S,T).
is_true(member(couple(E,F), event_b_identity)) :- equal_terms(E,F).
is_true(finite(bool_set)).
is_true(finite(set_extension(_))).
is_true(finite(interval(_,_))).
is_true(finite(empty_set)).
is_true(member(I,Nat)) :- is_natural_set(Nat), number(I), I >= 0.
is_true(member(I,Nat)) :- is_natural1_set(Nat), number(I), I >= 1.
Calls:
Name: >=/2 |
|
Name: number/1 |
|
Name: is_natural1_set/1 |
Module: sequent_prover |
Name: is_natural_set/1 |
Module: sequent_prover |
Name: equal_terms/2 |
Module: sequent_prover |
Name: is_less_eq/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
last_overwrite(overwrite(_,B),Res) :- !, last_overwrite(B,Res).
last_overwrite(B,B).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
list_implies([],[]).
list_implies([H1|T1], [H2|T2]) :-
implies(H1,H2),
list_implies(T1,T2).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: implies/2 |
Module: sequent_prover |
Called:
Name: stronger_list/2 |
Module: sequent_prover |
list_intersection([],_,[]).
list_intersection([Z|T],Ids,[Z|R]) :- member(Z,Ids), list_intersection(T,Ids,R).
list_intersection([Z|T],Ids,R) :- \+ member(Z,Ids), list_intersection(T,Ids,R).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: member/2 |
|
Name: not/1 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
| Module: sequent_prover |
list_representation(C,L) :- list_representation(C,[],L).
Calls:
Name: list_representation/3 |
Module: sequent_prover |
Called:
Name: list_representation/4 |
Module: sequent_prover |
Name: list_representation/2 |
Module: sequent_prover |
Name: collect_component/4 |
Module: sequent_prover |
| Module: sequent_prover |
list_representation('$'(X),L,Res) :- !, Res=[X|L].
list_representation(less_equal(A,B),OList,Res) :- !, list_representation(B,A,OList,NList), Res=[c(NList,greater_equal)].
list_representation(greater_equal(A,B),OList,Res) :- !, list_representation(A,B,OList,NList), Res=[c(NList,greater_equal)].
list_representation(less(A,B),OList,Res) :- !, list_representation(B,A,OList,NList), Res=[c(NList,greater)].
list_representation(greater(A,B),OList,Res) :- !, list_representation(A,B,OList,NList), Res=[c(NList,greater)].
list_representation(minus(A,B),OList,NList) :- !,
collect_subtrahend(minus(A,B),Subtraction),
Subtraction = [Minuend, Subtrahend],
exclude(zero, Subtrahend, NSubtrahend),
(NSubtrahend == [] -> NList = [Minuend] ;
append(OList,[c([Minuend, NSubtrahend],minus)],NList)).
list_representation(div(A,B),OList,NList) :- !,
collect_divisor(div(A,B),Division),
Division = [Divident, Divisor],
exclude(one, Divisor, NDivisor),
(NDivisor == [] -> NList = [Divident] ;
append(OList,[c([Divident, NDivisor],div)],NList)).
list_representation(C,OList,Res) :-
C=..[F,A,B],
member(F,[conjunct,disjunct,intersection,union]), !,
collect_components(A,B,OList,NList,F),
Res=[c(NList,F)].
list_representation(add(A,B),OList,Res) :- !,
collect_components(A,B,OList,NList,add),
exclude(zero, NList, NList2),
(NList2 == [] -> Res = [0] ;
NList2 \= [_]-> Res = [c(NList2,add)] ;
Res = NList2).
list_representation(multiplication(A,B),OList,Res) :- !,
collect_components(A,B,OList,NList,multiplication),
exclude(one, NList, NList2),
(member(0, NList2) -> Res = [0] ;
NList2 == [] -> Res = [1] ;
NList2 \= [_]-> Res = [c(NList2,multiplication)] ;
Res = NList2).
list_representation(set_extension(A),OList,Res) :- !, list_representation_of_list(A,OList,NList), sort(NList,S), Res=[c(S,set_extension)].
list_representation([A|T],OList,Res) :- !, list_representation_of_list([A|T],OList,NList), Res=[c(NList,list)].
list_representation(C,OList,Res) :- C=..[F,A], !, list_representation(A,OList,NList), Res=[c(NList,F)].
list_representation(C,OList,Res) :-
C=..[F,A,B],!,
list_representation(A,B,OList,NList), Res=[c(NList,F)].
list_representation(X,L,[X|L]) :- atomic(X).
Calls:
Name: atomic/1 |
|
Name: =/2 |
|
Name: list_representation/4 |
Module: sequent_prover |
Name: ! |
|
Name: =../2 |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
| Module: sequent_prover | |
Name: sort/2 |
|
Name: \=/2 |
|
Name: ->/3 |
|
Name: ==/2 |
|
Name: member/2 |
|
Name: exclude/3 |
Module: foo_error |
Name: collect_components/5 |
Module: sequent_prover |
Name: append/3 |
|
Name: collect_divisor/2 |
Module: sequent_prover |
Name: collect_subtrahend/2 |
Module: sequent_prover |
Called:
Name: list_representation/4 |
Module: sequent_prover |
Name: list_representation/2 |
Module: sequent_prover |
Name: collect_component/4 |
Module: sequent_prover |
| Module: sequent_prover |
list_representation(A,B,OList,L3) :-
list_representation(A,OList,L1),
list_representation(B,[],L2),
append(L1,L2,L3).
Calls:
Name: append/3 |
|
Name: list_representation/3 |
Module: sequent_prover |
Called:
Name: list_representation/4 |
Module: sequent_prover |
Name: list_representation/2 |
Module: sequent_prover |
Name: collect_component/4 |
Module: sequent_prover |
| Module: sequent_prover |
list_representation_of_list([],OList,OList).
list_representation_of_list([A|T],OList,NList) :- list_representation(A,OList,L1), list_representation_of_list(T,[],L2),append(L1,L2,NList).
Calls:
Name: append/3 |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: list_representation/3 |
Module: sequent_prover |
Called:
Name: list_representation/3 |
Module: sequent_prover |
list_subtract([],_,[]) :- !.
list_subtract([E|T],L,R) :- memberchk(E,L), !, list_subtract(T,L,R).
list_subtract([E|T],L,[E|R]) :- list_subtract(T,L,R).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: ! |
|
Name: memberchk/2 |
Called:
Name: free_identifiers/2 |
Module: sequent_prover |
list_to_op([A],A,_).
list_to_op([A,B|L],Res,Op) :- C=..[Op,A,B], list_to_op(L,C,Res,Op).
Calls:
Name: list_to_op/4 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: distri_setminus/2 |
Module: sequent_prover |
Name: remove_from_op/4 |
Module: sequent_prover |
Name: distri_l/5 |
Module: sequent_prover |
Name: simp_rule/5 |
Module: sequent_prover |
Name: distribute_op/5 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: remove_duplicates/3 |
Module: sequent_prover |
list_to_op([],C,C,_).
list_to_op([X|T],C,Res,Op) :- NC=..[Op,C,X], list_to_op(T,NC,Res,Op).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: distri_setminus/2 |
Module: sequent_prover |
Name: remove_from_op/4 |
Module: sequent_prover |
Name: distri_l/5 |
Module: sequent_prover |
Name: simp_rule/5 |
Module: sequent_prover |
Name: distribute_op/5 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: remove_duplicates/3 |
Module: sequent_prover |
load_from_po_file(File,Hyps,Goal,PO,[rawsets(RawSets)]) :-
disprover_test_runner:load_po_file(File),
disprover_test_runner:get_disprover_po(PO,Context,RawGoal,RawAllHyps,_RawSelHyps,_RodinStatus),
get_normalised_bexpr(RawGoal,Goal),
maplist(get_normalised_bexpr,RawAllHyps,Hyps),
bmachine_eventb:extract_ctx_sections(Context,_Name,_Extends,RawSets,_Constants,_AbstractConstants,_Axioms,_Theorems).
Calls:
Name: extract_ctx_sections/8 |
Module: bmachine_eventb |
Name: maplist/3 |
Module: foo_error |
Name: get_normalised_bexpr/2 |
Module: sequent_prover |
Name: get_disprover_po/6 |
Module: disprover_test_runner |
Name: load_po_file/1 |
Module: disprover_test_runner |
lower_bound(Hyps,B,X) :- member(L,Hyps), is_less_eq(L,B,X), number(B).
lower_bound(Hyps,B1,X) :- member(L,Hyps), is_less(L,B,X), number(B), B1 is B+1.
lower_bound(Hyps,B,X) :- member(Eq,Hyps), is_equality(Eq,B,X), number(B).
Calls:
Name: number/1 |
|
Name: is_equality/3 |
Module: sequent_prover |
Name: member/2 |
|
Name: is/2 |
|
Name: is_less/3 |
Module: sequent_prover |
Name: is_less_eq/3 |
Module: sequent_prover |
Called:
Name: derive_goal/2 |
Module: sequent_prover |
map_dom([couple(X,_)],[X]) :- !.
map_dom([couple(X,_)|T],[X|R]) :- map_dom(T,R).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
map_ran([couple(_,A)],[A]) :- !.
map_ran([couple(_,B)|T],[B|R]) :- map_ran(T,R).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
max_list([H|T],Max) :- number(H) -> max_list(T,H,Max) ; max_list(T,Max).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: max_list/3 |
Module: sequent_prover |
Name: number/1 |
|
Name: ->/3 |
Called:
Name: max_list/2 |
Module: sequent_prover |
max_list([],Max,Max).
max_list([H|T],Max0,Max) :-
number(H),!,
Max1 is max(H,Max0),
max_list(T,Max1,Max).
max_list([_|T],Max0,Max) :-
max_list(T,Max0,Max).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: is/2 |
|
Name: ! |
|
Name: number/1 |
Called:
Name: max_list/2 |
Module: sequent_prover |
member_couples(E,F,[Q],_,[member(couple(E,F),Q)]).
member_couples(E,F,[P|Q],[X|T],[member(couple(E,X),P)|R]) :- member_couples(X,F,Q,T,R).
Calls:
Name: RECURSIVE_CALL/5 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
member_hyps(Goal,Hyps) :-
(member(Goal,Hyps) -> true
; equiv(Goal,G2), member(G2,Hyps) -> true), !.
member_hyps(Goal,Hyps) :-
ground(Goal),
member(G2,Hyps),
comparable(Goal,G2),
list_representation(Goal,L1),
list_representation(G2,L2),
equal_length(L1,L2),
stronger_list(L2,L1).
Calls:
Name: stronger_list/2 |
Module: sequent_prover |
Name: equal_length/2 |
Module: sequent_prover |
Name: list_representation/2 |
Module: sequent_prover |
Name: comparable/2 |
Module: sequent_prover |
Name: member/2 |
|
Name: ground/1 |
|
Name: ! |
|
Name: true |
|
Name: equiv/2 |
Module: sequent_prover |
Name: ->/2 |
|
Name: ->/3 |
Called:
Name: axiom/3 |
Module: sequent_prover |
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
Name: all_in_set/3 |
Module: sequent_prover |
Name: axiom2/3 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
member_intersection(E,intersection(A,B),Conj) :-
member_intersection(E,A,ConjA),
member_intersection(E,B,ConjB),!,
Conj = conjunct(ConjA,ConjB).
member_intersection(E,A,member(E,A)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
member_of(Op,X,Term) :- Term=..[Op,A,B], !, (el_of_op(A,X,Op) ; el_of_op(B,X,Op)).
Calls:
Name: el_of_op/3 |
Module: sequent_prover |
Name: ! |
|
Name: =../2 |
Called:
Name: simp_rule/5 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: simp_rule/4 |
Module: sequent_prover |
member_union(E,union(A,B),Disj) :- member_union(E,A,DisjA), member_union(E,B,DisjB), !, Disj = disjunct(DisjA,DisjB).
member_union(E,A,member(E,A)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
min_list([H|T], Min) :- number(H) -> min_list(T,H,Min) ; min_list(T,Min).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: min_list/3 |
Module: sequent_prover |
Name: number/1 |
|
Name: ->/3 |
Called:
Name: min_list/2 |
Module: sequent_prover |
min_list([],Min,Min).
min_list([H|T],Min0,Min) :-
number(H),!,
Min1 is min(H,Min0),
min_list(T,Min1,Min).
min_list([_|T],Min0,Min) :-
min_list(T,Min0,Min).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: is/2 |
|
Name: ! |
|
Name: number/1 |
Called:
Name: min_list/2 |
Module: sequent_prover |
negate(truth,Res) :- !, Res=falsity.
negate(falsity,Res) :- !, Res=truth.
negate(equal(X,Y),R) :- !, R=not_equal(X,Y).
negate(not_equal(X,Y),R) :- !, R=equal(X,Y).
negate(greater(X,Y),R) :- !, R=less_equal(X,Y).
negate(less(X,Y),R) :- !, R=greater_equal(X,Y).
negate(greater_equal(X,Y),R) :- !, R=less(X,Y).
negate(less_equal(X,Y),R) :- !, R=greater(X,Y).
negate(disjunct(X,Y),R) :- !, R=conjunct(NX,NY), negate(X,NX), negate(Y,NY).
negate(conjunct(X,Y),R) :- !, R=disjunct(NX,NY), negate(X,NX), negate(Y,NY).
negate(implication(X,Y),R) :- !, R=conjunct(X,NY), negate(Y,NY).
negate(negation(X),R) :- !, R=X.
negate(P,negation(P)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Called:
Name: trans2/3 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
neutral_element(conjunct,true) :- !.
neutral_element(disjunct,false) :- !.
neutral_element(add,0) :- !.
neutral_element(multiplication,1) :- !.
neutral_element(_,placeholder).
Calls:
Name: ! |
Called:
Name: select_op/4 |
Module: sequent_prover |
Name: conjoin/4 |
Module: sequent_prover |
new_function(Expr,F) :- used_identifiers(Expr,L), possible_function(X), F = '$'(X), \+ member(F,L), !.
Calls:
Name: ! |
|
Name: member/2 |
|
Name: not/1 |
|
Name: =/2 |
|
Name: possible_function/1 |
Module: sequent_prover |
Name: used_identifiers/2 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
new_identifier(Expr,I) :-
used_identifiers(Expr,L),
possible_identifier(X),
I = '$'(X),
\+ member(I,L),!.
Calls:
Name: ! |
|
Name: member/2 |
|
Name: not/1 |
|
Name: =/2 |
|
Name: possible_identifier/1 |
Module: sequent_prover |
Name: used_identifiers/2 |
Module: sequent_prover |
Called:
Name: trans1/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
new_identifiers(Expr,Nr,Ids) :- used_identifiers(Expr,L), possible_identifier(X), I = '$'(X), \+ member(I,L), !, range_ids(X,Nr,Ids).
Calls:
Name: range_ids/3 |
Module: sequent_prover |
Name: ! |
|
Name: member/2 |
|
Name: not/1 |
|
Name: =/2 |
|
Name: possible_identifier/1 |
Module: sequent_prover |
Name: used_identifiers/2 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
of_integer_type(E,Hyps,Info) :-
get_scope(Hyps,Info,[identifier(STypes)]),
member(b(identifier(E),integer,_),STypes).
Calls:
Name: member/2 |
|
Name: get_scope/3 |
Module: sequent_prover |
Called:
Name: simp_rule_with_hyps/5 |
Module: sequent_prover |
only_max([],_,List,List).
only_max([E|R],I,Filtered, Res) :-
\+ number(E),!,
append(Filtered,[E],New),
only_max(R,I,New,Res).
only_max([E|R],I,Filtered,Res) :-
E < I,
only_max(R,I,Filtered,Res).
only_max([E|R],I,Filtered,Res) :-
E =:= I,
member(E,Filtered),
only_max(R,I,Filtered,Res).
only_max([E|R],I,Filtered,Res) :-
E =:= I,
\+ member(E,Filtered),
append(Filtered,[E],New),
only_max(R,I,New,Res).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: append/3 |
|
Name: member/2 |
|
Name: not/1 |
|
Name: =:=/2 |
|
Name: </2 |
|
Name: ! |
|
Name: number/1 |
Called:
Name: remove_smaller/3 |
Module: sequent_prover |
only_min([],_,List,List).
only_min([E|R],I,Filtered, Res) :-
\+ number(E),!,
append(Filtered,[E],New),
only_min(R,I,New,Res).
only_min([E|R],I,Filtered,Res) :-
E > I,
only_min(R,I,Filtered,Res).
only_min([E|R],I,Filtered,Res) :-
E =:= I,
member(E,Filtered),
only_min(R,I,Filtered,Res).
only_min([E|R],I,Filtered,Res) :-
E =:= I,
\+ member(E,Filtered),
append(Filtered,[E],New),
only_min(R,I,New,Res).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: append/3 |
|
Name: member/2 |
|
Name: not/1 |
|
Name: =:=/2 |
|
Name: >/2 |
|
Name: ! |
|
Name: number/1 |
Called:
Name: remove_greater/3 |
Module: sequent_prover |
op_to_list(Term,NList,Op) :- op_to_list(Term,[],NList,Op).
Calls:
Name: op_to_list/4 |
Module: sequent_prover |
Called:
Name: distri_setminus/2 |
Module: sequent_prover |
Name: distri_l/5 |
Module: sequent_prover |
Name: remove_from_op/4 |
Module: sequent_prover |
Name: simp_rule/5 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: remove_duplicates/3 |
Module: sequent_prover |
Name: distribute_op/5 |
Module: sequent_prover |
op_to_list(Term,OList,NList,Op) :-
Term=..[Op,A,B],!,
op_to_list(B,OList,L1,Op),
op_to_list(A,L1,NList,Op).
op_to_list(Term,L,[Term|L],_).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: ! |
|
Name: =../2 |
Called:
Name: distri_setminus/2 |
Module: sequent_prover |
Name: distri_l/5 |
Module: sequent_prover |
Name: remove_from_op/4 |
Module: sequent_prover |
Name: simp_rule/5 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: remove_duplicates/3 |
Module: sequent_prover |
Name: distribute_op/5 |
Module: sequent_prover |
or_equal([],_,D,D).
or_equal([A|L],E,D,Res) :- or_equal(L,E,disjunct(D,equal(E,A)),Res).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
overwrite_type([Ty|R],_,ListOut,Info) :- type_expression(Ty,Info), !, overwrite_type(R,[Ty],ListOut,Info).
overwrite_type([S|R],Prev,ListOut,Info) :- append(Prev,[S],ListIn), overwrite_type(R,ListIn,ListOut,Info).
overwrite_type([],L,L,_).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: append/3 |
|
Name: ! |
|
Name: type_expression/2 |
Module: sequent_prover |
Called:
Name: simp_rule/5 |
Module: sequent_prover |
parse_input(Param,Res) :-
ground(Param),
(number(Param) -> number_codes(Param,CParam) ; atom_codes(Param,CParam)),
bmachine:b_parse_only(formula,CParam,Parsed,_,_Error),
translate:transform_raw(Parsed,TExpr),
adapt_for_eventb(TExpr,Res).
Calls:
Name: adapt_for_eventb/2 |
Module: sequent_prover |
Name: transform_raw/2 |
Module: translate |
Name: b_parse_only/5 |
Module: bmachine |
Name: atom_codes/2 |
|
Name: number_codes/2 |
|
Name: number/1 |
|
Name: ->/3 |
|
Name: ground/1 |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
possible_function(Z) :- func_id(Z).
possible_function(Z) :- func_id(X), func_id(Y), atom_concat(X,Y,Z).
Calls:
Name: atom_concat/3 |
|
Name: func_id/1 |
Module: sequent_prover |
Called:
Name: new_function/2 |
Module: sequent_prover |
possible_identifier(Z) :- identifier(Z).
possible_identifier(Z) :- identifier(X), identifier(Y), atom_concat(X,Y,Z).
Calls:
Name: atom_concat/3 |
|
Name: identifier/1 |
Module: sequent_prover |
Called:
Name: get_wd_pos_of_expr/4 |
Module: sequent_prover |
Name: new_identifier/2 |
Module: sequent_prover |
Name: new_identifiers/3 |
Module: sequent_prover |
prop(success,goal).
prop(sequent(_,X,_), '='('GOAL',XS)) :- translate_term(X,XS).
prop(sequent(Hyps,_,_),'='(HypNr,XS)) :- nth1(Nr,Hyps,X),
translate_term(X,XS), ajoin(['HYP',Nr],HypNr).
prop(sequent(_,_,Cont),'='('CONTINUATION',P)) :- cont_length(Cont,P).
prop(state(S,_),Val) :- prop(S,Val).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: cont_length/2 |
Module: sequent_prover |
Name: ajoin/2 |
Module: tools |
Name: translate_term/2 |
Module: sequent_prover |
Name: nth1/3 |
Module: foo_error |
prove_predicate(Hyps,Goal) :-
get_typed_ast(Goal,TGoal),
maplist(get_typed_ast,Hyps,THyps),
atelierb_provers_interface:prove_predicate(THyps,TGoal,proved).
Calls:
Name: prove_predicate/3 |
Module: atelierb_provers_interface |
Name: maplist/3 |
Module: foo_error |
Name: get_typed_ast/2 |
Module: sequent_prover |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
range(X,I,I,['$'(XI)]) :- atom_int_concat(X,I,XI).
range(X,I,K,['$'(XI)|L]) :- I < K, I1 is I + 1, atom_int_concat(X,I,XI), range(X,I1,K,L).
Calls:
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: atom_int_concat/3 |
Module: sequent_prover |
Name: is/2 |
|
Name: </2 |
Called:
Name: range_ids/3 |
Module: sequent_prover |
range_ids(X,Nr,L) :- range(X,1,Nr,L).
Calls:
Name: range/4 |
Module: sequent_prover |
Called:
Name: new_identifiers/3 |
Module: sequent_prover |
remove_duplicates(L,Res) :- without_duplicates(L,[],Res), L \= Res.
Calls:
Name: \=/2 |
|
Name: without_duplicates/3 |
Module: sequent_prover |
Called:
Name: remove_duplicates/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
remove_duplicates(C,Res,Op) :-
op_to_list(C,List,Op),
remove_duplicates(List,ResL),
list_to_op(ResL,Res,Op).
Calls:
Name: list_to_op/3 |
Module: sequent_prover |
Name: remove_duplicates/2 |
Module: sequent_prover |
Name: op_to_list/3 |
Module: sequent_prover |
Called:
Name: remove_duplicates/3 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
remove_from_list(_,[],[]).
remove_from_list(E,[E|T],T2) :- remove_from_list(E,T,T2).
remove_from_list(E,[X|T],[X|T2]) :- X \= E, remove_from_list(E,T,T2).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: \=/2 |
Called:
Name: remove_from_op/4 |
Module: sequent_prover |
remove_from_op(El,Term,NewTerm,Op) :-
op_to_list(Term,List,Op),
remove_from_list(El,List,List0),
list_to_op(List0,NewTerm,Op).
Calls:
Name: list_to_op/3 |
Module: sequent_prover |
Name: remove_from_list/3 |
Module: sequent_prover |
Name: op_to_list/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
remove_greater(L,I,Res) :- only_min(L,I,[],Res), L \= Res.
Calls:
Name: \=/2 |
|
Name: only_min/4 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
remove_meta_info(Key,Info,Value,Info1) :-
get_meta_info(Key,Info,Content),
Old=..[Key,Content],
select(Value,Content,Content0),
New=..[Key,Content0],
select(Old,Info,New,Info1).
Calls:
Name: select/4 |
Module: foo_error |
Name: =../2 |
|
Name: select/3 |
Module: foo_error |
Name: get_meta_info/3 |
Module: sequent_prover |
Called:
Name: trans2/3 |
Module: sequent_prover |
remove_minus([NE|R],[E|T],NrN) :- is_minus(NE,E), remove_minus(R,T,Nr), NrN is Nr + 1, !.
remove_minus([E|R],[E|T],Nr) :- remove_minus(R,T,Nr).
remove_minus([],[],0).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: ! |
|
Name: is/2 |
|
Name: is_minus/2 |
Module: sequent_prover |
Called:
Name: change_sign/3 |
Module: sequent_prover |
remove_smaller(L,I,Res) :- only_max(L,I,[],Res), L \= Res.
Calls:
Name: \=/2 |
|
Name: only_max/4 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
remove_unused_identifier(L,P,Used) :-
member(Z,L),
used_identifiers(P,Ids),
member(Z,Ids),
list_intersection(L,Ids,Used),
Used \= L.
Calls:
Name: \=/2 |
|
Name: list_intersection/3 |
Module: sequent_prover |
Name: member/2 |
|
Name: used_identifiers/2 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
reorder(C,Res,Op) :-
C=..[Op,A,B],
B=..[Op,L,Rest],!,
R=..[Op,A,L],
append_to_op(Rest,R,Res,Op).
reorder(C,C,Op) :- C=..[Op,_,_].
Calls:
Name: =../2 |
|
Name: append_to_op/4 |
Module: sequent_prover |
Name: ! |
Called:
Name: simp_rule/4 |
Module: sequent_prover |
replace_functor(concat,power_of).
replace_functor(power_of,cartesian_product).
replace_functor(minus_or_set_subtract,minus).
replace_functor(mult_or_cart,multiplication).
replace_functor(F,F).
Called:
Name: adapt_for_eventb/2 |
Module: sequent_prover |
rewrite(X,Y,E,NewE) :- equal_terms(X,E),!, NewE=Y.
rewrite(_X,_Y,E,NewE) :- atomic(E),!, NewE=E.
rewrite(_X,_Y,'$'(E),NewE) :- atomic(E),!, NewE='$'(E).
rewrite(X,_,E,NewE) :- with_ids(E,Ids), member(X,Ids),!, NewE=E.
rewrite(X,Y,C,NewC) :- C=..[Op|Args],
maplist(rewrite(X,Y), Args,NewArgs),
NewC =.. [Op|NewArgs].
Calls:
Name: =../2 |
|
Name: maplist/3 |
Module: foo_error |
Name: =/2 |
|
Name: ! |
|
Name: member/2 |
|
Name: with_ids/2 |
Module: sequent_prover |
Name: atomic/1 |
|
Name: equal_terms/2 |
Module: sequent_prover |
Called:
Name: trans1/4 |
Module: sequent_prover |
Name: symb_trans/4 |
Module: sequent_prover |
select_conjunct(X,conjunct(A,B),Rest) :- !,
(select_conjunct(X,A,RA), conjoin(RA,B,Rest)
;
select_conjunct(X,B,RB), conjoin(A,RB,Rest)).
select_conjunct(X,X,truth).
Calls:
Name: conjoin/3 |
Module: sequent_prover |
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: ! |
Called:
Name: trans2/3 |
Module: sequent_prover |
select_op(X,C,Rest,Op) :- C=..[Op,A,B],
(select_op(X,A,RA,Op), conjoin(RA,B,Rest,Op)
;
select_op(X,B,RB,Op), conjoin(A,RB,Rest,Op)), !.
select_op(X,X,E,Op) :- neutral_element(Op,E).
select_op(X,Y,E,Op) :- neutral_element(Op,E), equal_terms(X,Y).
Calls:
Name: equal_terms/2 |
Module: sequent_prover |
Name: neutral_element/2 |
Module: sequent_prover |
Name: ! |
|
Name: conjoin/4 |
Module: sequent_prover |
Name: RECURSIVE_CALL/4 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
Name: simp_rule/4 |
Module: sequent_prover |
Name: distri_setminus/2 |
Module: sequent_prover |
select_op(X,C,Z,New,Op) :- C=..[Op,A,B],
(select_op(X,A,Z,RA,Op), conjoin(RA,B,New,Op) ;
select_op(X,B,Z,RB,Op), conjoin(A,RB,New,Op)), !.
select_op(X,X,Z,Z,_) :- !.
select_op(X,Y,Z,Z,_) :- equal_terms(X,Y).
Calls:
Name: equal_terms/2 |
Module: sequent_prover |
Name: ! |
|
Name: conjoin/4 |
Module: sequent_prover |
Name: RECURSIVE_CALL/5 |
Module: sequent_prover |
Name: =../2 |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
Name: simp_rule/4 |
Module: sequent_prover |
Name: distri_setminus/2 |
Module: sequent_prover |
select_types(Types,Selected) :- sort(Types,Sorted), select_types_aux(Sorted,Selected).
Calls:
Name: select_types_aux/2 |
Module: sequent_prover |
Name: sort/2 |
Called:
Name: get_scope/3 |
Module: sequent_prover |
select_types_aux([],[]).
select_types_aux([b(identifier(X),any,_)|R],Res) :- member(b(identifier(X),T,_),R), T \= any, !, select_types_aux(R,Res).
select_types_aux([Id|R],[Id|Res]) :- select_types_aux(R,Res).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: ! |
|
Name: \=/2 |
|
Name: member/2 |
Called:
Name: select_types/2 |
Module: sequent_prover |
simp_rule(not_equal(L,L),falsity,'SIMP_MULTI_NOTEQUAL').
simp_rule(less_equal(I,J),Res,'SIMP_LIT_LE') :- number(I), number(J), (I =< J -> Res=truth ; Res=falsity). % where I and J are literals
simp_rule(less(I,J),Res,'SIMP_LIT_LT') :- number(I), number(J), (I < J -> Res=truth ; Res=falsity).
simp_rule(greater_equal(I,J),Res,'SIMP_LIT_GE') :- number(I), number(J), (I >= J -> Res=truth ; Res=falsity).
simp_rule(greater(I,J),Res,'SIMP_LIT_GT') :- number(I), number(J), (I > J -> Res=truth ; Res=falsity).
simp_rule(equal(I,J),Res,'SIMP_LIT_EQUAL') :- number(I), number(J), (I = J -> Res=truth ; Res=falsity).
simp_rule(not_equal(L,R),negation(equal(L,R)),'SIMP_NOTEQUAL').
simp_rule(domain(event_b_comprehension_set(Ids,couple(E,_),P)),event_b_comprehension_set(Ids,E,P),'SIMP_DOM_LAMBDA').
simp_rule(range(event_b_comprehension_set(Ids,couple(_,F),P)),event_b_comprehension_set(Ids,F,P),'SIMP_RAN_LAMBDA').
simp_rule(negation(equal(Set,empty_set)),exists([X],member(X,Set)),'DEF_SPECIAL_NOT_EQUAL') :- new_identifier(Set,X).
simp_rule(Expr,Res,'SIMP_SETENUM_EQUAL_EMPTY') :-is_empty(Expr,set_extension(L)), length(L,LL),
(LL > 0 -> Res = falsity ; Res = truth).
simp_rule(Expr,greater(I,J),'SIMP_UPTO_EQUAL_EMPTY') :- is_empty(Expr,interval(I,J)).
simp_rule(Eq,falsity,'SIMP_UPTO_EQUAL_INTEGER') :- is_equality(Eq,interval(_,_),Z), is_integer_set(Z).
simp_rule(Eq,falsity,'SIMP_UPTO_EQUAL_NATURAL') :- is_equality(Eq,interval(_,_),Nat), is_natural_set(Nat).
simp_rule(Eq,falsity,'SIMP_UPTO_EQUAL_NATURAL1') :- is_equality(Eq,interval(_,_),Nat), is_natural1_set(Nat).
simp_rule(Expr,falsity,'SIMP_SPECIAL_EQUAL_REL') :- is_empty(Expr,relations(_,_)).
simp_rule(Expr,conjunct(negation(equal(A,empty_set)),equal(B,empty_set)),'SIMP_SPECIAL_EQUAL_RELDOM') :-
is_empty(Expr,R),
(R = total_relation(A,B) ;
R = total_function(A,B)).
simp_rule(Expr,conjunct(equal(A,empty_set),negation(equal(B,empty_set))),'SIMP_SREL_EQUAL_EMPTY') :-
is_empty(Expr,surjection_relation(A,B)).
simp_rule(Expr,equivalence(equal(A,empty_set),negation(equal(B,empty_set))),'SIMP_STREL_EQUAL_EMPTY') :-
is_empty(Expr,total_surjection_relation(A,B)).
simp_rule(Expr,equal(R,empty_set),'SIMP_DOM_EQUAL_EMPTY') :- is_empty(Expr,domain(R)).
simp_rule(Expr,equal(R,empty_set),'SIMP_RAN_EQUAL_EMPTY') :- is_empty(Expr,range(R)).
simp_rule(Expr,equal(intersection(range(P),domain(Q)),empty_set),'SIMP_FCOMP_EQUAL_EMPTY') :- is_empty(Expr,composition(P,Q)).
simp_rule(Expr,equal(intersection(range(Q),domain(P)),empty_set),'SIMP_BCOMP_EQUAL_EMPTY') :- is_empty(Expr,ring(P,Q)).
simp_rule(Expr,equal(intersection(domain(R),S),empty_set),'SIMP_DOMRES_EQUAL_EMPTY') :- is_empty(Expr,domain_restriction(S,R)).
simp_rule(Expr,subset(domain(R),S),'SIMP_DOMSUB_EQUAL_EMPTY') :- is_empty(Expr,domain_subtraction(S,R)).
simp_rule(Expr,equal(intersection(range(R),S),empty_set),'SIMP_RANRES_EQUAL_EMPTY') :- is_empty(Expr,range_restriction(R,S)).
simp_rule(Expr,subset(range(R),S),'SIMP_RANSUB_EQUAL_EMPTY') :- is_empty(Expr,range_subtraction(R,S)).
simp_rule(Expr,equal(R,empty_set),'SIMP_CONVERSE_EQUAL_EMPTY') :- is_empty(Expr,reverse(R)).
simp_rule(Expr,equal(domain_restriction(S,R),empty_set),'SIMP_RELIMAGE_EQUAL_EMPTY') :- is_empty(Expr,image(R,S)).
simp_rule(Expr,Res,'SIMP_OVERL_EQUAL_EMPTY') :- is_empty(Expr,Over), Over = overwrite(_,_), and_empty(Over,Res,overwrite).
simp_rule(Expr,equal(intersection(domain(P),domain(Q)),empty_set),'SIMP_DPROD_EQUAL_EMPTY') :- is_empty(Expr,direct_product(P,Q)).
simp_rule(Expr,disjunct(equal(P,empty_set),equal(Q,empty_set)),'SIMP_PPROD_EQUAL_EMPTY') :- is_empty(Expr,parallel_product(P,Q)).
simp_rule(Expr,falsity,'SIMP_ID_EQUAL_EMPTY') :- is_empty(Expr,event_b_identity).
simp_rule(Expr,falsity,'SIMP_PRJ1_EQUAL_EMPTY') :- is_empty(Expr,event_b_first_projection_v2).
simp_rule(Expr,falsity,'SIMP_PRJ2_EQUAL_EMPTY') :- is_empty(Expr,event_b_second_projection_v2).
simp_rule(Eq,P,'SIMP_LIT_EQUAL_KBOOL_TRUE') :- is_equality(Eq,convert_bool(P),boolean_true).
simp_rule(Eq,negation(P),'SIMP_LIT_EQUAL_KBOOL_FALSE') :- is_equality(Eq,convert_bool(P),boolean_false).
simp_rule(convert_bool(Eq),P,'SIMP_KBOOL_LIT_EQUAL_TRUE') :- is_equality(Eq,P,boolean_true).
simp_rule(implication(truth,P),P,'SIMP_SPECIAL_IMP_BTRUE_L').
simp_rule(implication(P,falsity),negation(P),'SIMP_SPECIAL_IMP_BFALSE_R').
simp_rule(not_member(L,R),negation(member(L,R)),'SIMP_NOTIN').
simp_rule(not_subset_strict(L,R),negation(subset_strict(L,R)),'SIMP_NOTSUBSET').
simp_rule(not_subset(L,R),negation(subset(L,R)),'SIMP_NOTSUBSETEQ').
simp_rule(I,equal(E,boolean_true),'SIMP_SPECIAL_NOT_EQUAL_FALSE') :- is_no_equality(I,E,boolean_false).
simp_rule(I,equal(E,boolean_false),'SIMP_SPECIAL_NOT_EQUAL_TRUE') :- is_no_equality(I,E,boolean_true).
simp_rule(forall(X,P1,P2),Res,'SIMP_FORALL_AND') :- P2 = conjunct(_,_), distribute_forall(X,P1,P2,Res).
simp_rule(exists(X,D),Res,'SIMP_EXISTS_OR') :- D = disjunct(_,_), distribute_exists(X,D,Res).
simp_rule(exists(X,implication(P,Q)),implication(forall(X,truth,P),exists(X,Q)),'SIMP_EXISTS_IMP').
simp_rule(forall(L,P1,P2),forall(Used,P1,P2),'SIMP_FORALL') :- remove_unused_identifier(L,P1,Used).
simp_rule(exists(L,P),exists(Used,P),'SIMP_EXISTS') :- remove_unused_identifier(L,P,Used).
simp_rule(negation(forall(X,P1,P2)),exists(X,negation(implication(P1,P2))),'DERIV_NOT_FORALL').
simp_rule(negation(exists(X,P)),forall(X,truth,negation(P)),'DERIV_NOT_EXISTS').
simp_rule(event_b_comprehension_set(Ids,E,P),event_b_comprehension_set(Used,E,P),'SIMP_COMPSET') :- % own rule
remove_unused_identifier(Ids,P,Used).
simp_rule(equal(boolean_true,boolean_false),falsity,'SIMP_SPECIAL_EQUAL_TRUE').
simp_rule(equal(couple(E,F),couple(G,H)),conjunct(equal(E,G),equal(F,H)),'SIMP_EQUAL_MAPSTO').
simp_rule(equal(SetE,SetF),equal(E,F),'SIMP_EQUAL_SING') :- singleton_set(SetE,E),singleton_set(SetF,F).
simp_rule(set_subtraction(S,S),empty_set,'SIMP_MULTI_SETMINUS').
simp_rule(set_subtraction(S,empty_set),S,'SIMP_SPECIAL_SETMINUS_R').
simp_rule(set_subtraction(empty_set,_),empty_set,'SIMP_SPECIAL_SETMINUS_L').
simp_rule(member(E,set_subtraction(_,set_extension(L))),falsity,'DERIV_MULTI_IN_SETMINUS') :- member(F,L), equal_terms(E,F).
simp_rule(member(E,U),truth,'DERIV_MULTI_IN_BUNION') :- U = union(_,_),
member_of(union,set_extension(L),U),
member(F,L),
equal_terms(E,F).
simp_rule(convert_bool(truth),boolean_true,'SIMP_SPECIAL_KBOOL_BTRUE').
simp_rule(convert_bool(falsity),boolean_false,'SIMP_SPECIAL_KBOOL_BFALSE').
simp_rule(subset(Union,T),Res,'DISTRI_SUBSETEQ_BUNION_SING') :-
member_of(union,SetF,Union),
singleton_set(SetF,_),
union_subset_member(T,Union,Res).
simp_rule(finite(S),exists([N,F],member(F,total_bijection(interval(1,N),S))),'DEF_FINITE') :-
new_identifier(S,N),
new_function(S,F).
simp_rule(finite(U),Conj,'SIMP_FINITE_BUNION') :- U = union(_,_), finite_union(U,Conj).
simp_rule(finite(pow_subset(S)),finite(S),'SIMP_FINITE_POW').
simp_rule(finite(cartesian_product(S,T)),disjunct(disjunct(equal(S,empty_set),equal(T,empty_set)),conjunct(finite(S),finite(T))),'DERIV_FINITE_CPROD').
simp_rule(finite(reverse(R)),finite(R),'SIMP_FINITE_CONVERSE').
simp_rule(finite(domain_restriction(E,event_b_identity)),finite(E),'SIMP_FINITE_ID_DOMRES').
simp_rule(finite(domain_restriction(E,event_b_first_projection_v2)),finite(E),'SIMP_FINITE_PRJ1_DOMRES').
simp_rule(finite(domain_restriction(E,event_b_second_projection_v2)),finite(E),'SIMP_FINITE_PRJ2_DOMRES').
simp_rule(finite(Nat),falsity,'SIMP_FINITE_NATURAL') :- is_natural_set(Nat).
simp_rule(finite(Nat),falsity,'SIMP_FINITE_NATURAL1') :- is_natural1_set(Nat).
simp_rule(finite(Z),falsity,'SIMP_FINITE_INTEGER') :- is_integer_set(Z).
simp_rule(Eq,P,'SIMP_SPECIAL_EQV_BTRUE') :- is_equivalence(Eq,P,truth).
simp_rule(Eq,negation(P),'SIMP_SPECIAL_EQV_BFALSE') :- is_equivalence(Eq,P,falsity).
simp_rule(subset_strict(A,B),conjunct(subset(A,B),negation(equal(A,B))),'DEF_SUBSET').
simp_rule(subset_strict(_,empty_set),falsity,'SIMP_SPECIAL_SUBSET_R').
simp_rule(subset_strict(empty_set,S),negation(equal(S,empty_set)),'SIMP_SPECIAL_SUBSET_L').
simp_rule(subset_strict(S,T),falsity,'SIMP_MULTI_SUBSET') :- equal_terms(S,T).
simp_rule(C,Res,'DISTRI_PROD_PLUS') :- distri(C,Res,multiplication,add).
simp_rule(C,Res,'DISTRI_PROD_MINUS') :- distri(C,Res,multiplication,minus).
simp_rule(C,Res,'DISTRI_AND_OR') :- distri(C,Res,conjunct,disjunct).
simp_rule(C,Res,'DISTRI_OR_AND') :- distri(C,Res,disjunct,conjunct).
simp_rule(implication(P,Q),implication(negation(Q),negation(P)),'DERIV_IMP').
simp_rule(implication(P,implication(Q,R)),implication(conjunct(P,Q),R),'DERIV_IMP_IMP').
simp_rule(implication(P,C),Res,'DISTRI_IMP_AND') :- C = conjunct(_,_), and_imp(C,P,Res,conjunct).
simp_rule(implication(D,R),Res,'DISTRI_IMP_OR') :- D = disjunct(_,_), and_imp(D,R,Res,disjunct).
simp_rule(equivalence(P,Q),conjunct(implication(P,Q),implication(Q,P)),'DEF_EQV').
simp_rule(C,P,'SIMP_SPECIAL_AND_BTRUE') :- C = conjunct(P,truth) ; C = conjunct(truth,P).
simp_rule(D,P,'SIMP_SPECIAL_OR_BFALSE') :- D = disjunct(P,falsity) ; D = disjunct(falsity,P).
simp_rule(implication(NotP,P),P,'SIMP_MULTI_IMP_NOT_L') :- is_negation(P,NotP).
simp_rule(implication(P,NotP),NotP,'SIMP_MULTI_IMP_NOT_R') :- is_negation(P,NotP).
simp_rule(Eq,falsity,'SIMP_MULTI_EQV_NOT') :- is_equivalence(Eq,P,NotP), is_negation(P,NotP).
simp_rule(implication(C,Q),truth,'SIMP_MULTI_IMP_AND') :- member_of(conjunct,Q,C).
simp_rule(negation(truth),falsity,'SIMP_SPECIAL_NOT_BTRUE').
simp_rule(Expr,equal(set_subtraction(I0,C),empty_set),'SIMP_BINTER_SETMINUS_EQUAL_EMPTY') :-
is_empty(Expr,I),
member_of(intersection,set_subtraction(B,C),I),
select_op(minus(B,C),I,B,I0,intersection).
simp_rule(Expr,Res,'SIMP_BUNION_EQUAL_EMPTY') :- is_empty(Expr,Union), Union = union(_,_), and_empty(Union,Res,union).
simp_rule(Expr,subset(A,B),'SIMP_SETMINUS_EQUAL_EMPTY') :- is_empty(Expr,set_subtraction(A,B)).
simp_rule(Expr,forall([X],P,equal(E,empty_set)),'SIMP_QUNION_EQUAL_EMPTY') :- is_empty(Expr,quantified_union([X],P,E)).
simp_rule(Expr,falsity,'SIMP_NATURAL_EQUAL_EMPTY') :- is_empty(Expr,Nat), is_natural_set(Nat).
simp_rule(Expr,falsity,'SIMP_NATURAL1_EQUAL_EMPTY') :- is_empty(Expr,Nat), is_natural1_set(Nat).
simp_rule(Expr,disjunct(equal(S,empty_set),equal(T,empty_set)),'SIMP_CPROD_EQUAL_EMPTY') :- is_empty(Expr,cartesian_product(S,T)).
simp_rule(member(X,SetA),equal(X,A),'SIMP_IN_SING') :-
singleton_set(SetA,A).
simp_rule(subset(SetA,S),member(A,S),'SIMP_SUBSETEQ_SING') :- singleton_set(SetA,A).
simp_rule(subset(Union,S),Conj,'DERIV_SUBSETEQ_BUNION') :- Union = union(_,_), union_subset(S,Union,Conj).
simp_rule(subset(S,Inter),Conj,'DERIV_SUBSETEQ_BINTER') :- Inter = intersection(_,_), subset_inter(S,Inter,Conj).
simp_rule(member(_,empty_set),falsity,'SIMP_SPECIAL_IN') .
simp_rule(member(B,S),truth,'SIMP_MULTI_IN') :- S = set_extension(L), length(L,LL), LL > 1, member(B,L).
simp_rule(set_extension(L),set_extension(Res),'SIMP_MULTI_SETENUM') :- remove_duplicates(L,Res).
simp_rule(subset(S,U),truth,'SIMP_SUBSETEQ_BUNION') :- member_of(union,S,U).
simp_rule(subset(I,S),truth,'SIMP_SUBSETEQ_BINTER') :- member_of(intersection,S,I).
simp_rule(implication(C,negation(Q)),negation(C),'SIMP_MULTI_IMP_AND_NOT_R') :- member_of(conjunct,Q,C).
simp_rule(implication(C,Q),negation(C),'SIMP_MULTI_IMP_AND_NOT_L') :- member_of(conjunct,negation(Q),C).
simp_rule(U,S,'SIMP_SPECIAL_BUNION') :- U = union(S,empty_set) ; U = union(empty_set,S).
simp_rule(Eq,subset(NewU,T),'SIMP_MULTI_EQUAL_BUNION') :-
is_equality(Eq,U,T),
member_of(union,T,U),
remove_from_op(T,U,NewU,union).
simp_rule(Eq,subset(T,NewI),'SIMP_MULTI_EQUAL_BINTER') :-
is_equality(Eq,I,T),
member_of(intersection,T,I),
remove_from_op(T,I,NewI,intersection).
simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_EQUAL_RELDOMRAN') :- R=..[Op,empty_set,empty_set],
member(Op,[total_surjection,total_bijection,total_surjection_relation]).
simp_rule(domain(cartesian_product(E,F)),E,'SIMP_MULTI_DOM_CPROD') :- equal_terms(E,F).
simp_rule(range(cartesian_product(E,F)),E,'SIMP_MULTI_RAN_CPROD') :- equal_terms(E,F).
simp_rule(image(cartesian_product(SetE,S),SetF),S,'SIMP_MULTI_RELIMAGE_CPROD_SING') :-
singleton_set(SetE,E),
singleton_set(SetF,F),
equal_terms(E,F).
simp_rule(image(set_extension([couple(E,G)]),SetF),set_extension([G]),'SIMP_MULTI_RELIMAGE_SING_MAPSTO') :-
singleton_set(SetF,F),
equal_terms(E,F).
simp_rule(domain(domain_restriction(A,F)),intersection(domain(F),A),'SIMP_MULTI_DOM_DOMRES').
simp_rule(domain(domain_subtraction(A,F)),set_subtraction(domain(F),A),'SIMP_MULTI_DOM_DOMSUB').
simp_rule(range(range_restriction(F,A)),intersection(range(F),A),'SIMP_MULTI_RAN_RANRES').
simp_rule(range(range_subtraction(F,A)),set_subtraction(range(F),A),'SIMP_MULTI_RAN_RANSUB').
simp_rule(M,exists([Y],member(couple(R,Y),F)),'DEF_IN_DOM') :-
M = member(R,domain(F)),
new_identifier(M,Y).
simp_rule(M,exists([X],member(couple(X,R),F)),'DEF_IN_RAN') :-
M = member(R,range(F)),
new_identifier(M,X).
simp_rule(member(couple(E,F),reverse(R)),member(couple(F,E),R),'DEF_IN_CONVERSE').
simp_rule(member(couple(E,F),domain_restriction(S,R)),conjunct(member(E,S),member(couple(E,F),R)),'DEF_IN_DOMRES').
simp_rule(member(couple(E,F),range_restriction(R,T)),conjunct(member(couple(E,F),R),member(F,T)),'DEF_IN_RANRES').
simp_rule(member(couple(E,F),domain_subtraction(S,R)),conjunct(not_member(E,S),member(couple(E,F),R)),'DEF_IN_DOMSUB').
simp_rule(member(couple(E,F),range_subtraction(R,T)),conjunct(member(couple(E,F),R),not_member(F,T)),'DEF_IN_RANSUB').
simp_rule(member(F,image(R,W)),exists([X],conjunct(member(X,W),member(couple(X,F),R))),'DEF_IN_RELIMAGE') :-
new_identifier(image(R,W),X).
simp_rule(M,exists(Ids,Res),'DEF_IN_FCOMP') :-
M = member(couple(E,F),Comp),
Comp = composition(_,_),
op_to_list(Comp,List,composition),
length(List,Length),
L1 is Length - 1,
new_identifiers(M,L1,Ids),
member_couples(E,F,List,Ids,ConjList),
list_to_op(ConjList,Res,conjunct).
simp_rule(composition(SetEF,SetGH),set_extension([couple(E,H)]),'DERIV_FCOMP_SING') :-
singleton_set(SetEF,couple(E,F)),
singleton_set(SetGH,couple(G,H)),
equal_terms(F,G).
simp_rule(overwrite(P,Q),union(domain_subtraction(domain(Q),P),Q),'DEF_OVERL').
simp_rule(member(couple(E,F),event_b_identity),equal(E,F),'DEF_IN_ID').
simp_rule(member(couple(E,couple(F,G)),direct_product(P,Q)),conjunct(member(couple(E,F),P),member(couple(E,G),Q)),'DEF_IN_DPROD').
simp_rule(member(couple(couple(E,G),couple(F,H)),parallel_product(P,Q)),conjunct(member(couple(E,F),P),member(couple(G,H),Q)),'DEF_IN_PPROD').
simp_rule(member(R,relations(S,T)),subset(R,cartesian_product(S,T)),'DEF_IN_REL').
simp_rule(member(R,total_relation(S,T)),conjunct(member(R,relations(S,T)),equal(domain(R),S)),'DEF_IN_RELDOM').
simp_rule(member(R,surjection_relation(S,T)),conjunct(member(R,relations(S,T)),equal(range(R),T)),'DEF_IN_RELRAN').
simp_rule(member(R,total_surjection_relation(S,T)),conjunct(conjunct(member(R,relations(S,T)),equal(domain(R),S)),equal(range(R),T)),'DEF_IN_RELDOMRAN').
simp_rule(M,conjunct(Conj1,Conj2),'DEF_IN_FCT') :-
M = member(F,partial_function(S,T)),
Conj1 = member(F,relations(S,T)),
new_identifiers(M,3,Ids),
Ids = [X,Y,Z],
Conj2 = forall(Ids,conjunct(member(couple(X,Y),F),member(couple(X,Z),F)),equal(Y,Z)).
simp_rule(member(X,total_function(Dom,Ran)),conjunct(Conj1,Conj2),'DEF_IN_TFCT') :-
Conj1 = member(X,partial_function(Dom,Ran)),
Conj2 = equal(domain(X),Dom).
simp_rule(member(F,partial_injection(S,T)),conjunct(member(F,partial_function(S,T)),member(reverse(F),partial_function(T,S))),'DEF_IN_INJ').
simp_rule(member(F,total_injection(S,T)),conjunct(member(F,partial_injection(S,T)),equal(domain(F),S)),'DEF_IN_TINJ').
simp_rule(member(F,partial_surjection(S,T)),conjunct(member(F,partial_function(S,T)),equal(range(F),T)),'DEF_IN_SURJ').
simp_rule(member(F,total_surjection(S,T)),conjunct(member(F,partial_surjection(S,T)),equal(domain(F),S)),'DEF_IN_TSURJ').
simp_rule(member(F,total_bijection(S,T)),conjunct(member(F,total_injection(S,T)),equal(range(F),T)),'DEF_IN_BIJ').
simp_rule(C,Res,'DISTRI_BCOMP_BUNION') :- distri_r(C,Res,ring,union).
simp_rule(C,Res,'DISTRI_FCOMP_BUNION') :- distri(C,Res,composition,union).
simp_rule(C,Res,'DISTRI_DPROD_BUNION') :- distri_r(C,Res,direct_product,union).
simp_rule(C,Res,'DISTRI_DPROD_BINTER') :- distri_r(C,Res,direct_product,intersection).
simp_rule(C,Res,'DISTRI_DPROD_SETMINUS') :- distri_r(C,Res,direct_product,set_subtraction).
simp_rule(C,Res,'DISTRI_DPROD_OVERL') :- distri_r(C,Res,direct_product,overwrite).
simp_rule(C,Res,'DISTRI_PPROD_BUNION') :- distri_r(C,Res,parallel_product,union).
simp_rule(C,Res,'DISTRI_PPROD_BINTER') :- distri_r(C,Res,parallel_product,intersection).
simp_rule(C,Res,'DISTRI_PPROD_SETMINUS') :- distri_r(C,Res,parallel_product,set_subtraction).
simp_rule(C,Res,'DISTRI_PPROD_OVERL') :- distri_r(C,Res,parallel_product,overwrite).
simp_rule(C,Res,'DISTRI_OVERL_BUNION_L') :- distri_l(C,Res,overwrite,union).
simp_rule(C,Res,'DISTRI_OVERL_BINTER_L') :- distri_l(C,Res,overwrite,intersection).
simp_rule(C,Res,'DISTRI_DOMRES_BUNION') :- distri(C,Res,domain_restriction,union).
simp_rule(C,Res,'DISTRI_DOMRES_BINTER') :- distri(C,Res,domain_restriction,intersection).
simp_rule(C,Res,'DISTRI_DOMRES_DPROD') :- distri_r(C,Res,domain_restriction,direct_product).
simp_rule(C,Res,'DISTRI_DOMRES_OVERL') :- distri_r(C,Res,domain_restriction,overwrite).
simp_rule(C,Res,'DISTRI_DOMRES_SETMINUS') :- distri(C,Res,domain_restriction,set_subtraction).
simp_rule(C,Res,'DISTRI_DOMSUB_BUNION_R') :- distri_r(C,Res,domain_subtraction,union).
simp_rule(C,Res,'DISTRI_DOMSUB_BUNION_L') :- distri_l(C,Res,domain_subtraction,union,intersection).
simp_rule(C,Res,'DISTRI_DOMSUB_BINTER_R') :- distri_r(C,Res,domain_subtraction,intersection).
simp_rule(C,Res,'DISTRI_DOMSUB_BINTER_L') :- distri_l(C,Res,domain_subtraction,intersection,union).
simp_rule(C,Res,'DISTRI_DOMSUB_DPROD') :- distri_r(C,Res,domain_subtraction,direct_product).
simp_rule(C,Res,'DISTRI_DOMSUB_OVERL') :- distri_r(C,Res,domain_subtraction,overwrite).
simp_rule(C,Res,'DISTRI_RANRES_BUNION') :- distri(C,Res,range_restriction,union).
simp_rule(C,Res,'DISTRI_RANRES_BINTER') :- distri(C,Res,range_restriction,intersection).
simp_rule(C,Res,'DISTRI_RANRES_SETMINUS') :- distri(C,Res,range_restriction,set_subtraction).
simp_rule(C,Res,'DISTRI_RANSUB_BUNION') :- distri(C,Res,range_subtraction,union).
simp_rule(C,Res,'DISTRI_RANSUB_BINTER') :- distri(C,Res,range_subtraction,intersection).
simp_rule(C,Res,'DISTRI_CONVERSE_BUNION') :- C = reverse(U), U = union(_,_), distri_reverse(U,Res,union).
simp_rule(C,Res,'DISTRI_CONVERSE_BINTER') :- C = reverse(I), I = intersection(_,_), distri_reverse(I,Res,intersection).
simp_rule(C,Res,'DISTRI_CONVERSE_SETMINUS') :- C = reverse(S), S = set_subtraction(_,_), distri_reverse(S,Res,set_subtraction).
simp_rule(C,Res,'DISTRI_CONVERSE_BCOMP') :- C = reverse(R), R = ring(_,_), distri_reverse_reverse(R,Res,ring).
simp_rule(C,Res,'DISTRI_CONVERSE_FCOMP') :- C = reverse(R), R = composition(_,_), distri_reverse_reverse(R,Res,composition).
simp_rule(reverse(parallel_product(S,R)),parallel_product(reverse(S),reverse(R)),'DISTRI_CONVERSE_PPROD').
simp_rule(reverse(domain_restriction(S,R)),range_restriction(reverse(R),S),'DISTRI_CONVERSE_DOMRES').
simp_rule(reverse(domain_subtraction(S,R)),range_subtraction(reverse(R),S),'DISTRI_CONVERSE_DOMSUB').
simp_rule(reverse(range_restriction(R,S)),domain_restriction(S,reverse(R)),'DISTRI_CONVERSE_RANRES').
simp_rule(reverse(range_subtraction(R,S)),domain_subtraction(S,reverse(R)),'DISTRI_CONVERSE_RANSUB').
simp_rule(domain(U),Res,'DISTRI_DOM_BUNION') :- U = union(_,_), distri_union(U,Res,domain).
simp_rule(range(U),Res,'DISTRI_RAN_BUNION') :- U = union(_,_), distri_union(U,Res,range).
simp_rule(image(R,U),Res,'DISTRI_RELIMAGE_BUNION_R') :- U = union(_,_), image_union(R,U,Res).
simp_rule(image(U,S),Res,'DISTRI_RELIMAGE_BUNION_L') :- U = union(_,_), union_image(U,S,Res).
simp_rule(member(LB,interval(LB,UB)),truth,'lower_bound_in_interval') :- number(LB), number(UB), LB =< UB. % own rule: lower bound in interval
simp_rule(member(Nr,interval(LB,UB)),truth,'SIMP_IN_UPTO') :- number(LB), number(UB), number(Nr), LB =< Nr, Nr =< UB. % own rule
simp_rule(member(Nr,interval(LB,UB)),falsity,'SIMP_IN_UPTO') :- number(LB), number(UB), number(Nr), (Nr =< LB ; UB =< Nr). % own rule
simp_rule(member(E,U),Res,'DEF_IN_BUNION') :- U = union(_,_), member_union(E,U,Res).
simp_rule(member(E,I),Res,'DEF_IN_BINTER') :- I = intersection(_,_), member_intersection(E,I,Res).
simp_rule(member(couple(E,F),cartesian_product(S,T)),conjunct(member(E,S),member(F,T)),'DEF_IN_MAPSTO').
simp_rule(member(E,pow_subset(S)),subset(E,S),'DEF_IN_POW').
simp_rule(member(E,pow1_subset(S)),conjunct(member(E,pow_subset(S)),not_equal(S,empty_set)),'DEF_IN_POW1').
simp_rule(S,forall([X],member(X,A),member(X,B)),'DEF_SUBSETEQ') :- S = subset(A,B), new_identifier(S,X).
simp_rule(member(E,set_subtraction(S,T)),conjunct(member(E,S),negation(member(E,T))),'DEF_IN_SETMINUS').
simp_rule(member(E,set_extension(L)),D,'DEF_IN_SETENUM') :- L = [A,B|T],
or_equal(T,E,disjunct(equal(E,A),equal(E,B)),D).
simp_rule(M,exists([X],conjunct(member(X,S),member(E,X))),'DEF_IN_KUNION') :-
M = member(E,general_union(S)),
new_identifier(M,X).
simp_rule(member(E,general_intersection(S)),forall([X],member(X,S),member(E,X)),'DEF_IN_KINTER') :- new_identifier(S,X).
simp_rule(member(E,interval(L,R)),conjunct(less_equal(L,E),less_equal(E,R)),'DEF_IN_UPTO').
simp_rule(C,Res,'DISTRI_BUNION_BINTER') :- distri(C,Res,union,intersection).
simp_rule(C,Res,'DISTRI_BINTER_BUNION') :- distri(C,Res,intersection,union).
simp_rule(C,Res,'DISTRI_BINTER_SETMINUS') :- distri(C,Res,intersection,set_subtraction).
simp_rule(C,Res,'DISTRI_SETMINUS_BUNION') :- distri_setminus(C,Res).
simp_rule(C,Res,'DISTRI_CPROD_BINTER') :- distri(C,Res,cartesian_product,intersection).
simp_rule(C,Res,'DISTRI_CPROD_BUNION') :- distri(C,Res,cartesian_product,union).
simp_rule(C,Res,'DISTRI_CPROD_SETMINUS') :- distri(C,Res,cartesian_product,set_subtraction).
simp_rule(subset(set_subtraction(A,B),S),subset(A,union(B,S)),'DERIV_SUBSETEQ_SETMINUS_L').
simp_rule(subset(S,set_subtraction(A,B)),conjunct(subset(S,A),equal(intersection(S,B),empty_set)),'DERIV_SUBSETEQ_SETMINUS_R').
simp_rule(partition(S,L),Res,'DEF_PARTITION') :-
length(L,LL), LL > 1,
list_to_op(L,U,union),
Eq = equal(S,U),
findall(equal(intersection(X,Y),empty_set),(all_pairs(L,Pairs), member([X,Y],Pairs)), Disjoint),
list_to_op([Eq|Disjoint],Res,conjunct).
simp_rule(partition(S,[]),equal(S,empty_set),'SIMP_EMPTY_PARTITION').
simp_rule(partition(S,[T]),equal(S,T),'SIMP_SINGLE_PARTITION').
simp_rule(domain(set_extension(L)),set_extension(Res),'SIMP_DOM_SETENUM') :-
map_dom(L,Dom),
without_duplicates(Dom,[],Res).
simp_rule(range(set_extension(L)),set_extension(Res),'SIMP_RAN_SETENUM') :-
map_ran(L,Ran),
without_duplicates(Ran,[],Res).
simp_rule(general_union(pow_subset(S)),S,'SIMP_KUNION_POW').
simp_rule(general_union(pow1_subset(S)),S,'SIMP_KUNION_POW1').
simp_rule(general_union(set_extension([empty_set])),empty_set,'SIMP_SPECIAL_KUNION').
simp_rule(quantified_union([_],falsity,_),empty_set,'SIMP_SPECIAL_QUNION').
simp_rule(general_intersection(set_extension([empty_set])),empty_set,'SIMP_SPECIAL_KINTER').
simp_rule(general_intersection(pow_subset(S)),S,'SIMP_KINTER_POW').
simp_rule(pow_subset(empty_set),set_extension([empty_set]),'SIMP_SPECIAL_POW').
simp_rule(pow1_subset(empty_set),empty_set,'SIMP_SPECIAL_POW1').
simp_rule(event_b_comprehension_set(Ids,X,member(X,S)),S,'SIMP_COMPSET_IN') :-
used_identifiers(X,Ids),
free_identifiers(S,Free),
list_intersection(Ids,Free,[]).
simp_rule(event_b_comprehension_set(Ids,X,subset(X,S)),pow_subset(S),'SIMP_COMPSET_SUBSETEQ') :-
used_identifiers(X,Ids),
free_identifiers(S,Free),
list_intersection(Ids,Free,[]).
simp_rule(event_b_comprehension_set(_,_,falsity),empty_set,'SIMP_SPECIAL_COMPSET_BFALSE').
simp_rule(Expr,forall(Ids,truth,negation(P)),'SIMP_SPECIAL_EQUAL_COMPSET') :-
is_empty(Expr,event_b_comprehension_set(Ids,_,P)).
simp_rule(R,S,'SIMP_SPECIAL_OVERL') :- R = overwrite(S,empty_set) ; R = overwrite(empty_set,S).
simp_rule(domain(reverse(R)),range(R),'SIMP_DOM_CONVERSE').
simp_rule(range(reverse(R)),domain(R),'SIMP_RAN_CONVERSE').
simp_rule(domain_restriction(empty_set,_),empty_set,'SIMP_SPECIAL_DOMRES_L').
simp_rule(domain_restriction(_,empty_set),empty_set,'SIMP_SPECIAL_DOMRES_R').
simp_rule(domain_restriction(domain(R),R),R,'SIMP_MULTI_DOMRES_DOM').
simp_rule(domain_restriction(range(R),reverse(R)),reverse(R),'SIMP_MULTI_DOMRES_RAN').
simp_rule(domain_restriction(S,domain_restriction(T,event_b_identity)),domain_restriction(intersection(S,T),event_b_identity),'SIMP_DOMRES_DOMRES_ID').
simp_rule(domain_restriction(S,domain_subtraction(T,event_b_identity)),domain_restriction(set_subtraction(S,T),event_b_identity),'SIMP_DOMRES_DOMSUB_ID').
simp_rule(range_restriction(_,empty_set),empty_set,'SIMP_SPECIAL_RANRES_R').
simp_rule(range_restriction(empty_set,_),empty_set,'SIMP_SPECIAL_RANRES_L').
simp_rule(range_restriction(domain_restriction(S,event_b_identity),T),domain_restriction(intersection(S,T),event_b_identity),'SIMP_RANRES_DOMRES_ID').
simp_rule(range_restriction(domain_subtraction(S,event_b_identity),T),domain_restriction(set_subtraction(T,S),event_b_identity),'SIMP_RANRES_DOMSUB_ID').
simp_rule(range_restriction(R,range(R)),R,'SIMP_MULTI_RANRES_RAN').
simp_rule(range_restriction(reverse(R),domain(R)),reverse(R),'SIMP_MULTI_RANRES_DOM').
simp_rule(range_restriction(event_b_identity,S),domain_restriction(S,event_b_identity),'SIMP_RANRES_ID').
simp_rule(range_subtraction(event_b_identity,S),domain_subtraction(S,event_b_identity),'SIMP_RANSUB_ID').
simp_rule(domain_subtraction(empty_set,R),R,'SIMP_SPECIAL_DOMSUB_L').
simp_rule(domain_subtraction(_,empty_set),empty_set,'SIMP_SPECIAL_DOMSUB_R').
simp_rule(domain_subtraction(domain(R),R),empty_set,'SIMP_MULTI_DOMSUB_DOM').
simp_rule(domain_subtraction(range(R),reverse(R)),empty_set,'SIMP_MULTI_DOMSUB_RAN').
simp_rule(domain_subtraction(S,domain_restriction(T,event_b_identity)),domain_restriction(set_subtraction(T,S),event_b_identity),'SIMP_DOMSUB_DOMRES_ID').
simp_rule(domain_subtraction(S,domain_subtraction(T,event_b_identity)),domain_subtraction(union(S,T),event_b_identity),'SIMP_DOMSUB_DOMSUB_ID').
simp_rule(range_subtraction(R,empty_set),R,'SIMP_SPECIAL_RANSUB_R').
simp_rule(range_subtraction(empty_set,_),empty_set,'SIMP_SPECIAL_RANSUB_L').
simp_rule(range_subtraction(reverse(R),domain(R)),empty_set,'SIMP_MULTI_RANSUB_DOM').
simp_rule(range_subtraction(R,range(R)),empty_set,'SIMP_MULTI_RANSUB_RAN').
simp_rule(range_subtraction(domain_restriction(S,event_b_identity),T),domain_restriction(set_subtraction(S,T),event_b_identity),'SIMP_RANSUB_DOMRES_ID').
simp_rule(range_subtraction(domain_subtraction(S,event_b_identity),T),domain_subtraction(union(S,T),event_b_identity),'SIMP_RANSUB_DOMSUB_ID').
simp_rule(C,R,'SIMP_TYPE_FCOMP_ID') :- C = composition(R,event_b_identity) ; C = composition(event_b_identity,R).
simp_rule(C,R,'SIMP_TYPE_BCOMP_ID') :- C = ring(R,event_b_identity) ; C = ring(event_b_identity,R).
simp_rule(direct_product(_,empty_set),empty_set,'SIMP_SPECIAL_DPROD_R').
simp_rule(direct_product(empty_set,_),empty_set,'SIMP_SPECIAL_DPROD_L').
simp_rule(direct_product(cartesian_product(S,T),cartesian_product(U,V)),
cartesian_product(intersection(S,U),cartesian_product(T,V)),'SIMP_DPROD_CPROD').
simp_rule(PP,empty_set,'SIMP_SPECIAL_PPROD') :- PP = parallel_product(_,empty_set) ; PP = parallel_product(empty_set,_).
simp_rule(parallel_product(cartesian_product(S,T),cartesian_product(U,V)),
cartesian_product(cartesian_product(S,U),cartesian_product(T,V)),'SIMP_PPROD_CPROD').
simp_rule(image(_,empty_set),empty_set,'SIMP_SPECIAL_RELIMAGE_R').
simp_rule(image(empty_set,_),empty_set,'SIMP_SPECIAL_RELIMAGE_L').
simp_rule(image(R,domain(R)),range(R),'SIMP_MULTI_RELIMAGE_DOM').
simp_rule(image(event_b_identity,T),T,'SIMP_RELIMAGE_ID').
simp_rule(image(domain_restriction(S,event_b_identity),T),intersection(S,T),'SIMP_RELIMAGE_DOMRES_ID').
simp_rule(image(domain_subtraction(S,event_b_identity),T),set_subtraction(T,S),'SIMP_RELIMAGE_DOMSUB_ID').
simp_rule(image(reverse(range_subtraction(_,S)),S),empty_set,'SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB').
simp_rule(image(reverse(range_restriction(R,S)),S),image(reverse(R),S),'SIMP_MULTI_RELIMAGE_CONVERSE_RANRES').
simp_rule(image(reverse(domain_subtraction(S,R)),T),
set_subtraction(image(reverse(R),T),S),'SIMP_RELIMAGE_CONVERSE_DOMSUB').
simp_rule(image(range_subtraction(R,S),T),set_subtraction(image(R,T),S),'DERIV_RELIMAGE_RANSUB').
simp_rule(image(range_restriction(R,S),T),intersection(image(R,T),S),'DERIV_RELIMAGE_RANRES').
simp_rule(image(domain_subtraction(S,_),S),empty_set,'SIMP_MULTI_RELIMAGE_DOMSUB').
simp_rule(image(domain_subtraction(S,R),T),image(R,set_subtraction(T,S)),'DERIV_RELIMAGE_DOMSUB').
simp_rule(image(domain_restriction(S,R),T),image(R,intersection(S,T)),'DERIV_RELIMAGE_DOMRES').
simp_rule(reverse(empty_set),empty_set,'SIMP_SPECIAL_CONVERSE').
simp_rule(reverse(event_b_identity),event_b_identity,'SIMP_SPECIAL_ID').
simp_rule(member(couple(E,F),set_subtraction(_,event_b_identity)),falsity,'SIMP_SPECIAL_IN_SETMINUS_ID') :- equal_terms(E,F).
simp_rule(member(couple(E,F),domain_restriction(S,event_b_identity)),member(E,S),'SIMP_SPECIAL_IN_DOMRES_ID') :-
equal_terms(E,F).
simp_rule(member(couple(E,F),set_subtraction(R,domain_restriction(S,event_b_identity))),
member(couple(E,F),domain_subtraction(S,R)),'SIMP_SPECIAL_IN_DOMRES_ID') :- equal_terms(E,F).
simp_rule(reverse(cartesian_product(S,T)),cartesian_product(T,S),'SIMP_CONVERSE_CPROD').
simp_rule(reverse(set_extension(L)),set_extension(NewL),'SIMP_CONVERSE_SETENUM') :- convert_map_to(L,NewL).
simp_rule(reverse(event_b_comprehension_set(Ids,couple(X,Y),P)),
event_b_comprehension_set(Ids,couple(Y,X),P),'SIMP_CONVERSE_COMPSET').
simp_rule(composition(domain_restriction(S,event_b_identity),R),domain_restriction(S,R),'SIMP_FCOMP_ID_L').
simp_rule(composition(R,domain_restriction(S,event_b_identity)),range_restriction(R,S),'SIMP_FCOMP_ID_R').
simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_REL_R') :- R=..[Op,_,empty_set],
member(Op,[relations,surjection_relation,partial_function,partial_injection,partial_surjection]).
simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_REL_L') :- R=..[Op,empty_set,_],
member(Op,[relations,total_relation,partial_function,total_function,partial_injection,total_injection]).
simp_rule(function(event_b_first_projection_v2,couple(E,_)),E,'SIMP_FUNIMAGE_PRJ1').
simp_rule(function(event_b_second_projection_v2,couple(_,F)),F,'SIMP_FUNIMAGE_PRJ2').
simp_rule(member(couple(E,function(F,E)),F),truth,'SIMP_IN_FUNIMAGE').
simp_rule(member(couple(function(reverse(F),E),E),F),truth,'SIMP_IN_FUNIMAGE_CONVERSE_L').
simp_rule(member(couple(function(F,E),E),reverse(F)),truth,'SIMP_IN_FUNIMAGE_CONVERSE_R').
simp_rule(function(set_extension(L),_),E,'SIMP_MULTI_FUNIMAGE_SETENUM_LL') :- all_map_to(L,E).
simp_rule(function(set_extension(L),X),Y,'SIMP_MULTI_FUNIMAGE_SETENUM_LR') :- member(couple(Z,Y),L), equal_terms(X,Z).
simp_rule(function(Over,X),Y,'SIMP_MULTI_FUNIMAGE_OVERL_SETENUM') :-
Over = overwrite(_,_),
last_overwrite(Over,set_extension(L)),
member(couple(Z,Y),L),
equal_terms(X,Z).
simp_rule(function(U,X),Y,'SIMP_MULTI_FUNIMAGE_BUNION_SETENUM') :-
member_of(union,set_extension(L),U),
member(couple(Z,Y),L),
equal_terms(X,Z).
simp_rule(function(cartesian_product(_,set_extension([F])),_),F,'SIMP_FUNIMAGE_CPROD').
simp_rule(function(F,function(reverse(F),E)),E,'SIMP_FUNIMAGE_FUNIMAGE_CONVERSE').
simp_rule(function(reverse(F),function(F,E)),E,'SIMP_FUNIMAGE_CONVERSE_FUNIMAGE').
simp_rule(function(set_extension(L),function(set_extension(L2),E)),E,'SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM') :-
convert_map_to(L,LConverted),
equal_terms(LConverted,L2).
simp_rule(Eq,member(couple(X,Y),F),'DEF_EQUAL_FUNIMAGE') :- is_equality(Eq,function(F,X),Y).
simp_rule(domain_restriction(SetE,event_b_identity),set_extension([couple(E,E)]),'DERIV_ID_SING') :- singleton_set(SetE,E).
simp_rule(domain(empty_set),empty_set,'SIMP_SPECIAL_DOM').
simp_rule(range(empty_set),empty_set,'SIMP_SPECIAL_RAN').
simp_rule(reverse(reverse(R)),R,'SIMP_CONVERSE_CONVERSE').
simp_rule(function(event_b_identity,X),X,'SIMP_FUNIMAGE_ID').
simp_rule(member(E,Nat),less_equal(0,E),'DEF_IN_NATURAL') :- is_natural_set(Nat).
simp_rule(member(E,Nat),less_equal(1,E),'DEF_IN_NATURAL1') :- is_natural1_set(Nat).
simp_rule(div(E,1),E,'SIMP_SPECIAL_DIV_1').
simp_rule(div(0,_),0,'SIMP_SPECIAL_DIV_0').
simp_rule(power_of(E,1),E,'SIMP_SPECIAL_EXPN_1_R').
simp_rule(power_of(1,_),1,'SIMP_SPECIAL_EXPN_1_L').
simp_rule(power_of(_,0),1,'SIMP_SPECIAL_EXPN_0').
simp_rule(A,S,'SIMP_SPECIAL_PLUS') :- A = add(S,0) ; A = add(0,S).
simp_rule(Prod,Res,Rule) :-
Prod = multiplication(_,_),
op_to_list(Prod,L,multiplication),
change_sign(L,NL,Nr),
list_to_op(NL,New,multiplication),
(Nr mod 2 =:= 0 -> Rule = 'SIMP_SPECIAL_PROD_MINUS_EVEN', Res = New
; Rule = 'SIMP_SPECIAL_PROD_MINUS_ODD', Res = unary_minus(New)).
simp_rule(unary_minus(I),J,'SIMP_LIT_MINUS') :- number(I), J is I * (-1).
simp_rule(minus(E,0),E,'SIMP_SPECIAL_MINUS_R').
simp_rule(minus(0,E),unary_minus(E),'SIMP_SPECIAL_MINUS_L').
simp_rule(unary_minus(F),E,'SIMP_MINUS_MINUS') :- is_minus(F,E).
simp_rule(minus(E,F),add(E,F2),'SIMP_MINUS_UNMINUS') :- is_minus(F,F2).
simp_rule(minus(E,F),0,'SIMP_MULTI_MINUS') :- equal_terms(E,F).
simp_rule(minus(S,C),S0,'SIMP_MULTI_MINUS_PLUS_L') :- select_op(C,S,S0,add).
simp_rule(minus(C,S),unary_minus(S0),'SIMP_MULTI_MINUS_PLUS_R') :- select_op(C,S,S0,add).
simp_rule(minus(S1,S2),minus(S01,S02),'SIMP_MULTI_MINUS_PLUS_PLUS') :-
member_of(add,El,S1),
select_op(El,S1,S01,add),
select_op(El,S2,S02,add),
S01 = add(_,_),
S02 = add(_,_).
simp_rule(S,S1,'SIMP_MULTI_PLUS_MINUS') :-
member_of(add,minus(C,D),S),
select_op(D,S,S0,add),
select_op(minus(C,D),S0,C,S1,add).
simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_PLUS') :-
Ex=..[Rel,L,R],
comparison(Rel),
R = add(_,_),
member_of(add,El,L),
select_op(El,L,L0,add),
select_op(El,R,R0,add),
Res=..[Rel,L0,R0].
simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_R') :-
Ex=..[Rel,C,R],
comparison(Rel),
R = add(_,_),
select_op(C,R,R0,add),
Res=..[Rel,0,R0].
simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_L') :-
Ex=..[Rel,L,C],
comparison(Rel),
L = add(_,_),
select_op(C,L,L0,add),
Res=..[Rel,L0,0].
simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_R') :-
Ex=..[Rel,L,R],
comparison(Rel),
L = minus(A,C1),
R = minus(B,C2),
equal_terms(C1,C2),
Res=..[Rel,A,B].
simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_L') :-
Ex=..[Rel,L,R],
comparison(Rel),
L = minus(C1,A),
R = minus(C2,B),
equal_terms(C1,C2),
Res=..[Rel,B,A].
simp_rule(P,E,'SIMP_SPECIAL_PROD_1') :- P = multiplication(E,1) ; P = multiplication(1,E).
simp_rule(min(set_extension(L)),min(set_extension(Res)),'SIMP_LIT_MIN') :-
min_list(L,I),
remove_greater(L,I,Res).
simp_rule(max(set_extension(L)),max(set_extension(Res)),'SIMP_LIT_MAX') :-
max_list(L,I),
remove_smaller(L,I,Res).
simp_rule(card(empty_set),0,'SIMP_SPECIAL_CARD').
simp_rule(card(set_extension([_])),1,'SIMP_CARD_SING').
simp_rule(Eq,equal(S,empty_set),'SIMP_SPECIAL_EQUAL_CARD') :- is_equality(Eq,card(S),0).
simp_rule(card(pow_subset(S)),power_of(2,card(S)),'SIMP_CARD_POW').
simp_rule(card(union(S,T)),minus(add(card(S),card(T)),card(intersection(S,T))),'SIMP_CARD_BUNION').
simp_rule(card(reverse(R)),card(R),'SIMP_CARD_CONVERSE').
simp_rule(card(domain_restriction(S,event_b_identity)),S,'SIMP_CARD_ID_DOMRES').
simp_rule(card(domain_restriction(E,event_b_first_projection_v2)),E,'SIMP_CARD_PRJ1_DOMRES').
simp_rule(card(domain_restriction(E,event_b_second_projection_v2)),E,'SIMP_CARD_PRJ2_DOMRES').
simp_rule(P,falsity,'SIMP_MULTI_LT') :- is_less(P,E,F), equal_terms(E,F). % covers SIMP_MULTI_GT too
simp_rule(div(NE,NF),div(E,F),'SIMP_DIV_MINUS') :- is_minus(NE,E), is_minus(NF,F).
simp_rule(div(E,F),1,'SIMP_MULTI_DIV') :- equal_terms(E,F).
simp_rule(modulo(0,_),0,'SIMP_SPECIAL_MOD_0').
simp_rule(modulo(_,1),0,'SIMP_SPECIAL_MOD_1').
simp_rule(modulo(E,F),1,'SIMP_MULTI_MOD') :- equal_terms(E,F).
simp_rule(min(SetE),E,'SIMP_MIN_SING') :- singleton_set(SetE,E).
simp_rule(max(SetE),E,'SIMP_MAX_SING') :- singleton_set(SetE,E).
simp_rule(div(P1,E2),P0,'SIMP_MULTI_DIV_PROD') :-
member_of(multiplication,E1,P1),
equal_terms(E1,E2),
select_op(E1,P1,P0,multiplication).
simp_rule(card(set_extension(L)),LL,'SIMP_TYPE_CARD') :- length(L,LL).
simp_rule(card(interval(I,J)),Res,'SIMP_LIT_CARD_UPTO') :- number(I), number(J), I =< J, Res is J - I + 1.
simp_rule(card(interval(I,J)),0,'SIMP_LIT_CARD_UPTO') :- number(I), number(J), I > J. % from "Proposal for an extensible rule-based prover for Event-B", pg. 7
simp_rule(P,negation(equal(S,empty_set)),'SIMP_LIT_LE_CARD_1') :- is_less_eq(P,1,card(S)).
simp_rule(P,negation(equal(S,empty_set)),'SIMP_LIT_LT_CARD_0') :- is_less(P,0,card(S)).
simp_rule(Eq,exists([X],equal(S,set_extension([X]))),'SIMP_LIT_EQUAL_CARD_1') :-
is_equality(Eq,card(S),1),
new_identifier(S,X).
simp_rule(member(card(S),Nat),negation(equal(S,empty_set)),'SIMP_CARD_NATURAL1') :- is_natural1_set(Nat).
simp_rule(Eq,exists([F],member(F,total_bijection(interval(1,K),S))),'DEF_EQUAL_CARD') :-
is_equality(Eq,card(S),K),
new_function(conjunct(S,K),F).
simp_rule(equal(card(S),card(T)),exists([F],member(F,total_bijection(S,T))),'SIMP_EQUAL_CARD') :-
new_function(conjunct(S,T),F).
simp_rule(member(0,Nat),falsity,'SIMP_SPECIAL_IN_NATURAL1') :- is_natural1_set(Nat).
simp_rule(interval(I,J),empty_set,'SIMP_LIT_UPTO') :- number(I), number(J), I > J.
simp_rule(member(NI,Nat),falsity,'SIMP_LIT_IN_MINUS_NATURAL') :-
is_natural_set(Nat),
(NI = unary_minus(I), number(I), I > 0
; number(NI), NI < 0).
simp_rule(member(NI,Nat),falsity,'SIMP_LIT_IN_MINUS_NATURAL1') :-
is_natural1_set(Nat),
(NI = unary_minus(I), number(I), I >= 0
; number(NI), NI < 0).
simp_rule(min(Nat),0,'SIMP_MIN_NATURAL') :- is_natural_set(Nat).
simp_rule(min(Nat),1,'SIMP_MIN_NATURAL1') :- is_natural1_set(Nat).
simp_rule(max(interval(_,F)),F,'SIMP_MAX_UPTO').
simp_rule(min(interval(E,_)),E,'SIMP_MIN_UPTO').
simp_rule(Eq,conjunct(member(E,S),forall([X],member(X,S),less_equal(E,X))),'DEF_EQUAL_MIN') :-
is_equality(Eq,E,min(S)),
new_identifier(member(E,S),X).
simp_rule(Eq,conjunct(member(E,S),forall([X],member(X,S),greater_equal(E,X))),'DEF_EQUAL_MAX') :-
is_equality(Eq,E,max(S)),
new_identifier(member(E,S),X).
simp_rule(min(U),min(New),'SIMP_MIN_BUNION_SING') :- U = union(_,_), select_op(set_extension([min(T)]),U,T,New,union).
simp_rule(max(U),max(New),'SIMP_MAX_BUNION_SING') :- U = union(_,_), select_op(set_extension([max(T)]),U,T,New,union).
simp_rule(Expr,falsity,'SIMP_POW_EQUAL_EMPTY') :- is_empty(Expr,pow_subset(_)).
simp_rule(Expr,equal(S,empty_set),'SIMP_POW1_EQUAL_EMPTY') :- is_empty(Expr,pow1_subset(S)).
simp_rule(Expr,subset(S,set_extension([empty_set])),'SIMP_KUNION_EQUAL_EMPTY') :- is_empty(Expr,general_union(S)).
simp_rule(negation(P),Q,'Propagate negation') :- negate(P,Q), Q \= negation(_). % De-Morgan and similar rules to propagate negation
simp_rule(P,truth,'Evaluate tautology') :- is_true(P).
Calls:
Called:
Name: simp_rule/6 |
Module: sequent_prover |
simp_rule(D,implication(negation(P),D0),'DEF_OR',OuterOp) :- OuterOp \= disjunct, D = disjunct(_,_), select_op(P,D,D0,disjunct).
simp_rule(C,falsity,'SIMP_SPECIAL_AND_BFALSE',OuterOp) :- OuterOp \= conjunct, member_of(conjunct,falsity,C).
simp_rule(D,truth,'SIMP_SPECIAL_OR_BTRUE',OuterOp) :- OuterOp \= disjunct, member_of(disjunct,truth,D).
simp_rule(C,Res,'SIMP_MULTI_AND',OuterOp) :- OuterOp \= conjunct, remove_duplicates(C,Res,conjunct).
simp_rule(D,Res,'SIMP_MULTI_OR',OuterOp) :- OuterOp \= disjunct, remove_duplicates(D,Res,disjunct).
simp_rule(C,falsity,'SIMP_MULTI_AND_NOT',OuterOp) :-
OuterOp \= conjunct,
member_of(conjunct,Q,C),
member_of(conjunct,NotQ,C),
is_negation(Q,NotQ).
simp_rule(D,truth,'SIMP_MULTI_OR_NOT',OuterOp) :-
OuterOp \= disjunct,
member_of(disjunct,Q,D),
member_of(disjunct,NotQ,D),
is_negation(Q,NotQ).
simp_rule(I,empty_set,'SIMP_SPECIAL_BINTER',OuterOp) :- OuterOp \= intersection, member_of(intersection,empty_set,I).
simp_rule(I,Res,'SIMP_MULTI_BINTER',OuterOp) :- OuterOp \= intersection, remove_duplicates(I,Res,intersection).
simp_rule(U,Res,'SIMP_MULTI_BUNION',OuterOp) :- OuterOp \= union, remove_duplicates(U,Res,union).
simp_rule(C,empty_set,'SIMP_SPECIAL_CPROD',OuterOp) :- OuterOp \= cartesian_product, member_of(cartesian_product,empty_set,C).
simp_rule(C,empty_set,'SIMP_SPECIAL_FCOMP',OuterOp) :- OuterOp \= composition, member_of(composition,empty_set,C).
simp_rule(Comp,empty_set,'SIMP_SPECIAL_BCOMP',OuterOp) :- OuterOp \= ring, member_of(ring,empty_set,Comp).
simp_rule(C,Res,'DEF_BCOMP',OuterOp) :- OuterOp \= ring, C = ring(_,_), bwd_to_fwd_comp(C,Comp), reorder(Comp,Res,composition).
simp_rule(P,0,'SIMP_SPECIAL_PROD_0',OuterOp) :- OuterOp \= multiplication, member_of(multiplication,0,P).
Calls:
Name: member_of/3 |
Module: sequent_prover |
Name: \=/2 |
|
Name: reorder/3 |
Module: sequent_prover |
Name: bwd_to_fwd_comp/2 |
Module: sequent_prover |
Name: =/2 |
|
Name: remove_duplicates/3 |
Module: sequent_prover |
Name: is_negation/2 |
Module: sequent_prover |
Name: select_op/4 |
Module: sequent_prover |
Called:
Name: simp_rule/6 |
Module: sequent_prover |
simp_rule(U,Ty,'SIMP_TYPE_BUNION',OuterOp,Info) :- OuterOp \= union, member_of(union,Ty,U), type_expression(Ty,Info).
simp_rule(Over,Res,'SIMP_TYPE_OVERL_CPROD',OuterOp,Info) :-
OuterOp \= overwrite,
Over = overwrite(_,_),
op_to_list(Over,List,overwrite),
overwrite_type(List,[],ResList,Info),
List \= ResList,
list_to_op(ResList,Res,overwrite).
Calls:
Name: list_to_op/3 |
Module: sequent_prover |
Name: \=/2 |
|
Name: overwrite_type/4 |
Module: sequent_prover |
Name: op_to_list/3 |
Module: sequent_prover |
Name: =/2 |
|
Name: type_expression/2 |
Module: sequent_prover |
Name: member_of/3 |
Module: sequent_prover |
Called:
Name: simp_rule/6 |
Module: sequent_prover |
simp_rule(X,NewX,Rule,Op,Descr,Info) :-
(simp_rule(X,NewX,Rule)
; simp_rule(X,NewX,Rule,Op)
; simp_rule_with_info(X,NewX,Rule,Info)
; simp_rule(X,NewX,Rule,Op,Info)),
create_descr(Rule,X,Descr).
simp_rule(X,NewX,Rule,_,Descr,_) :- simp_rule_with_descr(X,NewX,Rule,Descr).
simp_rule(Expr,Res,Expr,_,Descr,_) :- compute(Expr,Res), create_descr('Compute',Expr,Descr).
simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,P], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,Q].
simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,P,R], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,Q,R].
simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,R,P], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,R,Q].
Calls:
Name: =../2 |
|
Name: RECURSIVE_CALL/6 |
Module: sequent_prover |
Name: create_descr/3 |
Module: sequent_prover |
Name: compute/2 |
Module: sequent_prover |
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
Name: simp_rule/5 |
Module: sequent_prover |
Name: simp_rule_with_info/4 |
Module: sequent_prover |
Name: simp_rule/4 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Called:
Name: simp_rule/6 |
Module: sequent_prover |
simp_rule_with_descr(couple(function(event_b_first_projection_v2,E),function(event_b_second_projection_v2,F)),E,Rule,Rule) :-
Rule = 'SIMP_MAPSTO_PRJ1_PRJ2',
equal_terms(E,F).
simp_rule_with_descr(domain(successor),Z,Rule,Rule) :- Rule = 'SIMP_DOM_SUCC', is_integer_set(Z).
simp_rule_with_descr(range(successor),Z,Rule,Rule) :- Rule = 'SIMP_RAN_SUCC', is_integer_set(Z).
simp_rule_with_descr(predecessor,reverse(successor),Rule,Rule) :- Rule = 'DEF_PRED'.
simp_rule_with_descr(Expr,negation(member(A,SetB)),'SIMP_BINTER_SING_EQUAL_EMPTY'(A),Descr) :-
is_empty(Expr,Inter),
is_inter(Inter,SetA,SetB),
singleton_set(SetA,A),
create_descr('SIMP_BINTER_SING_EQUAL_EMPTY',A,Descr).
Calls:
Name: create_descr/3 |
Module: sequent_prover |
Name: singleton_set/2 |
Module: sequent_prover |
Name: is_inter/3 |
Module: sequent_prover |
Name: is_empty/2 |
Module: sequent_prover |
Name: =/2 |
|
Name: is_integer_set/1 |
Module: sequent_prover |
Name: equal_terms/2 |
Module: sequent_prover |
Called:
Name: simp_rule/6 |
Module: sequent_prover |
simp_rule_with_hyps(domain(R),E,'DERIV_DOM_TOTALREL',Hyps) :- member_hyps(member(R,FT),Hyps), is_rel(FT,total,E,_).
simp_rule_with_hyps(range(R),F,'DERIV_RAN_SURJREL',Hyps) :- member_hyps(member(R,FT),Hyps), is_surj(FT,_,F).
simp_rule_with_hyps(function(domain_restriction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMRES',Hyps) :-
member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
simp_rule_with_hyps(function(domain_subtraction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMSUB',Hyps) :-
member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
simp_rule_with_hyps(function(range_restriction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANRES',Hyps) :-
member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
simp_rule_with_hyps(function(range_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANSUB',Hyps) :-
member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
simp_rule_with_hyps(function(set_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_SETMINUS',Hyps) :-
member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
simp_rule_with_hyps(card(set_subtraction(S,T)),minus(card(S),card(T)),'SIMP_CARD_SETMINUS',Hyps) :-
member_hyps(subset(T,S),Hyps),
(member_hyps(finite(T),Hyps)
; member_hyps(finite(S),Hyps)).
simp_rule_with_hyps(card(set_subtraction(S,set_extension(L))),minus(card(S),card(set_extension(L))),Rule,Hyps) :-
Rule = 'SIMP_CARD_SETMINUS_SETENUM',
all_in_set(L,S,Hyps).
simp_rule_with_hyps(L,less(A,B),'DERIV_LESS',Hyps) :- is_less_eq(L,A,B), is_no_equality(Ex,A,B), member(Ex,Hyps).
Calls:
Name: member/2 |
|
Name: is_no_equality/3 |
Module: sequent_prover |
Name: is_less_eq/3 |
Module: sequent_prover |
Name: all_in_set/3 |
Module: sequent_prover |
Name: =/2 |
|
Name: member_hyps/2 |
Module: sequent_prover |
Name: is_fun/4 |
Module: sequent_prover |
Name: is_surj/3 |
Module: sequent_prover |
Name: is_rel/4 |
Module: sequent_prover |
Called:
Name: simp_rule_with_hyps/5 |
Module: sequent_prover |
simp_rule_with_hyps(X,NewX,Rule,Hyps,_) :- simp_rule_with_hyps(X,NewX,Rule,Hyps).
simp_rule_with_hyps(Ex,disjunct(greater('$'(E),F),less('$'(E),F)),'DERIV_NOT_EQUAL',Hyps,Info) :-
is_no_equality(Ex,'$'(E),F),
(number(F) ; of_integer_type(E,Hyps,Info)).
simp_rule_with_hyps(C,NewC,Rule,Hyps,Info) :- C=..[F,P], simp_rule_with_hyps(P,Q,Rule,Hyps,Info), NewC=..[F,Q].
simp_rule_with_hyps(C,NewC,Rule,Hyps,Info) :- C=..[F,P,R], simp_rule_with_hyps(P,Q,Rule,Hyps,Info), NewC=..[F,Q,R].
simp_rule_with_hyps(C,NewC,Rule,Hyps,Info) :- C=..[F,R,P], simp_rule_with_hyps(P,Q,Rule,Hyps,Info), NewC=..[F,R,Q].
Calls:
Name: =../2 |
|
Name: RECURSIVE_CALL/5 |
Module: sequent_prover |
Name: of_integer_type/3 |
Module: sequent_prover |
Name: number/1 |
|
Name: is_no_equality/3 |
Module: sequent_prover |
Name: simp_rule_with_hyps/4 |
Module: sequent_prover |
Called:
Name: simp_rule_with_hyps/5 |
Module: sequent_prover |
simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_DOMSUB_EQUAL_TYPE',Info) :-
is_equality(Eq,domain_subtraction(S,R),Ty),
type_expression(Ty,Info).
simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_RANSUB_EQUAL_TYPE',Info) :-
is_equality(Eq,range_subtraction(R,S),Ty),
type_expression(Ty,Info).
simp_rule_with_info(Eq,equal(R,reverse(Ty)),'SIMP_CONVERSE_EQUAL_TYPE',Info) :-
is_equality(Eq,reverse(R),Ty),
type_expression(Ty,Info).
simp_rule_with_info(subset(_,Ty),truth,'SIMP_TYPE_SUBSETEQ',Info) :- type_expression(Ty,Info).
simp_rule_with_info(set_subtraction(_,Ty),empty_set,'SIMP_TYPE_SETMINUS',Info) :- type_expression(Ty,Info).
simp_rule_with_info(set_subtraction(Ty,set_subtraction(Ty,S)),S,'SIMP_TYPE_SETMINUS_SETMINUS',Info) :- type_expression(Ty,Info).
simp_rule_with_info(member(_,Ty),truth,'SIMP_TYPE_IN',Info) :- type_expression(Ty,Info).
simp_rule_with_info(subset_strict(S,Ty),not_equal(S,Ty),'SIMP_TYPE_SUBSET_L',Info) :- type_expression(Ty,Info).
simp_rule_with_info(Eq,conjunct(equal(A,Ty),equal(B,empty_set)),'SIMP_SETMINUS_EQUAL_TYPE',Info) :-
is_equality(Eq,set_subtraction(A,B),Ty),
type_expression(Ty,Info).
simp_rule_with_info(Eq,Res,'SIMP_BINTER_EQUAL_TYPE',Info) :-
is_equality(Eq,I,Ty),
I = intersection(_,_),
type_expression(Ty,Info),
and_equal_type(I,Ty,Res).
simp_rule_with_info(Eq,equal(S,set_extension([Ty])),'SIMP_KINTER_EQUAL_TYPE',Info) :-
is_equality(Eq,general_intersection(S),Ty),
type_expression(Ty,Info).
simp_rule_with_info(Expr,falsity,'SIMP_TYPE_EQUAL_EMPTY',Info) :- is_empty(Expr,Ty), type_expression(Ty,Info).
simp_rule_with_info(Eq,forall([X],P,equal(E,Ty)),'SIMP_QINTER_EQUAL_TYPE',Info) :-
is_equality(Eq,quantified_intersection([X],P,E),Ty),
type_expression(Ty,Info).
simp_rule_with_info(I,S,'SIMP_TYPE_BINTER',Info) :- (I = intersection(S,Ty) ; I = intersection(Ty,S)), type_expression(Ty,Info).
simp_rule_with_info(Eq,falsity,'SIMP_TYPE_EQUAL_RELDOMRAN',Info) :-
is_equality(Eq,R,Ty),
type_expression(Ty,Info),
is_rel(R,_,_,_),
R=..[Op,_,_],
\+ member(Op,[relations,partial_function,partial_injection]).
simp_rule_with_info(member(Prj,RT),truth,Rule,Info) :-
(Prj = event_b_first_projection_v2, Rule = 'DERIV_PRJ1_SURJ'
; Prj = event_b_second_projection_v2, Rule = 'DERIV_PRJ2_SURJ'),
is_rel(RT,_,Ty1,Ty2),
\+ is_inj(RT,Ty1,Ty2),
type_expression(Ty1,Info),
type_expression(Ty2,Info).
simp_rule_with_info(member(event_b_identity,RT),truth,'DERIV_ID_BIJ',Info) :- is_rel(RT,_,Ty,Ty), type_expression(Ty,Info).
simp_rule_with_info(domain_restriction(Ty,R),R,'SIMP_TYPE_DOMRES',Info) :- type_expression(Ty,Info).
simp_rule_with_info(range_restriction(R,Ty),R,'SIMP_TYPE_RANRES',Info) :- type_expression(Ty,Info).
simp_rule_with_info(domain_subtraction(Ty,R),R,'SIMP_TYPE_DOMSUB',Info) :- type_expression(Ty,Info).
simp_rule_with_info(range_subtraction(R,Ty),R,'SIMP_TYPE_RANSUB',Info) :- type_expression(Ty,Info).
simp_rule_with_info(image(R,Ty),range(R),'SIMP_TYPE_RELIMAGE',Info) :- type_expression(Ty,Info).
Calls:
Name: type_expression/2 |
Module: sequent_prover |
Name: is_rel/4 |
Module: sequent_prover |
Name: is_inj/3 |
Module: sequent_prover |
Name: not/1 |
|
Name: =/2 |
|
Name: member/2 |
|
Name: =../2 |
|
Name: is_equality/3 |
Module: sequent_prover |
Name: is_empty/2 |
Module: sequent_prover |
Name: and_equal_type/3 |
Module: sequent_prover |
Called:
Name: simp_rule/6 |
Module: sequent_prover |
singleton_set(set_extension([X]),X).
Called:
Name: simp_rule/3 |
Module: sequent_prover |
Name: simp_rule_with_descr/4 |
Module: sequent_prover |
Name: union_subset_member/3 |
Module: sequent_prover |
sort_components([],[]).
sort_components([c(L,T)|Rest], Res) :-
member(T,[disjunct,conjunct,union,intersection,add,multiplication,equal,not_equal,negation,unary_minus,equivalence,set_extension,list]), !,
sort_list(L,SL),
sort_components(Rest,R),
Res=[c(SL,T)|R].
sort_components([c(L,T)|Rest], Res) :- !, % non-commutative
sort_components(L,L2),
sort_components(Rest,R),
Res=[c(L2,T)|R].
sort_components([E|Rest], [E|R]) :- atomic(E), !, sort_components(Rest,R).
sort_components([E|Rest], [F|R]) :- sort_list(E,F), sort_components(Rest,R).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: sort_list/2 |
Module: sequent_prover |
Name: ! |
|
Name: atomic/1 |
|
Name: =/2 |
|
Name: member/2 |
Called:
Name: sort_list/2 |
Module: sequent_prover |
sort_list(L,R) :- sort_components(L,S), samsort(S,R).
Calls:
Name: samsort/2 |
Module: foo_error |
Name: sort_components/2 |
Module: sequent_prover |
Called:
Name: equal_lists/2 |
Module: sequent_prover |
Name: sort_components/2 |
Module: sequent_prover |
Name: stronger_list/2 |
Module: sequent_prover |
start(state(sequent(SHyps,Goal,success),Info),[description(PO)]) :- start2(Hyps,Goal,PO,Info), sort(Hyps,SHyps),
translate:set_unicode_mode, translate:set_force_eventb_mode.
Calls:
Name: set_force_eventb_mode/0 |
Module: translate |
Name: set_unicode_mode/0 |
Module: translate |
Name: sort/2 |
|
Name: start2/4 |
Module: sequent_prover |
start2([equal('$'(x),2)],
conjunct(equal('$'(y),'$'(y)),equal('$'(x),2)),'simple example 1').
start2([equal('$'(x),2)],
implication(equal('$'(y),'$'(x)),equal('$'(y),2)),'simple example 2').
start2([equal('$'(x),2)],
disjunct(negation(equal('$'(y),'$'(x))),equal('$'(y),2)),'simple example 3').
start2(
[equal(intersection(set_extension(['$'(red)]),set_extension(['$'(green)])),empty_set),
member('$'(peds_colour),set_extension(['$'(red),'$'(green)])), % inv2,2
equal('$'(peds_go),convert_bool(equal('$'(peds_colour),'$'(green)))), % inv2,4
member('$'(new_colour),set_extension(['$'(red),'$'(green),'$'(yellow),'$'(redyellow)])), %grd1
implication(disjunct(equal('$'(new_colour),'$'(green)),
disjunct(equal('$'(new_colour),'$'(yellow)),
equal('$'(new_colour),'$'(redyellow)))),
equal('$'(peds_colour),'$'(red))),
equal('$'(new_value),convert_bool(disjunct(equal('$'(new_colour),'$'(green)),
disjunct(equal('$'(new_colour),'$'(yellow)),
equal('$'(new_colour),'$'(redyellow))))))
],
implication(equal('$'(new_value),boolean_true),equal('$'(peds_go),boolean_false))
,'SKS sheet 10').
start2(
[member('$'(n),natural1_set),
member('$'(arr),total_function(interval(1,'$'(n)),natural1_set)),
member('$'(mxi),interval(1,'$'(n))),
forall(['$'(j)],member('$'(j),interval(1,'$'(n))),greater_equal(function('$'(arr),'$'(mxi)),function('$'(arr),'$'(j))))
],
conjunct(conjunct(conjunct(
member('$'(arr),partial_function(interval(1,'$'(n)),natural1_set)),
member('$'(mxi),domain('$'(arr)))),
not_equal(range('$'(arr)),empty_set)),
exists(['$'(b)],forall(['$'(x)],member('$'(x),range('$'(arr))),greater_equal('$'(b),'$'(x)))))
,'SKS sheet 11').
Called:
Name: start/2 |
Module: sequent_prover |
start2(Hyps,Goal,PO,[]) :- start2(Hyps,Goal,PO).
Calls:
Name: start2/3 |
Module: sequent_prover |
Called:
Name: start/2 |
Module: sequent_prover |
stronger_list(L1,L2) :- sort_list(L1,SL1), sort_list(L2,SL2), list_implies(SL1,SL2).
Calls:
Name: list_implies/2 |
Module: sequent_prover |
Name: sort_list/2 |
Module: sequent_prover |
Called:
Name: member_hyps/2 |
Module: sequent_prover |
subset_inter(S,intersection(A,B),Conj) :- subset_inter(S,A,ConjA), subset_inter(S,B,ConjB), Conj = conjunct(ConjA,ConjB), !.
subset_inter(S,A,subset(S,A)).
Calls:
Name: ! |
|
Name: =/2 |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
symb_trans(Rule,state(Sequent,Info),state(NewSequent,Info)) :- symb_trans(Rule,Sequent,NewSequent,Info).
Calls:
Name: symb_trans/4 |
Module: sequent_prover |
Called:
Name: symb_trans/3 |
Module: sequent_prover |
symb_trans(add_hyp(Hyp),sequent(Hyps0,Goal,Cont),NewSequent,Info) :- % CUT
parse_input(Hyp,TExpr),
well_def_hyps:normalize_predicate(TExpr,NormExpr),
get_wd_pos(NormExpr,Hyps0,Info,POs),
add_hyps(POs,Hyps0,Hyps1),
translate_finite_expr(NormExpr,NewExpr),
add_hyps([NewExpr|POs],Hyps0,Hyps2),
add_wd_pos(Hyps0,POs,sequent(Hyps1,NewExpr,sequent(Hyps2,Goal,Cont)),NewSequent).
symb_trans(distinct_case(Pred),sequent(Hyps0,Goal,Cont),NewSequent,Info) :-
parse_input(Pred,TExpr),
well_def_hyps:normalize_predicate(TExpr,NormExpr),
get_wd_pos(NormExpr,Hyps0,Info,POs),
translate_finite_expr(NormExpr,NewExpr),
add_hyps([NewExpr|POs],Hyps0,Hyps1),
add_hyps([negation(NewExpr)|POs],Hyps0,Hyps2),
add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont)),NewSequent).
symb_trans(exists_inst(Inst),sequent(Hyps,exists([X|Ids],Pred),Cont),NewSequent,Info) :-
parse_input(Inst,TExpr),
well_def_hyps:normalize_expression(TExpr,NormExpr),
rewrite(X,NormExpr,Pred,Goal1),
(Ids = [] -> Goal = Goal1 ; Goal = exists(Ids,Goal1)),
get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
add_wd_pos(Hyps,POs,sequent(Hyps,Goal,Cont),NewSequent).
symb_trans(forall_inst(Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
parse_input(Inst,TExpr),
well_def_hyps:normalize_expression(TExpr,NormExpr),
select(Hyp,Hyps,NewHyp,NewHyps),
Hyp = forall([X|Ids],P,Q),
rewrite(X,NormExpr,P,P1),
rewrite(X,NormExpr,Q,Q1),
(Ids = [] -> NewHyp = implication(P1,Q1) ; NewHyp = forall(Ids,P1,Q1)),
get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
add_wd_pos(Hyps,POs,sequent(NewHyps,Goal,Cont),NewSequent).
symb_trans(forall_inst_mp(Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
parse_input(Inst,TExpr),
well_def_hyps:normalize_expression(TExpr,NormExpr),
rewrite(X,NormExpr,P,P1),
rewrite(X,NormExpr,Q,Q1),
get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
select(forall([X],P,Q),Hyps,Hyps0),
add_hyps(POs,Hyps0,Hyps1),
add_hyps([Q1|POs],Hyps0,Hyps2),
add_wd_pos(Hyps,POs,sequent(Hyps1,P1,sequent(Hyps2,Goal,Cont)),NewSequent).
symb_trans(forall_inst_mt(Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
parse_input(Inst,TExpr),
well_def_hyps:normalize_expression(TExpr,NormExpr),
rewrite(X,NormExpr,negation(P),P1),
rewrite(X,NormExpr,negation(Q),Q1),
get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
select(forall([X],P,Q),Hyps,Hyps0),
add_hyps(POs,Hyps0,Hyps1),
add_hyps([P1|POs],Hyps0,Hyps2),
add_wd_pos(Hyps,POs,sequent(Hyps1,Q1,sequent(Hyps2,Goal,Cont)),NewSequent).
symb_trans(ml_pp,sequent(Hyps,Goal,Cont),Cont,_) :-
get_typed_ast(Goal,TGoal),
maplist(get_typed_ast,Hyps,THyps),
atelierb_provers_interface:prove_predicate(THyps,TGoal,proved).
symb_trans(rewrite_hyp(HypNr,NewHyp),sequent(Hyps,Goal,Cont),sequent(NewHyps,Goal,Cont),Info) :-
ground(HypNr),
get_hyp(Hyps,HypNr,SelHyp),
parse_input(NewHyp,TExpr),
b_interpreter_check:norm_pred_check(TExpr,RewrittenHyp),
select(SelHyp,Hyps,Hyps0),
get_wd_pos(RewrittenHyp,Hyps,Info,[]),
prove_predicate([SelHyp],RewrittenHyp),
translate_finite_expr(RewrittenHyp,NewExpr),
add_hyp(NewExpr,Hyps0,NewHyps).
symb_trans(derive_hyp(HypNrs,NewHyp),sequent(Hyps,Goal,Cont),sequent(NewHyps,Goal,Cont),Info) :-
ground(HypNrs),
split_atom(HypNrs,[','],Indices),
maplist(get_hyp(Hyps),Indices,SelHyps),
parse_input(NewHyp,TExpr),
b_interpreter_check:norm_pred_check(TExpr,NormExpr),
get_wd_pos(NormExpr,Hyps,Info,[]),
prove_predicate(SelHyps,NormExpr),
translate_finite_expr(NormExpr,NewExpr),
add_hyp(NewExpr,Hyps,NewHyps).
Calls:
Name: add_hyp/3 |
Module: sequent_prover |
Name: translate_finite_expr/2 |
Module: sequent_prover |
Name: prove_predicate/2 |
Module: sequent_prover |
Name: get_wd_pos/4 |
Module: sequent_prover |
Name: norm_pred_check/2 |
Module: b_interpreter_check |
Name: parse_input/2 |
Module: sequent_prover |
Name: maplist/3 |
Module: foo_error |
Name: split_atom/3 |
Module: foo_error |
Name: ground/1 |
|
Name: select/3 |
Module: foo_error |
Name: get_hyp/3 |
Module: sequent_prover |
Name: prove_predicate/3 |
Module: atelierb_provers_interface |
Name: get_typed_ast/2 |
Module: sequent_prover |
Name: add_wd_pos/4 |
Module: sequent_prover |
Name: add_hyps/3 |
Module: sequent_prover |
Name: get_wd_pos_of_expr/4 |
Module: sequent_prover |
Name: rewrite/4 |
Module: sequent_prover |
Name: normalize_expression/2 |
Module: well_def_hyps |
Name: =/2 |
|
Name: ->/3 |
|
Name: select/4 |
Module: foo_error |
Name: normalize_predicate/2 |
Module: well_def_hyps |
Called:
Name: symb_trans/3 |
Module: sequent_prover |
symb_trans_enabled(Rule,state(Sequent,_)) :- symb_trans_enabled(Rule,Sequent).
symb_trans_enabled(add_hyp,sequent(_,_,_)).
symb_trans_enabled(distinct_case,sequent(_,_,_)).
symb_trans_enabled(exists_inst,sequent(_,exists(_,_),_)).
symb_trans_enabled(forall_inst,sequent(Hyps,_,_)) :- memberchk(forall(_,_,_),Hyps).
symb_trans_enabled(forall_inst_mp,sequent(Hyps,_,_)) :- memberchk(forall([_],_,_),Hyps).
symb_trans_enabled(forall_inst_mt,sequent(Hyps,_,_)) :- memberchk(forall([_],_,_),Hyps).
symb_trans_enabled(ml_pp,sequent(_,_,_)).
symb_trans_enabled(rewrite_hyp,sequent(_,_,_)).
symb_trans_enabled(derive_hyp,sequent(_,_,_)).
Calls:
Name: memberchk/2 |
|
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
trans(Rule,state(Sequent,Info),state(NewSequent,Info)) :- trans1(Rule,Sequent,NewSequent).
Calls:
Name: trans1/3 |
Module: sequent_prover |
Called:
| Module: test_sequent_prover | |
Name: test_transition/3 |
Module: test_sequent_prover |
trans(Rule,state(Sequent,Info),state(NewSequent,Info),Descr) :- trans1(Rule,Sequent,NewSequent,Descr).
trans(simplify_goal(Rule),state(sequent(Hyps,Goal,Cont),Info),
state(sequent(Hyps,NewGoal,Cont),Info),[description(Descr)]) :-
simp_rule(Goal,NewGoal,Rule,level0,Descr,Info)
; simp_rule_with_hyps(Goal,NewGoal,Rule,Hyps,Info), create_descr(Rule,Goal,Descr).
trans(simplify_hyp(Rule,Hyp),state(sequent(Hyps,Goal,Cont),Info),
state(sequent(SHyps,Goal,Cont),Info),[description(Descr)]) :-
select(Hyp,Hyps,NewHyp,NewHyps),
(simp_rule(Hyp,NewHyp,Rule,level0,Descr,Info)
; simp_rule_with_hyps(Hyp,NewHyp,Rule,Hyps,Info), create_descr(Rule,Hyp,Descr)),
without_duplicates(NewHyps,SHyps).
trans(mon_deselect(Nr),state(sequent(Hyps,Goal,Cont),Info),state(sequent(Hyps0,Goal,Cont),Info1),[description(Descr)]) :-
nth1(Nr,Hyps,Hyp,Hyps0),
add_meta_info(des_hyps,Info,Hyp,Info1),
create_descr(mon_deselect,Hyp,Descr).
trans(RuleArg,state(Sequent,Info),state(NewSequent,Info1),[description(Descr)]) :-
(trans2(RuleArg,Sequent,NewSequent), Info1 = Info
; trans2(RuleArg,state(Sequent,Info),state(NewSequent,Info1))),
RuleArg=..[Rule,Arg], create_descr(Rule,Arg,Descr).
trans(RuleArg,state(sequent(Hyps,Goal,Cont),Info),state(Cont,Info),[description(Descr)]) :-
axiom2(RuleArg,Hyps,Goal), RuleArg=..[Rule,Arg], create_descr(Rule,Arg,Descr).
Calls:
Name: create_descr/3 |
Module: sequent_prover |
Name: =../2 |
|
Name: axiom2/3 |
Module: sequent_prover |
Name: trans2/3 |
Module: sequent_prover |
Name: =/2 |
|
Name: add_meta_info/4 |
Module: sequent_prover |
Name: nth1/4 |
Module: foo_error |
Name: without_duplicates/2 |
Module: sequent_prover |
Name: simp_rule_with_hyps/5 |
Module: sequent_prover |
Name: simp_rule/6 |
Module: sequent_prover |
Name: select/4 |
Module: foo_error |
Name: trans1/4 |
Module: sequent_prover |
Called:
| Module: test_sequent_prover | |
Name: test_transition/3 |
Module: test_sequent_prover |
trans1(Rule,sequent(Hyps,Goal,Cont),Cont) :- axiom(Rule,Hyps,Goal).
trans1(dbl_hyp,sequent(Hyps,Goal,Cont),sequent(SHyps,Goal,Cont)) :-
% not really necessary if we remove duplicates in Hyps everywhere else
without_duplicates(Hyps,SHyps), SHyps \= Hyps.
trans1(or_r,sequent(Hyps,disjunct(GA,GB),Cont),sequent(Hyps1,GA,Cont)) :-
negate(GB,NotGB), % we could also negate GA and use GB as goal
add_hyp(NotGB,Hyps,Hyps1).
trans1(imp_r,sequent(Hyps,implication(G1,G2),Cont),
sequent(Hyps1,G2,Cont)) :-
add_hyp(G1,Hyps,Hyps1).
trans1(and_r,sequent(Hyps,conjunct(G1,G2),Cont),
sequent(Hyps,G1,sequent(Hyps,G2,Cont))).
trans1(neg_in,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
member(member(E,set_extension(L)),Hyps),
member(InEq,Hyps),
is_no_equality(InEq,E,B),
member(C,L),
equal_terms(B,C),
select(C,L,R),
select(member(E,set_extension(L)),Hyps,member(E,set_extension(R)),Hyps1).
trans1(xst_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
Hyp = exists(_,P),
select(Hyp,Hyps,P,Hyps1).
trans1(all_r,sequent(Hyps,forall(_,P,Q),Cont),sequent(Hyps,implication(P,Q),Cont)).
trans1(contradict_r,sequent(Hyps,Goal,Cont),sequent(Hyps0,falsity,Cont)) :-
add_hyp(negation(Goal),Hyps,Hyps0).
trans1(upper_bound_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(Set),Cont)) :-
Goal = exists([B],forall([X],member(X,Set),greater_equal(B,X))). % TODO: Set must not contain any bound variable
trans1(fin_lt_0,sequent(Hyps,finite(S),Cont),sequent(Hyps,Goal1,sequent(Hyps,Goal2,Cont))):-
new_identifier(S,X),
new_identifier(member(S,X),N),
Goal1 = exists([N],forall([X],member(X,S),less_equal(N,X))),
Goal2 = subset(S,set_subtraction(integer_set,natural1_set)).
trans1(fin_ge_0,sequent(Hyps,finite(S),Cont),sequent(Hyps,Goal1,sequent(Hyps,Goal2,Cont))):-
new_identifier(S,X),
new_identifier(member(S,X),N),
Goal1 = exists([N],forall([X],member(X,S),less_equal(X,N))),
Goal2 = subset(S,natural_set).
trans1(fin_binter_r,sequent(Hyps,finite(I),Cont),sequent(Hyps,Disj,Cont)) :-
I = intersection(_,_),
finite_intersection(I,Disj).
trans1(fin_kinter_r,sequent(Hyps,finite(general_intersection(S)),Cont),
sequent(Hyps,conjunct(exists([X],member(X,S)),finite(X)),Cont)) :- new_identifier(S,X).
trans1(fin_qinter_r,sequent(Hyps,finite(quantified_intersection([X],P,E)),Cont),
sequent(Hyps,conjunct(exists([X],member(X,P)),finite(E)),Cont)).
trans1(fin_kunion_r,sequent(Hyps,finite(general_union(S)),Cont),
sequent(Hyps,conjunct(finite(S),forall([X],member(X,S),finite(X))),Cont)) :- new_identifier(S,X).
trans1(fin_qunion_r,sequent(Hyps,finite(quantified_union([X],P,E)),Cont),
sequent(Hyps,conjunct(finite(event_b_comprehension_set([X],E,P)),forall([X],P,finite(E))),Cont)).
trans1(fin_setminus_r,sequent(Hyps,finite(set_subtraction(S,_)),Cont),sequent(Hyps,finite(S),Cont)).
trans1(fin_rel_img_r,sequent(Hyps,finite(image(F,_)),Cont),sequent(Hyps,finite(F),Cont)).
trans1(fin_rel_ran_r,sequent(Hyps,finite(range(F)),Cont),sequent(Hyps,finite(F),Cont)).
trans1(fin_rel_dom_r,sequent(Hyps,finite(domain(F)),Cont),sequent(Hyps,finite(F),Cont)).
trans1(fin_fun_dom,sequent(Hyps,finite(Fun),Cont),sequent(Hyps,truth,Cont1)) :-
member_hyps(member(Fun,FunType),Hyps),
is_fun(FunType,_,Dom,_),
(member_hyps(finite(Dom),Hyps)
-> Cont1 = Cont
; Cont1 = sequent(Hyps,finite(Dom),Cont)).
trans1(fin_fun_ran,sequent(Hyps,finite(Fun),Cont),sequent(Hyps,truth,Cont1)) :-
member_hyps(member(Fun,FunType),Hyps),
is_inj(FunType,_,Ran),
(member_hyps(finite(Ran),Hyps)
-> Cont1 = Cont
; Cont1 = sequent(Hyps,finite(Ran),Cont)).
trans1(sim_ov_rel,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),relations(A,B)),Cont),
sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
member_hyps(member(Fun,FunType),Hyps),
is_rel(FunType,_,A,B).
trans1(sim_ov_trel,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),total_relation(A,B)),Cont),
sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
member_hyps(member(Fun,FunType),Hyps),
is_rel(FunType,total,A,B).
trans1(sim_ov_pfun,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),partial_function(A,B)),Cont),
sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
member_hyps(member(Fun,FunType),Hyps),
is_fun(FunType,_,A,B).
trans1(sim_ov_tfun,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),total_function(A,B)),Cont),
sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
member_hyps(member(Fun,FunType),Hyps),
is_fun(FunType,total,A,B).
trans1(skip_to_cont,sequent(Hyps,Goal,Cont),NewState) :-
\+ cont_length(Cont,0),
append_sequents(Cont,sequent(Hyps,Goal,success),NewState).
Calls:
Name: append_sequents/3 |
Module: sequent_prover |
Name: cont_length/2 |
Module: sequent_prover |
Name: not/1 |
|
Name: is_fun/4 |
Module: sequent_prover |
Name: member_hyps/2 |
Module: sequent_prover |
Name: is_rel/4 |
Module: sequent_prover |
Name: =/2 |
|
Name: ->/3 |
|
Name: is_inj/3 |
Module: sequent_prover |
Name: new_identifier/2 |
Module: sequent_prover |
Name: finite_intersection/2 |
Module: sequent_prover |
Name: add_hyp/3 |
Module: sequent_prover |
Name: select/4 |
Module: foo_error |
Name: select/3 |
Module: foo_error |
Name: equal_terms/2 |
Module: sequent_prover |
Name: member/2 |
|
Name: is_no_equality/3 |
Module: sequent_prover |
Name: negate/2 |
Module: sequent_prover |
Name: \=/2 |
|
Name: without_duplicates/2 |
Module: sequent_prover |
Name: axiom/3 |
Module: sequent_prover |
Called:
Name: trans/3 |
Module: sequent_prover |
trans1(eq(Dir,X,Y),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,Cont),[description(Descr)]) :- select(equal(X,Y),Hyps,Hyps0),
(Dir=lr,
maplist(rewrite(X,Y),Hyps0,Hyps1),
rewrite(X,Y,Goal,Goal1)
; Dir=rl,
maplist(rewrite(Y,X),Hyps0,Hyps1),
rewrite(Y,X,Goal,Goal1)),
create_descr(eq,Dir,equal(X,Y),Descr).
trans1(eqv(Dir,X,Y),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,Cont),[description(Descr)]) :- select(equivalence(X,Y),Hyps,Hyps0),
(Dir=lr,
maplist(rewrite(X,Y),Hyps0,Hyps1),
rewrite(X,Y,Goal,Goal1)
; Dir=rl,
maplist(rewrite(Y,X),Hyps0,Hyps1),
rewrite(Y,X,Goal,Goal1)),
create_descr(eq,Dir,equal(X,Y),Descr).
Calls:
Name: create_descr/4 |
Module: sequent_prover |
Name: rewrite/4 |
Module: sequent_prover |
Name: maplist/3 |
Module: foo_error |
Name: =/2 |
|
Name: select/3 |
Module: foo_error |
Called:
Name: trans/3 |
Module: sequent_prover |
trans2(and_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
Hyp = conjunct(P,Q),
select(Hyp,Hyps,Hyps0),
add_hyps(P,Q,Hyps0,Hyps1).
trans2(imp_l1(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
Imp = implication(P,Q),
select(Imp,Hyps,implication(NewP,Q),Hyps1),
select_conjunct(PP,P,NewP),
member(H,Hyps),
equal_terms(H,PP).
trans2(reselect_hyp(Hyp),state(sequent(Hyps,Goal,Cont),Info),state(sequent(Hyps1,Goal,Cont),Info1)) :-
remove_meta_info(des_hyps,Info,Hyp,Info1),
add_hyp(Hyp,Hyps,Hyps1).
trans2(imp_and_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
Hyp = implication(P,conjunct(Q,R)),
select(Hyp,Hyps,Hyps0),
add_hyps(implication(P,Q),implication(P,R),Hyps0,Hyps1).
trans2(imp_or_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
Hyp = implication(disjunct(P,Q),R),
select(Hyp,Hyps,Hyps0),
add_hyps(implication(P,R),implication(Q,R),Hyps0,Hyps1).
trans2(contradict_l(P),sequent(Hyps,Goal,Cont),sequent(Hyps1,NotP,Cont)):-
select(P,Hyps,Hyps0),
negate(P,NotP),
negate(Goal,NotGoal),
add_hyp(NotGoal,Hyps0,Hyps1).
trans2(or_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
Hyp = disjunct(P,Q),
select(Hyp,Hyps,Hyps0),
add_hyp(P,Hyps0,Hyps1),
add_hyp(Q,Hyps0,Hyps2).
trans2(case(D),sequent(Hyps,Goal,Cont),NewState) :-
member(D,Hyps),
D = disjunct(_,_),
select(D,Hyps,Hyps0),
extract_disjuncts(D,Hyps0,Goal,Cont,NewState).
trans2(imp_case(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
Imp = implication(P,Q),
select(Imp,Hyps,Hyps0),
add_hyp(negation(P),Hyps0,Hyps1),
add_hyp(Q,Hyps0,Hyps2).
trans2(mh(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps0,P,sequent(Hyps1,Goal,Cont))) :-
Imp = implication(P,Q),
select(Imp,Hyps,Hyps0),
add_hyp(Q,Hyps0,Hyps1).
trans2(hm(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps0,negation(Q),sequent(Hyps1,Goal,Cont))) :-
Imp = implication(P,Q),
select(Imp,Hyps,Hyps0),
add_hyp(negation(P),Hyps0,Hyps1).
Calls:
Name: add_hyp/3 |
Module: sequent_prover |
Name: select/3 |
Module: foo_error |
Name: =/2 |
|
Name: extract_disjuncts/5 |
Module: sequent_prover |
Name: member/2 |
|
Name: negate/2 |
Module: sequent_prover |
Name: add_hyps/4 |
Module: sequent_prover |
Name: remove_meta_info/4 |
Module: sequent_prover |
Name: equal_terms/2 |
Module: sequent_prover |
Name: select_conjunct/3 |
Module: sequent_prover |
Name: select/4 |
Module: foo_error |
Called:
Name: trans/4 |
Module: sequent_prover |
trans_prop(add_hyp,param_names(['Hyp'])).
trans_prop(distinct_case,param_names(['Pred'])).
trans_prop(exists_inst,param_names(['Inst'])).
trans_prop(forall_inst,param_names(['Inst'])).
trans_prop(forall_inst_mp,param_names(['Inst'])).
trans_prop(forall_inst_mt,param_names(['Inst'])).
trans_prop(ml_pp,param_names([])).
trans_prop(rewrite_hyp,param_names(['HypNr','NewHyp'])).
trans_prop(derive_hyp,param_names(['HypNrs','NewHyp'])).
translate_finite_expr(Term,Term) :- atomic(Term).
translate_finite_expr(member(S,fin_subset(S)),finite(S)).
translate_finite_expr(Term,Result) :-
Term=..[F|Args],
maplist(translate_finite_expr,Args,NewArgs),
Result=..[F|NewArgs].
Calls:
Name: =../2 |
|
Name: maplist/3 |
Module: foo_error |
Name: atomic/1 |
Called:
Name: symb_trans/4 |
Module: sequent_prover |
translate_term(Term,Str) :-
catch(well_def_hyps:translate_norm_expr_with_limit(Term,300,Str), % probably only works when ProB is run from source
_Exc,Str=Term).
Calls:
Name: catch/3 |
Called:
Name: prop/2 |
Module: sequent_prover |
Name: create_descr/3 |
Module: sequent_prover |
Name: cell_content/5 |
Module: sequent_prover |
Name: create_descr/4 |
Module: sequent_prover |
type_expression(bool_set,_).
type_expression(Z,_) :- is_integer_set(Z).
type_expression('$'(Set),Info) :- get_meta_info(rawsets,Info,RawSets), member(deferred_set(_,Set),RawSets).
type_expression(pow_subset(Ty),Info) :- type_expression(Ty,Info).
type_expression(cartesian_product(Ty1,Ty2),Info) :- type_expression(Ty1,Info), type_expression(Ty2,Info).
Calls:
Name: RECURSIVE_CALL/2 |
Module: sequent_prover |
Name: member/2 |
|
Name: get_meta_info/3 |
Module: sequent_prover |
Name: is_integer_set/1 |
Module: sequent_prover |
Called:
Name: simp_rule_with_info/4 |
Module: sequent_prover |
Name: simp_rule/5 |
Module: sequent_prover |
Name: overwrite_type/4 |
Module: sequent_prover |
union_image(union(A,B),S,Union) :- union_image(A,S,L), union_image(B,S,R), !, Union = union(L,R).
union_image(A,S,image(A,S)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
union_subset(S,union(A,B),Conj) :- union_subset(S,A,ConjA), union_subset(S,B,ConjB), !, Conj = conjunct(ConjA,ConjB).
union_subset(S,A,subset(A,S)).
Calls:
Name: =/2 |
|
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
union_subset_member(T,union(A,B),Conj) :-
union_subset_member(T,A,ConjA),
union_subset_member(T,B,ConjB),!,
Conj = conjunct(ConjA,ConjB).
union_subset_member(T,SetF,member(F,T)) :- singleton_set(SetF,F), !.
union_subset_member(T,A,subset(A,T)).
Calls:
Name: ! |
|
Name: singleton_set/2 |
Module: sequent_prover |
Name: =/2 |
|
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Called:
Name: simp_rule/3 |
Module: sequent_prover |
upper_bound(Hyps,X,B) :- member(L,Hyps),is_less_eq(L,X,B), number(B).
upper_bound(Hyps,X,B1) :- member(L,Hyps), is_less(L,X,B), number(B), B1 is B-1.
upper_bound(Hyps,X,B) :- member(Eq,Hyps), is_equality(Eq,X,B), number(B).
Calls:
Name: number/1 |
|
Name: is_equality/3 |
Module: sequent_prover |
Name: member/2 |
|
Name: is/2 |
|
Name: is_less/3 |
Module: sequent_prover |
Name: is_less_eq/3 |
Module: sequent_prover |
Called:
Name: derive_goal/2 |
Module: sequent_prover |
used_identifiers(Term,[]) :- atomic(Term), !.
used_identifiers(Term,[Term]) :- Term = '$'(E), atomic(E), !.
used_identifiers(C,Res) :-
C =.. [_|Args],
maplist(used_identifiers,Args,L),
append(L,Res).
Calls:
Name: append/2 |
Module: foo_error |
Name: maplist/3 |
Module: foo_error |
Name: =../2 |
|
Name: ! |
|
Name: atomic/1 |
|
Name: =/2 |
Called:
Name: new_identifier/2 |
Module: sequent_prover |
Name: new_function/2 |
Module: sequent_prover |
Name: simp_rule/3 |
Module: sequent_prover |
Name: new_identifiers/3 |
Module: sequent_prover |
Name: get_typed_identifiers/2 |
Module: sequent_prover |
| Module: sequent_prover |
with_ids(exists(Ids,_),Ids).
with_ids(event_b_comprehension_set(Ids,_),Ids).
with_ids(forall(Ids,_,_),Ids).
with_ids(quantified_union(Ids,_,_),Ids).
with_ids(quantified_intersection(Ids,_,_),Ids).
Called:
Name: rewrite/4 |
Module: sequent_prover |
Name: get_typed_identifiers/2 |
Module: sequent_prover |
without_duplicates(L,Res) :- without_duplicates(L,[],Res).
Calls:
Name: without_duplicates/3 |
Module: sequent_prover |
Called:
Name: trans/4 |
Module: sequent_prover |
Name: add_hyps/3 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
Name: add_hyp/3 |
Module: sequent_prover |
Name: add_hyps/4 |
Module: sequent_prover |
without_duplicates([],List,List).
without_duplicates([E|R],Filtered,Res) :-
member(F,Filtered),
equal_terms(E,F),!,
without_duplicates(R,Filtered,Res).
without_duplicates([E|R],Filtered, Res) :-
\+ member(E,Filtered),
append(Filtered,[E],New),
without_duplicates(R,New,Res).
Calls:
Name: RECURSIVE_CALL/3 |
Module: sequent_prover |
Name: append/3 |
|
Name: member/2 |
|
Name: not/1 |
|
Name: ! |
|
Name: equal_terms/2 |
Module: sequent_prover |
Called:
Name: trans/4 |
Module: sequent_prover |
Name: add_hyps/3 |
Module: sequent_prover |
Name: trans1/3 |
Module: sequent_prover |
Name: add_hyp/3 |
Module: sequent_prover |
Name: add_hyps/4 |
Module: sequent_prover |