author | wenzelm |
Wed, 26 Nov 2014 20:05:34 +0100 | |
changeset 59058 | a78612c67ec0 |
parent 58957 | c9e744ea8a38 |
child 59498 | 50b60f501b05 |
permissions | -rw-r--r-- |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
1 |
(* Title: HOL/Library/Old_SMT/old_z3_proof_methods.ML |
40662 | 2 |
Author: Sascha Boehme, TU Muenchen |
3 |
||
4 |
Proof methods for Z3 proof reconstruction. |
|
5 |
*) |
|
6 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
7 |
signature OLD_Z3_PROOF_METHODS = |
40662 | 8 |
sig |
9 |
val prove_injectivity: Proof.context -> cterm -> thm |
|
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
10 |
val prove_ite: Proof.context -> cterm -> thm |
40662 | 11 |
end |
12 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
13 |
structure Old_Z3_Proof_Methods: OLD_Z3_PROOF_METHODS = |
40662 | 14 |
struct |
15 |
||
16 |
||
17 |
fun apply tac st = |
|
18 |
(case Seq.pull (tac 1 st) of |
|
19 |
NONE => raise THM ("tactic failed", 1, [st]) |
|
20 |
| SOME (st', _) => st') |
|
21 |
||
22 |
||
23 |
||
45392
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
24 |
(* if-then-else *) |
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
25 |
|
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
26 |
val pull_ite = mk_meta_eq |
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
27 |
@{lemma "f (if P then x else y) = (if P then f x else f y)" by simp} |
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
28 |
|
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
29 |
fun pull_ites_conv ct = |
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
30 |
(Conv.rewr_conv pull_ite then_conv |
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
31 |
Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct |
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
32 |
|
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
33 |
fun prove_ite ctxt = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
34 |
Old_Z3_Proof_Tools.by_tac ctxt ( |
45392
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
35 |
CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv)) |
52732 | 36 |
THEN' rtac @{thm refl}) |
45392
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
37 |
|
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
38 |
|
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset
|
39 |
|
40662 | 40 |
(* injectivity *) |
41 |
||
42 |
local |
|
43 |
||
44 |
val B = @{typ bool} |
|
45263 | 45 |
fun mk_univ T = Const (@{const_name top}, HOLogic.mk_setT T) |
40662 | 46 |
fun mk_inj_on T U = |
45263 | 47 |
Const (@{const_name inj_on}, (T --> U) --> HOLogic.mk_setT T --> B) |
40662 | 48 |
fun mk_inv_into T U = |
45263 | 49 |
Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T) |
40662 | 50 |
|
51 |
fun mk_inv_of ctxt ct = |
|
52 |
let |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
53 |
val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct) |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
54 |
val inv = Old_SMT_Utils.certify ctxt (mk_inv_into dT rT) |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
55 |
val univ = Old_SMT_Utils.certify ctxt (mk_univ dT) |
40662 | 56 |
in Thm.mk_binop inv univ ct end |
57 |
||
58 |
fun mk_inj_prop ctxt ct = |
|
59 |
let |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
60 |
val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct) |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
61 |
val inj = Old_SMT_Utils.certify ctxt (mk_inj_on dT rT) |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
62 |
val univ = Old_SMT_Utils.certify ctxt (mk_univ dT) |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
63 |
in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end |
40662 | 64 |
|
65 |
||
66 |
val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
|
67 |
||
40663 | 68 |
fun prove_inj_prop ctxt def lhs = |
40662 | 69 |
let |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
70 |
val (ct, ctxt') = Old_SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
71 |
val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)] |
40662 | 72 |
in |
73 |
Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
|
52732 | 74 |
|> apply (rtac @{thm injI}) |
40662 | 75 |
|> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
76 |
|> Goal.norm_result ctxt' o Goal.finish ctxt' |
40662 | 77 |
|> singleton (Variable.export ctxt' ctxt) |
78 |
end |
|
79 |
||
40663 | 80 |
fun prove_rhs ctxt def lhs = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
81 |
Old_Z3_Proof_Tools.by_tac ctxt ( |
40663 | 82 |
CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
58957 | 83 |
THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI}) |
52732 | 84 |
THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) |
40662 | 85 |
|
86 |
||
87 |
fun expand thm ct = |
|
88 |
let |
|
89 |
val cpat = Thm.dest_arg (Thm.rhs_of thm) |
|
90 |
val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct)) |
|
91 |
val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm |
|
92 |
val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm |
|
93 |
in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end |
|
94 |
||
40663 | 95 |
fun prove_lhs ctxt rhs = |
40662 | 96 |
let |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
97 |
val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs))) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
98 |
val conv = Old_SMT_Utils.binders_conv (K (expand eq)) ctxt |
40662 | 99 |
in |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
100 |
Old_Z3_Proof_Tools.by_tac ctxt ( |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
101 |
CONVERSION (Old_SMT_Utils.prop_conv conv) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
102 |
THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt)) |
40662 | 103 |
end |
104 |
||
105 |
||
40663 | 106 |
fun mk_inv_def ctxt rhs = |
40662 | 107 |
let |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
40840
diff
changeset
|
108 |
val (ct, ctxt') = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
109 |
Old_SMT_Utils.dest_all_cbinders (Old_SMT_Utils.dest_cprop rhs) ctxt |
40662 | 110 |
val (cl, cv) = Thm.dest_binop ct |
111 |
val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45392
diff
changeset
|
112 |
val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf)) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
113 |
in Thm.assume (Old_SMT_Utils.mk_cequals cg cu) end |
40662 | 114 |
|
115 |
fun prove_inj_eq ctxt ct = |
|
116 |
let |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
40840
diff
changeset
|
117 |
val (lhs, rhs) = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58957
diff
changeset
|
118 |
apply2 Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct)) |
41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41328
diff
changeset
|
119 |
val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs) |
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41328
diff
changeset
|
120 |
val rhs_thm = |
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41328
diff
changeset
|
121 |
Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs) |
40662 | 122 |
in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end |
123 |
||
124 |
||
125 |
val swap_eq_thm = mk_meta_eq @{thm eq_commute} |
|
126 |
val swap_disj_thm = mk_meta_eq @{thm disj_commute} |
|
127 |
||
128 |
fun swap_conv dest eq = |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58957
diff
changeset
|
129 |
Old_SMT_Utils.if_true_conv ((op <) o apply2 Term.size_of_term o dest) |
40662 | 130 |
(Conv.rewr_conv eq) |
131 |
||
132 |
val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
133 |
val swap_disj_conv = swap_conv Old_SMT_Utils.dest_disj swap_disj_thm |
40662 | 134 |
|
135 |
fun norm_conv ctxt = |
|
136 |
swap_eq_conv then_conv |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
137 |
Conv.arg1_conv (Old_SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
138 |
Conv.arg_conv (Old_SMT_Utils.binders_conv (K swap_eq_conv) ctxt) |
40662 | 139 |
|
140 |
in |
|
141 |
||
40663 | 142 |
fun prove_injectivity ctxt = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
143 |
Old_Z3_Proof_Tools.by_tac ctxt ( |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
144 |
CONVERSION (Old_SMT_Utils.prop_conv (norm_conv ctxt)) |
52732 | 145 |
THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt))) |
40662 | 146 |
|
147 |
end |
|
148 |
||
149 |
end |