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