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.36  by (simp add: diff_def)
    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.44  apply (simp_all add: le_iff)
    1.45 @@ -293,13 +293,13 @@
    1.46  by (force dest!: add_left_cancel_natify)
    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.59  by (drule add_le_elim1_natify, auto)
    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.81  apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
    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.88  apply (subst add_commute, subst add_commute, rule add_le_mono1, 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.94 -apply (rule add_lt_le_mono) 
    1.95 -apply (auto intro: leI) 
    1.96 +apply (rule add_lt_le_mono)
    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.102  by (simp add: pred_def)
   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)"}*}