author  blanchet 
Thu, 28 Aug 2014 00:40:38 +0200  
changeset 58059  4e477dcd050a 
parent 58058  1a0b18176548 
child 58957  c9e744ea8a38 
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_reconstruction.ML 
36898  2 
Author: Sascha Boehme, TU Muenchen 
3 

4 
Proof reconstruction for proofs found by Z3. 

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_RECONSTRUCTION = 
36898  8 
sig 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

9 
val add_z3_rule: thm > Context.generic > Context.generic 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

10 
val reconstruct: Proof.context > Old_SMT_Translate.recon > string list > int list * thm 
36898  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_Reconstruction: OLD_Z3_PROOF_RECONSTRUCTION = 
36898  14 
struct 
15 

16 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

17 
fun z3_exn msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

18 
("Z3 proof reconstruction: " ^ msg)) 
36898  19 

20 

21 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

22 
(* net of schematic rules *) 
36898  23 

24 
local 

25 
val description = "declaration of Z3 proof rules" 

26 

27 
val eq = Thm.eq_thm 

28 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

29 
structure Old_Z3_Rules = Generic_Data 
36898  30 
( 
31 
type T = thm Net.net 

32 
val empty = Net.empty 

33 
val extend = I 

34 
val merge = Net.merge eq 

35 
) 

36 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

37 
fun prep context = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

38 
`Thm.prop_of o rewrite_rule (Context.proof_of context) [Old_Z3_Proof_Literals.rewrite_true] 
36898  39 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

40 
fun ins thm context = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

41 
context > Old_Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

42 
fun rem thm context = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

43 
context > Old_Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net) 
36898  44 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

45 
val add = Thm.declaration_attribute ins 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

46 
val del = Thm.declaration_attribute rem 
36898  47 
in 
48 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

49 
val add_z3_rule = ins 
36898  50 

51 
fun by_schematic_rule ctxt ct = 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

52 
the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct) 
36898  53 

57957  54 
val _ = Theory.setup 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

55 
(Attrib.setup @{binding old_z3_rule} (Attrib.add_del add del) description #> 
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

56 
Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get)) 
36898  57 

58 
end 

59 

60 

61 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

62 
(* proof tools *) 
36898  63 

64 
fun named ctxt name prover ct = 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

65 
let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") 
36898  66 
in prover ct end 
67 

68 
fun NAMED ctxt name tac i st = 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

69 
let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") 
36898  70 
in tac i st end 
71 

72 
fun pretty_goal ctxt thms t = 

73 
[Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] 

74 
> not (null thms) ? cons (Pretty.big_list "assumptions:" 

75 
(map (Display.pretty_thm ctxt) thms)) 

76 

77 
fun try_apply ctxt thms = 

78 
let 

79 
fun try_apply_err ct = Pretty.string_of (Pretty.chunks [ 

80 
Pretty.big_list ("Z3 found a proof," ^ 

81 
" but proof reconstruction failed at the following subgoal:") 

82 
(pretty_goal ctxt thms (Thm.term_of ct)), 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

83 
Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")]) 
36898  84 

85 
fun apply [] ct = error (try_apply_err ct) 

86 
 apply (prover :: provers) ct = 

87 
(case try prover ct of 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

88 
SOME thm => (Old_SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm) 
36898  89 
 NONE => apply provers ct) 
90 

43893
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

91 
fun schematic_label full = "schematic rules" > full ? suffix " (full)" 
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

92 
fun schematic ctxt full ct = 
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

93 
ct 
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

94 
> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms 
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

95 
> named ctxt (schematic_label full) (by_schematic_rule ctxt) 
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

96 
> fold Thm.elim_implies thms 
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

97 

f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset

98 
in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end 
36898  99 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

100 
local 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

101 
val rewr_if = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

102 
@{lemma "(if P then Q1 else Q2) = ((P > Q1) & (~P > Q2))" by simp} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

103 
in 
42793  104 

105 
fun HOL_fast_tac ctxt = 

106 
Classical.fast_tac (put_claset HOL_cs ctxt) 

107 

108 
fun simp_fast_tac ctxt = 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

109 
Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if]) 
42793  110 
THEN_ALL_NEW HOL_fast_tac ctxt 
111 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

112 
end 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

113 

36898  114 

115 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

116 
(* theorems and proofs *) 
36898  117 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

118 
(** theorem incarnations **) 
36898  119 

120 
datatype theorem = 

121 
Thm of thm  (* theorem without special features *) 

122 
MetaEq of thm  (* meta equality "t == s" *) 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

123 
Literals of thm * Old_Z3_Proof_Literals.littab 
36898  124 
(* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) 
125 

126 
fun thm_of (Thm thm) = thm 

127 
 thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq} 

128 
 thm_of (Literals (thm, _)) = thm 

129 

130 
fun meta_eq_of (MetaEq thm) = thm 

131 
 meta_eq_of p = mk_meta_eq (thm_of p) 

132 

133 
fun literals_of (Literals (_, lits)) = lits 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

134 
 literals_of p = Old_Z3_Proof_Literals.make_littab [thm_of p] 
36898  135 

136 

137 

138 
(** core proof rules **) 

139 

140 
(* assumption *) 

41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

141 

36898  142 
local 
58057  143 
val remove_trigger = mk_meta_eq @{thm trigger_def} 
144 
val remove_weight = mk_meta_eq @{thm weight_def} 

145 
val remove_fun_app = mk_meta_eq @{thm fun_app_def} 

36898  146 

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset

147 
fun rewrite_conv _ [] = Conv.all_conv 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

148 
 rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) 
36898  149 

41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

150 
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

151 
remove_fun_app, Old_Z3_Proof_Literals.rewrite_true] 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

152 

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset

153 
fun rewrite _ [] = I 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset

154 
 rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) 
36898  155 

41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

156 
fun lookup_assm assms_net ct = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

157 
Old_Z3_Proof_Tools.net_instances assms_net ct 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

158 
> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct)) 
36898  159 
in 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

160 

fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

161 
fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt = 
36898  162 
let 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

163 
val eqs = map (rewrite ctxt [Old_Z3_Proof_Literals.rewrite_true]) rewrite_rules 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

164 
val eqs' = union Thm.eq_thm eqs prep_rules 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

165 

fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

166 
val assms_net = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

167 
assms 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

168 
> map (apsnd (rewrite ctxt eqs')) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

169 
> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

170 
> Old_Z3_Proof_Tools.thm_net_of snd 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

171 

fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

172 
fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

173 

fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

174 
fun assume thm ctxt = 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

175 
let 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

176 
val ct = Thm.cprem_of thm 1 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

177 
val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

178 
in (Thm.implies_elim thm thm', ctxt') end 
36898  179 

45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

180 
fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) = 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

181 
let 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

182 
val (thm, ctxt') = 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

183 
if exact then (Thm.implies_elim thm1 th, ctxt) 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

184 
else assume thm1 ctxt 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

185 
val thms' = if exact then thms else th :: thms 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

186 
in 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

187 
((insert (op =) i is, thms'), 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

188 
(ctxt', Inttab.update (idx, Thm thm) ptab)) 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

189 
end 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

190 

13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

191 
fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) = 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

192 
let 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

193 
val thm1 = 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

194 
Thm.trivial ct 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

195 
> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

196 
val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

197 
in 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

198 
(case lookup_assm assms_net (Thm.cprem_of thm2 1) of 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

199 
[] => 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

200 
let val (thm, ctxt') = assume thm1 ctxt 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

201 
in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

202 
 ithms => fold (add1 idx thm1) ithms cx) 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

203 
end 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

204 
in fold add asserted (([], []), (ctxt, Inttab.empty)) end 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

205 

36898  206 
end 
207 

208 

209 
(* P = Q ==> P ==> Q or P > Q ==> P ==> Q *) 

210 
local 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

211 
val precomp = Old_Z3_Proof_Tools.precompose2 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

212 
val comp = Old_Z3_Proof_Tools.compose 
36898  213 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

214 
val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

215 
val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

216 

6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

217 
val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

218 
val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp} 
36898  219 
in 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

220 
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p) 
36898  221 
 mp p_q p = 
222 
let 

223 
val pq = thm_of p_q 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

224 
val thm = comp iffD1_c pq handle THM _ => comp mp_c pq 
36898  225 
in Thm (Thm.implies_elim thm p) end 
226 
end 

227 

228 

229 
(* and_elim: P1 & ... & Pn ==> Pi *) 

230 
(* not_or_elim: ~(P1  ...  Pn) ==> ~Pi *) 

231 
local 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

232 
fun is_sublit conj t = Old_Z3_Proof_Literals.exists_lit conj (fn u => u aconv t) 
36898  233 

234 
fun derive conj t lits idx ptab = 

235 
let 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

236 
val lit = the (Old_Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

237 
val ls = Old_Z3_Proof_Literals.explode conj false false [t] lit 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

238 
val lits' = fold Old_Z3_Proof_Literals.insert_lit ls 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

239 
(Old_Z3_Proof_Literals.delete_lit lit lits) 
36898  240 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

241 
fun upd thm = Literals (thm_of thm, lits') 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

242 
val ptab' = Inttab.map_entry idx upd ptab 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

243 
in (the (Old_Z3_Proof_Literals.lookup_lit lits' t), ptab') end 
36898  244 

245 
fun lit_elim conj (p, idx) ct ptab = 

246 
let val lits = literals_of p 

247 
in 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

248 
(case Old_Z3_Proof_Literals.lookup_lit lits (Old_SMT_Utils.term_of ct) of 
36898  249 
SOME lit => (Thm lit, ptab) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

250 
 NONE => apfst Thm (derive conj (Old_SMT_Utils.term_of ct) lits idx ptab)) 
36898  251 
end 
252 
in 

253 
val and_elim = lit_elim true 

254 
val not_or_elim = lit_elim false 

255 
end 

256 

257 

258 
(* P1, ..., Pn  False ==>  ~P1  ...  ~Pn *) 

259 
local 

260 
fun step lit thm = 

261 
Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

262 
val explode_disj = Old_Z3_Proof_Literals.explode false false false 
36898  263 
fun intro hyps thm th = fold step (explode_disj hyps th) thm 
264 

265 
fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

266 
val ccontr = Old_Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr} 
36898  267 
in 
268 
fun lemma thm ct = 

269 
let 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

270 
val cu = Old_Z3_Proof_Literals.negate (Thm.dest_arg ct) 
44058  271 
val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

272 
val th = Old_Z3_Proof_Tools.under_assumption (intro hyps thm) cu 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

273 
in Thm (Old_Z3_Proof_Tools.compose ccontr th) end 
36898  274 
end 
275 

276 

277 
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) 

278 
local 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

279 
val explode_disj = Old_Z3_Proof_Literals.explode false true false 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

280 
val join_disj = Old_Z3_Proof_Literals.join false 
36898  281 
fun unit thm thms th = 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

282 
let 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

283 
val t = @{const Not} $ Old_SMT_Utils.prop_of thm 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

284 
val ts = map Old_SMT_Utils.prop_of thms 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

285 
in 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

286 
join_disj (Old_Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

287 
end 
36898  288 

289 
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) 

290 
fun dest ct = pairself dest_arg2 (Thm.dest_binop ct) 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

291 
val contrapos = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

292 
Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} 
36898  293 
in 
294 
fun unit_resolution thm thms ct = 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

295 
Old_Z3_Proof_Literals.negate (Thm.dest_arg ct) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

296 
> Old_Z3_Proof_Tools.under_assumption (unit thm thms) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

297 
> Thm o Old_Z3_Proof_Tools.discharge thm o Old_Z3_Proof_Tools.compose contrapos 
36898  298 
end 
299 

300 

301 
(* P ==> P == True or P ==> P == False *) 

302 
local 

303 
val iff1 = @{lemma "P ==> P == (~ False)" by simp} 

304 
val iff2 = @{lemma "~P ==> P == False" by simp} 

305 
in 

306 
fun iff_true thm = MetaEq (thm COMP iff1) 

307 
fun iff_false thm = MetaEq (thm COMP iff2) 

308 
end 

309 

310 

311 
(* distributivity of  over & *) 

312 
fun distributivity ctxt = Thm o try_apply ctxt [] [ 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

313 
named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] 
36898  314 
(* FIXME: not very well tested *) 
315 

316 

317 
(* Tseitinlike axioms *) 

318 
local 

319 
val disjI1 = @{lemma "(P ==> Q) ==> ~P  Q" by fast} 

320 
val disjI2 = @{lemma "(~P ==> Q) ==> P  Q" by fast} 

321 
val disjI3 = @{lemma "(~Q ==> P) ==> P  Q" by fast} 

322 
val disjI4 = @{lemma "(Q ==> P) ==> P  ~Q" by fast} 

323 

324 
fun prove' conj1 conj2 ct2 thm = 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

325 
let 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

326 
val littab = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

327 
Old_Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

328 
> cons Old_Z3_Proof_Literals.true_thm 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

329 
> Old_Z3_Proof_Literals.make_littab 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

330 
in Old_Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end 
36898  331 

332 
fun prove rule (ct1, conj1) (ct2, conj2) = 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

333 
Old_Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule 
36898  334 

335 
fun prove_def_axiom ct = 

336 
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) 

337 
in 

338 
(case Thm.term_of ct1 of 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

339 
@{const Not} $ (@{const HOL.conj} $ _ $ _) => 
36898  340 
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true) 
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

341 
 @{const HOL.conj} $ _ $ _ => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

342 
prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, true) 
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

343 
 @{const Not} $ (@{const HOL.disj} $ _ $ _) => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

344 
prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, false) 
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

345 
 @{const HOL.disj} $ _ $ _ => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

346 
prove disjI2 (Old_Z3_Proof_Literals.negate ct1, false) (ct2, true) 
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40680
diff
changeset

347 
 Const (@{const_name distinct}, _) $ _ => 
36898  348 
let 
349 
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

350 
val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv 
36898  351 
fun prv cu = 
352 
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) 

353 
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

354 
in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end 
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40680
diff
changeset

355 
 @{const Not} $ (Const (@{const_name distinct}, _) $ _) => 
36898  356 
let 
357 
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

358 
val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv 
36898  359 
fun prv cu = 
360 
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) 

361 
in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

362 
in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end 
36898  363 
 _ => raise CTERM ("prove_def_axiom", [ct])) 
364 
end 

365 
in 

366 
fun def_axiom ctxt = Thm o try_apply ctxt [] [ 

367 
named ctxt "conj/disj/distinct" prove_def_axiom, 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

368 
Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

369 
named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt (simp_fast_tac ctxt')))] 
36898  370 
end 
371 

372 

373 
(* local definitions *) 

374 
local 

375 
val intro_rules = [ 

376 
@{lemma "n == P ==> (~n  P) & (n  ~P)" by simp}, 

377 
@{lemma "n == (if P then s else t) ==> (~P  n = s) & (P  n = t)" 

378 
by simp}, 

379 
@{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] 

380 

381 
val apply_rules = [ 

382 
@{lemma "(~n  P) & (n  ~P) ==> P == n" by (atomize(full)) fast}, 

383 
@{lemma "(~P  n = s) & (P  n = t) ==> (if P then s else t) == n" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44488
diff
changeset

384 
by (atomize(full)) fastforce} ] 
36898  385 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

386 
val inst_rule = Old_Z3_Proof_Tools.match_instantiate Thm.dest_arg 
36898  387 

388 
fun apply_rule ct = 

389 
(case get_first (try (inst_rule ct)) intro_rules of 

390 
SOME thm => thm 

391 
 NONE => raise CTERM ("intro_def", [ct])) 

392 
in 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

393 
fun intro_def ct = Old_Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm 
36898  394 

395 
fun apply_def thm = 

396 
get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules 

397 
> the_default (Thm thm) 

398 
end 

399 

400 

401 
(* negation normal form *) 

402 
local 

403 
val quant_rules1 = ([ 

404 
@{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp}, 

405 
@{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [ 

406 
@{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp}, 

407 
@{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}]) 

408 

409 
val quant_rules2 = ([ 

410 
@{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp}, 

411 
@{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [ 

412 
@{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp}, 

413 
@{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}]) 

414 

415 
fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = ( 

52732  416 
rtac thm ORELSE' 
417 
(match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE' 

418 
(match_tac qs2 THEN' nnf_quant_tac thm qs)) i st 

36898  419 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

420 
fun nnf_quant_tac_varified vars eq = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

421 
nnf_quant_tac (Old_Z3_Proof_Tools.varify vars eq) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

422 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

423 
fun nnf_quant ctxt vars qs p ct = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

424 
Old_Z3_Proof_Tools.as_meta_eq ct 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

425 
> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs) 
36898  426 

427 
fun prove_nnf ctxt = try_apply ctxt [] [ 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

428 
named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq, 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

429 
Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

430 
named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt' (simp_fast_tac ctxt')))] 
36898  431 
in 
432 
fun nnf ctxt vars ps ct = 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

433 
(case Old_SMT_Utils.term_of ct of 
36898  434 
_ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => 
435 
if l aconv r 

436 
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

437 
else MetaEq (nnf_quant ctxt vars quant_rules1 (hd ps) ct) 
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

438 
 _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) => 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

439 
MetaEq (nnf_quant ctxt vars quant_rules2 (hd ps) ct) 
36898  440 
 _ => 
441 
let 

442 
val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

443 
(Old_Z3_Proof_Tools.unfold_eqs ctxt 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

444 
(map (Thm.symmetric o meta_eq_of) ps))) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

445 
in Thm (Old_Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) 
36898  446 
end 
447 

448 

449 

450 
(** equality proof rules **) 

451 

452 
(*  t = t *) 

453 
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) 

454 

455 

456 
(* s = t ==> t = s *) 

457 
local 

458 
val symm_rule = @{lemma "s = t ==> t == s" by simp} 

459 
in 

460 
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm) 

461 
 symm p = MetaEq (thm_of p COMP symm_rule) 

462 
end 

463 

464 

465 
(* s = t ==> t = u ==> s = u *) 

466 
local 

467 
val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp} 

468 
val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp} 

469 
val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp} 

470 
in 

471 
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2) 

472 
 trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1)) 

473 
 trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2)) 

474 
 trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3)) 

475 
end 

476 

477 

478 
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn 

479 
(reflexive antecendents are droppped) *) 

480 
local 

481 
exception MONO 

482 

483 
fun prove_refl (ct, _) = Thm.reflexive ct 

484 
fun prove_comb f g cp = 

485 
let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp 

486 
in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end 

487 
fun prove_arg f = prove_comb prove_refl f 

488 

489 
fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp 

490 

491 
fun prove_nary is_comb f = 

492 
let 

493 
fun prove (cp as (ct, _)) = f cp handle MONO => 

494 
if is_comb (Thm.term_of ct) 

495 
then prove_comb (prove_arg prove) prove cp 

496 
else prove_refl cp 

497 
in prove end 

498 

499 
fun prove_list f n cp = 

500 
if n = 0 then prove_refl cp 

501 
else prove_comb (prove_arg f) (prove_list f (n1)) cp 

502 

503 
fun with_length f (cp as (cl, _)) = 

504 
f (length (HOLogic.dest_list (Thm.term_of cl))) cp 

505 

506 
fun prove_distinct f = prove_arg (with_length (prove_list f)) 

507 

508 
fun prove_eq exn lookup cp = 

509 
(case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of 

510 
SOME eq => eq 

511 
 NONE => if exn then raise MONO else prove_refl cp) 

512 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

513 
val prove_exn = prove_eq true 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

514 
and prove_safe = prove_eq false 
36898  515 

516 
fun mono f (cp as (cl, _)) = 

517 
(case Term.head_of (Thm.term_of cl) of 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

518 
@{const HOL.conj} => prove_nary Old_Z3_Proof_Literals.is_conj (prove_exn f) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

519 
 @{const HOL.disj} => prove_nary Old_Z3_Proof_Literals.is_disj (prove_exn f) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

520 
 Const (@{const_name distinct}, _) => prove_distinct (prove_safe f) 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

521 
 _ => prove (prove_safe f)) cp 
36898  522 
in 
523 
fun monotonicity eqs ct = 

524 
let 

40680
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset

525 
fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)] 
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset

526 
val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs 
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset

527 
val lookup = AList.lookup (op aconv) teqs 
36898  528 
val cp = Thm.dest_binop (Thm.dest_arg ct) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

529 
in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end 
36898  530 
end 
531 

532 

533 
(*  f a b = f b a (where f is equality) *) 

534 
local 

535 
val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} 

536 
in 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

537 
fun commutativity ct = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

538 
MetaEq (Old_Z3_Proof_Tools.match_instantiate I 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

539 
(Old_Z3_Proof_Tools.as_meta_eq ct) rule) 
36898  540 
end 
541 

542 

543 

544 
(** quantifier proof rules **) 

545 

546 
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x) 

547 
P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *) 

548 
local 

549 
val rules = [ 

550 
@{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}, 

551 
@{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}] 

552 
in 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

553 
fun quant_intro ctxt vars p ct = 
36898  554 
let 
555 
val thm = meta_eq_of p 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

556 
val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

557 
val cu = Old_Z3_Proof_Tools.as_meta_eq ct 
52732  558 
val tac = REPEAT_ALL_NEW (match_tac rules') 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

559 
in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end 
36898  560 
end 
561 

562 

563 
(*  ((ALL x. P x)  Q) = (ALL x. P x  Q) *) 

564 
fun pull_quant ctxt = Thm o try_apply ctxt [] [ 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

565 
named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] 
36898  566 
(* FIXME: not very well tested *) 
567 

568 

569 
(*  (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) 

570 
fun push_quant ctxt = Thm o try_apply ctxt [] [ 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

571 
named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] 
36898  572 
(* FIXME: not very well tested *) 
573 

574 

575 
(*  (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *) 

576 
local 

42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset

577 
val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast} 
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset

578 
val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast} 
36898  579 

42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset

580 
fun elim_unused_tac i st = ( 
52732  581 
match_tac [@{thm refl}] 
582 
ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac) 

42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset

583 
ORELSE' ( 
52732  584 
match_tac [@{thm iff_allI}, @{thm iff_exI}] 
42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset

585 
THEN' elim_unused_tac)) i st 
36898  586 
in 
42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset

587 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

588 
fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt elim_unused_tac 
42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset

589 

36898  590 
end 
591 

592 

593 
(*  (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn)  P x1 ... xn) = P t1 ... tn *) 

594 
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

595 
named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] 
36898  596 
(* FIXME: not very well tested *) 
597 

598 

599 
(*  ~(ALL x1...xn. P x1...xn)  P a1...an *) 

600 
local 

601 
val rule = @{lemma "~ P x  Q ==> ~(ALL x. P x)  Q" by fast} 

602 
in 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

603 
fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt ( 
52732  604 
REPEAT_ALL_NEW (match_tac [rule]) 
605 
THEN' rtac @{thm excluded_middle}) 

36898  606 
end 
607 

608 

42196
9893b2913a44
save reflexivity steps in discharging Z3 Skolemization hypotheses
boehmes
parents:
42191
diff
changeset

609 
(*  (EX x. P x) = P c  ~(ALL x. P x) = ~ P c *) 
36898  610 
local 
42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

611 
val forall = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

612 
Old_SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all} 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

613 
(Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) 
42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

614 
fun mk_forall cv ct = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

615 
Thm.apply (Old_SMT_Utils.instT' cv forall) (Thm.lambda cv ct) 
36898  616 

42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

617 
fun get_vars f mk pred ctxt t = 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

618 
Term.fold_aterms f t [] 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

619 
> map_filter (fn v => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

620 
if pred v then SOME (Old_SMT_Utils.certify ctxt (mk v)) else NONE) 
36898  621 

42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

622 
fun close vars f ct ctxt = 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

623 
let 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

624 
val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst) 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

625 
val vs = frees_of ctxt (Thm.term_of ct) 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

626 
val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

627 
val vars_of = get_vars Term.add_vars Var (K true) ctxt' 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

628 
in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end 
36898  629 

42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

630 
val sk_rules = @{lemma 
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset

631 
"c = (SOME x. P x) ==> (EX x. P x) = P c" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset

632 
"c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)" 
42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

633 
by (metis someI_ex)+} 
36898  634 
in 
42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

635 

09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

636 
fun skolemize vars = 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

637 
apfst Thm oo close vars (yield_singleton Assumption.add_assumes) 
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

638 

09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

639 
fun discharge_sk_tac i st = ( 
52732  640 
rtac @{thm trans} i 
641 
THEN resolve_tac sk_rules i 

642 
THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1) 

643 
THEN rtac @{thm refl} i) st 

42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

644 

36898  645 
end 
646 

647 

42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

648 

36898  649 
(** theory proof rules **) 
650 

651 
(* theory lemmas: linear arithmetic, arrays *) 

652 
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

653 
Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

654 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

655 
NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

656 
ORELSE' NAMED ctxt' "simp+arith" ( 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

657 
Simplifier.asm_full_simp_tac (put_simpset simpset ctxt') 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

658 
THEN_ALL_NEW Arith_Data.arith_tac ctxt')))] 
36898  659 

660 

661 
(* rewriting: prove equalities: 

662 
* ACI of conjunction/disjunction 

663 
* contradiction, excluded middle 

664 
* logical rewriting rules (for negation, implication, equivalence, 

665 
distinct) 

666 
* normal forms for polynoms (integer/real arithmetic) 

667 
* quantifier elimination over linear arithmetic 

668 
* ... ? **) 

669 
local 

670 
fun spec_meta_eq_of thm = 

671 
(case try (fn th => th RS @{thm spec}) thm of 

672 
SOME thm' => spec_meta_eq_of thm' 

673 
 NONE => mk_meta_eq thm) 

674 

675 
fun prep (Thm thm) = spec_meta_eq_of thm 

676 
 prep (MetaEq thm) = thm 

677 
 prep (Literals (thm, _)) = spec_meta_eq_of thm 

678 

679 
fun unfold_conv ctxt ths = 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

680 
Conv.arg_conv (Conv.binop_conv (Old_Z3_Proof_Tools.unfold_eqs ctxt 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

681 
(map prep ths))) 
36898  682 

683 
fun with_conv _ [] prv = prv 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

684 
 with_conv ctxt ths prv = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

685 
Old_Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv 
36898  686 

687 
val unfold_conv = 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

688 
Conv.arg_conv (Conv.binop_conv 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

689 
(Conv.try_conv Old_Z3_Proof_Tools.unfold_distinct_conv)) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

690 
val prove_conj_disj_eq = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

691 
Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq 
40663  692 

41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41426
diff
changeset

693 
fun declare_hyps ctxt thm = 
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41426
diff
changeset

694 
(thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt)) 
36898  695 
in 
696 

42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

697 
val abstraction_depth = 3 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

698 
(* 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

699 
This value was chosen large enough to potentially catch exceptions, 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

700 
yet small enough to not cause too much harm. The value might be 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

701 
increased in the future, if reconstructing 'rewrite' fails on problems 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

702 
that get too much abstracted to be reconstructable. 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

703 
*) 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

704 

40663  705 
fun rewrite simpset ths ct ctxt = 
41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41426
diff
changeset

706 
apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [ 
40663  707 
named ctxt "conj/disj/distinct" prove_conj_disj_eq, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

708 
named ctxt "pullite" Old_Z3_Proof_Methods.prove_ite ctxt, 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

709 
Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

710 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

711 
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt')) 
42793  712 
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))), 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

713 
Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

714 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
52732  715 
(rtac @{thm iff_allI} ORELSE' K all_tac) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

716 
THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt')) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

717 
THEN_ALL_NEW ( 
42793  718 
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt') 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

719 
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

720 
Old_Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

721 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
52732  722 
(rtac @{thm iff_allI} ORELSE' K all_tac) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

723 
THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt')) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

724 
THEN_ALL_NEW ( 
42793  725 
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt') 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

726 
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

727 
named ctxt "injectivity" (Old_Z3_Proof_Methods.prove_injectivity ctxt), 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

728 
Old_Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt [] 
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

729 
(fn ctxt' => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

730 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
52732  731 
(rtac @{thm iff_allI} ORELSE' K all_tac) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

732 
THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt')) 
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

733 
THEN_ALL_NEW ( 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

734 
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt') 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

735 
ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac 
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset

736 
ctxt'))))]) ct)) 
36898  737 

738 
end 

739 

740 

741 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

742 
(* proof reconstruction *) 
36898  743 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

744 
(** tracing and checking **) 
36898  745 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

746 
fun trace_before ctxt idx = Old_SMT_Config.trace_msg ctxt (fn r => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

747 
"Z3: #" ^ string_of_int idx ^ ": " ^ Old_Z3_Proof_Parser.string_of_rule r) 
36898  748 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

749 
fun check_after idx r ps ct (p, (ctxt, _)) = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

750 
if not (Config.get ctxt Old_SMT_Config.trace) then () 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

751 
else 
36898  752 
let val thm = thm_of p > tap (Thm.join_proofs o single) 
753 
in 

754 
if (Thm.cprop_of thm) aconvc ct then () 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

755 
else 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

756 
z3_exn (Pretty.string_of (Pretty.big_list 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

757 
("proof step failed: " ^ quote (Old_Z3_Proof_Parser.string_of_rule r) ^ 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

758 
" (#" ^ string_of_int idx ^ ")") 
36898  759 
(pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

760 
[Pretty.block [Pretty.str "expected: ", 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

761 
Syntax.pretty_term ctxt (Thm.term_of ct)]]))) 
36898  762 
end 
763 

764 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

765 
(** overall reconstruction procedure **) 
36898  766 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

767 
local 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

768 
fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^ 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

769 
quote (Old_Z3_Proof_Parser.string_of_rule r)) 
36898  770 

41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

771 
fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

772 
(case (r, ps) of 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

773 
(* core rules *) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

774 
(Old_Z3_Proof_Parser.True_Axiom, _) => (Thm Old_Z3_Proof_Literals.true_thm, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

775 
 (Old_Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

776 
 (Old_Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

777 
 (Old_Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) => 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

778 
(mp q (thm_of p), cxp) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

779 
 (Old_Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) => 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

780 
(mp q (thm_of p), cxp) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

781 
 (Old_Z3_Proof_Parser.And_Elim, [(p, i)]) => 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

782 
and_elim (p, i) ct ptab > pair cx 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

783 
 (Old_Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) => 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

784 
not_or_elim (p, i) ct ptab > pair cx 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

785 
 (Old_Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

786 
 (Old_Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

787 
 (Old_Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) => 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

788 
(unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

789 
 (Old_Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

790 
 (Old_Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

791 
 (Old_Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

792 
 (Old_Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

793 
 (Old_Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx > rpair ptab 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

794 
 (Old_Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

795 
 (Old_Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

796 
 (Old_Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

797 
 (Old_Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp) 
36898  798 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

799 
(* equality rules *) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

800 
 (Old_Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

801 
 (Old_Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

802 
 (Old_Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

803 
 (Old_Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

804 
 (Old_Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

805 

57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

806 
(* quantifier rules *) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

807 
 (Old_Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro cx vars p ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

808 
 (Old_Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

809 
 (Old_Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

810 
 (Old_Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

811 
 (Old_Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

812 
 (Old_Z3_Proof_Parser.Quant_Inst, _) => (quant_inst cx ct, cxp) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

813 
 (Old_Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx > rpair ptab 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

814 

57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

815 
(* theory rules *) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

816 
 (Old_Z3_Proof_Parser.Th_Lemma _, _) => (* FIXME: use arguments *) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

817 
(th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

818 
 (Old_Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx > rpair ptab 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

819 
 (Old_Z3_Proof_Parser.Rewrite_Star, ps) => 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

820 
rewrite simpset (map fst ps) ct cx > rpair ptab 
36898  821 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

822 
 (Old_Z3_Proof_Parser.Nnf_Star, _) => not_supported r 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

823 
 (Old_Z3_Proof_Parser.Cnf_Star, _) => not_supported r 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

824 
 (Old_Z3_Proof_Parser.Transitivity_Star, _) => not_supported r 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

825 
 (Old_Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r 
36898  826 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

827 
 _ => raise Fail ("Z3: proof rule " ^ 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

828 
quote (Old_Z3_Proof_Parser.string_of_rule r) ^ 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

829 
" has an unexpected number of arguments.")) 
36898  830 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

831 
fun lookup_proof ptab idx = 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

832 
(case Inttab.lookup ptab idx of 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

833 
SOME p => (p, idx) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

834 
 NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

835 

41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

836 
fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

837 
let 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

838 
val Old_Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

839 
val ps = map (lookup_proof ptab) prems 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

840 
val _ = trace_before ctxt idx r 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

841 
val (thm, (ctxt', ptab')) = 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

842 
cxp 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

843 
> prove_step simpset vars r ps prop 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

844 
> tap (check_after idx r ps prop) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

845 
in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end 
36898  846 

42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

847 
fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

848 
@{thm reflexive}, Old_Z3_Proof_Literals.true_thm] 
42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

849 

45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

850 
fun discharge_assms_tac rules = 
52732  851 
REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac)) 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

852 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

853 
fun discharge_assms ctxt rules thm = 
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

854 
if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

855 
else 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset

856 
(case Seq.pull (discharge_assms_tac rules thm) of 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

857 
SOME (thm', _) => Goal.norm_result ctxt thm' 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

858 
 NONE => raise THM ("failed to discharge premise", 1, [thm])) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

859 

41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

860 
fun discharge rules outer_ctxt (p, (inner_ctxt, _)) = 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

861 
thm_of p 
42361  862 
> singleton (Proof_Context.export inner_ctxt outer_ctxt) 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

863 
> discharge_assms outer_ctxt (make_discharge_rules rules) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

864 
in 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

865 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

866 
fun reconstruct outer_ctxt recon output = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

867 
let 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

868 
val {context=ctxt, typs, terms, rewrite_rules, assms} = recon 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41172
diff
changeset

869 
val (asserted, steps, vars, ctxt1) = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

870 
Old_Z3_Proof_Parser.parse ctxt typs terms output 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

871 

57957  872 
val simpset = 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

873 
Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp}) 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

874 

fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

875 
val ((is, rules), cxp as (ctxt2, _)) = 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

876 
add_asserted outer_ctxt rewrite_rules assms asserted ctxt1 
36898  877 
in 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

878 
if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI}) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

879 
else 
41131
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

880 
(Thm @{thm TrueI}, cxp) 
fc9d503c3d67
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset

881 
> fold (prove simpset vars) steps 
42191
09377c05c561
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset

882 
> discharge rules outer_ctxt 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

883 
> pair [] 
36898  884 
end 
885 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

886 
end 
36898  887 

888 
end 