equal
deleted
inserted
replaced
8 signature SMTLIB2_ISAR = |
8 signature SMTLIB2_ISAR = |
9 sig |
9 sig |
10 val simplify_bool: term -> term |
10 val simplify_bool: term -> term |
11 val unlift_term: term list -> term -> term |
11 val unlift_term: term list -> term -> term |
12 val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term |
12 val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term |
13 val normalize_prems : Proof.context -> term -> (string * string list) list |
13 val normalizing_prems : Proof.context -> term -> (string * string list) list |
14 val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list -> |
14 val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list -> |
15 (''a * 'c) list -> 'c list -> 'c -> 'c -> ATP_Problem.atp_formula_role * 'c |
15 (''a * 'c) list -> 'c list -> 'c -> 'c -> ATP_Problem.atp_formula_role * 'c |
16 |
|
17 end; |
16 end; |
18 |
17 |
19 structure SMTLIB2_Isar: SMTLIB2_ISAR = |
18 structure SMTLIB2_Isar: SMTLIB2_ISAR = |
20 struct |
19 struct |
21 |
20 |
72 |> not (null ll_defs) ? unlift_term ll_defs |
71 |> not (null ll_defs) ? unlift_term ll_defs |
73 |> unskolemize_names |
72 |> unskolemize_names |
74 |> push_skolem_all_under_iff |
73 |> push_skolem_all_under_iff |
75 |> HOLogic.mk_Trueprop |
74 |> HOLogic.mk_Trueprop |
76 |
75 |
77 fun normalize_prems ctxt concl0 = |
76 fun normalizing_prems ctxt concl0 = |
78 SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ |
77 SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ |
79 SMT2_Normalize.abs_min_max_table |
78 SMT2_Normalize.abs_min_max_table |
80 |> map_filter (fn (c, th) => |
79 |> map_filter (fn (c, th) => |
81 if exists_Const (curry (op =) c o fst) concl0 then |
80 if exists_Const (curry (op =) c o fst) concl0 then |
82 let val s = short_thm_name ctxt th in SOME (s, [s]) end |
81 let val s = short_thm_name ctxt th in SOME (s, [s]) end |