1		% Heinrich Heine Universitaet Duesseldorf
2		% (c) 2025-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		% Implementation of a Sequent Prover
6		% where we can use the ProB animator to perform proof steps
7		% proof rules taken/adapted from https://wiki.event-b.org/index.php/Inference_Rules
8		% rewrite rules taken/adapted from https://wiki.event-b.org/index.php/All_Rewrite_Rules
9		% the term representation is the one from ProB's well_definedness prover
10
11		:- module(sequent_prover,[initialise_for_po_file/1,
12		cont_length/2,
13		get_continuations/2,
14		get_scope/3,
15		parse_input/3,
16		translate_norm_expr_term/2,
17		used_identifiers/2,
18
19		po_nr_label/2, normalised_hyps/3, normalised_goal/3
20		]).
21
22		:- use_module(probsrc(module_information),[module_info/2]).
23		:- module_info(group,sequent_prover).
24		:- module_info(description,'This module provides rewrite and inference rules for the sequent_prover').
25
26		:- use_module(library(lists)).
27		:- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2]).
28		:- use_module(probsrc(tools),[ajoin/2, flatten/2, list_intersection/3, list_difference/3]).
29		:- use_module(probsrc(translate),[transform_raw/2]).
30		:- use_module(wdsrc(well_def_hyps),[convert_norm_expr_to_raw/2,
31		normalize_expression/2, normalize_predicate/2]).
32		:- use_module(seqproversrc(sequent_auto_prover),[bounded_find_proof/5]).
33		:- use_module(seqproversrc(simplification_rules),[simplification_rule/6, is_true/1]).
34		:- use_module(seqproversrc(prover_utils)).
35
36		% ------------------------
37		:- dynamic normalised_hyps/3, normalised_goal/3, po_nr_label/2. % for BPR export
38
39		initialise_for_po_file(File) :-
40		retractall(normalised_pred(_,_,_)),
41		retractall(normalised_pred(_,_,_)),
42		retractall(po_nr_label(_,_)),
43		bb_put(po_counter,1),
44		load_from_po_file(File,Hyps,Goal,PO,PODesc,Info),
45		sort(Hyps,SHyps),
46		% for ProB XTL Mode: specifying the start states:
47		bb_get(po_counter,PONR),
48		assertz(po_nr_label(PONR,PO)),
49		assertz(xtl_interface:start(state(sequent(SHyps,Goal,success(PONR)),Info),[description(PODesc)])),
50		P1 is PONR+1, bb_put(po_counter,P1),
51		fail.
52		initialise_for_po_file(_) :-
53		% assert other xtl_interface predicates:
54		assertz((xtl_interface:trans(A,B,C) :- sequent_prover:sequent_prover_trans_start(A,B,C))),
55		assertz((xtl_interface:trans(A,B,C,D) :- sequent_prover:sequent_prover_trans_start_desc(A,B,C,D))),
56		assertz((xtl_interface:trans_prop(A,B) :- sequent_prover:trans_prop(A,B))),
57		assertz((xtl_interface:prop(A,B) :- sequent_prover:prop(A,B))),
58		assertz((xtl_interface:symb_trans(A,B,C,D) :- sequent_prover:symb_trans(A,B,C,D))),
59		assertz((xtl_interface:symb_trans_enabled(A,B) :- sequent_prover:symb_trans_enabled(A,B))),
60		assertz((xtl_interface:animation_function_result(A,B) :- sequent_prover:animation_function_result(A,B))),
61		assertz((xtl_interface:animation_image_right_click_transition(A,B,C) :- sequent_prover:animation_image_right_click_transition(A,B,C))),
62		assertz((xtl_interface:animation_image_right_click_transition(A,B,C,D) :- sequent_prover:animation_image_right_click_transition(A,B,C,D))),
63		assertz(xtl_interface:nr_state_properties(30)). % TODO: a dynamic solution would be nice.
64
65		:- use_module(probsrc(preferences),[get_preference/2]).
66		rodin_mode :- get_preference(sequent_prover_rodin_mode,true).
67
68		% declare these public as we will assert calls to them in the code above for initialise_for_po_file:
69		:- public prop/2, sequent_prover_trans/3, sequent_prover_trans_desc/4, symb_trans/4, symb_trans_enabled/2.
70		:- public animation_function_result/2, animation_image_right_click_transition/3, animation_image_right_click_transition/4.
71		:- public sequent_prover_trans_start/3, sequent_prover_trans_start_desc/4, trans_prop/2.
72
73		% ------------------------
74
75		get_normalised_bexpr(Expr,NormExpr) :-
76		transform_raw(Expr,TExpr),
77		normalize_predicate(TExpr,NormExpr).
78
79		:- use_module(probsrc(xtl_interface),[get_disprover_po/6]).
80		load_from_po_file(_File,Hyps,Goal,POLabel,FullPOLabel,[rawsets(RawSets),des_hyps(OtherHyps)]) :-
81		% we use the disprover_po facts already loaded in xtl_interface, load_po_file(File) not necessary
82		get_disprover_po(POLabel,Context,RawGoal,RawAllHyps,RawSelHyps,RodinStatus),
83		ajoin([POLabel,' (',RodinStatus,')'],FullPOLabel),
84		get_normalised_bexpr(RawGoal,Goal),
85		list_difference(RawAllHyps,RawSelHyps,RawNotSelHyps),
86		maplist(get_normalised_bexpr,RawSelHyps,Hyps),
87		maplist(get_normalised_bexpr,RawNotSelHyps,OtherHyps),
88		append(RawSelHyps,RawNotSelHyps,RawPreds), append(Hyps,OtherHyps,NormPreds),
89		assertz(normalised_hyps(POLabel,RawPreds,NormPreds)),
90		assertz(normalised_goal(POLabel,RawGoal,Goal)),
91		bmachine_eventb:extract_ctx_sections(Context,_Name,_Extends,RawSets,_Constants,_AbstractConstants,_Axioms,_Theorems).
92
93
94		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs) :-
95		get_scope(Hyps,Info,Scope),
96		get_identifier_types(Scope,IdsTypes),
97		new_aux_identifier(IdsTypes,Y), !,
98		get_wd_pos2(equal('$'(Y),NormExpr),Scope,POs).
99
100		get_wd_pos(NormExpr,Hyps,Info,POs) :-
101		get_scope(Hyps,Info,Scope),
102		get_wd_pos2(NormExpr,Scope,POs).
103
104		get_wd_pos2(NormExpr,Scope,POs) :-
105		convert_norm_expr_to_raw(NormExpr,ParsedRaw),
106		bmachine:b_type_check_raw_expr(ParsedRaw,Scope,TypedPred,open(_)),
107		well_def_hyps:empty_hyps(H),
108		well_def_analyser:compute_all_wd_pos(TypedPred,H,[],TPOs),
109		maplist(rewrite_type_set,TPOs,TPOsT),
110		maplist(normalize_predicate,TPOsT,POs).
111
112		get_scope(Hyps,Info,[identifier([])]) :-
113		get_meta_info(des_hyps,Info,DHyps),
114		append(Hyps,DHyps,[]), !.
115		get_scope(Hyps,Info,[identifier(Res)]) :-
116		get_meta_info(des_hyps,Info,DHyps),
117		append(Hyps,DHyps,AllHyps),
118		used_identifiers(AllHyps,Ids),
119		sort(Ids,SortedIds),
120		maplist(replace_bounded_ids(SortedIds),Hyps,HypsWithFreshBIds),!,
121		(HypsWithFreshBIds=[] -> HypsConj=truth
122		; list_to_op(HypsWithFreshBIds,HypsConj,conjunct)),
123		get_set_types(Ids,Info,SetIds),
124		get_typed_identifiers(HypsConj,[identifier(SetIds)],List),
125		append(SetIds,List,AllIds),
126		select_types(AllIds,Res).
127
128		replace_bounded_ids(_,E,Res) :- atomic(E),!,Res=E.
129		replace_bounded_ids(_,'$'(E),Res) :- atomic(E),!,Res='$'(E).
130		replace_bounded_ids(Ids,E,F) :-
131		with_ids(E,BIds), % expression has bounded ids
132		length(BIds,Len),
133		possible_identifier(X),
134		range_ids(X,Len,NewIds), % generate X_1, X_2, ... as NewIds
135		list_intersection(Ids,NewIds,[]), !, % check if these are fresh
136		rewrite_pairwise_ids(BIds,NewIds,E,F).
137		replace_bounded_ids(Ids,E,F) :- % E is a compound term not introducing bounded ids
138		E=..[Op|Args],
139		maplist(replace_bounded_ids(Ids),Args,NewArgs),
140		F=..[Op|NewArgs].
141
142		rewrite_pairwise_ids([],[],E,E).
143		rewrite_pairwise_ids([X|TX],[Y|TY],E,Res) :-
144		replace_id(X,Y,E,NewE),
145		rewrite_pairwise_ids(TX,TY,NewE,Res).
146
147		replace_id('$'(X),'$'(Y),'$'(X),'$'(Y)) :- atomic(X), !.
148		replace_id(X,Y,C,NewC) :- C=..[Op|Args],
149		maplist(replace_id(X,Y),Args,NewArgs),
150		NewC=..[Op|NewArgs].
151
152		filter_hyps([],[]).
153		filter_hyps([Expr|Hyps],Res) :- with_ids(Expr,_), !, filter_hyps(Hyps,Res).
154		filter_hyps([Expr|Hyps],[Expr|Res]) :- filter_hyps(Hyps,Res).
155
156		get_set_types([],_,[]).
157		get_set_types(['$'(SetId)|T],Info,[b(identifier(SetId),set(global(SetId)),[])|R]) :-
158		is_deferred_or_enumerated_set('$'(SetId),Info),!,
159		get_set_types(T,Info,R).
160		get_set_types([_|T],Info,R) :- get_set_types(T,Info,R).
161
162		rewrite_type_set(X,Res) :- \+ compound(X),!, Res=X.
163		rewrite_type_set(b(typeset,set(global(SET)),I),b(identifier(SET),set(global(SET)),I)) :- !.
164		rewrite_type_set(C,NewC) :- C=..[Op|Args],
165		maplist(rewrite_type_set,Args,NewArgs),
166		NewC =.. [Op|NewArgs].
167
168		in_scope(Id,[identifier(List)]) :- memberchk(b(identifier(Id),_,[]),List).
169
170
171
172		select_types(Types,Selected) :- sort(Types,Sorted), select_types_aux(Sorted,Selected).
173
174		select_types_aux([],[]).
175		select_types_aux([b(identifier(X),any,_)|R],Res) :- member(b(identifier(X),T,_),R), T \= any, !, select_types_aux(R,Res).
176		select_types_aux([Id|R],[Id|Res]) :- select_types_aux(R,Res).
177
178		get_typed_ast(NormExpr,TExpr) :-
179		convert_norm_expr_to_raw(NormExpr,RawExpr),
180		transform_raw(RawExpr,TExpr).
181
182		get_identifier_types([identifier(IdsTypes)],IdsTypes).
183
184		prove_predicate(Hyps,Goal) :-
185		get_typed_ast(Goal,TGoal),
186		maplist(get_typed_ast,Hyps,THyps),
187		atelierb_provers_interface:prove_predicate(THyps,TGoal,proved).
188
189
190
191		get_po_description(PONR,PO) :-
192		xtl_interface:start(state(sequent(_SHyps,_Goal,success(PONR)),_Info),[description(PO)]).
193
194
195		:- use_module(library(timeout), [time_out/3]).
196		% specifying properties that appear in the State Properties view:
197		prop(success(_Nr),goal).
198		prop(success(Nr),'='('DISCHARGED',PO)) :- get_po_description(Nr,PO).
199		prop(counter_example(_),'COUNTER_EXAMPLE_FOUND').
200		prop(counter_example(C),'='(ID,S)) :- member(binding(ID,_,S),C).
201		prop(sequent(_,X,_), '='('GOAL',XS)) :- translate_norm_expr_term(X,XS).
202		prop(sequent(Hyps,_,_),'='(HypNr,XS)) :- nth1(Nr,Hyps,X),
203		translate_norm_expr_term(X,XS), ajoin(['HYP',Nr],HypNr).
204		prop(sequent(_,_,Cont),'='('CONTINUATION',P)) :- cont_length(Cont,P).
205		prop(state(sequent(Hyps,Goal,_),Info),'='(AutoProofStepNr,ProofStep)) :-
206		(time_out(bounded_find_proof(sequent(Hyps,Goal,success(0)),Info,3,[],Proof),1500,TORes),
207		TORes = success
208		-> nth1(Nr,Proof,ProofStep),
209		ajoin(['AUTO-PROOF-',Nr],AutoProofStepNr)).
210
211		prop(state(S,_),Val) :- prop(S,Val).
212
213
214		cont_length(sequent(_,_,C),R) :- !, cont_length(C,R1), R is R1+1.
215		cont_length(success(_),R) :- !, R=0.
216		cont_length(C,R) :- add_internal_error('Illegal continuation:',cont_length(C,R)),R=0.
217
218		% ------------------------
219
220		:- discontiguous trans_prop/2, symb_trans_rule/4, symb_trans_rule/5, symb_trans_enabled/2.
221
222		sequent_prover_trans_start(Rule,state(Sequent,Info),NewState) :-
223		update_info(Sequent,Info,Info1),
224		sequent_prover_trans(Rule,state(Sequent,Info1),NewState).
225		sequent_prover_trans_start_desc(Rule,state(Sequent,Info),NewState,Descr) :-
226		update_info(Sequent,Info,Info1),
227		sequent_prover_trans_desc(Rule,state(Sequent,Info1),NewState,Descr).
228
229		update_info(Sequent,Info,Info1) :-
230		Sequent = sequent(Hyps,_,_),
231		get_scope(Hyps,Info,[identifier(IdsTypes)]),
232		update_meta_infos(ids_types,Info,IdsTypes,Info1).
233
234		% transition rules without description information:
235		sequent_prover_trans(Rule,state(Sequent,Info),state(NewSequent,Info)) :-
236		trans_with_info(Rule,Sequent,NewSequent,Info).
237
238		sequent_prover_trans(lasso,state(sequent(Hyps,Goal,Cont),Info),state(sequent(NewHyps,Goal,Cont),NewInfo)) :-
239		get_meta_info(des_hyps,Info,DesHyps),
240		used_identifiers_list([Goal|Hyps],UsedIds),
241		find_hyps_with(UsedIds,DesHyps,SelectedHyps),
242		SelectedHyps \= [],
243		add_hyps(SelectedHyps,Hyps,NewHyps),
244		list_difference(DesHyps,SelectedHyps,LeftDesHyps),
245		update_meta_infos(des_hyps,Info,LeftDesHyps,NewInfo).
246
247		% transition rules with description information:
248		sequent_prover_trans_desc(Rule,state(Sequent,Info),state(NewSequent,Info),Descr) :-
249		trans_desc_with_info(Rule,Sequent,NewSequent,Info,Descr).
250		sequent_prover_trans_desc(RuleArg,state(Sequent,Info),state(NewSequent,Info1),[description(Descr)]) :-
251		(trans_with_args(RuleArg,Sequent,NewSequent), Info1 = Info
252		; trans_with_args_info(RuleArg,state(Sequent,Info),state(NewSequent,Info1))
253		),
254		RuleArg=..[Rule,Arg], create_descr(Rule,Arg,Descr).
255		sequent_prover_trans_desc(mon_deselect(Nr),state(sequent(Hyps,Goal,Cont),Info),
256		state(sequent(Hyps0,Goal,Cont),Info1),[description(Descr)]) :-
257		nth1(Nr,Hyps,Hyp,Hyps0),
258		add_meta_info(des_hyps,Info,Hyp,Info1),
259		create_descr(mon_deselect,Hyp,Descr).
260
261		% transition rules requiring Infos and returning descriptions
262		trans_desc_with_info(Rule,Sequent,NewSequent,_Info,Desc) :-
263		trans_desc_wo_info(Rule,Sequent,NewSequent,Desc).
264		trans_desc_with_info(Rule,Sequent,NewSequent,Info,Desc) :-
265		trans_desc_simplification_rule(Rule,Sequent,NewSequent,Info,Desc).
266
267		trans_desc_simplification_rule(simplify_goal(Rule),sequent(Hyps,Goal,Cont),
268		NewSequent,Info,[description(Descr)]) :-
269		simplification_rule(Goal,NewGoal,Hyps,Rule,Descr,Info),
270		(rodin_mode, NewGoal=conjunct(_,_)
271		-> op_to_list(NewGoal,ListOfGoals,conjunct),
272		add_goals(Hyps,ListOfGoals,Cont,NewSequent)
273		; NewSequent=sequent(Hyps,NewGoal,Cont)).
274		trans_desc_simplification_rule(simplify_hyp(Rule,Hyp),sequent(Hyps,Goal,Cont),
275		sequent(SHyps,Goal,Cont),Info,[description(Descr)]) :-
276		select(Hyp,Hyps,NewHyp,NewHyps),
277		simplification_rule(Hyp,NewHyp,Hyps,Rule,Descr,Info),
278		(rodin_mode, NewHyp=conjunct(_,_)
279		-> append(PH,[NewHyp|TH],NewHyps),
280		op_to_list(NewHyp,NewConjHyps,conjunct),
281		append(NewConjHyps,TH,NTH),
282		append(PH,NTH,AddHyps)
283		; AddHyps=NewHyps),
284		without_duplicates(AddHyps,SHyps).
285
286
287		% transition rules without descriptions but with Info being passed
288		trans_with_info(Rule,Sequent,NewSequent,_Info) :- trans_wo_info(Rule,Sequent,NewSequent).
289		trans_with_info(deriv_le_card,sequent(Hyps,Goal,Cont),sequent(Hyps,subset(S,T),Cont),Info) :- % covers DERIV_GE_CARD too
290		is_less_eq(Goal,card(S),card(T)),
291		get_meta_info(ids_types,Info,IdsTypes),
292		same_type(S,T,IdsTypes).
293		trans_with_info(deriv_lt_card,sequent(Hyps,Goal,Cont),sequent(Hyps,subset_strict(S,T),Cont),Info) :- % / DERIV_GT_CARD
294		is_less(Goal,card(S),card(T)),
295		get_meta_info(ids_types,Info,IdsTypes),
296		same_type(S,T,IdsTypes).
297		trans_with_info(deriv_equal_card,sequent(Hyps,equal(card(S),card(T)),Cont),sequent(Hyps,equal(S,T),Cont),Info) :-
298		get_meta_info(ids_types,Info,IdsTypes),
299		same_type(S,T,IdsTypes).
300		trans_with_info(sim_rel_image_r,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
301		rewrite_once(image(F,set_extension([E])),set_extension([function(F,E)]),Goal,NewGoal),
302		get_wd_pos(NewGoal,Hyps,Info,POs),
303		add_wd_pos(Hyps,POs,sequent(Hyps,NewGoal,Cont),NewSequent).
304		trans_with_info(sim_rel_image_l,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
305		select(Hyp,Hyps,Hyps0),
306		rewrite_once(image(F,set_extension([E])),set_extension([function(F,E)]),Hyp,NewHyp),
307		add_hyp(NewHyp,Hyps0,Hyps1),
308		get_wd_pos(NewHyp,Hyps0,Info,POs),
309		add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,Cont),NewSequent).
310		trans_with_info(sim_fcomp_l,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
311		select(Hyp,Hyps,Hyps0),
312		Sub = function(Comp,X),
313		is_subterm(Sub,Hyp),
314		split_composition(Comp,F,G),
315		NewSub = function(G,function(F,X)),
316		rewrite_once(Sub,NewSub,Hyp,NewHyp),
317		add_hyp(NewHyp,Hyps0,Hyps1),
318		get_wd_pos(NewHyp,Hyps0,Info,POs),
319		add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,Cont),NewSequent).
320		trans_with_info(sim_fcomp_r,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
321		Sub = function(Comp,X),
322		is_subterm(Sub,Goal),
323		split_composition(Comp,F,G),
324		NewSub = function(G,function(F,X)),
325		rewrite_once(Sub,NewSub,Goal,NewGoal),
326		get_wd_pos(NewGoal,Hyps,Info,POs),
327		add_wd_pos(Hyps,POs,sequent(Hyps,NewGoal,Cont),NewSequent).
328		trans_with_info(xst_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont),Info) :-
329		Hyp = exists(Ids,P),
330		select(Hyp,Hyps,NewP,Hyps1),
331		get_meta_info(ids_types,Info,IdsTypes),
332		replace_used_ids(Ids,IdsTypes,NewIds),
333		rewrite_pairwise_rev(Ids,NewIds,P,NewP).
334		trans_with_info(all_r,sequent(Hyps,forall(Ids,P,Q),Cont),sequent(Hyps,NewImp,Cont),Info) :-
335		get_meta_info(ids_types,Info,IdsTypes),
336		replace_used_ids(Ids,IdsTypes,NewIds),
337		rewrite_pairwise_rev(Ids,NewIds,implication(P,Q),NewImp).
338		trans_with_info(Rule,sequent(Hyps,Goal,Cont),Cont,Info) :- axiom_with_info(Rule,Hyps,Goal,Info).
339		trans_with_info(Rule,sequent(Hyps,Goal,Cont),Cont,Info) :- (member(Hyp,Hyps), mb_goal(Rule,Hyp,Goal,Info)) ; mb_goal(Rule,Hyps,Goal).
340
341		% transitions which do not require Infos (about typed ids)
342		trans_wo_info(Rule,sequent(Hyps,Goal,Cont),Cont) :- axiom(Rule,Hyps,Goal).
343		trans_wo_info(dbl_hyp,sequent(Hyps,Goal,Cont),sequent(SHyps,Goal,Cont)) :-
344		% not really necessary if we remove duplicates in Hyps everywhere else
345		without_duplicates(Hyps,SHyps), SHyps \= Hyps.
346		trans_wo_info(or_r,sequent(Hyps,disjunct(GA,GB),Cont),sequent(Hyps1,GA,Cont)) :-
347		% Hyps |- G1 or G2 ===> Hyps,not(G1) |- G2
348		negate(GB,NotGB), % we could also negate GA and use GB as goal
349		add_hyp(NotGB,Hyps,Hyps1).
350		trans_wo_info(imp_r,sequent(Hyps,implication(G1,G2),Cont),
351		sequent(Hyps1,G2,Cont)) :-
352		% Hyps |- G1 => G2 ===> Hyps,G1 |- G2
353		add_hyp(G1,Hyps,Hyps1).
354		trans_wo_info(and_r,sequent(Hyps,conjunct(G1,G2),Cont),NewSequent) :-
355		% Hyps |- G1 & G2 ===> Hyps |- G1 + Hyps |- G2
356		op_to_list(conjunct(G1,G2),ListOfGoals,conjunct),
357		add_goals(Hyps,ListOfGoals,Cont,NewSequent).
358		trans_wo_info(neg_in,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :- % covers NEG_IN_L and NEG_IN_R
359		member(member(E,set_extension(L)),Hyps),
360		member(InEq,Hyps),
361		is_inequality(InEq,E,B),
362		member(C,L),
363		equal_terms(B,C),
364		select(C,L,R),
365		select(member(E,set_extension(L)),Hyps,member(E,set_extension(R)),Hyps1).
366		trans_wo_info(contradict_r,sequent(Hyps,Goal,Cont),sequent(Hyps0,falsity,Cont)) :-
367		Goal \= falsity, % proof rule is useless here; we just add not(falsity) to hyp
368		add_hyp(negation(Goal),Hyps,Hyps0).
369		trans_wo_info(lower_bound_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(Set),Cont)) :-
370		Goal = exists([B],forall([X],member(X,Set),less_equal(B,X))). % TODO: Set must not contain any bound variable
371		trans_wo_info(lower_bound_r,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(Set),Cont)) :-
372		Goal = exists([B],forall([X],member(X,Set),greater_equal(X,B))). % TODO: Set must not contain any bound variable
373		trans_wo_info(upper_bound_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(Set),Cont)) :-
374		Goal = exists([B],forall([X],member(X,Set),greater_equal(B,X))). % TODO: Set must not contain any bound variable
375		trans_wo_info(upper_bound_r,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(Set),Cont)) :-
376		Goal = exists([B],forall([X],member(X,Set),less_equal(X,B))). % TODO: Set must not contain any bound variable
377		trans_wo_info(fin_lt_0,sequent(Hyps,finite(S),Cont),sequent(Hyps,Goal1,sequent(Hyps,Goal2,Cont))):-
378		new_identifier(S,X),
379		new_identifier(member(S,X),N),
380		Goal1 = exists([N],forall([X],member(X,S),less_equal(N,X))),
381		Goal2 = subset(S,set_subtraction(integer_set,natural1_set)).
382		trans_wo_info(fin_ge_0,sequent(Hyps,finite(S),Cont),sequent(Hyps,Goal1,sequent(Hyps,Goal2,Cont))):-
383		new_identifier(S,X),
384		new_identifier(member(S,X),N),
385		Goal1 = exists([N],forall([X],member(X,S),less_equal(X,N))),
386		Goal2 = subset(S,natural_set).
387		trans_wo_info(fin_binter_r,sequent(Hyps,finite(I),Cont),sequent(Hyps,Disj,Cont)) :-
388		I = intersection(_,_),
389		finite_intersection(I,Disj).
390		trans_wo_info(fin_kinter_r,sequent(Hyps,finite(general_intersection(S)),Cont),
391		sequent(Hyps,conjunct(exists([X],member(X,S)),finite(X)),Cont)) :- new_identifier(S,X).
392		trans_wo_info(fin_qinter_r,sequent(Hyps,finite(quantified_intersection([X],P,E)),Cont),
393		sequent(Hyps,conjunct(exists([X],member(X,P)),finite(E)),Cont)).
394		trans_wo_info(fin_kunion_r,sequent(Hyps,finite(general_union(S)),Cont),
395		sequent(Hyps,conjunct(finite(S),forall([X],member(X,S),finite(X))),Cont)) :- new_identifier(S,X).
396		trans_wo_info(fin_qunion_r,sequent(Hyps,finite(quantified_union([X],P,E)),Cont),
397		sequent(Hyps,conjunct(finite(event_b_comprehension_set([X],E,P)),forall([X],P,finite(E))),Cont)).
398		trans_wo_info(fin_setminus_r,sequent(Hyps,finite(set_subtraction(S,_)),Cont),sequent(Hyps,finite(S),Cont)).
399		trans_wo_info(fin_rel_img_r,sequent(Hyps,finite(image(F,_)),Cont),sequent(Hyps,finite(F),Cont)).
400		trans_wo_info(fin_rel_ran_r,sequent(Hyps,finite(range(F)),Cont),sequent(Hyps,finite(F),Cont)).
401		trans_wo_info(fin_rel_dom_r,sequent(Hyps,finite(domain(F)),Cont),sequent(Hyps,finite(F),Cont)).
402		trans_wo_info(fin_fun_dom,sequent(Hyps,finite(Fun),Cont),sequent(Hyps,truth,Cont1)) :-
403		member_hyps(member(Fun,FunType),Hyps),
404		is_fun(FunType,_,Dom,_),
405		(member_hyps(finite(Dom),Hyps)
406		-> Cont1 = Cont
407		; Cont1 = sequent(Hyps,finite(Dom),Cont)).
408		trans_wo_info(fin_fun_ran,sequent(Hyps,finite(Fun),Cont),sequent(Hyps,truth,Cont1)) :-
409		member_hyps(member(Fun,FunType),Hyps),
410		is_inj(FunType,_,Ran),
411		(member_hyps(finite(Ran),Hyps)
412		-> Cont1 = Cont
413		; Cont1 = sequent(Hyps,finite(Ran),Cont)).
414		trans_wo_info(sim_ov_rel,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),relations(A,B)),Cont),
415		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
416		member_hyps(member(Fun,FunType),Hyps),
417		is_rel(FunType,_,A,B).
418		trans_wo_info(sim_ov_trel,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),total_relation(A,B)),Cont),
419		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
420		member_hyps(member(Fun,FunType),Hyps),
421		is_rel(FunType,total,A,B).
422		trans_wo_info(sim_ov_pfun,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),partial_function(A,B)),Cont),
423		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
424		member_hyps(member(Fun,FunType),Hyps),
425		is_fun(FunType,_,A,B).
426		trans_wo_info(sim_ov_tfun,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),total_function(A,B)),Cont),
427		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
428		member_hyps(member(Fun,FunType),Hyps),
429		is_fun(FunType,total,A,B).
430		trans_wo_info(fun_image_goal,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
431		wd_strict_term(Goal),
432		is_subterm(Hyp,Goal),
433		Hyp = function(F,E),
434		member(member(F,RType),Hyps),
435		is_rel(RType,_,_,Ran),
436		\+ member(member(function(F,E),Ran),Hyps),
437		add_hyp(member(function(F,E),Ran),Hyps,Hyps1).
438		trans_wo_info(ov_setenum_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
439		select(Hyp,Hyps,Hyps0),
440		wd_strict_term(Hyp),
441		Fun = function(overwrite(F,set_extension([couple(E,V)])),G),
442		rewrite_once(Fun,V,Hyp,Hyp1),
443		add_hyps([equal(G,E),Hyp1],Hyps0,Hyps1),
444		rewrite_once(Fun,function(domain_subtraction(set_extension([E]),F),G),Hyp,Hyp2),
445		add_hyps([negation(equal(G,E)),Hyp2],Hyps0,Hyps2).
446		trans_wo_info(ov_setenum_r,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,sequent(Hyps2,Goal2,Cont))) :-
447		wd_strict_term(Goal),
448		Fun = function(overwrite(F,set_extension([couple(E,V)])),G),
449		rewrite_once(Fun,V,Goal,Goal1),
450		add_hyp(equal(G,E),Hyps,Hyps1),
451		rewrite_once(Fun,function(domain_subtraction(set_extension([E]),F),G),Goal,Goal2),
452		add_hyp(negation(equal(G,E)),Hyps,Hyps2).
453		trans_wo_info(ov_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
454		select(Hyp,Hyps,Hyps0),
455		wd_strict_term(Hyp),
456		Fun = function(overwrite(F,S),G),
457		rewrite_once(Fun,function(S,G),Hyp,Hyp1),
458		add_hyps([member(G,domain(S)),Hyp1],Hyps0,Hyps1),
459		rewrite_once(Fun,function(domain_subtraction(domain(S),F),G),Hyp,Hyp2),
460		add_hyps([negation(member(G,domain(S))),Hyp2],Hyps0,Hyps2).
461		trans_wo_info(ov_r,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,sequent(Hyps2,Goal2,Cont))) :-
462		wd_strict_term(Goal),
463		Fun = function(overwrite(F,S),G),
464		rewrite_once(Fun,function(S,G),Goal,Goal1),
465		add_hyp(member(G,domain(S)),Hyps,Hyps1),
466		rewrite_once(Fun,function(domain_subtraction(domain(S),F),G),Goal,Goal2),
467		add_hyp(negation(member(G,domain(S))),Hyps,Hyps2).
468		trans_wo_info(subset_inter,sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont)) :-
469		member_hyps(subset(T,U),Hyps),
470		free_identifiers(Goal,Ids),
471		member(T,Ids), % T and U are not bound
472		member(U,Ids),
473		is_subterm(Inter,Goal),
474		select_op(U,Inter,Inter0,intersection),
475		rewrite_once(Inter,Inter0,Goal,NewGoal),
476		member_of(intersection,T,Inter).
477		trans_wo_info(in_inter,sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont)) :-
478		member_hyps(member(E,T),Hyps),
479		free_identifiers(Goal,Ids),
480		member(E,Ids),
481		member(T,Ids),
482		is_subterm(Inter,Goal),
483		select_op(T,Inter,Inter0,intersection),
484		rewrite_once(Inter,Inter0,Goal,NewGoal),
485		member_of(intersection,set_extension([E]),Inter).
486		trans_wo_info(notin_inter,sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont)) :-
487		member_hyps(negation(member(E,T)),Hyps),
488		free_identifiers(Goal,Ids),
489		member(E,Ids),
490		member(T,Ids),
491		Inter = intersection(_,_),
492		is_subterm(Inter,Goal),
493		rewrite_once(Inter,empty_set,Goal,NewGoal),
494		member_of(intersection,set_extension([E]),Inter),
495		member_of(intersection,T,Inter).
496		trans_wo_info(card_interv,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,sequent(Hyps2,Goal2,Cont))) :-
497		wd_strict_term(Goal),
498		rewrite_once(card(interval(A,B)),add(minus(B,A),1),Goal,Goal1),
499		rewrite_once(card(interval(A,B)),0,Goal,Goal2),
500		add_hyp(less_equal(A,B),Hyps,Hyps1),
501		add_hyp(less(B,A),Hyps,Hyps2).
502		trans_wo_info(card_empty_interv,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
503		select(Hyp,Hyps,Hyps0),
504		wd_strict_term(Hyp),
505		rewrite_once(card(interval(A,B)),add(minus(B,A),1),Hyp,Hyp1),
506		rewrite_once(card(interval(A,B)),0,Hyp,Hyp2),
507		add_hyps([less_equal(A,B),Hyp1],Hyps0,Hyps1),
508		add_hyps([less(B,A),Hyp2],Hyps0,Hyps2).
509		trans_wo_info(simp_card_setminus_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps1,Goal,Cont))) :-
510		select(Hyp,Hyps,Hyps0),
511		rewrite_once(card(set_subtraction(S,T)),minus(card(S),card(intersection(S,T))),Hyp,Hyp1),
512		add_hyp(Hyp1,Hyps0,Hyps1).
513		trans_wo_info(simp_card_setminus_r,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps,NewGoal,Cont))) :-
514		rewrite_once(card(set_subtraction(S,T)),minus(card(S),card(intersection(S,T))),Goal,NewGoal).
515		trans_wo_info(simp_card_cprod_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps,finite(T),sequent(NewHyps,Goal,Cont)))) :-
516		select(Hyp,Hyps,NewHyp,NewHyps),
517		rewrite_once(card(cartesian_product(S,T)),multiplication(card(S),card(T)),Hyp,NewHyp).
518		trans_wo_info(simp_card_cprod_r,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps,finite(T),sequent(Hyps,NewGoal,Cont)))) :-
519		rewrite_once(card(cartesian_product(S,T)),multiplication(card(S),card(T)),Goal,NewGoal).
520		trans_wo_info(skip_to_cont,sequent(Hyps,Goal,Cont),NewState) :-
521		Cont \= success(_),
522		append_sequents(Cont,sequent(Hyps,Goal,success(PO_Nr)),NewState,PO_Nr).
523
524		finite_intersection(intersection(A,B),Disj) :- finite_intersection(A,DisjA), finite_intersection(B,DisjB), !, Disj = disjunct(DisjA,DisjB).
525		finite_intersection(S,finite(S)).
526
527		% trans_desc_wo_info/4
528		trans_desc_wo_info(eq(Dir,X,Y),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,Cont),[description(Descr)]) :-
529		select(equal(X,Y),Hyps,Hyps0),
530		(Dir=lr,
531		maplist(rewrite(X,Y),Hyps0,Hyps1),
532		rewrite(X,Y,Goal,Goal1)
533		; Dir=rl,
534		maplist(rewrite(Y,X),Hyps0,Hyps1),
535		rewrite(Y,X,Goal,Goal1)),
536		create_descr(eq,Dir,equal(X,Y),Descr).
537		trans_desc_wo_info(eqv(Dir,X,Y),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,Cont),[description(Descr)]) :-
538		select(equivalence(X,Y),Hyps,Hyps0),
539		(Dir=lr,
540		maplist(rewrite(X,Y),Hyps0,Hyps1),
541		rewrite(X,Y,Goal,Goal1)
542		; Dir=rl,
543		maplist(rewrite(Y,X),Hyps0,Hyps1),
544		rewrite(Y,X,Goal,Goal1)),
545		create_descr(eq,Dir,equal(X,Y),Descr).
546
547		trans_with_args(and_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
548		% P & Q,... |- Goal ===> P,Q,... |- GOAL
549		Hyp = conjunct(P,Q),
550		select(Hyp,Hyps,Hyps0),
551		add_hyps(P,Q,Hyps0,Hyps1).
552		trans_with_args(imp_l1(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :- % covers auto_mh
553		Imp = implication(P,Q),
554		select(Imp,Hyps,Res,Hyps1),
555		select_conjunct(PP,P,NewP),
556		member_hyps(PP,Hyps),
557		(NewP = truth -> Res = Q ; Res = implication(NewP,Q)).
558		trans_with_args(imp_and_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
559		Hyp = implication(P,conjunct(Q,R)),
560		select(Hyp,Hyps,Hyps0),
561		add_hyps(implication(P,Q),implication(P,R),Hyps0,Hyps1).
562		trans_with_args(imp_or_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
563		Hyp = implication(disjunct(P,Q),R),
564		select(Hyp,Hyps,Hyps0),
565		add_hyps(implication(P,R),implication(Q,R),Hyps0,Hyps1).
566		trans_with_args(contradict_l(P),sequent(Hyps,Goal,Cont),sequent(Hyps1,NotP,Cont)):-
567		select(P,Hyps,Hyps0),
568		negate(P,NotP),
569		negate(Goal,NotGoal),
570		add_hyp(NotGoal,Hyps0,Hyps1).
571		trans_with_args(or_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
572		Hyp = disjunct(P,Q),
573		select(Hyp,Hyps,Hyps0),
574		add_hyp(P,Hyps0,Hyps1),
575		add_hyp(Q,Hyps0,Hyps2).
576		trans_with_args(case(D),sequent(Hyps,Goal,Cont),NewState) :-
577		member(D,Hyps),
578		D = disjunct(_,_),
579		select(D,Hyps,Hyps0),
580		extract_disjuncts(D,Hyps0,Goal,Cont,NewState).
581		trans_with_args(imp_case(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
582		Imp = implication(P,Q),
583		select(Imp,Hyps,Hyps0),
584		add_hyp(negation(P),Hyps0,Hyps1),
585		add_hyp(Q,Hyps0,Hyps2).
586		trans_with_args(mh(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps0,P,sequent(Hyps1,Goal,Cont))) :-
587		Imp = implication(P,Q), % we prove P first and then can add Q as hypothesis
588		select(Imp,Hyps,Hyps0),
589		add_hyp(Q,Hyps0,Hyps1).
590		trans_with_args(hm(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps0,negation(Q),sequent(Hyps1,Goal,Cont))) :-
591		Imp = implication(P,Q), % we prove not(Q) and then can add not(P) as hypothesis
592		select(Imp,Hyps,Hyps0),
593		add_hyp(negation(P),Hyps0,Hyps1).
594		trans_with_args(def_expn_step(power_of(E,P)),sequent(Hyps,Goal,Cont),sequent(Hyps,not_equal(P,0),sequent(NewHyps,Goal,Cont))) :-
595		select(Hyp,Hyps,Hyps0),
596		rewrite_once(power_of(E,P),multiplication(E,power_of(E,minus(P,1))),Hyp,NewHyp),
597		add_hyp(NewHyp,Hyps0,NewHyps).
598		trans_with_args(def_expn_step(power_of(E,P)),sequent(Hyps,Goal,Cont),sequent(Hyps,not_equal(P,0),sequent(Hyps,NewGoal,Cont))) :-
599		rewrite_once(power_of(E,P),multiplication(E,power_of(E,minus(P,1))),Goal,NewGoal).
600
601		% trans_with_args on entire state with info:
602		trans_with_args_info(reselect_hyp(Hyp),state(sequent(Hyps,Goal,Cont),Info),state(sequent(Hyps1,Goal,Cont),Info1)) :-
603		remove_meta_info(des_hyps,Info,Hyp,Info1),
604		add_hyp(Hyp,Hyps,Hyps1).
605		trans_with_args_info(one_point_l(Eq),state(sequent(Hyps,Goal,Cont),Info),state(NewSequent,Info)) :-
606		select(forall(Ids,P,Q),Hyps,Hyps0),
607		select_conjunct(Eq,P,P0),
608		is_equality(Eq,E,Y),
609		select(Y,Ids,Ids0),
610		rewrite(Y,E,P0,P1),
611		rewrite(Y,E,Q,Q1),
612		(Ids0 = [] -> NewHyp = implication(P1,Q1) ; NewHyp = forall(Ids0,P1,Q1)),
613		add_hyp(NewHyp,Hyps0,Hyps1),
614		get_wd_pos_of_expr(E,Hyps,Info,POs),
615		add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,Cont),NewSequent).
616		trans_with_args_info(one_point_r(Eq),state(sequent(Hyps,forall(Ids,P,Q),Cont),Info),state(NewSequent,Info)) :-
617		select_conjunct(Eq,P,P0),
618		is_equality(Eq,E,Y),
619		select(Y,Ids,Ids0),
620		rewrite(Y,E,P0,P1),
621		rewrite(Y,E,Q,Q1),
622		(Ids0 = [] -> NewGoal = implication(P1,Q1) ; NewGoal = forall(Ids0,P1,Q1)),
623		get_wd_pos_of_expr(E,Hyps,Info,POs),
624		add_wd_pos(Hyps,POs,sequent(Hyps,NewGoal,Cont),NewSequent).
625		trans_with_args_info(induc_nat(X),state(sequent(Hyps,Goal,Cont),Info),
626		state(sequent(Hyps,member(X,natural_set),sequent(Hyps1,Goal,sequent(Hyps2,GoalN1,Cont))),Info)) :-
627		free_identifiers(Goal,Ids),
628		member(X,Ids),
629		of_integer_type(X,Info),
630		new_identifier(Goal,N),
631		add_hyp(equal(X,0),Hyps,Hyps1),
632		rewrite(X,N,Goal,GoalN),
633		add_hyps([member(N,natural_set),GoalN],Hyps,Hyps2),
634		rewrite(X,add(N,1),Goal,GoalN1).
635		trans_with_args_info(induc_nat_compl(X),state(sequent(Hyps,Goal,Cont),Info),
636		state(sequent(Hyps,member(X,natural_set),sequent(Hyps,Goal0,sequent(Hyps2,GoalN,Cont))),Info)) :-
637		free_identifiers(Goal,Ids),
638		member(X,Ids),
639		of_integer_type(X,Info),
640		new_identifiers(Goal,2,[K,N]),
641		rewrite(X,0,Goal,Goal0),
642		rewrite(X,N,Goal,GoalN),
643		rewrite(X,K,Goal,GoalK),
644		add_hyps([member(N,natural_set),forall([K],conjunct(less_equal(0,K),less(K,N)),GoalK)],Hyps,Hyps2).
645
646
647		/*
648		sequent_prover_trans(auto_simplify,state(Sequent,Info),state(NewSequent,Info)) :-
649		apply_simp_rules(Sequent,Info,NewSequent),
650		Sequent \= NewSequent.
651
652		apply_simp_rules(Sequent,Info,Res) :-
653		( sequent_prover_trans_desc(simplify_goal(Rule),state(Sequent,Info),state(NewSequent,Info),_)
654		; sequent_prover_trans_desc(simplify_hyp(Rule,_),state(Sequent,Info),state(NewSequent,Info),_)),
655		trivial_rule(Rule), !,
656		apply_simp_rules(NewSequent,Info,Res).
657		% apply_simp_rules(sequent(Hyps,Goal,Cont),_,Cont) :- axiom(Rule,Hyps,Goal), !.
658		apply_simp_rules(Sequent,_,Sequent).
659
660		trivial_rule(Rule) :- sub_atom(Rule,_,_,_,'MULTI').
661		trivial_rule(Rule) :- sub_atom(Rule,_,_,_,'SPECIAL').
662		trivial_rule(Rule) :- sub_atom(Rule,_,_,_,'TYPE').
663		trivial_rule('Evaluate tautology').
664
665		*/
666
667		symb_trans(Rule,state(Sequent,StateInfo),state(NewSequent,StateInfo),[]) :- symb_trans_rule(Rule,Sequent,NewSequent,StateInfo).
668		symb_trans(Rule,state(Sequent,StateInfo),state(NewSequent,StateInfo),TransInfo) :- symb_trans_rule(Rule,Sequent,NewSequent,StateInfo,TransInfo).
669		symb_trans_enabled(Rule,state(Sequent,_)) :- symb_trans_enabled(Rule,Sequent).
670
671		symb_trans_rule(add_hyp(Hyp),sequent(Hyps0,Goal,Cont),NewSequent,Info,[description(Desc)]) :- % CUT
672		parse_input(Hyp,add_hyp,TExpr),
673		normalize_predicate(TExpr,NormExpr),
674		get_wd_pos(NormExpr,Hyps0,Info,POs),
675		add_hyps(POs,Hyps0,Hyps1),
676		translate_finite_expr(NormExpr,NewExpr),
677		add_hyps([NewExpr|POs],Hyps0,Hyps2),
678		add_wd_pos(Hyps0,POs,sequent(Hyps1,NewExpr,sequent(Hyps2,Goal,Cont)),NewSequent),
679		translate_norm_expr_term(NormExpr,PrettyExpr),
680		ajoin(['add hypothesis: \'',PrettyExpr,'\''],Desc).
681		trans_prop(add_hyp,param_names(['Hyp'])).
682		symb_trans_enabled(add_hyp,sequent(_,_,_)).
683
684		symb_trans_rule(distinct_case(Pred),sequent(Hyps0,Goal,Cont),NewSequent,Info) :-
685		parse_input(Pred,distinct_case,TExpr),
686		normalize_predicate(TExpr,NormExpr),
687		get_wd_pos(NormExpr,Hyps0,Info,POs),
688		translate_finite_expr(NormExpr,NewExpr),
689		add_hyps([NewExpr|POs],Hyps0,Hyps1),
690		add_hyps([negation(NewExpr)|POs],Hyps0,Hyps2),
691		add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont)),NewSequent).
692		trans_prop(distinct_case,param_names(['Pred'])).
693		symb_trans_enabled(distinct_case,sequent(_,_,_)).
694
695		symb_trans_rule(exists_inst(Inst),sequent(Hyps,exists([X|Ids],Pred),Cont),NewSequent,Info) :-
696		parse_input(Inst,exists_inst,TExpr),
697		normalize_expression(TExpr,NormExpr),
698		rewrite(X,NormExpr,Pred,Goal1),
699		(Ids = [] -> Goal = Goal1 ; Goal = exists(Ids,Goal1)),
700		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
701		add_wd_pos(Hyps,POs,sequent(Hyps,Goal,Cont),NewSequent).
702		trans_prop(exists_inst,param_names(['Inst'])).
703		symb_trans_enabled(exists_inst,sequent(_,exists(_,_),_)).
704
705		symb_trans_rule(forall_inst(HypNr,Inst),sequent(Hyps,Goal,Cont),NewSequent,Info,[description(Desc)]) :-
706		get_hyp(Hyps,HypNr,SelHyp),
707		SelHyp = forall([X|Ids],P,Q), % TODO: is this compatible with Rodin?
708		parse_input(Inst,forall_inst,TExpr),
709		normalize_expression(TExpr,NormExpr),
710		select(SelHyp,Hyps,NewHyp,NewHyps),
711		rewrite(X,NormExpr,P,P1),
712		rewrite(X,NormExpr,Q,Q1),
713		(Ids = [] -> NewHyp = implication(P1,Q1) ; NewHyp = forall(Ids,P1,Q1)),
714		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
715		add_wd_pos(Hyps,POs,sequent(NewHyps,Goal,Cont),NewSequent),
716		translate_norm_expr_term(NormExpr,PrettyExpr),
717		X='$'(XName),
718		ajoin(['\x2200\ instantiation in hyp ',HypNr,' for ID ',XName,': \'',PrettyExpr,'\''],Desc).
719		trans_prop(forall_inst,param_names(['HypNr','Inst'])).
720		symb_trans_enabled(forall_inst(HypNr,none),sequent(Hyps,_,_)) :- nth1(HypNr,Hyps,forall(_,_,_)).
721
722		symb_trans_rule(forall_inst_mp(HypNr,Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
723		get_hyp(Hyps,HypNr,SelHyp),
724		SelHyp = forall([X],P,Q),
725		parse_input(Inst,forall_inst_mp,TExpr),
726		normalize_expression(TExpr,NormExpr),
727		rewrite(X,NormExpr,P,P1),
728		rewrite(X,NormExpr,Q,Q1),
729		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
730		select(SelHyp,Hyps,Hyps0),
731		add_hyps(POs,Hyps0,Hyps1),
732		add_hyps([Q1|POs],Hyps0,Hyps2),
733		add_wd_pos(Hyps,POs,sequent(Hyps1,P1,sequent(Hyps2,Goal,Cont)),NewSequent).
734		trans_prop(forall_inst_mp,param_names(['HypNr','Inst'])).
735		symb_trans_enabled(forall_inst_mp,sequent(Hyps,_,_)) :- memberchk(forall([_],_,_),Hyps).
736
737		symb_trans_rule(forall_inst_mt(HypNr,Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
738		get_hyp(Hyps,HypNr,SelHyp),
739		SelHyp = forall([X],P,Q),
740		parse_input(Inst,forall_inst_mt,TExpr),
741		normalize_expression(TExpr,NormExpr),
742		rewrite(X,NormExpr,negation(P),P1),
743		rewrite(X,NormExpr,negation(Q),Q1),
744		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
745		select(SelHyp,Hyps,Hyps0),
746		add_hyps(POs,Hyps0,Hyps1),
747		add_hyps([P1|POs],Hyps0,Hyps2),
748		add_wd_pos(Hyps,POs,sequent(Hyps1,Q1,sequent(Hyps2,Goal,Cont)),NewSequent).
749		trans_prop(forall_inst_mt,param_names(['HypNr','Inst'])).
750		symb_trans_enabled(forall_inst_mt,sequent(Hyps,_,_)) :- memberchk(forall([_],_,_),Hyps).
751
752		:- use_module(probsrc(b_ast_cleanup),[clean_up_pred_or_expr/3]).
753		symb_trans_rule(Command,sequent(Hyps,Goal,Cont),Cont,_) :- use_prover(Command,Hyps,Goal).
754
755		use_prover(Command,Hyps,Goal) :-
756		prover_command(Command,ProverList),
757		get_typed_ast(Goal,TGoal),
758		maplist(get_typed_ast,Hyps,THyps),
759		maplist(clean_up_pred_or_expr(_NonGroundExceptions1),THyps,CleanTHyps),
760		clean_up_pred_or_expr(_NonGroundExceptions2,TGoal,CleanTGoal), % TODO: exceptions
761		(bsyntaxtree:is_truth(CleanTGoal)
762		-> true % if ast_cleanup gives a true goal, we don't have to call a prover
763		; prove_sequent(ProverList,CleanTHyps,CleanTGoal)
764		).
765		prove_sequent(prob_wd_prover,THyps,TGoal) :- !,
766		well_def_analyser:prove_sequent(proving,TGoal,THyps).
767		prove_sequent(ProverList,THyps,TGoal) :-
768		atelierb_provers_interface:prove_predicate_with_provers(ProverList,THyps,TGoal,proved).
769		prover_command(ml_pp,[ml,pp]).
770		prover_command(ml,[ml]).
771		prover_command(pp,[pp]).
772		prover_command(prob_wd_prover,prob_wd_prover).
773		trans_prop(Cmd,param_names([])) :- prover_command(Cmd,_).
774		symb_trans_enabled(Cmd,sequent(_,_,_)) :- prover_command(Cmd,_).
775
776		symb_trans_rule(prob_disprover,sequent(Hyps,Goal,Cont),NewState,Info) :-
777		convert_norm_expr_to_raw(Goal,RawGoal),
778		maplist(convert_norm_expr_to_raw,Hyps,RawHyps),
779		AllHyps = RawHyps, SelectedHyps = RawHyps, Timeout = 1000,
780		% TO DO: pass information about top-level types, new deferred sets, ...
781		disprover:disprove(RawGoal,AllHyps,SelectedHyps,Timeout,OutResult),
782		format(user_output,'ProB Disprover Result = ~w (Info=~w)~n',[OutResult,Info]),
783		dispatch_result(OutResult,Cont,NewState).
784		trans_prop(prob_disprover,param_names([])).
785		symb_trans_enabled(prob_disprover,sequent(_,_,_)).
786
787		symb_trans_rule(z3,sequent(Hyps,Goal,Cont),NewState,Info) :-
788		(Hyps = [] -> ConjHyps=truth
789		; list_to_op(Hyps,ConjHyps,conjunct)),
790		convert_norm_expr_to_raw(conjunct(ConjHyps,negation(Goal)),Ast),
791		bmachine:b_type_check_raw_expr(Ast,[],Typed,open(no_quantifier)),
792		smt_solvers_interface:smt_solve_predicate(z3,Typed,_,Res),
793		format(user_output,'z3 Result = ~w (Info=~w)~n',[Res,Info]),
794		dispatch_result(Res,Cont,NewState).
795		trans_prop(z3,param_names([])).
796		symb_trans_enabled(z3,sequent(_,_,_)).
797
798		dispatch_result(contradiction_found,Cont,Cont).
799		dispatch_result(contradiction_in_hypotheses,Cont,Cont).
800		dispatch_result(solution_on_selected_hypotheses(S),_,counter_example(S)).
801		dispatch_result(solution(S),_,counter_example(S)).
802		% other results are no_solution_found(_) and time_out
803
804		symb_trans_rule(rewrite_hyp(HypNr,NewHyp),sequent(Hyps,Goal,Cont),sequent(NewHyps,Goal,Cont),Info) :-
805		get_hyp(Hyps,HypNr,SelHyp),
806		parse_input(NewHyp,rewrite_hyp,TExpr),
807		b_interpreter_check:norm_pred_check(TExpr,RewrittenHyp),
808		select(SelHyp,Hyps,Hyps0),
809		get_wd_pos(RewrittenHyp,Hyps,Info,[]),
810		prove_predicate([SelHyp],RewrittenHyp),
811		translate_finite_expr(RewrittenHyp,NewExpr),
812		add_hyp(NewExpr,Hyps0,NewHyps).
813		trans_prop(rewrite_hyp,param_names(['HypNr','NewHyp'])).
814		symb_trans_enabled(rewrite_hyp,sequent(_,_,_)).
815
816		:- use_module(probsrc(tools),[split_atom/3]).
817		symb_trans_rule(derive_hyp(HypNrs,NewHyp),sequent(Hyps,Goal,Cont),sequent(NewHyps,Goal,Cont),Info) :-
818		ground(HypNrs),
819		split_atom(HypNrs,[','],Indices),
820		maplist(get_hyp(Hyps),Indices,SelHyps),
821		parse_input(NewHyp,derive_hyp,TExpr),
822		b_interpreter_check:norm_pred_check(TExpr,NormExpr),
823		get_wd_pos(NormExpr,Hyps,Info,[]),
824		prove_predicate(SelHyps,NormExpr),
825		translate_finite_expr(NormExpr,NewExpr),
826		add_hyp(NewExpr,Hyps,NewHyps).
827		trans_prop(derive_hyp,param_names(['HypNrs','NewHyp'])).
828		symb_trans_enabled(derive_hyp,sequent(_,_,_)).
829
830		symb_trans_rule(dis_binter_r(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps,NormExpr,sequent(Hyps,NewGoal,Cont)),Info) :-
831		parse_input(PFun,dis_binter_r,TExpr),
832		normalize_predicate(TExpr,NormExpr),
833		NormExpr = member(reverse(F),partial_function(A,B)),
834		type_expression(A,Info),
835		type_expression(B,Info),
836		Sub = image(F,Inter),
837		Inter = intersection(_,_),
838		is_subterm(Sub,Goal),
839		image_intersection(F,Inter,NewSub),
840		rewrite_once(Sub,NewSub,Goal,NewGoal).
841		trans_prop(dis_binter_r,param_names(['PFun'])).
842		symb_trans_enabled(dis_binter_r,sequent(_,Goal,_)) :- is_subterm(image(_,Inter),Goal), Inter = intersection(_,_).
843
844		symb_trans_rule(dis_binter_l(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps0,NormExpr,sequent(Hyps1,Goal,Cont)),Info) :-
845		parse_input(PFun,dis_binter_l,TExpr),
846		normalize_predicate(TExpr,NormExpr),
847		NormExpr = member(reverse(F),partial_function(A,B)),
848		type_expression(A,Info),
849		type_expression(B,Info),
850		select(Hyp,Hyps,Hyps0),
851		Sub = image(F,Inter),
852		Inter = intersection(_,_),
853		is_subterm(Sub,Hyp),
854		Inter = intersection(_,_),
855		image_intersection(F,Inter,NewSub),
856		rewrite(Sub,NewSub,Hyp,NewHyp),
857		add_hyp(NewHyp,Hyps0,Hyps1).
858		trans_prop(dis_binter_l,param_names(['PFun'])).
859		symb_trans_enabled(dis_binter_l,sequent(Hyps,_,_)) :- member(Hyp,Hyps), is_subterm(image(_,Inter),Hyp), Inter = intersection(_,_).
860
861		symb_trans_rule(dis_setminus_r(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps,NormExpr,sequent(Hyps,NewGoal,Cont)),Info) :-
862		parse_input(PFun,dis_setminus_r,TExpr),
863		normalize_predicate(TExpr,NormExpr),
864		NormExpr = member(reverse(F),partial_function(A,B)),
865		type_expression(A,Info),
866		type_expression(B,Info),
867		rewrite(image(F,set_subtraction(S,T)),set_subtraction(image(F,S),image(F,T)),Goal,NewGoal).
868		trans_prop(dis_setminus_r,param_names(['PFun'])).
869		symb_trans_enabled(dis_setminus_r,sequent(_,Goal,_)) :- is_subterm(image(_,set_subtraction(_,_)),Goal).
870
871		symb_trans_rule(dis_setminus_l(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps0,NormExpr,sequent(Hyps1,Goal,Cont)),Info) :-
872		parse_input(PFun,dis_setminus_l,TExpr),
873		normalize_predicate(TExpr,NormExpr), !,
874		NormExpr = member(reverse(F),partial_function(A,B)),
875		type_expression(A,Info),
876		type_expression(B,Info),
877		select(Hyp,Hyps,Hyps0),
878		is_subterm(image(_,set_subtraction(_,_)),Hyp),
879		rewrite(image(F,set_subtraction(S,T)),set_subtraction(image(F,S),image(F,T)),Hyp,NewHyp),
880		add_hyp(NewHyp,Hyps0,Hyps1).
881		trans_prop(dis_setminus_l,param_names(['PFun'])).
882		symb_trans_enabled(dis_setminus_l,sequent(Hyps,_,_)) :- member(Hyp,Hyps), is_subterm(image(_,set_subtraction(_,_)),Hyp).
883
884		symb_trans_rule(fin_subseteq_r(Set),sequent(Hyps,finite(S),Cont),NewSequent,Info) :-
885		parse_input(Set,fin_subseteq_r,TExpr),
886		normalize_expression(TExpr,NormExpr),
887		get_meta_info(ids_types,Info,IdsTypes), % NormExpr has to be a set
888		same_type(S,NormExpr,IdsTypes),
889		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
890		add_wd_pos(Hyps,POs,sequent(Hyps,subset(S,NormExpr),sequent(Hyps,finite(NormExpr),Cont)),NewSequent).
891		trans_prop(fin_subseteq_r,param_names(['Set'])).
892		symb_trans_enabled(fin_subseteq_r,sequent(_,finite(_),_)).
893
894		symb_trans_rule(fin_fun1_r(PFun),sequent(Hyps,finite(F),Cont),NewSequent,Info) :-
895		parse_input(PFun,fin_fun1_r,TExpr),
896		normalize_expression(TExpr,NormExpr),
897		NormExpr = partial_function(S,T),
898		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
899		add_wd_pos(Hyps,POs,sequent(Hyps,member(F,partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
900		trans_prop(fin_fun1_r,param_names(['PFun'])).
901		symb_trans_enabled(fin_fun1_r,sequent(_,finite(_),_)).
902
903		symb_trans_rule(fin_fun2_r(PFun),sequent(Hyps,finite(F),Cont),NewSequent,Info) :-
904		parse_input(PFun,fin_fun2_r,TExpr),
905		normalize_expression(TExpr,NormExpr),
906		NormExpr = partial_function(S,T),
907		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
908		add_wd_pos(Hyps,POs,sequent(Hyps,member(reverse(F),partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
909		trans_prop(fin_fun2_r,param_names(['PFun'])).
910		symb_trans_enabled(fin_fun2_r,sequent(_,finite(_),_)).
911
912		symb_trans_rule(fin_fun_img_r(PFun),sequent(Hyps,finite(image(F,Set)),Cont),NewSequent,Info) :-
913		parse_input(PFun,fin_fun_img_r,TExpr),
914		normalize_expression(TExpr,NormExpr),
915		NormExpr = partial_function(S,T),
916		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
917		add_wd_pos(Hyps,POs,sequent(Hyps,member(F,partial_function(S,T)),sequent(Hyps,finite(Set),Cont)),NewSequent).
918		trans_prop(fin_fun_img_r,param_names(['PFun'])).
919		symb_trans_enabled(fin_fun_img_r,sequent(_,finite(image(_,_)),_)).
920
921		symb_trans_rule(fin_fun_ran_r(PFun),sequent(Hyps,finite(range(F)),Cont),NewSequent,Info) :-
922		parse_input(PFun,fin_fun_ran_r,TExpr),
923		normalize_expression(TExpr,NormExpr),
924		NormExpr = partial_function(S,T),
925		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
926		add_wd_pos(Hyps,POs,sequent(Hyps,member(F,partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
927		trans_prop(fin_fun_ran_r,param_names(['PFun'])).
928		symb_trans_enabled(fin_fun_ran_r,sequent(_,finite(range(_)),_)).
929
930		symb_trans_rule(fin_fun_dom_r(PFun),sequent(Hyps,finite(domain(F)),Cont),NewSequent,Info) :-
931		parse_input(PFun,fin_fun_dom_r,TExpr),
932		normalize_expression(TExpr,NormExpr),
933		NormExpr = partial_function(S,T),
934		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
935		add_wd_pos(Hyps,POs,sequent(Hyps,member(reverse(F),partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
936		trans_prop(fin_fun_dom_r,param_names(['PFun'])).
937		symb_trans_enabled(fin_fun_dom_r,sequent(_,finite(domain(_)),_)).
938
939		symb_trans_rule(fin_rel_r(Rel),sequent(Hyps,finite(R),Cont),NewSequent,Info) :-
940		parse_input(Rel,fin_rel_r,TExpr),
941		normalize_expression(TExpr,NormExpr), !,
942		NormExpr = relations(S,T),
943		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
944		add_wd_pos(Hyps,POs,sequent(Hyps,member(R,relations(S,T)),sequent(Hyps,finite(S),sequent(Hyps,finite(T),Cont))),NewSequent).
945		trans_prop(fin_rel_r,param_names(['Rel'])).
946		symb_trans_enabled(fin_rel_r,sequent(_,finite(_),_)).
947
948		parse_input(Param,Res) :- parse_input(Param,'?',Res).
949		parse_input(Param,Context,Res) :-
950		ground(Param),
951		(number(Param) -> number_codes(Param,CParam)
952		; Param = [Nr|_], number(Nr) -> CParam = Param % already codes list
953		; atom(Param) -> atom_codes(Param,CParam)
954		; ajoin(['Illegal input to proof rule ',Context,' (must be Prolog atom or string):'],Msg),
955		add_error(sequent_prover,Msg,Param), fail
956		),
957		bmachine:b_parse_only(formula,CParam,Parsed,_,_Error),
958		transform_raw(Parsed,TExpr),
959		adapt_for_eventb(TExpr,Res).
960
961		adapt_for_eventb(Term,Res) :- atomic(Term), !, Res=Term.
962		adapt_for_eventb(Term,Result) :-
963		Term=..[F|Args],
964		replace_functor(F,NewFunctor),
965		maplist(adapt_for_eventb,Args,NewArgs),
966		Result=..[NewFunctor|NewArgs].
967
968		replace_functor(F,NF) :-
969		replace_functor_eventb(F,EF), !, NF=EF.
970		replace_functor(F,F).
971
972		replace_functor_eventb(concat,power_of).
973		replace_functor_eventb(power_of,cartesian_product).
974		replace_functor_eventb(minus_or_set_subtract,minus).
975		replace_functor_eventb(mult_or_cart,multiplication).
976
977		translate_finite_expr(X,Y) :- rewrite(member(S,fin_subset(S)),finite(S),X,Y).
978
979		get_hyp(Hyps,Nr,Hyp) :-
980		number(Nr),
981		nth1(Nr,Hyps,Hyp).
982
983		add_hyp(Hyp,Hyps0,NewHyps) :- append(Hyps0,[Hyp],Hyps1), without_duplicates(Hyps1,NewHyps).
984		add_hyps(Hyp1,Hyp2,Hyps0,NewHyps) :- append(Hyps0,[Hyp1,Hyp2],Hyps1), without_duplicates(Hyps1,NewHyps).
985		add_hyps(NewHyps,Hyps,SHyps) :- append(Hyps,NewHyps,All), without_duplicates(All,SHyps).
986
987		% select and remove a conjunct:
988		select_conjunct(X,conjunct(A,B),Rest) :- !,
989		(select_conjunct(X,A,RA), conjoin(RA,B,Rest)
990		;
991		select_conjunct(X,B,RB), conjoin(A,RB,Rest)).
992		select_conjunct(X,X,truth).
993
994		conjoin(truth,X,R) :- !, R=X.
995		conjoin(X,truth,R) :- !, R=X.
996		conjoin(X,Y,conjunct(X,Y)).
997
998
999
1000
1001		% axioms: proof rules without antecedent, discharging goal directly
1002		axiom(hyp,Hyps,Goal) :- member_hyps(Goal,Hyps).
1003		axiom(hyp,Hyps,member(X,Nat)) :-
1004		is_natural_set(Nat),
1005		(member_hyps(greater_equal(X,0),Hyps) ; member_hyps(greater_equal(X,1),Hyps)).
1006		axiom(hyp_or,Hyps,Goal) :-
1007		member_of_bin_op(disjunct,P,Goal), % TODO: will not select a disjunction for P
1008		member_hyps(P,Hyps).
1009		axiom(false_hyp,Hyps,_Goal) :- member_hyps(falsity,Hyps).
1010		axiom(true_goal,_,truth).
1011		axiom(Rule,_Hyps,Goal) :- axiom_wo_hyps(Goal,Rule).
1012		axiom(cntr,Hyps,_) :-
1013		member(P,Hyps),
1014		(NotP = negation(P) ; negate(P,NotP)),
1015		select(P,Hyps,Hyps0),
1016		member_hyps(NotP,Hyps0).
1017		axiom(fin_rel,Hyps,finite(Fun)) :-
1018		member_hyps(member(Fun,FunType),Hyps),
1019		is_rel(FunType,_,Dom,Ran),
1020		member_hyps(finite(Dom),Hyps),
1021		member_hyps(finite(Ran),Hyps).
1022		axiom(fin_l_lower_bound,Hyps,exists([N],forall([X],member(X,S),LessEq))) :-
1023		member_hyps(finite(S),Hyps),
1024		is_less_eq(LessEq,N,X).
1025		axiom(fin_l_upper_bound,Hyps,exists([N],forall([X],member(X,S),LessEq))) :-
1026		member_hyps(finite(S),Hyps),
1027		is_less_eq(LessEq,X,N).
1028		axiom(derive_goal,Hyps,Goal) :- derive_goal(Hyps,Goal), \+ is_true(Goal), \+ axiom(hyp,Hyps,Goal).
1029
1030		% from chapter 2, "Modeling in Event-B"
1031		axiom(p2,Hyps,member(Add,Nat)) :-
1032		is_natural_set(Nat),
1033		member(member(N,Nat),Hyps),
1034		equal_terms(Add,add(N,1)).
1035		axiom(p2_,Hyps,member(Sub,Nat)) :-
1036		is_natural_set(Nat),
1037		member(L,Hyps),
1038		is_less(L,0,N),
1039		equal_terms(Sub,minus(N,1)).
1040		axiom(inc,Hyps,Goal) :-
1041		member(L,Hyps),
1042		is_less(L,N,M),
1043		equal_terms(Goal,less_equal(add(N,1),M)).
1044		axiom(dec,Hyps,Goal) :-
1045		member(L,Hyps),
1046		is_less_eq(L,N,M),
1047		equal_terms(Goal,less(minus(N,1),M)).
1048
1049		axiom_with_info(fun_goal,Hyps,member(F,partial_function(Ty1,Ty2)),Info) :-
1050		type_expression(Ty1,Info),
1051		type_expression(Ty2,Info),
1052		member_hyps(member(F,FType),Hyps),
1053		is_fun(FType,_,_,_).
1054		axiom_with_info(fun_goal_rec,Hyps,member(function(Fun,En),partial_function(Ty1,Ty2)),Info) :-
1055		type_expression(Ty1,Info),
1056		type_expression(Ty2,Info),
1057		function_of(Fun,F),
1058		member(member(F,FType),Hyps),
1059		fun_goal_check(FType,function(Fun,En)).
1060
1061		axiom_wo_hyps(true,true_goal).
1062		axiom_wo_hyps(eq(E,E),eql).
1063
1064
1065		% rules implemented MembershipGoal reasoner
1066		% mb_goal(Rule,Hyp,Goal,Info).
1067		mb_goal('SUBSET_SUBSETEQ',subset_strict(A,B),subset(A,B),_).
1068		mb_goal('DOM_SUBSET',subset(A,B),subset(domain(A),domain(B)),_).
1069		mb_goal('RAN_SUBSET',subset(A,B),subset(range(A),range(B)),_).
1070		mb_goal('EQUAL_SUBSETEQ',Eq,subset(A,B),Info) :-
1071		is_equality(Eq,A,B),
1072		get_meta_info(ids_types,Info,IdsTypes),
1073		check_type(A,B,IdsTypes,set(_)).
1074		mb_goal('IN_DOM_CPROD',member(X,domain(cartesian_product(A,_))),member(X,A),_).
1075		mb_goal('IN_RAN_CPROD',member(Y,range(cartesian_product(_,B))),member(Y,B),_).
1076		mb_goal('IN_DOM_REL',member(couple(X,_),F),member(X,domain(F)),_).
1077		mb_goal('IN_RAN_REL',member(couple(_,Y),F),member(Y,range(F)),_).
1078		mb_goal('SETENUM_SUBSET',subset(set_extension(L),A),member(X,A),_) :- member(X,L).
1079		mb_goal('OVR_RIGHT_SUBSET',subset(LHS1,A),subset(LHS2,A),_) :-
1080		op_to_list(LHS1,List1,overwrite),
1081		op_to_list(LHS2,List2,overwrite),
1082		append(L,List2,List1),
1083		L \= [].
1084		mb_goal('RELSET_SUBSET_CPROD',member(F,Rel),subset(F,cartesian_product(Dom,Ran)),_) :- is_rel(Rel,_,Dom,Ran).
1085
1086		% mb_goal(Rule,Hyps,Goal).
1087		mb_goal('DERIV_IN_SUBSET',Hyps,member(X,B)) :- member(member(X,A),Hyps), member(subset(A,B),Hyps).
1088
1089		derive_goal(Hyps,Goal) :-
1090		functor(Goal,F,2),
1091		(comparison(F) ; F = member),
1092		used_identifiers(Goal,GoalIds),
1093		find_hyps_with(GoalIds,Hyps,SelectedHyps),
1094		use_prover(prob_wd_prover,SelectedHyps,Goal).
1095
1096		find_hyps_with(_,[],[]).
1097		find_hyps_with(Ids,[Hyp|T],[Hyp|R]) :-
1098		used_identifiers(Hyp,HypIds),
1099		\+ list_intersection(Ids,HypIds,[]), !,
1100		find_hyps_with(Ids,T,R).
1101		find_hyps_with(Ids,[_|T],R) :- find_hyps_with(Ids,T,R).
1102
1103		/* not used:
1104		is_transitive(Hyps,Goal) :-
1105		Goal=..[F,L,R],
1106		comparison(F),
1107		F \= not_equal,
1108		is_transitive_aux(Hyps,F,L,R,[]).
1109
1110		is_transitive_aux(Hyps,F,L,R,_) :-
1111		Ex=..[F,L,R],
1112		(member(Ex,Hyps) ; equiv(Ex,G2), member(G2,Hyps)).
1113		is_transitive_aux(Hyps,F,L,R,Visited) :-
1114		Ex=..[F,L,M],
1115		(member(Ex,Hyps) ; equiv(Ex,G2), member(G2,Hyps)),
1116		\+ member(M,Visited),
1117		is_transitive_aux(Hyps,F,M,R,[L|Visited]).
1118
1119		lower_bound(Hyps,B,X) :- member(L,Hyps), is_less_eq(L,B,X), number(B).
1120		lower_bound(Hyps,B1,X) :- member(L,Hyps), is_less(L,B,X), number(B), B1 is B+1.
1121		lower_bound(Hyps,B,X) :- member(Eq,Hyps), is_equality(Eq,B,X), number(B).
1122
1123		upper_bound(Hyps,X,B) :- member(L,Hyps),is_less_eq(L,X,B), number(B).
1124		upper_bound(Hyps,X,B1) :- member(L,Hyps), is_less(L,X,B), number(B), B1 is B-1.
1125		upper_bound(Hyps,X,B) :- member(Eq,Hyps), is_equality(Eq,X,B), number(B).
1126		*/
1127
1128
1129		add_wd_pos(Hyps,POs,Sequent,NewSequent) :-
1130		rodin_mode, !,
1131		(POs=[] -> Conj=truth ; list_to_op(POs,Conj,conjunct)),
1132		% Rodin requires true goal for empty list and conjunction of WD conditions
1133		add_pos(Hyps,Sequent,NewSequent,[Conj]).
1134		add_wd_pos(Hyps,POs,Sequent,NewSequent) :-
1135		add_goals(Hyps,POs,Sequent,NewSequent).
1136
1137		add_goals(Hyps,POs,Sequent,NewSequent) :-
1138		reverse(POs,List),
1139		add_pos(Hyps,Sequent,NewSequent,List).
1140
1141		add_pos(_,Sequent,Sequent,[]) :- !.
1142		add_pos(Hyps,InnerSequent,NewSequent,[PO|R]) :- add_pos(Hyps,sequent(Hyps,PO,InnerSequent),NewSequent,R).
1143
1144		% add a sequent per disjunct
1145		extract_disjuncts(Q,Hyps0,Goal,Cont,sequent(Hyps,Goal,Cont)) :- Q \= disjunct(_,_), add_hyp(Q,Hyps0,Hyps).
1146		extract_disjuncts(disjunct(L,R),Hyps0,Goal,Cont,LRSequent) :-
1147		extract_disjuncts(L,Hyps0,Goal,success(PO_Nr),LSequent),
1148		extract_disjuncts(R,Hyps0,Goal,Cont,RSequent),
1149		append_sequents(LSequent,RSequent,LRSequent,PO_Nr).
1150
1151		% add sequents as last continuation
1152		append_sequents(sequent(Hyps,Goal,Cont),InnerCont,sequent(Hyps,Goal,Sequent),PO_Nr) :-
1153		(Cont = success(PO_Nr) -> Sequent = InnerCont
1154		; append_sequents(Cont,InnerCont,Sequent,PO_Nr)).
1155
1156		animation_function_result(state(counter_example(_),_),[((1,1),'Counter example found.')]).
1157		animation_function_result(state(success(Nr),_),[((1,1),Txt)]) :-
1158		(get_po_description(Nr,PO) -> ajoin(['Proof of ',PO,' succeeded.'],Txt)
1159		; Txt = 'Proof succeeded.').
1160		animation_function_result(state(Sequent,_),Matrix) :-
1161		Sequent = sequent(_,_,Cont),
1162		cont_length(Cont,LCont),
1163		findall(((RowNr,ColNr),Cell), (cell_content(RowNr,ColNr,Sequent,Cell,LCont)), Matrix).
1164
1165		cell_content(Row,Col,Sequent,Cell,_) :- % Auto-Proof buttons
1166		max_hyp_length(Sequent,0,LHyps),
1167		member(Col,[1,2,3]),D is Col+1,
1168		(Row is LHyps + 3, ajoin(['auto-',D],Cell)
1169		; Row is LHyps + 4, ajoin(['pure-',D],Cell)).
1170		cell_content(RowNr,ColNr,Sequent,Cell,LCont) :- cell_content2(RowNr,ColNr,Sequent,Cell,LCont).
1171
1172		max_hyp_length(sequent(Hyps,_,Cont),CurMax,Res) :- length(Hyps,Len),!,
1173		(Len>CurMax -> max_hyp_length(Cont,Len,Res) ; max_hyp_length(Cont,CurMax,Res)).
1174		max_hyp_length(_,Max,Max).
1175
1176		cell_content2(Row,1,sequent(Hyps,_,_),Cell,_) :- nth1(Row,Hyps,RowHyp), translate_norm_expr_term(RowHyp,Cell).
1177		cell_content2(Row,1,sequent(Hyps,_,_),'\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\',_) :-
1178		length(Hyps,LHyps), Row is LHyps + 1.
1179		cell_content2(Row,1,sequent(Hyps,Goal,_),Cell,_) :-
1180		length(Hyps,LHyps), Row is LHyps + 2, translate_norm_expr_term(Goal,Cell).
1181		cell_content2(Row,Col,Sequent,Cell,LCont) :-
1182		extract_continuations(Sequent,LCont,Cont,Col),
1183		cell_content2(Row,1,Cont,Cell,LCont).
1184
1185		extract_continuations(sequent(_,_,Cont),LCont,Cont,ColNr) :-
1186		cont_length(Cont,ActualLCont),
1187		ColNr is LCont - ActualLCont + 2.
1188		extract_continuations(sequent(_,_,Cont),LCont,FoundCont,ColNr) :-
1189		extract_continuations(Cont,LCont,FoundCont,ColNr).
1190
1191		get_continuations(success(_),[]).
1192		get_continuations(sequent(_,_,Cont),Conts) :- % ignore current sequent
1193		get_continuations2(Cont,Conts).
1194		get_continuations2(success(_),[]).
1195		get_continuations2(sequent(Hyps,Goal,NxtCont),[sequent(Hyps,Goal)|CT]) :-
1196		get_continuations2(NxtCont,CT).
1197
1198		find_transitions(Sequent,Info,Trans) :-
1199		findall(T,( sequent_prover_trans(T,state(Sequent,Info),_)
1200		; sequent_prover_trans_desc(T,state(Sequent,Info),_,_)),TransL),
1201		remove_dups(TransL,Trans).
1202
1203		% animation_image_right_click_transition(RowX,ColY,OperationTemplate,State)
1204		animation_image_right_click_transition(Row,1,Trans,state(sequent(Hyps,Goal,Cont),Info)) :- nth1(Row,Hyps,Hyp),
1205		select(Hyp,Hyps,Hyps0),
1206		find_transitions(sequent(Hyps,Goal,Cont),Info,AllTransitions),
1207		find_transitions(sequent(Hyps0,Goal,Cont),Info,Transitions0),
1208		member(Trans,AllTransitions),
1209		Trans \= mon_deselect(_),
1210		\+ member(Trans,Transitions0).
1211		animation_image_right_click_transition(Row,1,Trans,state(sequent(Hyps,Goal,Cont),Info)) :-
1212		length(Hyps,LHyps),
1213		Row is LHyps + 2, % click on goal
1214		find_transitions(sequent([],Goal,Cont),Info,Transitions),
1215		member(Trans,Transitions),
1216		Trans \= reselect_hyp(_).
1217		animation_image_right_click_transition(Row,_C,Proof,state(sequent(Hyps,Goal,_),Info)) :-
1218		length(Hyps,LHyps), Row is LHyps + 1, % click on divider line
1219		(bounded_find_proof(sequent(Hyps,Goal,success(0)),Info,3,[],Proof) -> true ; Proof = 'NO AUTO-PROOF-FOUND').
1220		animation_image_right_click_transition(Row,Col,Proof,state(sequent(Hyps,Goal,_),Info)) :-
1221		length(Hyps,LHyps), Row > LHyps + 2, % click on Auto-Proof buttons below goal
1222		Depth is Col+1,
1223		Opts = [use_eager_simplification|TOpts],
1224		(Row =:= LHyps+3 -> TOpts = [] ; TOpts = [disregard_rule(derive_goal)]),
1225		(bounded_find_proof(sequent(Hyps,Goal,success(0)),Info,Depth,Opts,Proof) -> true ; Proof = 'NO AUTO-PROOF-FOUND').
1226
1227		% animation_image_right_click_transition(X,Y,OperationTemplate)
1228		animation_image_right_click_transition(Row,1,mon_deselect(Row)).
1229
1230		% ------------------------
1231
1232
1233
1234
1235		function_of(F,F) :- F \= function(_,_).
1236		function_of(function(Fun,_),F) :- function_of(Fun,F).
1237
1238		fun_goal_check(Fun,F) :-
1239		F \= function(_,_),
1240		is_fun(Fun,_,_,_).
1241		fun_goal_check(Rel,function(F,_)) :-
1242		is_rel(Rel,_,_,Ran),
1243		fun_goal_check(Ran,F).
1244
1245
1246		rewrite_once(X,Y,E,NewE) :- is_subterm(X,E), rewrite_once2(X,Y,E,NewE), E \= NewE.
1247
1248		rewrite_once2(X,Y,E,NewE) :- equal_terms(X,E),!, NewE=Y.
1249		rewrite_once2(_X,_Y,E,NewE) :- atomic(E),!, NewE=E.
1250		rewrite_once2(_X,_Y,'$'(E),NewE) :- atomic(E),!, NewE='$'(E).
1251		rewrite_once2(X,Y,C,NewC) :- C=..[Op|Args],
1252		select(Arg,Args,NewArg,NewArgs),
1253		rewrite_once2(X,Y,Arg,NewArg),
1254		NewC =.. [Op|NewArgs].
1255
1256		wd_strict_term(T) :- atomic(T), !.
1257		wd_strict_term('$'(E)) :- atomic(E), !.
1258		wd_strict_term(T) :-
1259		\+ with_ids(T,_), % quantified_union, quantified_intersection, event_b_comprehension_set, forall, exists -> not WD strict
1260		T=..[F|Args],
1261		\+ not_wd_strict(F),
1262		wd_strict_args(Args).
1263
1264		wd_strict_args([]).
1265		wd_strict_args([T|Args]) :- wd_strict_term(T), wd_strict_args(Args).
1266
1267		not_wd_strict(implication).
1268		not_wd_strict(conjunct).
1269		not_wd_strict(disjunct).
1270
1271		is_subterm(Term,Term).
1272		is_subterm(Subterm,Term) :-
1273		Term=..[_|Args],
1274		member(Arg,Args),
1275		is_subterm(Subterm,Arg).
1276
1277
1278
1279		replace_used_ids([],_,[]).
1280		replace_used_ids(['$'(X)|T],IdsTypes,['$'(Y)|R]) :-
1281		member(b(identifier(X),_,_),IdsTypes), !,
1282		new_aux_identifier(IdsTypes,Y),
1283		replace_used_ids(T,[b(identifier(Y),any,[])|IdsTypes],R).
1284		replace_used_ids(['$'(X)|T],IdsTypes,['$'(X)|R]) :-
1285		replace_used_ids(T,[b(identifier(X),any,[])|IdsTypes],R).
1286
1287
1288
1289		same_type('$'(S),'$'(T),List) :-
1290		member(b(identifier(S),Type,_),List),
1291		member(b(identifier(T),Type,_),List),
1292		Type \= any.
1293
1294
1295
1296		image_intersection(F,intersection(A,B),Inter) :- image_intersection(F,A,L), image_intersection(F,B,R), !, Inter = intersection(L,R).
1297		image_intersection(F,A,image(F,A)).
1298
1299
1300
1301
1302
1303
1304
1305		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
1306		:- if(environ(prob_release,true)).
1307		% Don't include tests in release mode.
1308		:- else.
1309		:- use_module(test_sequent_prover).
1310		:- endif.