author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 60752  b48830b670a1 
permissions  rwrr 
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 higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

24 
(* ifthenelse *) 
828e08541cee
replace higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

25 

828e08541cee
replace higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

26 
val pull_ite = mk_meta_eq 
828e08541cee
replace higherorder 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 higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

28 

828e08541cee
replace higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

29 
fun pull_ites_conv ct = 
828e08541cee
replace higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

30 
(Conv.rewr_conv pull_ite then_conv 
828e08541cee
replace higherorder 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 higherorder 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 higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

35 
CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv)) 
60752  36 
THEN' resolve_tac ctxt @{thms refl}) 
45392
828e08541cee
replace higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

37 

828e08541cee
replace higherorder matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45263
diff
changeset

38 

828e08541cee
replace higherorder 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 

59586  53 
val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59590
diff
changeset

54 
val inv = Thm.cterm_of ctxt (mk_inv_into dT rT) 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59590
diff
changeset

55 
val univ = Thm.cterm_of ctxt (mk_univ dT) 
40662  56 
in Thm.mk_binop inv univ ct end 
57 

58 
fun mk_inj_prop ctxt ct = 

59 
let 

59586  60 
val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59590
diff
changeset

61 
val inj = Thm.cterm_of ctxt (mk_inj_on dT rT) 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59590
diff
changeset

62 
val univ = Thm.cterm_of ctxt (mk_univ dT) 
58058
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)) 

60752  74 
> apply (resolve_tac ctxt' @{thms injI}) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

75 
> apply (Tactic.solve_tac ctxt' [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}) 
60752  84 
THEN' resolve_tac ctxt [@{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 singleletter 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 singleletter 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)) 
60752  145 
THEN' CSUBGOAL (uncurry (resolve_tac ctxt o single o prove_inj_eq ctxt))) 
40662  146 

147 
end 

148 

149 
end 