author  haftmann 
Wed, 03 Dec 2008 15:58:44 +0100  
changeset 28952  15a4b2cf8c34 
parent 28262  src/HOL/arith_data.ML@aa7ca36d67fd 
child 29302  eb782d1dc07c 
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 

26101  8 
signature ARITH_DATA = 
9 
sig 

10 
val prove_conv: tactic > (MetaSimplifier.simpset > tactic) 

11 
> MetaSimplifier.simpset > term * term > thm 

12 
val simp_all_tac: thm list > MetaSimplifier.simpset > tactic 

13 

14 
val mk_sum: term list > term 

15 
val mk_norm_sum: term list > term 

16 
val dest_sum: term > term list 

17 

18 
val nat_cancel_sums_add: simproc list 

19 
val nat_cancel_sums: simproc list 

20 
val setup: Context.generic > Context.generic 

21 
end; 

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

22 

26101  23 
structure ArithData: ARITH_DATA = 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

25 

26101  26 
(** generic proof tools **) 
27 

28 
(* prove conversions *) 

29 

30 
fun prove_conv expand_tac norm_tac ss tu = (* FIXME avoid standard *) 

31 
mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] [] 

32 
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) 

33 
(K (EVERY [expand_tac, norm_tac ss])))); 

34 

35 
(* rewriting *) 

36 

37 
fun simp_all_tac rules = 

38 
let val ss0 = HOL_ss addsimps rules 

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

40 

41 

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

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

43 

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

45 

22997  46 
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; 
26101  47 
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT; 
48 

49 
in 

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

50 

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

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

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

53 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 
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 
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

56 
fun mk_norm_sum ts = 
21621  57 
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

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

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

60 

24095  61 

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

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

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

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

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

68 
(case try dest_plus tm of 
15531  69 
SOME (t, u) => dest_sum t @ dest_sum u 
70 
 NONE => [tm])); 

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

71 

24095  72 
end; 
73 

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

74 

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

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

76 

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

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

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

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

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

81 
val prove_conv = prove_conv; 
22838  82 
val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"}, 
83 
@{thm "add_0"}, @{thm "add_0_right"}]; 

22548  84 
val norm_tac2 = simp_all_tac @{thms add_ac}; 
18328  85 
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

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

87 

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

88 
fun gen_uncancel_tac rule ct = 
22838  89 
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

90 

24095  91 

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

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

93 

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

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

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

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

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

98 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; 
22838  99 
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

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

101 

24095  102 

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

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

104 

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

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

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

107 
open Sum; 
23881  108 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}; 
109 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT; 

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

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

112 

24095  113 

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

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

115 

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

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

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

118 
open Sum; 
23881  119 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}; 
120 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT; 

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

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

123 

24095  124 

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

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

126 

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

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

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

129 
open Sum; 
22997  130 
val mk_bal = HOLogic.mk_binop @{const_name HOL.minus}; 
131 
val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT; 

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

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

134 

24095  135 

136 
(* prepare nat_cancel simprocs *) 

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

137 

26101  138 
val nat_cancel_sums_add = 
28262
aa7ca36d67fd
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents:
26101
diff
changeset

139 
[Simplifier.simproc (the_context ()) "nateq_cancel_sums" 
26101  140 
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"] 
141 
(K EqCancelSums.proc), 

28262
aa7ca36d67fd
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents:
26101
diff
changeset

142 
Simplifier.simproc (the_context ()) "natless_cancel_sums" 
26101  143 
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"] 
144 
(K LessCancelSums.proc), 

28262
aa7ca36d67fd
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents:
26101
diff
changeset

145 
Simplifier.simproc (the_context ()) "natle_cancel_sums" 
26101  146 
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"] 
147 
(K LeCancelSums.proc)]; 

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

148 

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

149 
val nat_cancel_sums = nat_cancel_sums_add @ 
28262
aa7ca36d67fd
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents:
26101
diff
changeset

150 
[Simplifier.simproc (the_context ()) "natdiff_cancel_sums" 
26101  151 
["((l::nat) + m)  n", "(l::nat)  (m + n)", "Suc m  n", "m  Suc n"] 
152 
(K DiffCancelSums.proc)]; 

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

153 

26101  154 
val setup = 
24095  155 
Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); 
24076  156 

24095  157 
end; 