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