equal
deleted
inserted
replaced
85 |
85 |
86 (* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *) |
86 (* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *) |
87 lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard] |
87 lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard] |
88 |
88 |
89 |
89 |
90 (** natify: coercion to "nat" **) |
90 subsection{*@{text natify}, the Coercion to @{term nat}*} |
91 |
91 |
92 lemma pred_succ_eq [simp]: "pred(succ(y)) = y" |
92 lemma pred_succ_eq [simp]: "pred(succ(y)) = y" |
93 by (unfold pred_def, auto) |
93 by (unfold pred_def, auto) |
94 |
94 |
95 lemma natify_succ: "natify(succ(x)) = succ(natify(x))" |
95 lemma natify_succ: "natify(succ(x)) = succ(natify(x))" |
161 |
161 |
162 lemma div_natify2 [simp]: "m div natify(n) = m div n" |
162 lemma div_natify2 [simp]: "m div natify(n) = m div n" |
163 by (simp add: div_def) |
163 by (simp add: div_def) |
164 |
164 |
165 |
165 |
166 (*** Typing rules ***) |
166 subsection{*Typing rules*} |
167 |
167 |
168 (** Addition **) |
168 (** Addition **) |
169 |
169 |
170 lemma raw_add_type: "[| m:nat; n:nat |] ==> raw_add (m, n) : nat" |
170 lemma raw_add_type: "[| m:nat; n:nat |] ==> raw_add (m, n) : nat" |
171 by (induct_tac "m", auto) |
171 by (induct_tac "m", auto) |
216 apply (erule_tac [6] leE) |
216 apply (erule_tac [6] leE) |
217 apply (simp_all add: le_iff) |
217 apply (simp_all add: le_iff) |
218 done |
218 done |
219 |
219 |
220 |
220 |
221 (*** Addition ***) |
221 subsection{*Addition*} |
222 |
222 |
223 (*Natify has weakened this law, compared with the older approach*) |
223 (*Natify has weakened this law, compared with the older approach*) |
224 lemma add_0_natify [simp]: "0 #+ m = natify(m)" |
224 lemma add_0_natify [simp]: "0 #+ m = natify(m)" |
225 by (simp add: add_def) |
225 by (simp add: add_def) |
226 |
226 |
306 |
306 |
307 lemma add_lt_elim1: "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n" |
307 lemma add_lt_elim1: "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n" |
308 by (drule add_lt_elim1_natify, auto) |
308 by (drule add_lt_elim1_natify, auto) |
309 |
309 |
310 |
310 |
311 (*** Monotonicity of Addition ***) |
311 subsection{*Monotonicity of Addition*} |
312 |
312 |
313 (*strict, in 1st argument; proof is by rule induction on 'less than'. |
313 (*strict, in 1st argument; proof is by rule induction on 'less than'. |
314 Still need j:nat, for consider j = omega. Then we can have i<omega, |
314 Still need j:nat, for consider j = omega. Then we can have i<omega, |
315 which is the same as i:nat, but natify(j)=0, so the conclusion fails.*) |
315 which is the same as i:nat, but natify(j)=0, so the conclusion fails.*) |
316 lemma add_lt_mono1: "[| i<j; j:nat |] ==> i#+k < j#+k" |
316 lemma add_lt_mono1: "[| i<j; j:nat |] ==> i#+k < j#+k" |
400 |
400 |
401 lemma iff_cong2: "u <-> u' ==> (t==u) == (t==u')" |
401 lemma iff_cong2: "u <-> u' ==> (t==u) == (t==u')" |
402 by auto |
402 by auto |
403 |
403 |
404 |
404 |
405 (*** Multiplication [the simprocs need these laws] ***) |
405 subsection{*Multiplication*} |
406 |
406 |
407 lemma mult_0 [simp]: "0 #* m = 0" |
407 lemma mult_0 [simp]: "0 #* m = 0" |
408 by (simp add: mult_def) |
408 by (simp add: mult_def) |
409 |
409 |
410 lemma mult_succ [simp]: "succ(m) #* n = n #+ (m #* n)" |
410 lemma mult_succ [simp]: "succ(m) #* n = n #+ (m #* n)" |