author  webertj 
Sat, 29 Jul 2006 13:15:12 +0200  
changeset 20254  58b71535ed00 
parent 20217  25b068a99d2b 
child 20268  1fe9aed8fcac 
permissions  rwrr 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/arith_data.ML 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, Stefan Berghofer and Tobias Nipkow 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

4 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

5 
Various arithmetic proof procedures. 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

6 
*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

7 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

8 
(**) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

9 
(* 1. Cancellation of common terms *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

10 
(**) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

11 

13517  12 
structure NatArithUtils = 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

13 
struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

14 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

15 
(** abstract syntax of structure nat: 0, Suc, + **) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

16 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

17 
(* mk_sum, mk_norm_sum *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

18 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

19 
val one = HOLogic.mk_nat 1; 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19043
diff
changeset

20 
val mk_plus = HOLogic.mk_binop "HOL.plus"; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

21 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

22 
fun mk_sum [] = HOLogic.zero 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

23 
 mk_sum [t] = t 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

24 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

25 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

26 
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

27 
fun mk_norm_sum ts = 
15570  28 
let val (ones, sums) = List.partition (equal one) ts in 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

29 
funpow (length ones) HOLogic.mk_Suc (mk_sum sums) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

30 
end; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

31 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

32 
(* dest_sum *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

33 

19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19043
diff
changeset

34 
val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

35 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

36 
fun dest_sum tm = 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

37 
if HOLogic.is_zero tm then [] 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

38 
else 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

39 
(case try HOLogic.dest_Suc tm of 
15531  40 
SOME t => one :: dest_sum t 
41 
 NONE => 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

42 
(case try dest_plus tm of 
15531  43 
SOME (t, u) => dest_sum t @ dest_sum u 
44 
 NONE => [tm])); 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

45 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

46 
(** generic proof tools **) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

47 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

48 
(* prove conversions *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

49 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19823
diff
changeset

50 
fun prove_conv expand_tac norm_tac ss tu = (* FIXME avoid standard *) 
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19823
diff
changeset

51 
mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] [] 
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19823
diff
changeset

52 
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) 
17989  53 
(K (EVERY [expand_tac, norm_tac ss])))); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

54 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

55 
val subst_equals = prove_goal HOL.thy "[ t = s; u = t ] ==> u = s" 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

56 
(fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

57 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

58 
(* rewriting *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

59 

18328  60 
fun simp_all_tac rules = 
61 
let val ss0 = HOL_ss addsimps rules 

62 
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

63 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

64 
val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

65 
val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

66 

13517  67 
fun prep_simproc (name, pats, proc) = 
16834  68 
Simplifier.simproc (the_context ()) name pats proc; 
13517  69 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

70 
end; (* NatArithUtils *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

71 

13517  72 

73 
signature ARITH_DATA = 

74 
sig 

75 
val nat_cancel_sums_add: simproc list 

76 
val nat_cancel_sums: simproc list 

77 
end; 

78 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

79 

13517  80 
structure ArithData: ARITH_DATA = 
81 
struct 

82 

83 
open NatArithUtils; 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

84 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

85 
(** cancel common summands **) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

86 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

87 
structure Sum = 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

88 
struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

89 
val mk_sum = mk_norm_sum; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

90 
val dest_sum = dest_sum; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

91 
val prove_conv = prove_conv; 
18328  92 
val norm_tac1 = simp_all_tac add_rules; 
93 
val norm_tac2 = simp_all_tac add_ac; 

94 
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss; 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

95 
end; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

96 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

97 
fun gen_uncancel_tac rule ct = 
15531  98 
rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

99 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

100 
(* nat eq *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

101 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

102 
structure EqCancelSums = CancelSumsFun 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

103 
(struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

104 
open Sum; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

105 
val mk_bal = HOLogic.mk_eq; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

106 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; 
14331  107 
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

108 
end); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

109 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

110 
(* nat less *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

111 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

112 
structure LessCancelSums = CancelSumsFun 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

113 
(struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

114 
open Sum; 
19277  115 
val mk_bal = HOLogic.mk_binrel "Orderings.less"; 
116 
val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT; 

14331  117 
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

118 
end); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

119 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

120 
(* nat le *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

121 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

122 
structure LeCancelSums = CancelSumsFun 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

123 
(struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

124 
open Sum; 
19277  125 
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"; 
126 
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT; 

14331  127 
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

128 
end); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

129 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

130 
(* nat diff *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

131 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

132 
structure DiffCancelSums = CancelSumsFun 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

133 
(struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

134 
open Sum; 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19043
diff
changeset

135 
val mk_bal = HOLogic.mk_binop "HOL.minus"; 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19043
diff
changeset

136 
val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

137 
val uncancel_tac = gen_uncancel_tac diff_cancel; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

138 
end); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

139 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

140 
(** prepare nat_cancel simprocs **) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

141 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

142 
val nat_cancel_sums_add = map prep_simproc 
13462  143 
[("nateq_cancel_sums", 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19823
diff
changeset

144 
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], K EqCancelSums.proc), 
13462  145 
("natless_cancel_sums", 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19823
diff
changeset

146 
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], K LessCancelSums.proc), 
13462  147 
("natle_cancel_sums", 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19823
diff
changeset

148 
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], K LeCancelSums.proc)]; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

149 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

150 
val nat_cancel_sums = nat_cancel_sums_add @ 
13462  151 
[prep_simproc ("natdiff_cancel_sums", 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19823
diff
changeset

152 
["((l::nat) + m)  n", "(l::nat)  (m + n)", "Suc m  n", "m  Suc n"], K DiffCancelSums.proc)]; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

153 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

154 
end; (* ArithData *) 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

155 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

156 
open ArithData; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

157 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

158 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

159 
(**) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

160 
(* 2. Linear arithmetic *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

161 
(**) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

162 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

163 
(* Parameters data for general linear arithmetic functor *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

164 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

165 
structure LA_Logic: LIN_ARITH_LOGIC = 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

166 
struct 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

167 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

168 
val ccontr = ccontr; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

169 
val conjI = conjI; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

170 
val notI = notI; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

171 
val sym = sym; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

172 
val not_lessD = linorder_not_less RS iffD1; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

173 
val not_leD = linorder_not_le RS iffD1; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

174 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

175 
fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

176 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

177 
val mk_Trueprop = HOLogic.mk_Trueprop; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

178 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset

179 
fun atomize thm = case #prop(rep_thm thm) of 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset

180 
Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) => 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset

181 
atomize(thm RS conjunct1) @ atomize(thm RS conjunct2) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset

182 
 _ => [thm]; 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset

183 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

184 
fun neg_prop(TP$(Const("Not",_)$t)) = TP$t 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

185 
 neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT>HOLogic.boolT)$t); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

186 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

187 
fun is_False thm = 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

188 
let val _ $ t = #prop(rep_thm thm) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

189 
in t = Const("False",HOLogic.boolT) end; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

190 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

191 
fun is_nat(t) = fastype_of1 t = HOLogic.natT; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

192 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

193 
fun mk_nat_thm sg t = 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

194 
let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

195 
in instantiate ([],[(cn,ct)]) le0 end; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

196 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

197 
end; (* LA_Logic *) 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

198 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

199 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

200 
(* arith theory data *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

201 

16424  202 
structure ArithTheoryData = TheoryDataFun 
203 
(struct 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

204 
val name = "HOL/arith"; 
15185  205 
type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string list, presburger: (int > tactic) option}; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

206 

15531  207 
val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE}; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

208 
val copy = I; 
16424  209 
val extend = I; 
210 
fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1}, 

13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

211 
{splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) = 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

212 
{splits = Drule.merge_rules (splits1, splits2), 
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

213 
inj_consts = merge_lists inj_consts1 inj_consts2, 
15185  214 
discrete = merge_lists discrete1 discrete2, 
15531  215 
presburger = (case presburger1 of NONE => presburger2  p => p)}; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

216 
fun print _ _ = (); 
16424  217 
end); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

218 

18728  219 
val arith_split_add = Thm.declaration_attribute (fn thm => 
220 
Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => 

221 
{splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}))); 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

222 

13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

223 
fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => 
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

224 
{splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger}); 
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

225 

13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

226 
fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => 
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

227 
{splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger}); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

228 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

229 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

230 
signature HOL_LIN_ARITH_DATA = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

231 
sig 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

232 
include LIN_ARITH_DATA 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

233 
val fast_arith_split_limit : int ref 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

234 
end; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

235 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

236 
structure LA_Data_Ref: HOL_LIN_ARITH_DATA = 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

237 
struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

238 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

239 
(* internal representation of linear (in)equations *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

240 
type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool); 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

241 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

242 
(* Decomposition of terms *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

243 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

244 
(* typ > bool *) 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

245 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

246 
fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

247 
 nT _ = false; 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

248 

58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

249 
fun add_atom (t, m, (p, i)) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

250 
case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

251 
 SOME n => (AList.update (op =) (t, Rat.add (n, m)) p, i); 
10693  252 

253 
exception Zero; 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

254 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

255 
fun rat_of_term (numt, dent) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

256 
let 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

257 
val num = HOLogic.dest_binum numt 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

258 
val den = HOLogic.dest_binum dent 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

259 
in 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

260 
if den = 0 then raise Zero else Rat.rat_of_quotient (num, den) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

261 
end; 
10718  262 

263 
(* Warning: in rare cases number_of encloses a nonnumeral, 

264 
in which case dest_binum raises TERM; hence all the handles below. 

11334
a16eaf2a1edd
Allow Sucnumerals as coefficients in linarith formulae
nipkow
parents:
10906
diff
changeset

265 
Same for Sucterms that turn out not to be numerals  
a16eaf2a1edd
Allow Sucnumerals as coefficients in linarith formulae
nipkow
parents:
10906
diff
changeset

266 
although the simplifier should eliminate those anyway... 
10718  267 
*) 
268 

11334
a16eaf2a1edd
Allow Sucnumerals as coefficients in linarith formulae
nipkow
parents:
10906
diff
changeset

269 
fun number_of_Sucs (Const("Suc",_) $ n) = number_of_Sucs n + 1 
a16eaf2a1edd
Allow Sucnumerals as coefficients in linarith formulae
nipkow
parents:
10906
diff
changeset

270 
 number_of_Sucs t = if HOLogic.is_zero t then 0 
a16eaf2a1edd
Allow Sucnumerals as coefficients in linarith formulae
nipkow
parents:
10906
diff
changeset

271 
else raise TERM("number_of_Sucs",[]) 
a16eaf2a1edd
Allow Sucnumerals as coefficients in linarith formulae
nipkow
parents:
10906
diff
changeset

272 

10718  273 
(* decompose nested multiplications, bracketing them to the right and combining all 
274 
their coefficients 

275 
*) 

276 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

277 
(* (string * Term.typ) list > ... *) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

278 

13499  279 
fun demult inj_consts = 
280 
let 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

281 
fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = ( 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

282 
(case s of 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

283 
Const ("Numeral.number_of", _) $ n => 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

284 
demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

285 
 Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) => 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

286 
demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_binum n)))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

287 
 Const("Suc", _) $ _ => 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

288 
demult (t, Rat.mult (m, Rat.rat_of_int (number_of_Sucs s))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

289 
 Const ("HOL.times", _) $ s1 $ s2 => 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

290 
demult (mC $ s1 $ (mC $ s2 $ t), m) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

291 
 Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) => 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

292 
let 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

293 
val den = HOLogic.dest_binum dent 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

294 
in 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

295 
if den = 0 then raise Zero else demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den))) 
10718  296 
end 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

297 
 _ => 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

298 
atomult (mC, s, t, m) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

299 
) handle TERM _ => atomult (mC, s, t, m) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

300 
) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

301 
 demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) = ( 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

302 
let 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

303 
val den = HOLogic.dest_binum dent 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

304 
in 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

305 
if den = 0 then raise Zero else demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

306 
end 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

307 
handle TERM _ => (SOME atom, m) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

308 
) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

309 
 demult(Const("0",_),m) = (NONE, Rat.rat_of_int 0) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

310 
 demult(Const("1",_),m) = (NONE, m) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

311 
 demult(t as Const("Numeral.number_of",_)$n,m) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

312 
((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

313 
handle TERM _ => (SOME t,m)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

314 
 demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

315 
 demult(t as Const f $ x, m) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

316 
(if f mem inj_consts then SOME x else SOME t,m) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

317 
 demult(atom,m) = (SOME atom,m) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

318 
and 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

319 
atomult (mC, atom, t, m) = ( 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

320 
case demult (t, m) of (NONE, m') => (SOME atom, m') 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

321 
 (SOME t', m') => (SOME (mC $ atom $ t'), m') 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

322 
) 
13499  323 
in demult end; 
10718  324 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

325 
fun decomp2 inj_consts (rel, lhs, rhs) = 
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

326 
let 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

327 
(* Turn term into list of summand * multiplicity plus a constant *) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

328 
fun poly(Const("HOL.plus",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

329 
 poly(all as Const("HOL.minus",T) $ s $ t, m, pi) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

330 
if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

331 
 poly(all as Const("HOL.uminus",T) $ t, m, pi) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

332 
if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

333 
 poly(Const("0",_), _, pi) = pi 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

334 
 poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

335 
 poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

336 
 poly(t as Const("HOL.times",_) $ _ $ _, m, pi as (p,i)) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

337 
(case demult inj_consts (t,m) of 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

338 
(NONE,m') => (p,Rat.add(i,m)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

339 
 (SOME u,m') => add_atom(u,m',pi)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

340 
 poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

341 
(case demult inj_consts (t,m) of 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

342 
(NONE,m') => (p,Rat.add(i,m')) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

343 
 (SOME u,m') => add_atom(u,m',pi)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

344 
 poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

345 
((p,Rat.add(i,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum t)))) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

346 
handle TERM _ => add_atom all) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

347 
 poly(all as Const f $ x, m, pi) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

348 
if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

349 
 poly x = add_atom x 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

350 
val (p, i) = poly (lhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

351 
val (q, j) = poly (rhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0)) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

352 
in 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

353 
case rel of 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

354 
"Orderings.less" => SOME (p, i, "<", q, j) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

355 
 "Orderings.less_eq" => SOME (p, i, "<=", q, j) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

356 
 "op =" => SOME (p, i, "=", q, j) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

357 
 _ => NONE 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

358 
end handle Zero => NONE; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

359 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

360 
fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

361 
 negate NONE = NONE; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

362 

15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

363 
fun of_lin_arith_sort sg U = 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

364 
Type.of_sort (Sign.tsig_of sg) (U, ["Ring_and_Field.ordered_idom"]) 
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

365 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

366 
fun allows_lin_arith sg discrete (U as Type (D, [])) = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

367 
if of_lin_arith_sort sg U then 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

368 
(true, D mem discrete) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

369 
else (* special cases *) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

370 
if D mem discrete then (true, true) else (false, false) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

371 
 allows_lin_arith sg discrete U = 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

372 
(of_lin_arith_sort sg U, false); 
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

373 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

374 
fun decomp1 (sg, discrete, inj_consts) (T, xxx) = 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

375 
(case T of 
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

376 
Type("fun",[U,_]) => 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

377 
(case allows_lin_arith sg discrete U of 
15531  378 
(true,d) => (case decomp2 inj_consts xxx of NONE => NONE 
379 
 SOME(p,i,rel,q,j) => SOME(p,i,rel,q,j,d)) 

380 
 (false,_) => NONE) 

381 
 _ => NONE); 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

382 

10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

383 
fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs)) 
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

384 
 decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = 
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

385 
negate(decomp1 data (T,(rel,lhs,rhs))) 
15531  386 
 decomp2 data _ = NONE 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

387 

10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

388 
fun decomp sg = 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

389 
let 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

390 
val {discrete, inj_consts, ...} = ArithTheoryData.get sg 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

391 
in 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

392 
decomp2 (sg,discrete,inj_consts) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

393 
end; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

394 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

395 
fun number_of (n, T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n); 
10693  396 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

397 
(**) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

398 
(* code that performs certain goal transformations for linear arithmetic *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

399 
(**) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

400 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

401 
(* A "do nothing" variant of pre_decomp and pre_tac: 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

402 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

403 
fun pre_decomp sg Ts termitems = [termitems]; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

404 
fun pre_tac i = all_tac; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

405 
*) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

406 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

407 
(**) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

408 
(* the following code performs splitting of certain constants (e.g. min, *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

409 
(* max) in a linear arithmetic problem; similar to what split_tac later does *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

410 
(* to the proof state *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

411 
(**) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

412 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

413 
val fast_arith_split_limit = ref 9; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

414 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

415 
(* checks whether splitting with 'thm' is implemented *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

416 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

417 
(* Thm.thm > bool *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

418 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

419 
fun is_split_thm thm = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

420 
case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

421 
(case head_of lhs of 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

422 
Const (a, _) => a mem_string ["Orderings.max", "Orderings.min", "HOL.abs", "HOL.minus", "IntDef.nat", "Divides.op mod", "Divides.op div"] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

423 
 _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false)) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

424 
 _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false); 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

425 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

426 
(* substitute new for occurrences of old in a term, incrementing bound *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

427 
(* variables as needed when substituting inside an abstraction *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

428 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

429 
(* (term * term) list > term > term *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

430 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

431 
fun subst_term [] t = t 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

432 
 subst_term pairs t = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

433 
(case AList.lookup (op aconv) pairs t of 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

434 
SOME new => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

435 
new 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

436 
 NONE => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

437 
(case t of Abs (a, T, body) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

438 
let val pairs' = map (pairself (incr_boundvars 1)) pairs 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

439 
in Abs (a, T, subst_term pairs' body) end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

440 
 t1 $ t2 => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

441 
subst_term pairs t1 $ subst_term pairs t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

442 
 _ => t)); 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

443 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

444 
(* approximates the effect of one application of split_tac (followed by NNF *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

445 
(* normalization) on the subgoal represented by '(Ts, terms)'; returns a *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

446 
(* list of new subgoals (each again represented by a typ list for bound *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

447 
(* variables and a term list for premises), or NONE if split_tac would fail *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

448 
(* on the subgoal *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

449 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

450 
(* theory > typ list * term list > (typ list * term list) list option *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

451 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

452 
(* FIXME: currently only the effect of certain split theorems is reproduced *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

453 
(* (which is why we need 'is_split_thm'). A more canonical *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

454 
(* implementation should analyze the righthand side of the split *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

455 
(* theorem that can be applied, and modify the subgoal accordingly. *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

456 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

457 
fun split_once_items sg (Ts, terms) = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

458 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

459 
(* takes a list [t1, ..., tn] to the term *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

460 
(* tn' > ... > t1' > False , *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

461 
(* where ti' = HOLogic.dest_Trueprop ti *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

462 
(* term list > term *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

463 
fun REPEAT_DETERM_etac_rev_mp terms' = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

464 
fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

465 
val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg)) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

466 
val cmap = Splitter.cmap_of_split_thms split_thms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

467 
val splits = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

468 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

469 
if length splits > !fast_arith_split_limit then ( 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

470 
tracing ("fast_arith_split_limit exceeded (current value is " ^ string_of_int (!fast_arith_split_limit) ^ ")"); 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

471 
NONE 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

472 
) else ( 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

473 
case splits of [] => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

474 
NONE (* split_tac would fail: no possible split *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

475 
 ((_, _, _, split_type, split_term) :: _) => ( (* ignore all but the first possible split *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

476 
case strip_comb split_term of 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

477 
(* ?P (max ?i ?j) = ((?i <= ?j > ?P ?j) & (~ ?i <= ?j > ?P ?i)) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

478 
(Const ("Orderings.max", _), [t1, t2]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

479 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

480 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

481 
val terms1 = map (subst_term [(split_term, t1)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

482 
val terms2 = map (subst_term [(split_term, t2)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

483 
val t1_leq_t2 = Const ("Orderings.less_eq", split_type > split_type > HOLogic.boolT) $ t1 $ t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

484 
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

485 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

486 
val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

487 
val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

488 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

489 
SOME [(Ts, subgoal1), (Ts, subgoal2)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

490 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

491 
(* ?P (min ?i ?j) = ((?i <= ?j > ?P ?i) & (~ ?i <= ?j > ?P ?j)) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

492 
 (Const ("Orderings.min", _), [t1, t2]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

493 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

494 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

495 
val terms1 = map (subst_term [(split_term, t1)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

496 
val terms2 = map (subst_term [(split_term, t2)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

497 
val t1_leq_t2 = Const ("Orderings.less_eq", split_type > split_type > HOLogic.boolT) $ t1 $ t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

498 
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

499 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

500 
val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

501 
val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

502 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

503 
SOME [(Ts, subgoal1), (Ts, subgoal2)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

504 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

505 
(* ?P (abs ?a) = ((0 <= ?a > ?P ?a) & (?a < 0 > ?P ( ?a))) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

506 
 (Const ("HOL.abs", _), [t1]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

507 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

508 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

509 
val terms1 = map (subst_term [(split_term, t1)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

510 
val terms2 = map (subst_term [(split_term, Const ("HOL.uminus", split_type > split_type) $ t1)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

511 
val zero = Const ("0", split_type) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

512 
val zero_leq_t1 = Const ("Orderings.less_eq", split_type > split_type > HOLogic.boolT) $ zero $ t1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

513 
val t1_lt_zero = Const ("Orderings.less", split_type > split_type > HOLogic.boolT) $ t1 $ zero 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

514 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

515 
val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

516 
val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

517 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

518 
SOME [(Ts, subgoal1), (Ts, subgoal2)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

519 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

520 
(* ?P (?a  ?b) = ((?a < ?b > ?P 0) & (ALL d. ?a = ?b + d > ?P d)) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

521 
 (Const ("HOL.minus", _), [t1, t2]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

522 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

523 
(* "d" in the above theorem becomes a new bound variable after NNF *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

524 
(* transformation, therefore some adjustment of indices is necessary *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

525 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

526 
val zero = Const ("0", split_type) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

527 
val d = Bound 0 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

528 
val terms1 = map (subst_term [(split_term, zero)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

529 
val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

530 
val t1' = incr_boundvars 1 t1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

531 
val t2' = incr_boundvars 1 t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

532 
val t1_lt_t2 = Const ("Orderings.less", split_type > split_type > HOLogic.boolT) $ t1 $ t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

533 
val t1_eq_t2_plus_d = Const ("op =", split_type > split_type > HOLogic.boolT) $ t1' $ (Const ("HOL.plus", split_type > split_type > split_type) $ t2' $ d) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

534 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

535 
val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

536 
val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

537 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

538 
SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

539 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

540 
(* ?P (nat ?i) = ((ALL n. ?i = int n > ?P n) & (?i < 0 > ?P 0)) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

541 
 (Const ("IntDef.nat", _), [t1]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

542 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

543 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

544 
val zero_int = Const ("0", HOLogic.intT) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

545 
val zero_nat = Const ("0", HOLogic.natT) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

546 
val n = Bound 0 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

547 
val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

548 
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

549 
val t1' = incr_boundvars 1 t1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

550 
val t1_eq_int_n = Const ("op =", HOLogic.intT > HOLogic.intT > HOLogic.boolT) $ t1' $ (Const ("IntDef.int", HOLogic.natT > HOLogic.intT) $ n) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

551 
val t1_lt_zero = Const ("Orderings.less", HOLogic.intT > HOLogic.intT > HOLogic.boolT) $ t1 $ zero_int 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

552 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

553 
val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

554 
val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

555 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

556 
SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

557 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

558 
(* "?P ((?n::nat) mod (number_of ?k)) = ((number_of ?k = 0 > ?P ?n) & (~ (number_of ?k = 0) > (ALL i j. j < number_of ?k > ?n = number_of ?k * i + j > ?P j))) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

559 
 (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

560 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

561 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

562 
val zero = Const ("0", split_type) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

563 
val i = Bound 1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

564 
val j = Bound 0 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

565 
val terms1 = map (subst_term [(split_term, t1)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

566 
val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

567 
val t1' = incr_boundvars 2 t1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

568 
val t2' = incr_boundvars 2 t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

569 
val t2_eq_zero = Const ("op =", split_type > split_type > HOLogic.boolT) $ t2 $ zero 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

570 
val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type > split_type > HOLogic.boolT) $ t2' $ zero) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

571 
val j_lt_t2 = Const ("Orderings.less", split_type > split_type> HOLogic.boolT) $ j $ t2' 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

572 
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type > split_type > HOLogic.boolT) $ t1' $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

573 
(Const ("HOL.plus", split_type > split_type > split_type) $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

574 
(Const ("HOL.times", split_type > split_type > split_type) $ t2' $ i) $ j) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

575 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

576 
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

577 
val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

578 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

579 
SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

580 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

581 
(* "?P ((?n::nat) div (number_of ?k)) = ((number_of ?k = 0 > ?P 0) & (~ (number_of ?k = 0) > (ALL i j. j < number_of ?k > ?n = number_of ?k * i + j > ?P i))) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

582 
 (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

583 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

584 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

585 
val zero = Const ("0", split_type) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

586 
val i = Bound 1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

587 
val j = Bound 0 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

588 
val terms1 = map (subst_term [(split_term, zero)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

589 
val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

590 
val t1' = incr_boundvars 2 t1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

591 
val t2' = incr_boundvars 2 t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

592 
val t2_eq_zero = Const ("op =", split_type > split_type > HOLogic.boolT) $ t2 $ zero 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

593 
val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type > split_type > HOLogic.boolT) $ t2' $ zero) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

594 
val j_lt_t2 = Const ("Orderings.less", split_type > split_type> HOLogic.boolT) $ j $ t2' 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

595 
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type > split_type > HOLogic.boolT) $ t1' $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

596 
(Const ("HOL.plus", split_type > split_type > split_type) $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

597 
(Const ("HOL.times", split_type > split_type > split_type) $ t2' $ i) $ j) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

598 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

599 
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

600 
val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

601 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

602 
SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

603 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

604 
(* "?P ((?n::int) mod (number_of ?k)) = ((iszero (number_of ?k) > ?P ?n) & 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

605 
(neg (number_of (bin_minus ?k)) > (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j > ?P j)) & 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

606 
(neg (number_of ?k) > (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j > ?P j))) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

607 
 (Const ("Divides.op mod", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

608 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

609 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

610 
val zero = Const ("0", split_type) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

611 
val i = Bound 1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

612 
val j = Bound 0 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

613 
val terms1 = map (subst_term [(split_term, t1)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

614 
val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

615 
val t1' = incr_boundvars 2 t1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

616 
val (t2' as (_ $ k')) = incr_boundvars 2 t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

617 
val iszero_t2 = Const ("IntDef.iszero", split_type > HOLogic.boolT) $ t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

618 
val neg_minus_k = Const ("IntDef.neg", split_type > HOLogic.boolT) $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

619 
(number_of $ (Const ("Numeral.bin_minus", HOLogic.binT > HOLogic.binT) $ k')) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

620 
val zero_leq_j = Const ("Orderings.less_eq", split_type > split_type > HOLogic.boolT) $ zero $ j 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

621 
val j_lt_t2 = Const ("Orderings.less", split_type > split_type> HOLogic.boolT) $ j $ t2' 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

622 
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type > split_type > HOLogic.boolT) $ t1' $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

623 
(Const ("HOL.plus", split_type > split_type > split_type) $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

624 
(Const ("HOL.times", split_type > split_type > split_type) $ t2' $ i) $ j) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

625 
val neg_t2 = Const ("IntDef.neg", split_type > HOLogic.boolT) $ t2' 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

626 
val t2_lt_j = Const ("Orderings.less", split_type > split_type> HOLogic.boolT) $ t2' $ j 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

627 
val j_leq_zero = Const ("Orderings.less_eq", split_type > split_type > HOLogic.boolT) $ j $ zero 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

628 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

629 
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

630 
val subgoal2 = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

631 
@ hd terms2_3 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

632 
:: (if tl terms2_3 = [] then [not_false] else []) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

633 
@ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

634 
@ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

635 
val subgoal3 = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

636 
@ hd terms2_3 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

637 
:: (if tl terms2_3 = [] then [not_false] else []) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

638 
@ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

639 
@ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

640 
val Ts' = split_type :: split_type :: Ts 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

641 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

642 
SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

643 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

644 
(* "?P ((?n::int) div (number_of ?k)) = ((iszero (number_of ?k) > ?P 0) & 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

645 
(neg (number_of (bin_minus ?k)) > (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) > ?P i)) & 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

646 
(neg (number_of ?k) > (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) > ?P i))) *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

647 
 (Const ("Divides.op div", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

648 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

649 
val rev_terms = rev terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

650 
val zero = Const ("0", split_type) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

651 
val i = Bound 1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

652 
val j = Bound 0 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

653 
val terms1 = map (subst_term [(split_term, zero)]) rev_terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

654 
val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

655 
val t1' = incr_boundvars 2 t1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

656 
val (t2' as (_ $ k')) = incr_boundvars 2 t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

657 
val iszero_t2 = Const ("IntDef.iszero", split_type > HOLogic.boolT) $ t2 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

658 
val neg_minus_k = Const ("IntDef.neg", split_type > HOLogic.boolT) $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

659 
(number_of $ (Const ("Numeral.bin_minus", HOLogic.binT > HOLogic.binT) $ k')) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

660 
val zero_leq_j = Const ("Orderings.less_eq", split_type > split_type > HOLogic.boolT) $ zero $ j 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

661 
val j_lt_t2 = Const ("Orderings.less", split_type > split_type> HOLogic.boolT) $ j $ t2' 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

662 
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type > split_type > HOLogic.boolT) $ t1' $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

663 
(Const ("HOL.plus", split_type > split_type > split_type) $ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

664 
(Const ("HOL.times", split_type > split_type > split_type) $ t2' $ i) $ j) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

665 
val neg_t2 = Const ("IntDef.neg", split_type > HOLogic.boolT) $ t2' 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

666 
val t2_lt_j = Const ("Orderings.less", split_type > split_type> HOLogic.boolT) $ t2' $ j 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

667 
val j_leq_zero = Const ("Orderings.less_eq", split_type > split_type > HOLogic.boolT) $ j $ zero 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

668 
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

669 
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

670 
val subgoal2 = (HOLogic.mk_Trueprop neg_minus_k) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

671 
:: terms2_3 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

672 
@ not_false 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

673 
:: (map HOLogic.mk_Trueprop [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

674 
val subgoal3 = (HOLogic.mk_Trueprop neg_t2) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

675 
:: terms2_3 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

676 
@ not_false 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

677 
:: (map HOLogic.mk_Trueprop [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j]) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

678 
val Ts' = split_type :: split_type :: Ts 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

679 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

680 
SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

681 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

682 
(* this will only happen if a split theorem can be applied for which no code exists above  *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

683 
(* in which case either the split theorem should be implemented above, or 'is_split_thm' *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

684 
(* should be modified to filter it out *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

685 
 (t, ts) => ( 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

686 
warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ " (with " ^ Int.toString (length ts) ^ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

687 
" argument(s)) not implemented; proof reconstruction is likely to fail"); 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

688 
NONE 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

689 
)) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

690 
) 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

691 
end; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

692 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

693 
(* remove terms that do not satisfy p; change the order of the remaining *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

694 
(* terms in the same way as filter_prems_tac does *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

695 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

696 
(* (term > bool) > term list > term list *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

697 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

698 
fun filter_prems_tac_items p terms = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

699 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

700 
fun filter_prems (t, (left, right)) = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

701 
if p t then (left, right @ [t]) else (left @ right, []) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

702 
val (left, right) = foldl filter_prems ([], []) terms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

703 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

704 
right @ left 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

705 
end; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

706 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

707 
(* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

708 
(* subgoal that has 'terms' as premises *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

709 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

710 
(* term list > bool *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

711 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

712 
fun negated_term_occurs_positively terms = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

713 
List.exists (fn (TP $ (Const ("Not", _) $ t)) => member (op aconv) terms (TP $ t)  _ => false) terms; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

714 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

715 
(* theory > typ list * term list > (typ list * term list) list *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

716 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

717 
fun pre_decomp sg (Ts, terms) = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

718 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

719 
(* repeatedly split (including newly emerging subgoals) until no further *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

720 
(* splitting is possible *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

721 
(* (typ list * term list) list > (typ list * term list) list *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

722 
fun split_loop [] = [] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

723 
 split_loop (subgoal::subgoals) = ( 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

724 
case split_once_items sg subgoal of 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

725 
SOME new_subgoals => split_loop (new_subgoals @ subgoals) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

726 
 NONE => subgoal :: split_loop subgoals 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

727 
) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

728 
fun is_relevant t = isSome (decomp sg t) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

729 
val relevant_terms = filter_prems_tac_items is_relevant terms (* filter_prems_tac is_relevant *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

730 
val split_goals = split_loop [(Ts, relevant_terms)] (* split_tac, NNF normalization *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

731 
val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals (* necessary because split_once_tac may normalize terms *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

732 
val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm (* TRY (etac notE) THEN eq_assume_tac *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

733 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

734 
result 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

735 
end; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

736 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

737 
(* takes the ith subgoal [ A1; ...; An ] ==> B to *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

738 
(* An > ... > A1 > B, performs splitting with the given 'split_thms' *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

739 
(* (resulting in a different subgoal P), takes P to ~P ==> False, *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

740 
(* performs NNFnormalization of ~P, and eliminates conjunctions, *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

741 
(* disjunctions and existential quantifiers from the premises, possibly (in *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

742 
(* the case of disjunctions) resulting in several new subgoals, each of the *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

743 
(* general form [ Q1; ...; Qm ] ==> False. Fails if more than *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

744 
(* !fast_arith_split_limit splits are possible. *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

745 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

746 
(* Thm.thm list > int > Tactical.tactic *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

747 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

748 
fun split_once_tac split_thms i = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

749 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

750 
val nnf_simpset = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

751 
empty_ss setmkeqTrue mk_eq_True 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

752 
setmksimps (mksimps mksimps_pairs) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

753 
addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

754 
not_all, not_ex, not_not] 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

755 
fun prem_nnf_tac i st = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

756 
full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

757 
fun cond_split_tac i st = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

758 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

759 
val subgoal = Logic.nth_prem (i, Thm.prop_of st) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

760 
val Ts = rev (map snd (Logic.strip_params subgoal)) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

761 
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

762 
val cmap = Splitter.cmap_of_split_thms split_thms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

763 
val splits = Splitter.split_posns cmap (theory_of_thm st) Ts concl 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

764 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

765 
if length splits > !fast_arith_split_limit then 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

766 
no_tac st 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

767 
else 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

768 
split_tac split_thms i st 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

769 
end 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

770 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

771 
EVERY' [ 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

772 
REPEAT_DETERM o etac rev_mp, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

773 
cond_split_tac, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

774 
rtac ccontr, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

775 
prem_nnf_tac, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

776 
TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE)) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

777 
] i 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

778 
end; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

779 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

780 
(* remove irrelevant premises, then split the ith subgoal (and all new *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

781 
(* subgoals) by using 'split_once_tac' repeatedly. Betaetanormalize new *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

782 
(* subgoals and finally attempt to solve them by finding an immediate *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

783 
(* contradiction (i.e. a term and its negation) in their premises. *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

784 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

785 
(* int > Tactical.tactic *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

786 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

787 
fun pre_tac i st = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

788 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

789 
val sg = theory_of_thm st 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

790 
val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg)) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

791 
fun is_relevant t = isSome (decomp sg t) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

792 
in 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

793 
DETERM ( 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

794 
TRY (filter_prems_tac is_relevant i) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

795 
THEN ( 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

796 
(TRY o REPEAT_ALL_NEW (split_once_tac split_thms)) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

797 
THEN_ALL_NEW 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

798 
((fn j => PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal j) (Drule.beta_eta_conversion)))) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

799 
THEN' 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

800 
(TRY o (etac notE THEN' eq_assume_tac))) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

801 
) i 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

802 
) st 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

803 
end; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

804 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

805 
end; (* LA_Data_Ref *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

806 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

807 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

808 
structure Fast_Arith = 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

809 
Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

810 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

811 
val fast_arith_tac = Fast_Arith.lin_arith_tac false; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

812 
val fast_ex_arith_tac = Fast_Arith.lin_arith_tac; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

813 
val trace_arith = Fast_Arith.trace; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

814 
val fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

815 
val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

816 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

817 
local 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

818 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

819 
(* reduce contradictory <= to False. 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

820 
Most of the work is done by the cancel tactics. 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

821 
*) 
12931
2c0251fada94
solved the problem that Larry's simproce cancle_numerals(?) returns
nipkow
parents:
12480
diff
changeset

822 
val add_rules = 
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset

823 
[add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, 
19297
8f6e097d7b23
Removal of unnecessary simprules: simproc cancel_numerals now works without
paulson
parents:
19285
diff
changeset

824 
One_nat_def, 
17875  825 
order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, 
16473
b24c820a0b85
moving some generic inequalities from integer arith to nat arith
paulson
parents:
16424
diff
changeset

826 
zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

827 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset

828 
val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

829 
(fn prems => [cut_facts_tac prems 1, 
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset

830 
blast_tac (claset() addIs [add_mono]) 1])) 
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

831 
["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)", 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

832 
"(i = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)", 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

833 
"(i <= j) & (k = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)", 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

834 
"(i = j) & (k = l) ==> i + k = j + (l::'a::pordered_ab_semigroup_add)" 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

835 
]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

836 

15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

837 
val mono_ss = simpset() addsimps 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

838 
[add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono]; 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

839 

1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

840 
val add_mono_thms_ordered_field = 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

841 
map (fn s => prove_goal (the_context ()) s 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

842 
(fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

843 
["(i<j) & (k=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

844 
"(i=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

845 
"(i<j) & (k<=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

846 
"(i<=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

847 
"(i<j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"]; 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

848 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

849 
in 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

850 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

851 
val init_lin_arith_data = 
18708  852 
Fast_Arith.setup #> 
853 
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => 

15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

854 
{add_mono_thms = add_mono_thms @ 
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset

855 
add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field, 
10693  856 
mult_mono_thms = mult_mono_thms, 
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset

857 
inj_thms = inj_thms, 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

858 
lessD = lessD @ [Suc_leI], 
15923  859 
neqE = [linorder_neqE_nat, 
16485  860 
get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")], 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

861 
simpset = HOL_basic_ss addsimps add_rules 
17875  862 
addsimprocs [ab_group_add_cancel.sum_conv, 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

863 
ab_group_add_cancel.rel_conv] 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

864 
(*abel_cancel helps it work in abstract algebraic domains*) 
18708  865 
addsimprocs nat_cancel_sums_add}) #> 
866 
ArithTheoryData.init #> 

867 
arith_discrete "nat"; 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

868 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

869 
end; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

870 

13462  871 
val fast_nat_arith_simproc = 
16834  872 
Simplifier.simproc (the_context ()) "fast_nat_arith" 
13462  873 
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

874 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

875 
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

876 
useful to detect inconsistencies among the premises for subgoals which are 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

877 
*not* themselves (in)equalities, because the latter activate 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

878 
fast_nat_arith_simproc anyway. However, it seems cheaper to activate the 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

879 
solver all the time rather than add the additional check. *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

880 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

881 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

882 
(* arith proof method *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

883 

10516  884 
local 
885 

13499  886 
fun raw_arith_tac ex i st = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

887 
(* FIXME: K true should be replaced by a sensible test (perhaps "isSome o 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

888 
decomp sg"?) to speed things up in case there are lots of irrelevant 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

889 
terms involved; elimination of min/max can be optimized: 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

890 
(max m n + k <= r) = (m+k <= r & n+k <= r) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

891 
(l <= min m n + k) = (l <= m+k & l <= n+k) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

892 
*) 
13499  893 
refute_tac (K true) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

894 
(* Splitting is also done inside fast_arith_tac, but not completely  *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

895 
(* split_tac may use split theorems that have not been implemented in *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

896 
(* fast_arith_tac (cf. pre_decomp and split_once_items above). *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

897 
(* Therefore splitting outside of fast_arith_tac may allow us to prove *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

898 
(* some goals that fast_arith_tac alone would fail on. *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

899 
(REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st)))) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

900 
(fast_ex_arith_tac ex) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

901 
i st; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

902 

13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

903 
fun presburger_tac i st = 
16834  904 
(case ArithTheoryData.get (Thm.theory_of_thm st) of 
15531  905 
{presburger = SOME tac, ...} => 
16970  906 
(warning "Trying full Presburger arithmetic ..."; tac i st) 
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

907 
 _ => no_tac st); 
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

908 

10516  909 
in 
910 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

911 
val simple_arith_tac = FIRST' [fast_arith_tac, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

912 
ObjectLogic.atomize_tac THEN' raw_arith_tac true]; 
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

913 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

914 
val arith_tac = FIRST' [fast_arith_tac, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

915 
ObjectLogic.atomize_tac THEN' raw_arith_tac true, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

916 
presburger_tac]; 
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset

917 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

918 
val silent_arith_tac = FIRST' [fast_arith_tac, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

919 
ObjectLogic.atomize_tac THEN' raw_arith_tac false, 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

920 
presburger_tac]; 
10516  921 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

922 
fun arith_method prems = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset

923 
Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

924 

10516  925 
end; 
926 

15195  927 
(* antisymmetry: 
15197  928 
combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y 
15195  929 

930 
local 

931 
val antisym = mk_meta_eq order_antisym 

932 
val not_lessD = linorder_not_less RS iffD1 

933 
fun prp t thm = (#prop(rep_thm thm) = t) 

934 
in 

935 
fun antisym_eq prems thm = 

936 
let 

937 
val r = #prop(rep_thm thm); 

938 
in 

939 
case r of 

19277  940 
Tr $ ((c as Const("Orderings.less_eq",T)) $ s $ t) => 
15195  941 
let val r' = Tr $ (c $ t $ s) 
942 
in 

943 
case Library.find_first (prp r') prems of 

15531  944 
NONE => 
19277  945 
let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ s $ t)) 
15195  946 
in case Library.find_first (prp r') prems of 
15531  947 
NONE => [] 
948 
 SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)] 

15195  949 
end 
15531  950 
 SOME thm' => [thm' RS (thm RS antisym)] 
15195  951 
end 
19277  952 
 Tr $ (Const("Not",_) $ (Const("Orderings.less",T) $ s $ t)) => 
953 
let val r' = Tr $ (Const("Orderings.less_eq",T) $ s $ t) 

15195  954 
in 
955 
case Library.find_first (prp r') prems of 

15531  956 
NONE => 
19277  957 
let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ t $ s)) 
15195  958 
in case Library.find_first (prp r') prems of 
15531  959 
NONE => [] 
960 
 SOME thm' => 

15195  961 
[(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)] 
962 
end 

15531  963 
 SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)] 
15195  964 
end 
965 
 _ => [] 

966 
end 

967 
handle THM _ => [] 

968 
end; 

15197  969 
*) 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

970 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

971 
(* theory setup *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

972 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

973 
val arith_setup = 
18708  974 
init_lin_arith_data #> 
975 
(fn thy => (Simplifier.change_simpset_of thy (fn ss => ss 

17875  976 
addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc]) 
18708  977 
addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #> 
15221  978 
Method.add_methods 
17875  979 
[("arith", (arith_method o #2) oo Method.syntax Args.bang_facts, 
18708  980 
"decide linear arithmethic")] #> 
18728  981 
Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add, 
18708  982 
"declaration of split rules for arithmetic procedure")]; 