author  boehmes 
Mon, 20 Dec 2010 21:04:45 +0100  
changeset 41327  49feace87649 
parent 41300  528f5d00b542 
child 41328  6792a5c92a58 
permissions  rwrr 
36898  1 
(* Title: HOL/Tools/SMT/smt_normalize.ML 
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 

7 
signature SMT_NORMALIZE = 

8 
sig 

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

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

10 
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

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

12 
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

13 
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

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

15 
val setup: theory > theory 
36898  16 
end 
17 

18 
structure SMT_Normalize: SMT_NORMALIZE = 

19 
struct 

20 

40663  21 
structure U = SMT_Utils 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

22 
structure B = SMT_Builtin 
40663  23 

36898  24 

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

25 
(* general theorem normalizations *) 
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 
(** 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

28 

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

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

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

31 

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

32 
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

33 
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) 
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset

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

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

36 

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

37 
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

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

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

40 
 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

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

42 

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

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

44 

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

45 

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

46 
(** normalize definitions **) 
36898  47 

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

48 
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

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

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

51 
norm_def (thm RS @{thm fun_cong}) 
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 
 Const (@{const_name "=="}, _) $ _ $ 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

53 
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

54 
 _ => thm) 
36898  55 

56 

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

57 
(** atomization **) 
36898  58 

59 
fun atomize_conv ctxt ct = 

60 
(case Thm.term_of ct of 

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

61 
@{const "==>"} $ _ $ _ => 
36898  62 
Conv.binop_conv (atomize_conv ctxt) then_conv 
63 
Conv.rewr_conv @{thm atomize_imp} 

64 
 Const (@{const_name "=="}, _) $ _ $ _ => 

65 
Conv.binop_conv (atomize_conv ctxt) then_conv 

66 
Conv.rewr_conv @{thm atomize_eq} 

67 
 Const (@{const_name all}, _) $ Abs _ => 

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

68 
Conv.binder_conv (atomize_conv o snd) ctxt then_conv 
36898  69 
Conv.rewr_conv @{thm atomize_all} 
70 
 _ => Conv.all_conv) ct 

71 

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

72 
val setup_atomize = 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

73 
fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="}, 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

74 
@{const_name all}, @{const_name Trueprop}] 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40686
diff
changeset

75 

36898  76 

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

77 
(** unfold special quantifiers **) 
36898  78 

79 
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

80 
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

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

82 
by (rule ext) (simp only: Ex1_def)} 
36898  83 

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

84 
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

85 
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

86 

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

88 
by (rule ext)+ (rule Bex_def)} 
36898  89 

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

90 
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

91 
(@{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

92 

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

94 
 special_quant _ = NONE 
36898  95 

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

96 
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

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

98 
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

99 
 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

100 
in 
36898  101 

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

102 
fun unfold_special_quants_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

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

104 
(Conv.top_conv special_quant_conv ctxt) 
36898  105 

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

106 
val setup_unfolded_quants = fold (B.add_builtin_fun_ext'' o fst) special_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

107 

36898  108 
end 
109 

110 

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 
(** trigger inference **) 
36898  112 

113 
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

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

115 

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

116 
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

117 
 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

118 
 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

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

121 
 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

122 

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

124 
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

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

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

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

128 

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

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

131 
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

132 
 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

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

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

135 
 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

136 
 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

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

138 

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

140 
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

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

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_conv ctxt ct = 
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

144 
if proper_quant false proper_trigger (U.term_of ct) then 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

145 
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

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 

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

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

149 

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

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

152 
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

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

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

155 

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 
fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy 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

157 
 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

158 

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

160 
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

161 
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

162 

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

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

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

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

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

168 

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 
fun is_simp_lhs ctxt t = 
36898  170 
(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

171 
(Const c, ts as _ :: _) => 
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 
not (B.is_builtin_fun_ext ctxt c ts) andalso 
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 
forall (is_constr_pat (ProofContext.theory_of ctxt)) 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

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

175 

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

177 
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

178 

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

180 
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

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

182 
_ $ _ => 
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 
(case pairself (minimal_pats vs) (Thm.dest_comb 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

184 
([], []) => [[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 
 (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

186 
 _ => []) 
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

187 
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

188 

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

190 
 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

191 
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

192 
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

193 
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

194 
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

195 
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

196 

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 pat = U.mk_const_pat @{theory} @{const_name SMT.pat} U.destT1 
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 mk_pat ct = Thm.capply (U.instT' ct pat) ct 
36898  199 

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

200 
fun mk_clist T = pairself (Thm.cterm_of @{theory}) 
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 
(HOLogic.cons_const T, HOLogic.nil_const 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

202 
fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

203 
val mk_pat_list = mk_list (mk_clist @{typ SMT.pattern}) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

204 
val mk_mpat_list = mk_list (mk_clist @{typ "SMT.pattern 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

205 
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

206 

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

208 
mk_meta_eq @{lemma "p = SMT.trigger t p" by (simp add: trigger_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

209 

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

211 
 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

212 
let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) > rpair 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

213 
in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq 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

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

216 
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

217 
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

218 

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 
val vs = map Thm.term_of cvs 
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 
val thy = ProofContext.theory_of 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

221 

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

223 
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

224 
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

225 
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

226 
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

227 

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

229 

41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset

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

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

232 

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

233 
fun try_trigger_conv cv ct = 
41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset

234 
if U.under_quant has_trigger (U.term_of ct) then 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

235 
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

236 

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

237 
fun infer_trigger_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

238 
if Config.get ctxt SMT_Config.infer_triggers 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

239 
try_trigger_conv (U.under_quant_conv (infer_trigger_eq_conv ctxt) 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

240 
else Conv.all_conv 
36898  241 
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

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

244 
U.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) 
36898  245 

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

246 
val setup_trigger = fold B.add_builtin_fun_ext'' 
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 
[@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}] 
36898  248 

249 
end 

250 

251 

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

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

253 

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

254 
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

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

256 

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

257 
val has_no_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

258 
not o Term.exists_subterm (fn @{const SMT.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

259 

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

260 
fun is_weight (@{const SMT.weight} $ w $ 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

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

262 
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

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

264 
 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

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 
fun proper_trigger (@{const SMT.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

267 
 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

268 

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

269 
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

270 
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

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

272 
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

273 

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

274 
fun check_weight_conv ctxt ct = 
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

275 
if U.under_quant proper_trigger (U.term_of ct) then 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

276 
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

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 

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

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

280 

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

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

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

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

285 

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

287 
mk_meta_eq @{lemma "p = SMT.weight i p" by (simp add: weight_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

288 
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

289 
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

290 
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

291 
Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) 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

292 
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

293 

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

295 
 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

296 
let val cv = Conv.rewr_conv (mk_weight_eq 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

297 
in U.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

298 
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

299 

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

300 
fun weight_conv 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

301 
U.prop_conv (check_weight_conv ctxt then_conv add_weight_conv 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

302 

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 
val setup_weight = B.add_builtin_fun_ext'' @{const_name SMT.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

304 

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

305 
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

306 

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

307 

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

308 
(** combined general normalizations **) 
36898  309 

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

310 
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

311 
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

312 
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

313 
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

314 
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

315 
weight_conv weight ctxt 
36898  316 

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

317 
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

318 
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

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

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

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

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

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

324 

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

325 
fun drop_fact_warning 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

326 
let val pre = prefix "Warning: dropping assumption: " 
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 
in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) 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

328 

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_norm1_safe ctxt (i, (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 
if Config.get ctxt SMT_Config.drop_bad_facts 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

331 
(case try (gen_normalize1 ctxt weight) 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

332 
SOME thm' => SOME (i, 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

333 
 NONE => (drop_fact_warning ctxt thm; 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

334 
else SOME (i, 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

335 

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 
fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms 
36898  337 

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

338 

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

339 

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

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

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 
(** unfold trivial distincts **) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

343 

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

344 
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

345 
fun is_trivial_distinct (Const (@{const_name distinct}, _) $ 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

346 
(case try HOLogic.dest_list 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

347 
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

348 
 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

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

350 
 is_trivial_distinct _ = 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

351 

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

352 
val thms = 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

353 
"distinct [] = 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

354 
"distinct [x] = 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

355 
"distinct [x, y] = (x ~= y)" 
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 
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

357 
fun distinct_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

358 
U.if_true_conv is_trivial_distinct (Conv.rewrs_conv 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

359 
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

360 

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 
fun trivial_distinct_conv ctxt = U.if_exists_conv is_trivial_distinct 
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 
(Conv.top_conv distinct_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

363 

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

365 

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

366 

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

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

368 

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

370 
fun is_bool_case (Const (@{const_name "bool.bool_case"}, _)) = 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

371 
 is_bool_case _ = 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

372 

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

373 
val thm = 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

374 
"bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp} 
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 
fun unfold_conv _ = U.if_true_conv is_bool_case (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

377 
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

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 
fun rewrite_bool_case_conv ctxt = U.if_exists_conv is_bool_case 
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 
(Conv.top_conv unfold_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

381 

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 setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"} 
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 

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

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 

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

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

390 
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

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

392 
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

393 

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

395 
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

396 

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

398 
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

399 

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

401 
(@{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

402 

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 
fun is_builtinT ctxt T = B.is_builtin_typ_ext ctxt (Term.domain_type 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

404 

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

405 
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

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

407 
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

408 
 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

409 
 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

410 

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

411 
fun unfold_amm_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

412 
(case abs_min_max ctxt (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

413 
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

414 
 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

415 
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

416 

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

418 
U.if_exists_conv (is_some o abs_min_max 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

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

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 
val setup_abs_min_max = fold (B.add_builtin_fun_ext'' o fst) defs 
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 

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

424 

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 

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

427 

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

428 
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

429 
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

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

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

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

433 
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

434 

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

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

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

438 

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

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

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

441 

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

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 nat_consts = nat_ops @ [@{const number_of (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

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

446 

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

447 
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

448 

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

449 
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

450 

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

452 

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

453 
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

454 
 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

455 

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

456 
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

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

458 
"1 = nat 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

459 
"(number_of :: int => nat) = (%i. nat (number_of 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

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

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

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

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

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

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

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

467 
"op mod = (%a b. nat (int a mod 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

468 
by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib 
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 
nat_mod_distrib)} 
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 

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

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

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

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

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

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

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

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

479 
"int (n mod m) = int n mod 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

480 
"int (if P then n else m) = (if P then int n else 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

481 
by (auto simp add: int_mult zdiv_int zmod_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

482 

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

483 
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

484 
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

485 
val eq = U.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} 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

486 
val ss = HOL_ss 
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 
addsimps [@{thm Nat_Numeral.int_nat_number_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

488 
addsimps @{thms neg_simps} 
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 
fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 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

490 
in Goal.norm_result (Goal.prove_internal [] eq tac) 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

491 

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

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

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

495 
Conv.fun_conv (expand_head_conv cv) 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

496 
Thm.beta_conversion 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

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

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

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

501 
@{const of_nat (int)} $ (n as (@{const number_of (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

502 
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

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

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

505 
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

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

507 

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

509 

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

511 
U.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

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

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

514 

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

515 
and nat_conv ctxt = U.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

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

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

519 
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

520 

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

522 

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

524 
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

525 
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

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

528 
B.add_builtin_typ_ext (@{typ nat}, K true) #> 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41224
diff
changeset

529 
fold (B.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

530 

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

532 

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

533 

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

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

535 

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

536 
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

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

538 
rewrite negative numerals into positive 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

539 
rewrite Numeral0 into 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

540 
rewrite Numeral1 into 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

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

542 

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

543 
fun is_strange_number ctxt (t as Const (@{const_name number_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

544 
(case try HOLogic.dest_number 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

545 
SOME (_, i) => B.is_builtin_num ctxt t andalso i < 2 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

546 
 NONE => 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

547 
 is_strange_number _ _ = 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

548 

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 
val pos_num_ss = HOL_ss 
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 
addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}] 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset

551 
addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_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

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

553 
addsimps @{thms Int.normalize_bin_simps} 
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 
addsimps @{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

555 
"Int.Min =  Int.Bit1 Int.Pls" 
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 
"Int.Bit0 ( Int.Pls) =  Int.Pls" 
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 
"Int.Bit0 ( k) =  Int.Bit0 k" 
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 
"Int.Bit1 ( k) =  Int.Bit1 (Int.pred k)" 
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 
by simp_all (simp add: pred_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

560 

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

561 
fun norm_num_conv ctxt = U.if_conv (is_strange_number 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

562 
(Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_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 
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

564 

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 
fun normalize_numerals_conv ctxt = U.if_exists_conv (is_strange_number 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

566 
(Conv.top_sweep_conv norm_num_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

567 

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

569 

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 

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

572 

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

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

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

576 
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

577 
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

578 
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

579 

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

580 
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

581 

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

582 
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

583 
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

584 
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

585 
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

586 
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

587 

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

588 
fun unfold2 ithms 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

589 
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

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

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

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

593 

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

594 

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 

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

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

597 

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

598 
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

599 

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

600 
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

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

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

603 
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

604 
val extend = I 
41224  605 
fun merge data = U.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

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

607 

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

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

609 

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

610 
fun apply_extra_norms ithms 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

611 
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

612 
val cs = SMT_Config.solver_class_of 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

613 
val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs 
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

614 
in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) 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

615 

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

616 
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

617 
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

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

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

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

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

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

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

624 

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

625 
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

626 
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

627 
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

628 
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

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

630 
setup_bool_case #> 
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

631 
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

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

633 

36898  634 
end 