author  wenzelm 
Sat, 18 Jul 2015 20:47:08 +0200  
changeset 60752  b48830b670a1 
parent 60642  48dd1cefb4ae 
child 60949  ccbf9379e355 
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) 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58957
diff
changeset

290 
fun dest ct = apply2 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 

58957  415 
fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = ( 
60752  416 
resolve_tac ctxt [thm] ORELSE' 
58957  417 
(match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE' 
418 
(match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st 

36898  419 

58957  420 
fun nnf_quant_tac_varified ctxt vars eq = 
421 
nnf_quant_tac ctxt (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 
58957  425 
> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt 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 = 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58957
diff
changeset

485 
let val ((ct1, ct2), (cu1, cu2)) = apply2 Thm.dest_comb cp 
36898  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 = 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58957
diff
changeset

509 
(case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of 
36898  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 
58957  558 
val tac = REPEAT_ALL_NEW (match_tac ctxt 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 

58957  580 
fun elim_unused_tac ctxt i st = ( 
581 
match_tac ctxt [@{thm refl}] 

582 
ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt) 

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' ( 
58957  584 
match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}] 
585 
THEN' elim_unused_tac ctxt)) 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 

58957  588 
fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt) 
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 ( 
58957  604 
REPEAT_ALL_NEW (match_tac ctxt [rule]) 
60752  605 
THEN' resolve_tac ctxt @{thms 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 => 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59590
diff
changeset

620 
if pred v then SOME (Thm.cterm_of 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' 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59621
diff
changeset

628 
in 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59621
diff
changeset

629 
(Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm, 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59621
diff
changeset

630 
ctxt') 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59621
diff
changeset

631 
end 
36898  632 

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 
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

634 
"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

635 
"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

636 
by (metis someI_ex)+} 
36898  637 
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

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 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

640 
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

641 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

642 
fun discharge_sk_tac ctxt i st = ( 
60752  643 
resolve_tac ctxt @{thms trans} i 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

644 
THEN resolve_tac ctxt sk_rules i 
60752  645 
THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1) 
646 
THEN resolve_tac ctxt @{thms 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

647 

36898  648 
end 
649 

650 

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

651 

36898  652 
(** theory proof rules **) 
653 

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

655 
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

656 
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

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

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

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

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

661 
THEN_ALL_NEW Arith_Data.arith_tac ctxt')))] 
36898  662 

663 

664 
(* rewriting: prove equalities: 

665 
* ACI of conjunction/disjunction 

666 
* contradiction, excluded middle 

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

668 
distinct) 

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

670 
* quantifier elimination over linear arithmetic 

671 
* ... ? **) 

672 
local 

673 
fun spec_meta_eq_of thm = 

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

675 
SOME thm' => spec_meta_eq_of thm' 

676 
 NONE => mk_meta_eq thm) 

677 

678 
fun prep (Thm thm) = spec_meta_eq_of thm 

679 
 prep (MetaEq thm) = thm 

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

681 

682 
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

683 
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

684 
(map prep ths))) 
36898  685 

686 
fun with_conv _ [] prv = prv 

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

687 
 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

688 
Old_Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv 
36898  689 

690 
val unfold_conv = 

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

691 
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

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

693 
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

694 
Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq 
40663  695 

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

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

697 
(thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt)) 
36898  698 
in 
699 

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

700 
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

701 
(* 
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 
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

703 
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

704 
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

705 
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

706 
*) 
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

707 

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

709 
apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [ 
40663  710 
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

711 
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

712 
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

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

714 
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt')) 
42793  715 
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

716 
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

717 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
60752  718 
(resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

719 
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

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

722 
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

723 
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

724 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
60752  725 
(resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

726 
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

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

729 
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

730 
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

731 
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

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

733 
Old_Z3_Proof_Tools.by_tac ctxt' ( 
60752  734 
(resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset

735 
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

736 
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

737 
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

738 
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

739 
ctxt'))))]) ct)) 
36898  740 

741 
end 

742 

743 

744 

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

745 
(* proof reconstruction *) 
36898  746 

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

747 
(** tracing and checking **) 
36898  748 

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

749 
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

750 
"Z3: #" ^ string_of_int idx ^ ": " ^ Old_Z3_Proof_Parser.string_of_rule r) 
36898  751 

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

752 
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

753 
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

754 
else 
36898  755 
let val thm = thm_of p > tap (Thm.join_proofs o single) 
756 
in 

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

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

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

759 
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

760 
("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

761 
" (#" ^ string_of_int idx ^ ")") 
36898  762 
(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

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

764 
Syntax.pretty_term ctxt (Thm.term_of ct)]]))) 
36898  765 
end 
766 

767 

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

768 
(** overall reconstruction procedure **) 
36898  769 

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

770 
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

771 
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

772 
quote (Old_Z3_Proof_Parser.string_of_rule r)) 
36898  773 

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

774 
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

775 
(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

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

777 
(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

778 
 (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

779 
 (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

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

781 
(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

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

783 
(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

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

785 
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

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

787 
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

788 
 (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

789 
 (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

790 
 (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

791 
(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

792 
 (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

793 
 (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

794 
 (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

795 
 (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

796 
 (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

797 
 (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

798 
 (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

799 
 (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

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

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

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

803 
 (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

804 
 (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

805 
 (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

806 
 (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

807 
 (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

808 

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

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

810 
 (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

811 
 (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

812 
 (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

813 
 (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

814 
 (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

815 
 (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

816 
 (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

817 

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

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

819 
 (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

820 
(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

821 
 (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

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

823 
rewrite simpset (map fst ps) ct cx > rpair ptab 
36898  824 

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

825 
 (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

826 
 (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

827 
 (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

828 
 (Old_Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r 
36898  829 

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

830 
 _ => 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

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

832 
" has an unexpected number of arguments.")) 
36898  833 

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

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

835 
(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

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

837 
 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

838 

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

839 
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

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

841 
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

842 
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

843 
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

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

845 
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

846 
> 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

847 
> 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

848 
in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end 
36898  849 

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

850 
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

851 
@{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

852 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

853 
fun discharge_assms_tac ctxt rules = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

854 
REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt))) 
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

855 

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

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

857 
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

858 
else 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

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

860 
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

861 
 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

862 

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

863 
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

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

866 
> 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

867 
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

868 

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

869 
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

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

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

872 
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

873 
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

874 

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

876 
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

877 

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

878 
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

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

881 
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

882 
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

883 
(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

884 
> 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

885 
> 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

886 
> pair [] 
36898  887 
end 
888 

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

889 
end 
36898  890 

891 
end 