author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 35267  8dfd816713c6 
child 38715  6513ea67d95d 
permissions  rwrr 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

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

2 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

3 
Basic arithmetic for natural numbers. 
9436
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 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

6 
signature NAT_ARITH = 
26101  7 
sig 
8 
val mk_sum: term list > term 

9 
val mk_norm_sum: term list > term 

10 
val dest_sum: term > term list 

11 

12 
val nat_cancel_sums_add: simproc list 

13 
val nat_cancel_sums: simproc list 

14 
val setup: Context.generic > Context.generic 

15 
end; 

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

16 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

17 
structure Nat_Arith: NAT_ARITH = 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

19 

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

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

21 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

22 
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

23 
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; 
26101  24 

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

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

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

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

28 

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

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

30 
fun mk_norm_sum ts = 
21621  31 
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

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

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

34 

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

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

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

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

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

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

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

44 

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

45 

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

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

47 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

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

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

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

51 
val dest_sum = dest_sum; 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

52 
val prove_conv = Arith_Data.prove_conv2; 
35047
1b2bae06c796
hide fact Nat.add_0_right; make add_0_right from Groups priority
haftmann
parents:
34974
diff
changeset

53 
val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right}, 
35064
1bdef0c013d3
hide fact names clashing with fact names from Group.thy
haftmann
parents:
35047
diff
changeset

54 
@{thm Nat.add_0}, @{thm Nat.add_0_right}]; 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

55 
val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac}; 
18328  56 
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss; 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

57 
fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals} 
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

58 
in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end; 
9436
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 

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

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

62 
(struct 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

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

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

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

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

68 

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

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

70 
(struct 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

71 
open CommonCancelSums; 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

72 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}; 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

73 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT; 
22838  74 
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

75 
end); 
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 LeCancelSums = CancelSumsFun 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

78 
(struct 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

79 
open CommonCancelSums; 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

80 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}; 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

81 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT; 
22838  82 
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

83 
end); 
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 
structure DiffCancelSums = CancelSumsFun 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

86 
(struct 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

87 
open CommonCancelSums; 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

88 
val mk_bal = HOLogic.mk_binop @{const_name Groups.minus}; 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

89 
val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT; 
22838  90 
val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"}; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

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

92 

26101  93 
val nat_cancel_sums_add = 
32010  94 
[Simplifier.simproc @{theory} "nateq_cancel_sums" 
26101  95 
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"] 
96 
(K EqCancelSums.proc), 

32010  97 
Simplifier.simproc @{theory} "natless_cancel_sums" 
26101  98 
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"] 
99 
(K LessCancelSums.proc), 

32010  100 
Simplifier.simproc @{theory} "natle_cancel_sums" 
26101  101 
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"] 
102 
(K LeCancelSums.proc)]; 

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

103 

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

104 
val nat_cancel_sums = nat_cancel_sums_add @ 
32010  105 
[Simplifier.simproc @{theory} "natdiff_cancel_sums" 
26101  106 
["((l::nat) + m)  n", "(l::nat)  (m + n)", "Suc m  n", "m  Suc n"] 
107 
(K DiffCancelSums.proc)]; 

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

108 

26101  109 
val setup = 
24095  110 
Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); 
24076  111 

24095  112 
end; 