author | wenzelm |
Tue, 18 Mar 2008 20:33:29 +0100 | |
changeset 26315 | cb3badaa192e |
parent 24893 | b8ef7afe3a6b |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
9654
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9492
diff
changeset
|
1 |
(* Title: ZF/Arith.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
6 |
*) |
|
7 |
||
13163 | 8 |
(*"Difference" is subtraction of natural numbers. |
9 |
There are no negative numbers; we have |
|
10 |
m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. |
|
11 |
Also, rec(m, 0, %z w.z) is pred(m). |
|
12 |
*) |
|
13 |
||
13328 | 14 |
header{*Arithmetic Operators and Their Definitions*} |
15 |
||
16417 | 16 |
theory Arith imports Univ begin |
6070 | 17 |
|
13328 | 18 |
text{*Proofs about elementary arithmetic: addition, multiplication, etc.*} |
19 |
||
24893 | 20 |
definition |
21 |
pred :: "i=>i" (*inverse of succ*) where |
|
13361 | 22 |
"pred(y) == nat_case(0, %x. x, y)" |
6070 | 23 |
|
24893 | 24 |
definition |
25 |
natify :: "i=>i" (*coerces non-nats to nats*) where |
|
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
26 |
"natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a)) |
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
27 |
else 0)" |
6070 | 28 |
|
0 | 29 |
consts |
13163 | 30 |
raw_add :: "[i,i]=>i" |
31 |
raw_diff :: "[i,i]=>i" |
|
32 |
raw_mult :: "[i,i]=>i" |
|
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
33 |
|
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
34 |
primrec |
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
35 |
"raw_add (0, n) = n" |
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
36 |
"raw_add (succ(m), n) = succ(raw_add(m, n))" |
0 | 37 |
|
6070 | 38 |
primrec |
13163 | 39 |
raw_diff_0: "raw_diff(m, 0) = m" |
40 |
raw_diff_succ: "raw_diff(m, succ(n)) = |
|
41 |
nat_case(0, %x. x, raw_diff(m, n))" |
|
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
42 |
|
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
43 |
primrec |
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
44 |
"raw_mult(0, n) = 0" |
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
45 |
"raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))" |
13163 | 46 |
|
24893 | 47 |
definition |
48 |
add :: "[i,i]=>i" (infixl "#+" 65) where |
|
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
49 |
"m #+ n == raw_add (natify(m), natify(n))" |
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
50 |
|
24893 | 51 |
definition |
52 |
diff :: "[i,i]=>i" (infixl "#-" 65) where |
|
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
53 |
"m #- n == raw_diff (natify(m), natify(n))" |
0 | 54 |
|
24893 | 55 |
definition |
56 |
mult :: "[i,i]=>i" (infixl "#*" 70) where |
|
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
57 |
"m #* n == raw_mult (natify(m), natify(n))" |
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
58 |
|
24893 | 59 |
definition |
60 |
raw_div :: "[i,i]=>i" where |
|
13163 | 61 |
"raw_div (m, n) == |
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
62 |
transrec(m, %j f. if j<n | n=0 then 0 else succ(f`(j#-n)))" |
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
63 |
|
24893 | 64 |
definition |
65 |
raw_mod :: "[i,i]=>i" where |
|
13163 | 66 |
"raw_mod (m, n) == |
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
67 |
transrec(m, %j f. if j<n | n=0 then j else f`(j#-n))" |
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
68 |
|
24893 | 69 |
definition |
70 |
div :: "[i,i]=>i" (infixl "div" 70) where |
|
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
71 |
"m div n == raw_div (natify(m), natify(n))" |
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
72 |
|
24893 | 73 |
definition |
74 |
mod :: "[i,i]=>i" (infixl "mod" 70) where |
|
9492
72e429c66608
used natify with div and mod; also put in the divide-by-zero trick
paulson
parents:
9491
diff
changeset
|
75 |
"m mod n == raw_mod (natify(m), natify(n))" |
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset
|
76 |
|
24893 | 77 |
notation (xsymbols) |
78 |
mult (infixr "#\<times>" 70) |
|
9964 | 79 |
|
24893 | 80 |
notation (HTML output) |
81 |
mult (infixr "#\<times>" 70) |
|
13163 | 82 |
|
83 |
declare rec_type [simp] |
|
84 |
nat_0_le [simp] |
|
85 |
||
86 |
||
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
87 |
lemma zero_lt_lemma: "[| 0<k; k \<in> nat |] ==> \<exists>j\<in>nat. k = succ(j)" |
13163 | 88 |
apply (erule rev_mp) |
89 |
apply (induct_tac "k", auto) |
|
90 |
done |
|
91 |
||
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
92 |
(* [| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q *) |
13163 | 93 |
lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard] |
94 |
||
95 |
||
13356 | 96 |
subsection{*@{text natify}, the Coercion to @{term nat}*} |
13163 | 97 |
|
98 |
lemma pred_succ_eq [simp]: "pred(succ(y)) = y" |
|
99 |
by (unfold pred_def, auto) |
|
100 |
||
101 |
lemma natify_succ: "natify(succ(x)) = succ(natify(x))" |
|
102 |
by (rule natify_def [THEN def_Vrecursor, THEN trans], auto) |
|
103 |
||
104 |
lemma natify_0 [simp]: "natify(0) = 0" |
|
105 |
by (rule natify_def [THEN def_Vrecursor, THEN trans], auto) |
|
106 |
||
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
107 |
lemma natify_non_succ: "\<forall>z. x ~= succ(z) ==> natify(x) = 0" |
13163 | 108 |
by (rule natify_def [THEN def_Vrecursor, THEN trans], auto) |
109 |
||
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
110 |
lemma natify_in_nat [iff,TC]: "natify(x) \<in> nat" |
13163 | 111 |
apply (rule_tac a=x in eps_induct) |
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
112 |
apply (case_tac "\<exists>z. x = succ(z)") |
13163 | 113 |
apply (auto simp add: natify_succ natify_non_succ) |
114 |
done |
|
115 |
||
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
116 |
lemma natify_ident [simp]: "n \<in> nat ==> natify(n) = n" |
13163 | 117 |
apply (induct_tac "n") |
118 |
apply (auto simp add: natify_succ) |
|
119 |
done |
|
120 |
||
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
121 |
lemma natify_eqE: "[|natify(x) = y; x \<in> nat|] ==> x=y" |
13163 | 122 |
by auto |
123 |
||
124 |
||
125 |
(*** Collapsing rules: to remove natify from arithmetic expressions ***) |
|
126 |
||
127 |
lemma natify_idem [simp]: "natify(natify(x)) = natify(x)" |
|
128 |
by simp |
|
129 |
||
130 |
(** Addition **) |
|
131 |
||
132 |
lemma add_natify1 [simp]: "natify(m) #+ n = m #+ n" |
|
133 |
by (simp add: add_def) |
|
134 |
||
135 |
lemma add_natify2 [simp]: "m #+ natify(n) = m #+ n" |
|
136 |
by (simp add: add_def) |
|
137 |
||
138 |
(** Multiplication **) |
|
139 |
||
140 |
lemma mult_natify1 [simp]: "natify(m) #* n = m #* n" |
|
141 |
by (simp add: mult_def) |
|
142 |
||
143 |
lemma mult_natify2 [simp]: "m #* natify(n) = m #* n" |
|
144 |
by (simp add: mult_def) |
|
145 |
||
146 |
(** Difference **) |
|
147 |
||
148 |
lemma diff_natify1 [simp]: "natify(m) #- n = m #- n" |
|
149 |
by (simp add: diff_def) |
|
150 |
||
151 |
lemma diff_natify2 [simp]: "m #- natify(n) = m #- n" |
|
152 |
by (simp add: diff_def) |
|
153 |
||
154 |
(** Remainder **) |
|
155 |
||
156 |
lemma mod_natify1 [simp]: "natify(m) mod n = m mod n" |
|
157 |
by (simp add: mod_def) |
|
158 |
||
159 |
lemma mod_natify2 [simp]: "m mod natify(n) = m mod n" |
|
160 |
by (simp add: mod_def) |
|
161 |
||
162 |
||
163 |
(** Quotient **) |