author | blanchet |
Thu, 28 Aug 2014 00:40:38 +0200 | |
changeset 58064 | e9ab6f4c650b |
parent 58061 | 3d060f43accb |
child 58484 | b4c0e2b00036 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smtlib_isar.ML |
57704 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Mathias Fleury, ENS Rennes |
|
4 |
||
5 |
General tools for Isar proof reconstruction. |
|
6 |
*) |
|
7 |
||
58061 | 8 |
signature SMTLIB_ISAR = |
57704 | 9 |
sig |
10 |
val unlift_term: term list -> term -> term |
|
58064
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
11 |
val postprocess_step_conclusion: Proof.context -> thm list -> term list -> term -> term |
57705 | 12 |
val normalizing_prems : Proof.context -> term -> (string * string list) list |
57704 | 13 |
val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list -> |
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
14 |
(''a * 'c) list -> 'c list -> 'c -> (ATP_Problem.atp_formula_role * 'c) option |
58064
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
15 |
val unskolemize_names: Proof.context -> term -> term |
57704 | 16 |
end; |
17 |
||
58061 | 18 |
structure SMTLIB_Isar: SMTLIB_ISAR = |
57704 | 19 |
struct |
20 |
||
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
21 |
open ATP_Util |
57704 | 22 |
open ATP_Problem |
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
23 |
open ATP_Proof_Reconstruct |
57704 | 24 |
|
25 |
fun unlift_term ll_defs = |
|
26 |
let |
|
27 |
val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs |
|
28 |
||
29 |
fun un_free (t as Free (s, _)) = |
|
30 |
(case AList.lookup (op =) lifted s of |
|
31 |
SOME t => un_term t |
|
32 |
| NONE => t) |
|
33 |
| un_free t = t |
|
34 |
and un_term t = map_aterms un_free t |
|
35 |
in un_term end |
|
36 |
||
58064
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
37 |
(* Remove the "__" suffix for newly introduced variables (Skolems). It is not clear why "__" is |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
38 |
generated also for abstraction variables, but this is repaired here. *) |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
39 |
fun unskolemize_names ctxt = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
40 |
Term.map_abs_vars (perhaps (try Name.dest_skolem)) |
58064
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
41 |
#> Term.map_aterms (perhaps (try (fn Free (s, T) => |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
42 |
Free (s |> not (Variable.is_fixed ctxt s) ? Name.dest_skolem, T)))) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
43 |
|
58064
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
44 |
fun postprocess_step_conclusion ctxt rewrite_rules ll_defs = |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
45 |
let val thy = Proof_Context.theory_of ctxt in |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
46 |
Raw_Simplifier.rewrite_term thy rewrite_rules [] |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
47 |
#> Object_Logic.atomize_term thy |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
48 |
#> not (null ll_defs) ? unlift_term ll_defs |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
49 |
#> simplify_bool |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
50 |
#> unskolemize_names ctxt |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
51 |
#> HOLogic.mk_Trueprop |
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
52 |
end |
57704 | 53 |
|
57705 | 54 |
fun normalizing_prems ctxt concl0 = |
58061 | 55 |
SMT_Normalize.case_bool_entry :: SMT_Normalize.special_quant_table @ |
56 |
SMT_Normalize.abs_min_max_table |
|
57704 | 57 |
|> map_filter (fn (c, th) => |
58 |
if exists_Const (curry (op =) c o fst) concl0 then |
|
59 |
let val s = short_thm_name ctxt th in SOME (s, [s]) end |
|
60 |
else |
|
61 |
NONE) |
|
62 |
||
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
63 |
fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts |
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
64 |
concl_t = |
57704 | 65 |
(case ss of |
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
66 |
[s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s)) |
57704 | 67 |
| _ => |
68 |
if id = conjecture_id then |
|
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
69 |
SOME (Conjecture, concl_t) |
57704 | 70 |
else |
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
71 |
(case find_index (curry (op =) id) prem_ids of |
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
72 |
~1 => NONE (* lambda-lifting definition *) |
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
73 |
| i => SOME (Hypothesis, nth hyp_ts i))) |
57704 | 74 |
|
75 |
end; |