author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 62913  13252110a6fe 
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_tools.ML 
36898  2 
Author: Sascha Boehme, TU Muenchen 
3 

4 
Helper functions required for Z3 proof reconstruction. 

5 
*) 

6 

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

7 
signature OLD_Z3_PROOF_TOOLS = 
36898  8 
sig 
41172
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41123
diff
changeset

9 
(*modifying terms*) 
36898  10 
val as_meta_eq: cterm > cterm 
11 

41123  12 
(*theorem nets*) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
38864
diff
changeset

13 
val thm_net_of: ('a > thm) > 'a list > 'a Net.net 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset

14 
val net_instances: (int * thm) Net.net > cterm > (int * thm) list 
36898  15 
val net_instance: thm Net.net > cterm > thm option 
16 

41123  17 
(*proof combinators*) 
36898  18 
val under_assumption: (thm > thm) > cterm > thm 
19 
val with_conv: conv > (cterm > thm) > cterm > thm 

20 
val discharge: thm > thm > thm 

21 
val varify: string list > thm > thm 

22 
val unfold_eqs: Proof.context > thm list > conv 

23 
val match_instantiate: (cterm > cterm) > cterm > thm > thm 

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

24 
val by_tac: Proof.context > (int > tactic) > cterm > thm 
36898  25 
val make_hyp_def: thm > Proof.context > thm * Proof.context 
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:
42322
diff
changeset

26 
val by_abstraction: int > bool * bool > Proof.context > thm list > 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

27 
(Proof.context > cterm > thm) > cterm > thm 
36898  28 

41123  29 
(*a faster COMP*) 
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:
59634
diff
changeset

30 
type compose_data = cterm list * (cterm > cterm list) * thm 
36898  31 
val precompose: (cterm > cterm list) > thm > compose_data 
32 
val precompose2: (cterm > cterm * cterm) > thm > compose_data 

33 
val compose: compose_data > thm > thm 

34 

41123  35 
(*unfolding of 'distinct'*) 
36898  36 
val unfold_distinct_conv: conv 
37 

41123  38 
(*simpset*) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

39 
val add_simproc: Simplifier.simproc > Context.generic > Context.generic 
36898  40 
val make_simpset: Proof.context > thm list > simpset 
41 
end 

42 

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

43 
structure Old_Z3_Proof_Tools: OLD_Z3_PROOF_TOOLS = 
36898  44 
struct 
45 

46 

47 

41172
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41123
diff
changeset

48 
(* modifying terms *) 
36898  49 

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

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

51 
uncurry Old_SMT_Utils.mk_cequals (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct)) 
36898  52 

53 

54 

55 
(* theorem nets *) 

56 

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

57 
fun thm_net_of f xthms = 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
38864
diff
changeset

58 
let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
38864
diff
changeset

59 
in fold insert xthms Net.empty end 
36898  60 

61 
fun maybe_instantiate ct thm = 

62 
try Thm.first_order_match (Thm.cprop_of thm, ct) 

63 
> Option.map (fn inst => Thm.instantiate inst thm) 

64 

42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

65 
local 
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

66 
fun instances_from_net match f net ct = 
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

67 
let 
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

68 
val lookup = if match then Net.match_term else Net.unify_term 
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

69 
val xthms = lookup net (Thm.term_of ct) 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset

70 
fun select ct = map_filter (f (maybe_instantiate ct)) xthms 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset

71 
fun select' ct = 
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

72 
let val thm = Thm.trivial ct 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset

73 
in map_filter (f (try (fn rule => rule COMP thm))) xthms end 
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset

74 
in (case select ct of [] => select' ct  xthms' => xthms') end 
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

75 
in 
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

76 

45410  77 
fun net_instances net = 
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset

78 
instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm)) 
45410  79 
net 
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

80 

45410  81 
fun net_instance net = try hd o instances_from_net true I net 
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

82 

be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambdalifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset

83 
end 
36898  84 

85 

86 

87 
(* proof combinators *) 

88 

89 
fun under_assumption f ct = 

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

90 
let val ct' = Old_SMT_Utils.mk_cprop ct 
36898  91 
in Thm.implies_intr ct' (f (Thm.assume ct')) end 
92 

93 
fun with_conv conv prove ct = 

94 
let val eq = Thm.symmetric (conv ct) 

95 
in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end 

96 

97 
fun discharge p pq = Thm.implies_elim pq p 

98 

99 
fun varify vars = Drule.generalize ([], vars) 

100 

101 
fun unfold_eqs _ [] = Conv.all_conv 

102 
 unfold_eqs ctxt eqs = 

36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset

103 
Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt 
36898  104 

105 
fun match_instantiate f ct thm = 

106 
Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm 

107 

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

108 
fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1))) 
36898  109 

41123  110 
(* 
111 
 c x == t x ==> P (c x) 

112 
 

113 
c == t  P (c x) 

114 
*) 

36898  115 
fun make_hyp_def thm ctxt = 
116 
let 

117 
val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1) 

118 
val (cf, cvs) = Drule.strip_comb lhs 

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

119 
val eq = Old_SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs) 
36898  120 
fun apply cv th = 
121 
Thm.combination th (Thm.reflexive cv) 

122 
> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false)) 

123 
in 

124 
yield_singleton Assumption.add_assumes eq ctxt 

125 
>> Thm.implies_elim thm o fold apply cvs 

126 
end 

127 

128 

129 

130 
(* abstraction *) 

131 

132 
local 

133 

134 
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false) 

135 

136 
fun context_of (ctxt, _, _, _) = ctxt 

137 

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

138 
fun replace (_, (cv, ct)) = Thm.forall_elim ct o Thm.forall_intr cv 
36898  139 

140 
fun abs_instantiate (_, tab, _, beta_norm) = 

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

141 
fold replace (Termtab.dest tab) #> 
36898  142 
beta_norm ? Conv.fconv_rule (Thm.beta_conversion true) 
143 

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

144 
fun lambda_abstract cvs t = 
36898  145 
let 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

146 
val frees = map Free (Term.add_frees t []) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

147 
val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

148 
val vs = map (Term.dest_Free o Thm.term_of) cvs' 
44241  149 
in (fold_rev absfree vs t, cvs') end 
36898  150 

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:
42322
diff
changeset

151 
fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) = 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

152 
let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct) 
36898  153 
in 
154 
(case Termtab.lookup tab t of 

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

155 
SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx) 
36898  156 
 NONE => 
157 
let 

158 
val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59590
diff
changeset

159 
val cv = Thm.cterm_of ctxt' 
59586  160 
(Free (n, map Thm.typ_of_cterm cvs' > Thm.typ_of_cterm ct)) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

161 
val cu = Drule.list_comb (cv, cvs') 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45410
diff
changeset

162 
val e = (t, (cv, fold_rev Thm.lambda cvs' ct)) 
36898  163 
val beta_norm' = beta_norm orelse not (null cvs') 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

164 
in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end) 
36898  165 
end 
166 

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:
42322
diff
changeset

167 
fun abs_comb f g dcvs ct = 
36898  168 
let val (cf, cu) = Thm.dest_comb ct 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45410
diff
changeset

169 
in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end 
36898  170 

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

171 
fun abs_arg f = abs_comb (K pair) f 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

172 

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:
42322
diff
changeset

173 
fun abs_args f dcvs ct = 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

174 
(case Thm.term_of ct of 
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:
42322
diff
changeset

175 
_ $ _ => abs_comb (abs_args f) f dcvs ct 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

176 
 _ => pair ct) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

177 

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:
42322
diff
changeset

178 
fun abs_list f g dcvs ct = 
36898  179 
(case Thm.term_of ct of 
180 
Const (@{const_name Nil}, _) => pair ct 

181 
 Const (@{const_name Cons}, _) $ _ $ _ => 

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:
42322
diff
changeset

182 
abs_comb (abs_arg f) (abs_list f g) dcvs ct 
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:
42322
diff
changeset

183 
 _ => g dcvs ct) 
36898  184 

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:
42322
diff
changeset

185 
fun abs_abs f (depth, cvs) ct = 
36898  186 
let val (cv, cu) = Thm.dest_abs NONE ct 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45410
diff
changeset

187 
in f (depth, cv :: cvs) cu #>> Thm.lambda cv end 
36898  188 

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

189 
val is_atomic = 
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41328
diff
changeset

190 
(fn Free _ => true  Var _ => true  Bound _ => true  _ => false) 
36898  191 

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:
42322
diff
changeset

192 
fun abstract depth (ext_logic, with_theories) = 
36898  193 
let 
194 
fun abstr1 cvs ct = abs_arg abstr cvs ct 

195 
and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct 

196 
and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct 

197 
and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct 

198 

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:
42322
diff
changeset

199 
and abstr (dcvs as (d, cvs)) ct = 
36898  200 
(case Thm.term_of ct of 
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:
42322
diff
changeset

201 
@{const Trueprop} $ _ => abstr1 dcvs ct 
56245  202 
 @{const Pure.imp} $ _ $ _ => abstr2 dcvs 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:
40274
diff
changeset

203 
 @{const True} => pair ct 
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:
40274
diff
changeset

204 
 @{const False} => pair ct 
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:
42322
diff
changeset

205 
 @{const Not} $ _ => abstr1 dcvs ct 
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:
42322
diff
changeset

206 
 @{const HOL.conj} $ _ $ _ => abstr2 dcvs ct 
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:
42322
diff
changeset

207 
 @{const HOL.disj} $ _ $ _ => abstr2 dcvs ct 
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:
42322
diff
changeset

208 
 @{const HOL.implies} $ _ $ _ => abstr2 dcvs ct 
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:
42322
diff
changeset

209 
 Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 dcvs ct 
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40663
diff
changeset

210 
 Const (@{const_name distinct}, _) $ _ => 
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:
42322
diff
changeset

211 
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) dcvs ct 
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:
42322
diff
changeset

212 
else fresh_abstraction dcvs ct 
36898  213 
 Const (@{const_name If}, _) $ _ $ _ $ _ => 
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:
42322
diff
changeset

214 
if ext_logic then abstr3 dcvs ct else fresh_abstraction dcvs ct 
36898  215 
 Const (@{const_name All}, _) $ _ => 
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:
42322
diff
changeset

216 
if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct 
36898  217 
 Const (@{const_name Ex}, _) $ _ => 
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:
42322
diff
changeset

218 
if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

219 
 t => (fn cx => 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

220 
if is_atomic t orelse can HOLogic.dest_number t then (ct, cx) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

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

222 
Old_Z3_Interface.is_builtin_theory_term (context_of cx) t 
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:
42322
diff
changeset

223 
then abs_args abstr dcvs ct cx 
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:
42322
diff
changeset

224 
else if d = 0 then fresh_abstraction dcvs ct cx 
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:
42322
diff
changeset

225 
else 
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:
42322
diff
changeset

226 
(case Term.strip_comb t of 
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:
42322
diff
changeset

227 
(Const _, _) => abs_args abstr (d1, cvs) ct cx 
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:
42322
diff
changeset

228 
 (Free _, _) => abs_args abstr (d1, cvs) ct cx 
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:
42322
diff
changeset

229 
 _ => fresh_abstraction dcvs ct cx))) 
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:
42322
diff
changeset

230 
in abstr (depth, []) end 
36898  231 

59634  232 
val cimp = Thm.cterm_of @{context} @{const Pure.imp} 
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:
40274
diff
changeset

233 

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:
42322
diff
changeset

234 
fun deepen depth f x = 
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:
42322
diff
changeset

235 
if depth = 0 then f depth x 
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:
42322
diff
changeset

236 
else (case try (f depth) x of SOME y => y  NONE => deepen (depth  1) f x) 
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:
42322
diff
changeset

237 

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:
42322
diff
changeset

238 
fun with_prems depth thms f 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:
40274
diff
changeset

239 
fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct 
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:
42322
diff
changeset

240 
> deepen depth f 
36898  241 
> fold (fn prem => fn th => Thm.implies_elim th prem) thms 
242 

243 
in 

244 

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:
42322
diff
changeset

245 
fun by_abstraction depth mode ctxt thms prove = 
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:
42322
diff
changeset

246 
with_prems depth thms (fn d => fn ct => 
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:
42322
diff
changeset

247 
let val (cu, cx) = abstract d mode ct (abs_context 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:
42322
diff
changeset

248 
in abs_instantiate cx (prove (context_of cx) cu) end) 
36898  249 

250 
end 

251 

252 

253 

254 
(* a faster COMP *) 

255 

256 
type compose_data = cterm list * (cterm > cterm list) * thm 

257 

258 
fun list2 (x, y) = [x, y] 

259 

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:
59634
diff
changeset

260 
fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule) 
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:
59634
diff
changeset

261 
fun precompose2 f rule : compose_data = precompose (list2 o f) rule 
36898  262 

263 
fun compose (cvs, f, rule) thm = 

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:
59634
diff
changeset

264 
discharge thm (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule) 
36898  265 

266 

267 

268 
(* unfolding of 'distinct' *) 

269 

270 
local 

271 
val set1 = @{lemma "x ~: set [] == ~False" by simp} 

272 
val set2 = @{lemma "x ~: set [x] == False" by simp} 

273 
val set3 = @{lemma "x ~: set [y] == x ~= y" by simp} 

274 
val set4 = @{lemma "x ~: set (x # ys) == False" by simp} 

275 
val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp} 

276 

277 
fun set_conv ct = 

36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset

278 
(Conv.rewrs_conv [set1, set2, set3, set4] else_conv 
36898  279 
(Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct 
280 

40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40663
diff
changeset

281 
val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)} 
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40663
diff
changeset

282 
val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)} 
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40663
diff
changeset

283 
val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs" 
40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40164
diff
changeset

284 
by (simp add: distinct_def)} 
36898  285 

286 
fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 

287 
in 

288 
fun unfold_distinct_conv ct = 

36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset

289 
(Conv.rewrs_conv [dist1, dist2] else_conv 
36898  290 
(Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct 
291 
end 

292 

293 

294 

295 
(* simpset *) 

296 

297 
local 

298 
val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv} 

299 
val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2} 

300 
val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1} 

301 
val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3} 

302 

303 
fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm 

304 
fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) 

305 
 dest_binop t = raise TERM ("dest_binop", [t]) 

306 

61144  307 
fun prove_antisym_le ctxt ct = 
36898  308 
let 
61144  309 
val (le, r, s) = dest_binop (Thm.term_of ct) 
36898  310 
val less = Const (@{const_name less}, Term.fastype_of le) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

311 
val prems = Simplifier.prems_of ctxt 
36898  312 
in 
313 
(case find_first (eq_prop (le $ s $ r)) prems of 

314 
NONE => 

315 
find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems 

316 
> Option.map (fn thm => thm RS antisym_less1) 

317 
 SOME thm => SOME (thm RS antisym_le1)) 

318 
end 

319 
handle THM _ => NONE 

320 

61144  321 
fun prove_antisym_less ctxt ct = 
36898  322 
let 
61144  323 
val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct)) 
36898  324 
val le = Const (@{const_name less_eq}, Term.fastype_of less) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

325 
val prems = Simplifier.prems_of ctxt 
36898  326 
in 
327 
(case find_first (eq_prop (le $ r $ s)) prems of 

328 
NONE => 

329 
find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems 

330 
> Option.map (fn thm => thm RS antisym_less2) 

331 
 SOME thm => SOME (thm RS antisym_le2)) 

332 
end 

333 
handle THM _ => NONE 

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

334 

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

335 
val basic_simpset = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

336 
simpset_of (put_simpset HOL_ss @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

337 
addsimps @{thms field_simps} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

338 
addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}] 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

339 
addsimps @{thms arith_special} addsimps @{thms arith_simps} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

340 
addsimps @{thms rel_simps} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

341 
addsimps @{thms array_rules} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

342 
addsimps @{thms term_true_def} addsimps @{thms term_false_def} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

343 
addsimps @{thms z3div_def} addsimps @{thms z3mod_def} 
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60642
diff
changeset

344 
addsimprocs [@{simproc numeral_divmod}] 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

345 
addsimprocs [ 
61144  346 
Simplifier.make_simproc @{context} "fast_int_arith" 
347 
{lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}], 

62913  348 
proc = K Lin_Arith.simproc}, 
61144  349 
Simplifier.make_simproc @{context} "antisym_le" 
350 
{lhss = [@{term "(x::'a::order) \<le> y"}], 

62913  351 
proc = K prove_antisym_le}, 
61144  352 
Simplifier.make_simproc @{context} "antisym_less" 
353 
{lhss = [@{term "\<not> (x::'a::linorder) < y"}], 

62913  354 
proc = K prove_antisym_less}]) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

355 

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

356 
structure Simpset = Generic_Data 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

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

358 
type T = simpset 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

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

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

361 
val merge = Simplifier.merge_ss 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

362 
) 
36898  363 
in 
364 

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

365 
fun add_simproc simproc context = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

366 
Simpset.map (simpset_map (Context.proof_of context) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

367 
(fn ctxt => ctxt addsimprocs [simproc])) context 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

368 

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

369 
fun make_simpset ctxt rules = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset

370 
simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules) 
36898  371 

372 
end 

373 

374 
end 