tuned
authorwenzelm
Thu May 31 22:34:58 2001 +0200 (2001-05-31)
changeset 11357908b761cdfb0
parent 11356 8fbb19b84f94
child 11358 416ea5c009f5
tuned
src/HOL/Library/Nat_Infinity.thy
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Thu May 31 20:53:49 2001 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Thu May 31 22:34:58 2001 +0200
     1.3 @@ -42,130 +42,130 @@
     1.4  lemmas inat_splits = inat.split inat.split_asm
     1.5  
     1.6  text {*
     1.7 -  Below is a not quite complete set of theorems.  Use method @{text
     1.8 -  "(simp add: inat_defs split:inat_splits, arith?)"} to prove new
     1.9 -  theorems or solve arithmetic subgoals involving @{typ inat} on the
    1.10 -  fly.
    1.11 +  Below is a not quite complete set of theorems.  Use the method
    1.12 +  @{text "(simp add: inat_defs split:inat_splits, arith?)"} to prove
    1.13 +  new theorems or solve arithmetic subgoals involving @{typ inat} on
    1.14 +  the fly.
    1.15  *}
    1.16  
    1.17  subsection "Constructors"
    1.18  
    1.19  lemma Fin_0: "Fin 0 = 0"
    1.20 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.21 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.22  
    1.23  lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    1.24 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.25 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.26  
    1.27  lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    1.28 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.29 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.30  
    1.31  lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
    1.32 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.33 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.34  
    1.35  lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
    1.36 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.37 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.38  
    1.39  lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
    1.40 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.41 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.42  
    1.43  lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
    1.44 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.45 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.46  
    1.47  
    1.48  subsection "Ordering relations"
    1.49  
    1.50  lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
    1.51 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.52 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.53  
    1.54  lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
    1.55 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.56 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.57  
    1.58  lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
    1.59 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.60 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.61  
    1.62  lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
    1.63 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.64 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.65  
    1.66  lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
    1.67 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.68 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.69  
    1.70  lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
    1.71 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.72 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.73  
    1.74  lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
    1.75 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.76 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.77  
    1.78  lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
    1.79 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.80 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.81  
    1.82  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
    1.83 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.84 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.85  
    1.86  lemma i0_iless_iSuc [simp]: "0 < iSuc n"
    1.87 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.88 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.89  
    1.90  lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
    1.91 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.92 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.93  
    1.94  lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
    1.95 -  by (simp add:inat_defs split:inat_splits, arith?)
    1.96 +  by (simp add: inat_defs split:inat_splits, arith?)
    1.97  
    1.98  lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
    1.99 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.100 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.101  
   1.102  
   1.103  (* ----------------------------------------------------------------------- *)
   1.104  
   1.105  lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))"
   1.106 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.107 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.108  
   1.109  lemma ile_refl [simp]: "n \<le> (n::inat)"
   1.110 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.111 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.112  
   1.113  lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
   1.114 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.115 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.116  
   1.117  lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
   1.118 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.119 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.120  
   1.121  lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
   1.122 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.123 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.124  
   1.125  lemma Infty_ub [simp]: "n \<le> \<infinity>"
   1.126 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.127 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.128  
   1.129  lemma i0_lb [simp]: "(0::inat) \<le> n"
   1.130 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.131 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.132  
   1.133  lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
   1.134 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.135 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.136  
   1.137  lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
   1.138 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.139 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.140  
   1.141  lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
   1.142 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.143 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.144  
   1.145  lemma ileI1: "m < n ==> iSuc m \<le> n"
   1.146 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.147 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.148  
   1.149  lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)"
   1.150 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.151 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.152  
   1.153  lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)"
   1.154 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.155 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.156  
   1.157  lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)"
   1.158 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.159 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.160  
   1.161  lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   1.162 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.163 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.164  
   1.165  lemma ile_iSuc [simp]: "n \<le> iSuc n"
   1.166 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.167 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.168  
   1.169  lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
   1.170 -  by (simp add:inat_defs split:inat_splits, arith?)
   1.171 +  by (simp add: inat_defs split:inat_splits, arith?)
   1.172  
   1.173  lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   1.174    apply (induct_tac k)