src/ZF/Arith.thy
 changeset 46820 c656222c4dc1 parent 45608 13b101cee425 child 46821 ff6b0c1087f2
```     1.1 --- a/src/ZF/Arith.thy	Sun Mar 04 23:20:43 2012 +0100
1.2 +++ b/src/ZF/Arith.thy	Tue Mar 06 15:15:49 2012 +0000
1.3 @@ -6,10 +6,10 @@
1.4  (*"Difference" is subtraction of natural numbers.
1.5    There are no negative numbers; we have
1.6       m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
1.7 -  Also, rec(m, 0, %z w.z) is pred(m).
1.8 +  Also, rec(m, 0, %z w.z) is pred(m).
1.9  *)
1.10
1.11 -header{*Arithmetic Operators and Their Definitions*}
1.12 +header{*Arithmetic Operators and Their Definitions*}
1.13
1.14  theory Arith imports Univ begin
1.15
1.16 @@ -87,7 +87,7 @@
1.17  apply (induct_tac "k", auto)
1.18  done
1.19
1.20 -(* [| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q *)
1.21 +(* @{term"[| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q"} *)
1.22  lemmas zero_lt_natE = zero_lt_lemma [THEN bexE]
1.23
1.24
1.25 @@ -102,7 +102,7 @@
1.26  lemma natify_0 [simp]: "natify(0) = 0"
1.27  by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
1.28
1.29 -lemma natify_non_succ: "\<forall>z. x ~= succ(z) ==> natify(x) = 0"
1.30 +lemma natify_non_succ: "\<forall>z. x \<noteq> succ(z) ==> natify(x) = 0"
1.31  by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
1.32
1.33  lemma natify_in_nat [iff,TC]: "natify(x) \<in> nat"
1.34 @@ -214,8 +214,8 @@
1.35  lemma diff_0 [simp]: "m #- 0 = natify(m)"
1.37
1.38 -lemma diff_le_self: "m\<in>nat ==> (m #- n) le m"
1.39 -apply (subgoal_tac " (m #- natify (n)) le m")
1.40 +lemma diff_le_self: "m\<in>nat ==> (m #- n) \<le> m"
1.41 +apply (subgoal_tac " (m #- natify (n)) \<le> m")
1.42  apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct)
1.43  apply (erule_tac [6] leE)
1.45 @@ -293,13 +293,13 @@
1.47
1.48  (*Thanks to Sten Agerholm*)
1.49 -lemma add_le_elim1_natify: "k#+m le k#+n ==> natify(m) le natify(n)"
1.50 -apply (rule_tac P = "natify(k) #+m le natify(k) #+n" in rev_mp)
1.51 +lemma add_le_elim1_natify: "k#+m \<le> k#+n ==> natify(m) \<le> natify(n)"
1.52 +apply (rule_tac P = "natify(k) #+m \<le> natify(k) #+n" in rev_mp)
1.53  apply (rule_tac [2] n = "natify(k) " in nat_induct)
1.54  apply auto
1.55  done
1.56
1.57 -lemma add_le_elim1: "[| k#+m le k#+n; m \<in> nat; n \<in> nat |] ==> m le n"
1.58 +lemma add_le_elim1: "[| k#+m \<le> k#+n; m \<in> nat; n \<in> nat |] ==> m \<le> n"
1.60
1.61  lemma add_lt_elim1_natify: "k#+m < k#+n ==> natify(m) < natify(n)"
1.62 @@ -334,21 +334,21 @@
1.63  lemma Ord_lt_mono_imp_le_mono:
1.64    assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
1.65        and ford:    "!!i. i:k ==> Ord(f(i))"
1.66 -      and leij:    "i le j"
1.67 +      and leij:    "i \<le> j"
1.68        and jink:    "j:k"
1.69 -  shows "f(i) le f(j)"
1.70 -apply (insert leij jink)
1.71 +  shows "f(i) \<le> f(j)"
1.72 +apply (insert leij jink)
1.73  apply (blast intro!: leCI lt_mono ford elim!: leE)
1.74  done
1.75
1.76  text{*@{text "\<le>"} monotonicity, 1st argument*}
1.77 -lemma add_le_mono1: "[| i le j; j\<in>nat |] ==> i#+k le j#+k"
1.78 -apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck)
1.79 +lemma add_le_mono1: "[| i \<le> j; j\<in>nat |] ==> i#+k \<le> j#+k"
1.80 +apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck)
1.82  done
1.83
1.84  text{*@{text "\<le>"} monotonicity, both arguments*}
1.85 -lemma add_le_mono: "[| i le j; k le l; j\<in>nat; l\<in>nat |] ==> i#+k le j#+l"
1.86 +lemma add_le_mono: "[| i \<le> j; k \<le> l; j\<in>nat; l\<in>nat |] ==> i#+k \<le> j#+l"
1.87  apply (rule add_le_mono1 [THEN le_trans], assumption+)
1.89  done
1.90 @@ -365,8 +365,8 @@
1.91
1.92  text{*Less-than: in other words, strict in both arguments*}
1.93  lemma add_lt_mono: "[| i<j; k<l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
1.95 -apply (auto intro: leI)
1.97 +apply (auto intro: leI)
1.98  done
1.99
1.100  (** Subtraction is the inverse of addition. **)
1.101 @@ -400,12 +400,12 @@
1.103
1.104  lemma eq_succ_imp_eq_m1: "[|i = succ(j); i\<in>nat|] ==> j = i #- 1 & j \<in>nat"
1.105 -by simp
1.106 +by simp
1.107
1.108  lemma pred_Un_distrib:
1.109 -    "[|i\<in>nat; j\<in>nat|] ==> pred(i Un j) = pred(i) Un pred(j)"
1.110 -apply (erule_tac n=i in natE, simp)
1.111 -apply (erule_tac n=j in natE, simp)
1.112 +    "[|i\<in>nat; j\<in>nat|] ==> pred(i \<union> j) = pred(i) \<union> pred(j)"
1.113 +apply (erule_tac n=i in natE, simp)
1.114 +apply (erule_tac n=j in natE, simp)
1.115  apply (simp add:  succ_Un_distrib [symmetric])
1.116  done
1.117
1.118 @@ -414,23 +414,23 @@
1.119  by (simp add: pred_def split: split_nat_case)
1.120
1.121  lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)";
1.122 -apply (rule_tac m=i and n=j in diff_induct)
1.123 +apply (rule_tac m=i and n=j in diff_induct)
1.124  apply (auto simp add: pred_def nat_imp_quasinat split: split_nat_case)
1.125  done
1.126
1.127  lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)";
1.128  apply (insert nat_diff_pred [of "natify(i)" "natify(j)"])
1.129 -apply (simp add: natify_succ [symmetric])
1.130 +apply (simp add: natify_succ [symmetric])
1.131  done
1.132
1.133  lemma nat_diff_Un_distrib:
1.134 -    "[|i\<in>nat; j\<in>nat; k\<in>nat|] ==> (i Un j) #- k = (i#-k) Un (j#-k)"
1.135 -apply (rule_tac n=k in nat_induct)
1.136 -apply (simp_all add: diff_succ_eq_pred pred_Un_distrib)
1.137 +    "[|i\<in>nat; j\<in>nat; k\<in>nat|] ==> (i \<union> j) #- k = (i#-k) \<union> (j#-k)"
1.138 +apply (rule_tac n=k in nat_induct)
1.139 +apply (simp_all add: diff_succ_eq_pred pred_Un_distrib)
1.140  done
1.141
1.142  lemma diff_Un_distrib:
1.143 -    "[|i\<in>nat; j\<in>nat|] ==> (i Un j) #- k = (i#-k) Un (j#-k)"
1.144 +    "[|i\<in>nat; j\<in>nat|] ==> (i \<union> j) #- k = (i#-k) \<union> (j#-k)"
1.145  by (insert nat_diff_Un_distrib [of i j "natify(k)"], simp)
1.146
1.147  text{*We actually prove @{term "i #- j #- k = i #- (j #+ k)"}*}
```