author  wenzelm 
Tue, 31 Jul 2007 19:40:26 +0200  
changeset 24095  785c3cd7fcb5 
parent 24076  ae946f751c44 
child 25484  4c98517601ce 
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$ 
24095  3 
Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

4 

24095  5 
Basic arithmetic proof tools. 
9436
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 

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

9 

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

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

12 

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

13 
(** abstract syntax of structure nat: 0, Suc, + **) 
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 
(* mk_sum, mk_norm_sum *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

16 

22997  17 
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; 
9436
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 
fun mk_sum [] = HOLogic.zero 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

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

22 

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

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

24 
fun mk_norm_sum ts = 
21621  25 
let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

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

28 

24095  29 

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

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

31 

22997  32 
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

33 

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

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

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

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

37 
(case try HOLogic.dest_Suc tm of 
21621  38 
SOME t => HOLogic.Suc_zero :: dest_sum t 
15531  39 
 NONE => 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

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

43 

24095  44 

45 

9436
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 

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

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

57 

18328  58 
fun simp_all_tac rules = 
59 
let val ss0 = HOL_ss addsimps rules 

60 
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

61 

13517  62 
fun prep_simproc (name, pats, proc) = 
16834  63 
Simplifier.simproc (the_context ()) name pats proc; 
13517  64 

24095  65 
end; 
66 

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

67 

13517  68 

24095  69 
(** ArithData **) 
70 

13517  71 
signature ARITH_DATA = 
72 
sig 

73 
val nat_cancel_sums_add: simproc list 

74 
val nat_cancel_sums: simproc list 

24095  75 
val arith_data_setup: Context.generic > Context.generic 
13517  76 
end; 
77 

78 
structure ArithData: ARITH_DATA = 

79 
struct 

80 

81 
open NatArithUtils; 

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

82 

24095  83 

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

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

85 

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

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

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

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

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

90 
val prove_conv = prove_conv; 
22838  91 
val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"}, 
92 
@{thm "add_0"}, @{thm "add_0_right"}]; 

22548  93 
val norm_tac2 = simp_all_tac @{thms add_ac}; 
18328  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 = 
22838  98 
rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

99 

24095  100 

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

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

102 

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

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

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

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

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

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

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

110 

24095  111 

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

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

113 

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

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

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

116 
open Sum; 
23881  117 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}; 
118 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT; 

22838  119 
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"}; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

121 

24095  122 

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

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

124 

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

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

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

127 
open Sum; 
23881  128 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}; 
129 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT; 

22838  130 
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"}; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

132 

24095  133 

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

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

135 

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

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

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

138 
open Sum; 
22997  139 
val mk_bal = HOLogic.mk_binop @{const_name HOL.minus}; 
140 
val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT; 

22838  141 
val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"}; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

143 

24095  144 

145 
(* prepare nat_cancel simprocs *) 

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

146 

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

147 
val nat_cancel_sums_add = map prep_simproc 
13462  148 
[("nateq_cancel_sums", 
20268  149 
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], 
150 
K EqCancelSums.proc), 

13462  151 
("natless_cancel_sums", 
20268  152 
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], 
153 
K LessCancelSums.proc), 

13462  154 
("natle_cancel_sums", 
20268  155 
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], 
156 
K LeCancelSums.proc)]; 

9436
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 
val nat_cancel_sums = nat_cancel_sums_add @ 
13462  159 
[prep_simproc ("natdiff_cancel_sums", 
20268  160 
["((l::nat) + m)  n", "(l::nat)  (m + n)", "Suc m  n", "m  Suc n"], 
161 
K DiffCancelSums.proc)]; 

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

162 

24095  163 
val arith_data_setup = 
164 
Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); 

24076  165 

166 

24095  167 
(* FIXME dead code *) 
15195  168 
(* antisymmetry: 
15197  169 
combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y 
15195  170 

171 
local 

172 
val antisym = mk_meta_eq order_antisym 

22548  173 
val not_lessD = @{thm linorder_not_less} RS iffD1 
15195  174 
fun prp t thm = (#prop(rep_thm thm) = t) 
175 
in 

176 
fun antisym_eq prems thm = 

177 
let 

178 
val r = #prop(rep_thm thm); 

179 
in 

180 
case r of 

23881  181 
Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) => 
15195  182 
let val r' = Tr $ (c $ t $ s) 
183 
in 

184 
case Library.find_first (prp r') prems of 

15531  185 
NONE => 
23881  186 
let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t)) 
15195  187 
in case Library.find_first (prp r') prems of 
15531  188 
NONE => [] 
189 
 SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)] 

15195  190 
end 
15531  191 
 SOME thm' => [thm' RS (thm RS antisym)] 
15195  192 
end 
23881  193 
 Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) => 
194 
let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t) 

15195  195 
in 
196 
case Library.find_first (prp r') prems of 

15531  197 
NONE => 
23881  198 
let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s)) 
15195  199 
in case Library.find_first (prp r') prems of 
15531  200 
NONE => [] 
201 
 SOME thm' => 

15195  202 
[(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)] 
203 
end 

15531  204 
 SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)] 
15195  205 
end 
206 
 _ => [] 

207 
end 

208 
handle THM _ => [] 

209 
end; 

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

211 

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

213 

24095  214 
open ArithData; 