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

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

4 
Normalization steps on theorems required by SMT solvers. 
36898  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_SMT_NORMALIZE = 
36898  8 
sig 
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
51717
diff
changeset

9 
val drop_fact_warning: Proof.context > thm > unit 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

10 
val atomize_conv: Proof.context > conv 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

11 
type extra_norm = Proof.context > thm list * thm list > thm list * thm list 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

12 
val add_extra_norm: Old_SMT_Utils.class * extra_norm > Context.generic > 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

13 
Context.generic 
41300
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

14 
val normalize: (int * (int option * thm)) list > Proof.context > 
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

15 
(int * thm) list * Proof.context 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

16 
val setup: theory > theory 
36898  17 
end 
18 

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

19 
structure Old_SMT_Normalize: OLD_SMT_NORMALIZE = 
36898  20 
struct 
21 

54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
51717
diff
changeset

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

23 
Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o 
61268  24 
Thm.string_of_thm ctxt) 
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
51717
diff
changeset

25 

36898  26 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

27 
(* general theorem normalizations *) 
36898  28 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

29 
(** instantiate elimination rules **) 
40685
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

30 

dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

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

32 
val (cpfalse, cfalse) = 
59634  33 
`Old_SMT_Utils.mk_cprop (Thm.cterm_of @{context} @{const False}) 
40685
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

34 

dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

35 
fun inst f ct thm = 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

36 
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of 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:
60352
diff
changeset

37 
in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end 
40685
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

38 
in 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

39 

dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

40 
fun instantiate_elim thm = 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

41 
(case Thm.concl_of thm of 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

42 
@{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

43 
 Var _ => inst I cpfalse thm 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

44 
 _ => thm) 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

45 

dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

46 
end 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

47 

dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

48 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

49 
(** normalize definitions **) 
36898  50 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

51 
fun norm_def thm = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

52 
(case Thm.prop_of thm of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

53 
@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

54 
norm_def (thm RS @{thm fun_cong}) 
56245  55 
 Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

56 
norm_def (thm RS @{thm meta_eq_to_obj_eq}) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

57 
 _ => thm) 
36898  58 

59 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

60 
(** atomization **) 
36898  61 

62 
fun atomize_conv ctxt ct = 

63 
(case Thm.term_of ct of 

56245  64 
@{const Pure.imp} $ _ $ _ => 
36898  65 
Conv.binop_conv (atomize_conv ctxt) then_conv 
66 
Conv.rewr_conv @{thm atomize_imp} 

56245  67 
 Const (@{const_name Pure.eq}, _) $ _ $ _ => 
36898  68 
Conv.binop_conv (atomize_conv ctxt) then_conv 
69 
Conv.rewr_conv @{thm atomize_eq} 

56245  70 
 Const (@{const_name Pure.all}, _) $ Abs _ => 
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset

71 
Conv.binder_conv (atomize_conv o snd) ctxt then_conv 
36898  72 
Conv.rewr_conv @{thm atomize_all} 
73 
 _ => Conv.all_conv) ct 

74 

41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

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

76 
fold Old_SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, 
56245  77 
@{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}] 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

78 

36898  79 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

80 
(** unfold special quantifiers **) 
36898  81 

82 
local 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

83 
val ex1_def = mk_meta_eq @{lemma 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

84 
"Ex1 = (%P. EX x. P x & (ALL y. P y > y = x))" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

85 
by (rule ext) (simp only: Ex1_def)} 
36898  86 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

87 
val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A > P x)" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

88 
by (rule ext)+ (rule Ball_def)} 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

89 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

90 
val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

91 
by (rule ext)+ (rule Bex_def)} 
36898  92 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

93 
val special_quants = [(@{const_name Ex1}, ex1_def), 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

94 
(@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

95 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

96 
fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

97 
 special_quant _ = NONE 
36898  98 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

99 
fun special_quant_conv _ ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

100 
(case special_quant (Thm.term_of ct) of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

101 
SOME thm => Conv.rewr_conv thm 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

102 
 NONE => Conv.all_conv) ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

103 
in 
36898  104 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

106 
Old_SMT_Utils.if_exists_conv (is_some o special_quant) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

107 
(Conv.top_conv special_quant_conv ctxt) 
36898  108 

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

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

110 
fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

111 

36898  112 
end 
113 

114 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

115 
(** trigger inference **) 
36898  116 

117 
local 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

118 
(*** check trigger syntax ***) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

119 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

120 
fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

121 
 dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

122 
 dest_trigger _ = NONE 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

123 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

124 
fun eq_list [] = false 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

125 
 eq_list (b :: bs) = forall (equal b) bs 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

126 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

127 
fun proper_trigger t = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

128 
t 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

129 
> these o try HOLogic.dest_list 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

130 
> map (map_filter dest_trigger o these o try HOLogic.dest_list) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

131 
> (fn [] => false  bss => forall eq_list bss) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

132 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

133 
fun proper_quant inside f t = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

134 
(case t of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

135 
Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

136 
 Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

137 
 @{const trigger} $ p $ u => 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

138 
(if inside then f p else false) andalso proper_quant false f u 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

139 
 Abs (_, _, u) => proper_quant false f u 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

140 
 u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

141 
 _ => true) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

142 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

143 
fun check_trigger_error ctxt t = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

144 
error ("SMT triggers must only occur under quantifier and multipatterns " ^ 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

145 
"must have the same kind: " ^ Syntax.string_of_term ctxt t) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

146 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

148 
if proper_quant false proper_trigger (Old_SMT_Utils.term_of ct) then 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41327
diff
changeset

149 
Conv.all_conv ct 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

150 
else check_trigger_error ctxt (Thm.term_of ct) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

151 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

152 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

153 
(*** infer simple triggers ***) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

154 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

155 
fun dest_cond_eq ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

156 
(case Thm.term_of ct of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

157 
Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

158 
 @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

159 
 _ => raise CTERM ("no equation", [ct])) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

160 

58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58058
diff
changeset

161 
fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

162 
 get_constrs _ _ = [] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

163 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

164 
fun is_constr thy (n, T) = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

165 
let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

166 
in can (the o find_first match o get_constrs thy o Term.body_type) T end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

167 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

168 
fun is_constr_pat thy t = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

169 
(case Term.strip_comb t of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

170 
(Free _, []) => true 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

171 
 (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

172 
 _ => false) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

173 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

174 
fun is_simp_lhs ctxt t = 
36898  175 
(case Term.strip_comb t of 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

176 
(Const c, ts as _ :: _) => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

177 
not (Old_SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso 
42361  178 
forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

179 
 _ => false) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

180 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

181 
fun has_all_vars vs t = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

182 
subset (op aconv) (vs, map Free (Term.add_frees t [])) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

183 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

184 
fun minimal_pats vs ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

185 
if has_all_vars vs (Thm.term_of ct) then 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

186 
(case Thm.term_of ct of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

187 
_ $ _ => 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58112
diff
changeset

188 
(case apply2 (minimal_pats vs) (Thm.dest_comb ct) of 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

189 
([], []) => [[ct]] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

190 
 (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') 
41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset

191 
 _ => []) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

192 
else [] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

193 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

194 
fun proper_mpat _ _ _ [] = false 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

195 
 proper_mpat thy gen u cts = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

196 
let 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

197 
val tps = (op ~~) (`gen (map Thm.term_of cts)) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

198 
fun some_match u = tps > exists (fn (t', t) => 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

199 
Pattern.matches thy (t', u) andalso not (t aconv u)) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

200 
in not (Term.exists_subterm some_match u) end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

201 

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

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

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

204 
fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct 
36898  205 

59634  206 
fun mk_clist T = apply2 (Thm.cterm_of @{context}) (HOLogic.cons_const T, HOLogic.nil_const T) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

207 
fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil 
58057  208 
val mk_pat_list = mk_list (mk_clist @{typ pattern}) 
209 
val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"}) 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

210 
fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

211 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

212 
val trigger_eq = 
58057  213 
mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)} 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

214 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

215 
fun insert_trigger_conv [] ct = Conv.all_conv ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

216 
 insert_trigger_conv ctss ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

217 
let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) > rpair ct 
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:
60352
diff
changeset

218 
in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

219 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

220 
fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

221 
let 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

222 
val (lhs, rhs) = dest_cond_eq ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

223 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

224 
val vs = map Thm.term_of cvs 
42361  225 
val thy = Proof_Context.theory_of ctxt 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

226 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

227 
fun get_mpats ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

228 
if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

229 
else [] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

230 
val gen = Variable.export_terms ctxt outer_ctxt 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

231 
val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs)) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

232 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

233 
in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

234 

58057  235 
fun has_trigger (@{const trigger} $ _ $ _) = true 
41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset

236 
 has_trigger _ = false 
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset

237 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

239 
if Old_SMT_Utils.under_quant has_trigger (Old_SMT_Utils.term_of ct) then 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41327
diff
changeset

240 
Conv.all_conv ct 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

241 
else Conv.try_conv cv ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

242 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

244 
if Config.get ctxt Old_SMT_Config.infer_triggers then 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41327
diff
changeset

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

246 
(Old_SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

247 
else Conv.all_conv 
36898  248 
in 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

249 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

251 
Old_SMT_Utils.prop_conv 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41327
diff
changeset

252 
(check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) 
36898  253 

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

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

255 
fold Old_SMT_Builtin.add_builtin_fun_ext'' 
58057  256 
[@{const_name pat}, @{const_name nopat}, @{const_name trigger}] 
36898  257 

258 
end 

259 

260 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

261 
(** adding quantifier weights **) 
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

262 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

263 
local 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

264 
(*** check weight syntax ***) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

265 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

266 
val has_no_weight = 
58057  267 
not o Term.exists_subterm (fn @{const weight} => true  _ => false) 
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

268 

58057  269 
fun is_weight (@{const weight} $ w $ t) = 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

270 
(case try HOLogic.dest_number w of 
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset

271 
SOME (_, i) => i >= 0 andalso has_no_weight t 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

272 
 _ => false) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

273 
 is_weight t = has_no_weight t 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

274 

58057  275 
fun proper_trigger (@{const trigger} $ _ $ t) = is_weight t 
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset

276 
 proper_trigger t = is_weight t 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

277 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

278 
fun check_weight_error ctxt t = 
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset

279 
error ("SMT weight must be a nonnegative number and must only occur " ^ 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

280 
"under the topmost quantifier and an optional trigger: " ^ 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

281 
Syntax.string_of_term ctxt t) 
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

282 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

284 
if Old_SMT_Utils.under_quant proper_trigger (Old_SMT_Utils.term_of ct) then 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41327
diff
changeset

285 
Conv.all_conv ct 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

286 
else check_weight_error ctxt (Thm.term_of ct) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

287 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

288 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

289 
(*** insertion of weights ***) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

290 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

291 
fun under_trigger_conv cv ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

292 
(case Thm.term_of ct of 
58057  293 
@{const trigger} $ _ $ _ => Conv.arg_conv cv 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

294 
 _ => cv) ct 
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

295 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

296 
val weight_eq = 
58057  297 
mk_meta_eq @{lemma "p = weight i p" by (simp add: weight_def)} 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

298 
fun mk_weight_eq w = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

299 
let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

300 
in 
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:
60352
diff
changeset

301 
Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)]) 
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:
60352
diff
changeset

302 
weight_eq 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

303 
end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

304 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

305 
fun add_weight_conv NONE _ = Conv.all_conv 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

306 
 add_weight_conv (SOME weight) ctxt = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

307 
let val cv = Conv.rewr_conv (mk_weight_eq weight) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

308 
in Old_SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end 
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

309 
in 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

310 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

311 
fun weight_conv weight ctxt = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

312 
Old_SMT_Utils.prop_conv 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41327
diff
changeset

313 
(check_weight_conv ctxt then_conv add_weight_conv weight ctxt) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

314 

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

315 
val setup_weight = Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name weight} 
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

316 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

317 
end 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

318 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset

319 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

320 
(** combined general normalizations **) 
36898  321 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

322 
fun gen_normalize1_conv ctxt weight = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

323 
atomize_conv ctxt then_conv 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

324 
unfold_special_quants_conv ctxt then_conv 
41327
49feace87649
added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
boehmes
parents:
41300
diff
changeset

325 
Thm.beta_conversion true then_conv 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

326 
trigger_conv ctxt then_conv 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

327 
weight_conv weight ctxt 
36898  328 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

329 
fun gen_normalize1 ctxt weight thm = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

330 
thm 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

331 
> instantiate_elim 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

332 
> norm_def 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

333 
> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

334 
> Drule.forall_intr_vars 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

335 
> Conv.fconv_rule (gen_normalize1_conv ctxt weight) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

336 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

337 
fun gen_norm1_safe ctxt (i, (weight, thm)) = 
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
51717
diff
changeset

338 
(case try (gen_normalize1 ctxt weight) thm of 
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
51717
diff
changeset

339 
SOME thm' => SOME (i, thm') 
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
51717
diff
changeset

340 
 NONE => (drop_fact_warning ctxt thm; NONE)) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

341 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

342 
fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms 
36898  343 

41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

344 

d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

345 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

346 
(* unfolding of definitions and theoryspecific rewritings *) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

347 

50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

348 
fun expand_head_conv cv ct = 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

349 
(case Thm.term_of ct of 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

350 
_ $ _ => 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

351 
Conv.fun_conv (expand_head_conv cv) then_conv 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

352 
Conv.try_conv (Thm.beta_conversion false) 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

353 
 _ => cv) ct 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

354 

74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

355 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

356 
(** rewrite bool case expressions as if expressions **) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

357 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

358 
local 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54883
diff
changeset

359 
fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true 
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54883
diff
changeset

360 
 is_case_bool _ = false 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

361 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

362 
val thm = mk_meta_eq @{lemma 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54883
diff
changeset

363 
"case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp} 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

364 

50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

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

366 
Old_SMT_Utils.if_true_conv (is_case_bool o Term.head_of) 
50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

367 
(expand_head_conv (Conv.rewr_conv thm)) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

368 
in 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

369 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54883
diff
changeset

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

371 
Old_SMT_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

372 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54883
diff
changeset

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

374 
Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"} 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

375 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

376 
end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

377 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

378 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

379 
(** unfold abs, min and max **) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

380 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

381 
local 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

382 
val abs_def = mk_meta_eq @{lemma 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

383 
"abs = (%a::'a::abs_if. if a < 0 then  a else a)" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

384 
by (rule ext) (rule abs_if)} 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

385 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

386 
val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

387 
by (rule ext)+ (rule min_def)} 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

388 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

389 
val max_def = mk_meta_eq @{lemma "max = (%a b. if a <= b then b else a)" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

390 
by (rule ext)+ (rule max_def)} 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

391 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

392 
val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def), 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

393 
(@{const_name abs}, abs_def)] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

394 

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

395 
fun is_builtinT ctxt T = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

396 
Old_SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

397 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

398 
fun abs_min_max ctxt (Const (n, T)) = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

399 
(case AList.lookup (op =) defs n of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

400 
NONE => NONE 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

401 
 SOME thm => if is_builtinT ctxt T then SOME thm else NONE) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

402 
 abs_min_max _ _ = NONE 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

403 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

404 
fun unfold_amm_conv ctxt ct = 
50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

405 
(case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

406 
SOME thm => expand_head_conv (Conv.rewr_conv thm) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

407 
 NONE => Conv.all_conv) ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

408 
in 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

409 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

411 
Old_SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

412 
(Conv.top_conv unfold_amm_conv ctxt) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

413 

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

414 
val setup_abs_min_max = fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) defs 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

415 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

416 
end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

417 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

418 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

419 
(** embedding of standard natural number operations into integer operations **) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

420 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

421 
local 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

422 
val nat_embedding = @{lemma 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

423 
"ALL n. nat (int n) = n" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

424 
"ALL i. i >= 0 > int (nat i) = i" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

425 
"ALL i. i < 0 > int (nat i) = 0" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

426 
by simp_all} 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

427 

41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

428 
val simple_nat_ops = [ 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

429 
@{const less (nat)}, @{const less_eq (nat)}, 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

430 
@{const Suc}, @{const plus (nat)}, @{const minus (nat)}] 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

431 

a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

432 
val mult_nat_ops = 
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
62348
diff
changeset

433 
[@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}] 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

434 

a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

435 
val nat_ops = simple_nat_ops @ mult_nat_ops 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

436 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset

437 
val nat_consts = nat_ops @ [@{const numeral (nat)}, 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

438 
@{const zero_class.zero (nat)}, @{const one_class.one (nat)}] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

439 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

440 
val nat_int_coercions = [@{const of_nat (int)}, @{const nat}] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

441 

41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

442 
val builtin_nat_ops = nat_int_coercions @ simple_nat_ops 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

443 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

444 
val is_nat_const = member (op aconv) nat_consts 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

445 

41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

446 
fun is_nat_const' @{const of_nat (int)} = true 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

447 
 is_nat_const' t = is_nat_const t 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

448 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

449 
val expands = map mk_meta_eq @{lemma 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

450 
"0 = nat 0" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

451 
"1 = nat 1" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset

452 
"(numeral :: num => nat) = (%i. nat (numeral i))" 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

453 
"op < = (%a b. int a < int b)" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

454 
"op <= = (%a b. int a <= int b)" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

455 
"Suc = (%a. nat (int a + 1))" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

456 
"op + = (%a b. nat (int a + int b))" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

457 
"op  = (%a b. nat (int a  int b))" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

458 
"op * = (%a b. nat (int a * int b))" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

459 
"op div = (%a b. nat (int a div int b))" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

460 
"op mod = (%a b. nat (int a mod int b))" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44718
diff
changeset

461 
by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+} 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

462 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

463 
val ints = map mk_meta_eq @{lemma 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

464 
"int 0 = 0" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

465 
"int 1 = 1" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

466 
"int (Suc n) = int n + 1" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

467 
"int (n + m) = int n + int m" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

468 
"int (n  m) = int (nat (int n  int m))" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

469 
"int (n * m) = int n * int m" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

470 
"int (n div m) = int n div int m" 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

471 
"int (n mod m) = int n mod int m" 
62348  472 
by (auto simp add: of_nat_mult zdiv_int zmod_int)} 
50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

473 

74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

474 
val int_if = mk_meta_eq @{lemma 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

475 
"int (if P then n else m) = (if P then int n else int m)" 
50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

476 
by simp} 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

477 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

478 
fun mk_number_eq ctxt i lhs = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

480 
val eq = Old_SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51575
diff
changeset

481 
val tac = 
62348  482 
Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm of_nat_numeral}]) 1 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54489
diff
changeset

483 
in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

484 

50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

485 
fun ite_conv cv1 cv2 = 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

486 
Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

487 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

488 
fun int_conv ctxt ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

489 
(case Thm.term_of ct of 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset

490 
@{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) => 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

491 
Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

492 
 @{const of_nat (int)} $ _ => 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

493 
(Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv 
50601
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

494 
(Conv.rewr_conv int_if then_conv 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

495 
ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv 
74da81de127f
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)
boehmes
parents:
47207
diff
changeset

496 
Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

497 
 _ => Conv.no_conv) ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

498 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

499 
and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

500 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

502 
Old_SMT_Utils.if_conv (is_nat_const o Term.head_of) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

503 
(expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

504 
(int_conv ctxt) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

505 

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

506 
and nat_conv ctxt = Old_SMT_Utils.if_exists_conv is_nat_const' 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

507 
(Conv.top_sweep_conv expand_conv ctxt) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

508 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

509 
val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

510 
in 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

511 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

512 
val nat_as_int_conv = nat_conv 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

513 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

514 
fun add_nat_embedding thms = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

515 
if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

516 
else (thms, []) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

517 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

519 
Old_SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

520 
fold (Old_SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

521 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

522 
end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

523 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

524 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

525 
(** normalize numerals **) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

526 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

527 
local 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

528 
(* 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

529 
rewrite Numeral1 into 1 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

530 
rewrite  0 into 0 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

531 
*) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

532 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

533 
fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

534 
true 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

535 
 is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

536 
true 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

537 
 is_irregular_number _ = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

538 
false; 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

539 

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

540 
fun is_strange_number ctxt t = is_irregular_number t andalso Old_SMT_Builtin.is_builtin_num ctxt t; 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

541 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

542 
val proper_num_ss = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51575
diff
changeset

543 
simpset_of (put_simpset HOL_ss @{context} 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

544 
addsimps @{thms Num.numeral_One minus_zero}) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

545 

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

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

547 
Old_SMT_Utils.if_conv (is_strange_number ctxt) 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54293
diff
changeset

548 
(Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

549 
in 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

550 

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

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

552 
Old_SMT_Utils.if_exists_conv (is_strange_number ctxt) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41327
diff
changeset

553 
(Conv.top_sweep_conv norm_num_conv ctxt) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

554 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

555 
end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

556 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

557 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

558 
(** combined unfoldings and rewritings **) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

559 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

560 
fun unfold_conv ctxt = 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54883
diff
changeset

561 
rewrite_case_bool_conv ctxt then_conv 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

562 
unfold_abs_min_max_conv ctxt then_conv 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

563 
nat_as_int_conv ctxt then_conv 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

564 
Thm.beta_conversion true 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

565 

41300
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

566 
fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) 
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

567 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

568 
fun burrow_ids f ithms = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

569 
let 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

570 
val (is, thms) = split_list ithms 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

571 
val (thms', extra_thms) = f thms 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

572 
in (is ~~ thms') @ map (pair ~1) extra_thms end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

573 

51575  574 
fun unfold2 ctxt ithms = 
41300
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

575 
ithms 
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

576 
> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) 
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

577 
> burrow_ids add_nat_embedding 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

578 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

579 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

580 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

581 
(* overall normalization *) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

582 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

583 
type extra_norm = Proof.context > thm list * thm list > thm list * thm list 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

584 

e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

585 
structure Extra_Norms = Generic_Data 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

587 
type T = extra_norm Old_SMT_Utils.dict 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

588 
val empty = [] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

590 
fun merge data = Old_SMT_Utils.dict_merge fst data 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

591 
) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

592 

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

593 
fun add_extra_norm (cs, norm) = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

594 
Extra_Norms.map (Old_SMT_Utils.dict_update (cs, norm)) 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

595 

51575  596 
fun apply_extra_norms ctxt ithms = 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

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

598 
val cs = Old_SMT_Config.solver_class_of ctxt 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

599 
val es = Old_SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs 
51575  600 
in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

601 

43116  602 
local 
603 
val ignored = member (op =) [@{const_name All}, @{const_name Ex}, 

604 
@{const_name Let}, @{const_name If}, @{const_name HOL.eq}] 

605 

606 
val schematic_consts_of = 

607 
let 

58057  608 
fun collect (@{const trigger} $ p $ t) = 
43116  609 
collect_trigger p #> collect t 
610 
 collect (t $ u) = collect t #> collect u 

611 
 collect (Abs (_, _, t)) = collect t 

612 
 collect (t as Const (n, _)) = 

613 
if not (ignored n) then Monomorph.add_schematic_consts_of t else I 

614 
 collect _ = I 

615 
and collect_trigger t = 

616 
let val dest = these o try HOLogic.dest_list 

617 
in fold (fold collect_pat o dest) (dest t) end 

58057  618 
and collect_pat (Const (@{const_name pat}, _) $ t) = collect t 
619 
 collect_pat (Const (@{const_name nopat}, _) $ t) = collect t 

43116  620 
 collect_pat _ = I 
621 
in (fn t => collect t Symtab.empty) end 

622 
in 

623 

51575  624 
fun monomorph ctxt xthms = 
43116  625 
let val (xs, thms) = split_list xthms 
626 
in 

51575  627 
map (pair 1) thms 
628 
> Monomorph.monomorph schematic_consts_of ctxt 

629 
> maps (uncurry (map o pair)) o map2 pair xs o map (map snd) 

43116  630 
end 
631 

632 
end 

633 

41300
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

634 
fun normalize iwthms ctxt = 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

635 
iwthms 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

636 
> gen_normalize ctxt 
41300
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

637 
> unfold1 ctxt 
51575  638 
> monomorph ctxt 
639 
> unfold2 ctxt 

640 
> apply_extra_norms ctxt 

41300
528f5d00b542
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required
boehmes
parents:
41280
diff
changeset

641 
> rpair ctxt 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

642 

41072
9f9bc1bdacef
be more flexible: store SMT builtin symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset

643 
val setup = Context.theory_map ( 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

644 
setup_atomize #> 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

645 
setup_unfolded_quants #> 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

646 
setup_trigger #> 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

647 
setup_weight #> 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54883
diff
changeset

648 
setup_case_bool #> 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

649 
setup_abs_min_max #> 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

650 
setup_nat_as_int) 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

651 

36898  652 
end 