6 *) |
6 *) |
7 |
7 |
8 signature SMTLIB_ISAR = |
8 signature SMTLIB_ISAR = |
9 sig |
9 sig |
10 val unlift_term: term list -> term -> term |
10 val unlift_term: term list -> term -> term |
11 val postprocess_step_conclusion: theory -> thm list -> term list -> term -> term |
11 val postprocess_step_conclusion: Proof.context -> thm list -> term list -> term -> term |
12 val normalizing_prems : Proof.context -> term -> (string * string list) list |
12 val normalizing_prems : Proof.context -> term -> (string * string list) list |
13 val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list -> |
13 val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list -> |
14 (''a * 'c) list -> 'c list -> 'c -> (ATP_Problem.atp_formula_role * 'c) option |
14 (''a * 'c) list -> 'c list -> 'c -> (ATP_Problem.atp_formula_role * 'c) option |
15 val unskolemize_names: term -> term |
15 val unskolemize_names: Proof.context -> term -> term |
16 end; |
16 end; |
17 |
17 |
18 structure SMTLIB_Isar: SMTLIB_ISAR = |
18 structure SMTLIB_Isar: SMTLIB_ISAR = |
19 struct |
19 struct |
20 |
20 |
32 | NONE => t) |
32 | NONE => t) |
33 | un_free t = t |
33 | un_free t = t |
34 and un_term t = map_aterms un_free t |
34 and un_term t = map_aterms un_free t |
35 in un_term end |
35 in un_term end |
36 |
36 |
37 (* It is not entirely clear why this should be necessary, especially for abstractions variables. *) |
37 (* Remove the "__" suffix for newly introduced variables (Skolems). It is not clear why "__" is |
38 val unskolemize_names = |
38 generated also for abstraction variables, but this is repaired here. *) |
|
39 fun unskolemize_names ctxt = |
39 Term.map_abs_vars (perhaps (try Name.dest_skolem)) |
40 Term.map_abs_vars (perhaps (try Name.dest_skolem)) |
40 #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T)))) |
41 #> Term.map_aterms (perhaps (try (fn Free (s, T) => |
|
42 Free (s |> not (Variable.is_fixed ctxt s) ? Name.dest_skolem, T)))) |
41 |
43 |
42 fun postprocess_step_conclusion thy rewrite_rules ll_defs = |
44 fun postprocess_step_conclusion ctxt rewrite_rules ll_defs = |
43 Raw_Simplifier.rewrite_term thy rewrite_rules [] |
45 let val thy = Proof_Context.theory_of ctxt in |
44 #> Object_Logic.atomize_term thy |
46 Raw_Simplifier.rewrite_term thy rewrite_rules [] |
45 #> not (null ll_defs) ? unlift_term ll_defs |
47 #> Object_Logic.atomize_term thy |
46 #> simplify_bool |
48 #> not (null ll_defs) ? unlift_term ll_defs |
47 #> unskolemize_names |
49 #> simplify_bool |
48 #> HOLogic.mk_Trueprop |
50 #> unskolemize_names ctxt |
|
51 #> HOLogic.mk_Trueprop |
|
52 end |
49 |
53 |
50 fun normalizing_prems ctxt concl0 = |
54 fun normalizing_prems ctxt concl0 = |
51 SMT_Normalize.case_bool_entry :: SMT_Normalize.special_quant_table @ |
55 SMT_Normalize.case_bool_entry :: SMT_Normalize.special_quant_table @ |
52 SMT_Normalize.abs_min_max_table |
56 SMT_Normalize.abs_min_max_table |
53 |> map_filter (fn (c, th) => |
57 |> map_filter (fn (c, th) => |