32 val hol_const_types_only: unit -> unit |
32 val hol_const_types_only: unit -> unit |
33 val hol_no_types: unit -> unit |
33 val hol_no_types: unit -> unit |
34 val hol_typ_level: unit -> ResHolClause.type_level |
34 val hol_typ_level: unit -> ResHolClause.type_level |
35 val run_relevance_filter: bool ref |
35 val run_relevance_filter: bool ref |
36 val invoke_atp_ml : ProofContext.context * thm -> unit |
36 val invoke_atp_ml : ProofContext.context * thm -> unit |
|
37 val add_claset : unit -> unit |
|
38 val add_simpset : unit -> unit |
|
39 val add_clasimp : unit -> unit |
|
40 val add_atpset : unit -> unit |
|
41 val rm_claset : unit -> unit |
|
42 val rm_simpset : unit -> unit |
|
43 val rm_atpset : unit -> unit |
|
44 val rm_clasimp : unit -> unit |
37 end; |
45 end; |
38 |
46 |
39 structure ResAtp : RES_ATP = |
47 structure ResAtp : RES_ATP = |
40 struct |
48 struct |
41 |
49 |
115 val include_simpset = ref false; |
123 val include_simpset = ref false; |
116 val include_claset = ref false; |
124 val include_claset = ref false; |
117 val include_atpset = ref true; |
125 val include_atpset = ref true; |
118 val add_simpset = (fn () => include_simpset:=true); |
126 val add_simpset = (fn () => include_simpset:=true); |
119 val add_claset = (fn () => include_claset:=true); |
127 val add_claset = (fn () => include_claset:=true); |
120 val add_clasimp = (fn () => include_simpset:=true;include_claset:=true); |
128 val add_clasimp = (fn () => (include_simpset:=true;include_claset:=true)); |
121 val add_atpset = (fn () => include_atpset:=true); |
129 val add_atpset = (fn () => include_atpset:=true); |
122 val rm_simpset = (fn () => include_simpset:=false); |
130 val rm_simpset = (fn () => include_simpset:=false); |
123 val rm_claset = (fn () => include_claset:=false); |
131 val rm_claset = (fn () => include_claset:=false); |
124 val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false); |
132 val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false)); |
125 val rm_atpset = (fn () => include_atpset:=false); |
133 val rm_atpset = (fn () => include_atpset:=false); |
126 |
134 |
127 (*** paths for HOL helper files ***) |
135 (*** paths for HOL helper files ***) |
128 fun full_typed_comb_inclS () = |
136 fun full_typed_comb_inclS () = |
129 helper_path "E_HOME" "additionals/full_comb_inclS" |
137 helper_path "E_HOME" "additionals/full_comb_inclS" |
266 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen) |
274 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen) |
267 | lit_lg P (lg,seen) = |
275 | lit_lg P (lg,seen) = |
268 let val (pred,args) = strip_comb P |
276 let val (pred,args) = strip_comb P |
269 val (lg',seen') = if pred mem seen then (lg,seen) |
277 val (lg',seen') = if pred mem seen then (lg,seen) |
270 else pred_lg pred (lg,seen) |
278 else pred_lg pred (lg,seen) |
|
279 val _ = if is_fol_logic lg' then () else warning ("Found a HOL predicate: " ^ (Term.str_of_term pred)) |
271 in |
280 in |
272 term_lg args (lg',seen') |
281 term_lg args (lg',seen') |
273 end; |
282 end; |
274 |
283 |
275 fun lits_lg [] (lg,seen) = (lg,seen) |
284 fun lits_lg [] (lg,seen) = (lg,seen) |
276 | lits_lg (lit::lits) (FOL,seen) = |
285 | lits_lg (lit::lits) (FOL,seen) = |
277 lits_lg lits (lit_lg lit (FOL,seen)) |
286 let val (lg,seen') = lit_lg lit (FOL,seen) |
|
287 val _ = if is_fol_logic lg then () else warning ("Found a HOL literal: " ^ (Term.str_of_term lit)) |
|
288 in |
|
289 lits_lg lits (lg,seen') |
|
290 end |
278 | lits_lg lits (lg,seen) = (lg,seen); |
291 | lits_lg lits (lg,seen) = (lg,seen); |
279 |
292 |
|
293 |
|
294 fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = |
|
295 dest_disj_aux t (dest_disj_aux t' disjs) |
|
296 | dest_disj_aux t disjs = t::disjs; |
|
297 |
|
298 fun dest_disj t = dest_disj_aux t []; |
280 |
299 |
281 fun logic_of_clause tm (lg,seen) = |
300 fun logic_of_clause tm (lg,seen) = |
282 let val tm' = HOLogic.dest_Trueprop tm |
301 let val tm' = HOLogic.dest_Trueprop tm |
283 val disjs = HOLogic.dest_disj tm' |
302 val disjs = dest_disj tm' |
284 in |
|
285 lits_lg disjs (lg,seen) |
|
286 end; |
|
287 |
|
288 fun lits_lg [] (lg,seen) = (lg,seen) |
|
289 | lits_lg (lit::lits) (FOL,seen) = |
|
290 lits_lg lits (lit_lg lit (FOL,seen)) |
|
291 | lits_lg lits (lg,seen) = (lg,seen); |
|
292 |
|
293 |
|
294 fun logic_of_clause tm (lg,seen) = |
|
295 let val tm' = HOLogic.dest_Trueprop tm |
|
296 val disjs = HOLogic.dest_disj tm' |
|
297 in |
303 in |
298 lits_lg disjs (lg,seen) |
304 lits_lg disjs (lg,seen) |
299 end; |
305 end; |
300 |
306 |
301 fun logic_of_clauses [] (lg,seen) = (lg,seen) |
307 fun logic_of_clauses [] (lg,seen) = (lg,seen) |
302 | logic_of_clauses (cls::clss) (FOL,seen) = |
308 | logic_of_clauses (cls::clss) (FOL,seen) = |
303 logic_of_clauses clss (logic_of_clause cls (FOL,seen)) |
309 let val (lg,seen') = logic_of_clause cls (FOL,seen) |
|
310 val _ = if is_fol_logic lg then () else warning ("Found a HOL clause: " ^ (Term.str_of_term cls)) |
|
311 in |
|
312 logic_of_clauses clss (lg,seen') |
|
313 end |
304 | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); |
314 | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); |
305 |
315 |
306 fun logic_of_nclauses [] (lg,seen) = (lg,seen) |
316 fun logic_of_nclauses [] (lg,seen) = (lg,seen) |
307 | logic_of_nclauses (cls::clss) (FOL,seen) = |
317 | logic_of_nclauses (cls::clss) (FOL,seen) = |
308 logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen)) |
318 logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen)) |