src/HOL/Library/Nat_Infinity.thy
changeset 25134 3d4953e88449
parent 25112 98824cc791c0
child 25594 43c718438f9f
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sun Oct 21 14:21:54 2007 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sun Oct 21 14:53:44 2007 +0200
     1.3 @@ -51,132 +51,132 @@
     1.4  subsection "Constructors"
     1.5  
     1.6  lemma Fin_0: "Fin 0 = 0"
     1.7 -  by (simp add: inat_defs split:inat_splits)
     1.8 +by (simp add: inat_defs split:inat_splits)
     1.9  
    1.10  lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    1.11 -  by (simp add: inat_defs split:inat_splits)
    1.12 +by (simp add: inat_defs split:inat_splits)
    1.13  
    1.14  lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    1.15 -  by (simp add: inat_defs split:inat_splits)
    1.16 +by (simp add: inat_defs split:inat_splits)
    1.17  
    1.18  lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
    1.19 -  by (simp add: inat_defs split:inat_splits)
    1.20 +by (simp add: inat_defs split:inat_splits)
    1.21  
    1.22  lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
    1.23 -  by (simp add: inat_defs split:inat_splits)
    1.24 +by (simp add: inat_defs split:inat_splits)
    1.25  
    1.26  lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
    1.27 -  by (simp add: inat_defs split:inat_splits)
    1.28 +by (simp add: inat_defs split:inat_splits)
    1.29  
    1.30  lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
    1.31 -  by (simp add: inat_defs split:inat_splits)
    1.32 +by (simp add: inat_defs split:inat_splits)
    1.33  
    1.34  
    1.35  subsection "Ordering relations"
    1.36  
    1.37  lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
    1.38 -  by (simp add: inat_defs split:inat_splits)
    1.39 +by (simp add: inat_defs split:inat_splits)
    1.40  
    1.41  lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
    1.42 -  by (simp add: inat_defs split:inat_splits, arith)
    1.43 +by (simp add: inat_defs split:inat_splits, arith)
    1.44  
    1.45  lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
    1.46 -  by (simp add: inat_defs split:inat_splits)
    1.47 +by (simp add: inat_defs split:inat_splits)
    1.48  
    1.49  lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
    1.50 -  by (simp add: inat_defs split:inat_splits)
    1.51 +by (simp add: inat_defs split:inat_splits)
    1.52  
    1.53  lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
    1.54 -  by (simp add: inat_defs split:inat_splits)
    1.55 +by (simp add: inat_defs split:inat_splits)
    1.56  
    1.57  lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
    1.58 -  by (simp add: inat_defs split:inat_splits)
    1.59 +by (simp add: inat_defs split:inat_splits)
    1.60  
    1.61  lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
    1.62 -  by (simp add: inat_defs split:inat_splits)
    1.63 +by (simp add: inat_defs split:inat_splits)
    1.64  
    1.65  lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
    1.66 -  by (simp add: inat_defs split:inat_splits)
    1.67 +by (simp add: inat_defs split:inat_splits)
    1.68  
    1.69  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
    1.70 -  by (simp add: neq0_conv inat_defs split:inat_splits)
    1.71 +by (fastsimp simp: inat_defs split:inat_splits)
    1.72  
    1.73  lemma i0_iless_iSuc [simp]: "0 < iSuc n"
    1.74 -  by (simp add: inat_defs split:inat_splits)
    1.75 +by (simp add: inat_defs split:inat_splits)
    1.76  
    1.77  lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
    1.78 -  by (simp add: inat_defs split:inat_splits)
    1.79 +by (simp add: inat_defs split:inat_splits)
    1.80  
    1.81  lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
    1.82 -  by (simp add: inat_defs split:inat_splits)
    1.83 +by (simp add: inat_defs split:inat_splits)
    1.84  
    1.85  lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
    1.86 -  by (simp add: inat_defs split:inat_splits)
    1.87 +by (simp add: inat_defs split:inat_splits)
    1.88  
    1.89  
    1.90  
    1.91  lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
    1.92 -  by (simp add: inat_defs split:inat_splits, arith)
    1.93 +by (simp add: inat_defs split:inat_splits, arith)
    1.94  
    1.95  lemma ile_refl [simp]: "n \<le> (n::inat)"
    1.96 -  by (simp add: inat_defs split:inat_splits)
    1.97 +by (simp add: inat_defs split:inat_splits)
    1.98  
    1.99  lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
   1.100 -  by (simp add: inat_defs split:inat_splits)
   1.101 +by (simp add: inat_defs split:inat_splits)
   1.102  
   1.103  lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
   1.104 -  by (simp add: inat_defs split:inat_splits)
   1.105 +by (simp add: inat_defs split:inat_splits)
   1.106  
   1.107  lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
   1.108 -  by (simp add: inat_defs split:inat_splits)
   1.109 +by (simp add: inat_defs split:inat_splits)
   1.110  
   1.111  lemma Infty_ub [simp]: "n \<le> \<infinity>"
   1.112 -  by (simp add: inat_defs split:inat_splits)
   1.113 +by (simp add: inat_defs split:inat_splits)
   1.114  
   1.115  lemma i0_lb [simp]: "(0::inat) \<le> n"
   1.116 -  by (simp add: inat_defs split:inat_splits)
   1.117 +by (simp add: inat_defs split:inat_splits)
   1.118  
   1.119  lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
   1.120 -  by (simp add: inat_defs split:inat_splits)
   1.121 +by (simp add: inat_defs split:inat_splits)
   1.122  
   1.123  lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
   1.124 -  by (simp add: inat_defs split:inat_splits, arith)
   1.125 +by (simp add: inat_defs split:inat_splits, arith)
   1.126  
   1.127  lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
   1.128 -  by (simp add: inat_defs split:inat_splits)
   1.129 +by (simp add: inat_defs split:inat_splits)
   1.130  
   1.131  lemma ileI1: "m < n ==> iSuc m \<le> n"
   1.132 -  by (simp add: inat_defs split:inat_splits)
   1.133 +by (simp add: inat_defs split:inat_splits)
   1.134  
   1.135  lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
   1.136 -  by (simp add: inat_defs split:inat_splits, arith)
   1.137 +by (simp add: inat_defs split:inat_splits, arith)
   1.138  
   1.139  lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
   1.140 -  by (simp add: inat_defs split:inat_splits)
   1.141 +by (simp add: inat_defs split:inat_splits)
   1.142  
   1.143  lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
   1.144 -  by (simp add: inat_defs split:inat_splits, arith)
   1.145 +by (simp add: inat_defs split:inat_splits, arith)
   1.146  
   1.147  lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   1.148 -  by (simp add: inat_defs split:inat_splits)
   1.149 +by (simp add: inat_defs split:inat_splits)
   1.150  
   1.151  lemma ile_iSuc [simp]: "n \<le> iSuc n"
   1.152 -  by (simp add: inat_defs split:inat_splits)
   1.153 +by (simp add: inat_defs split:inat_splits)
   1.154  
   1.155  lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
   1.156 -  by (simp add: inat_defs split:inat_splits)
   1.157 +by (simp add: inat_defs split:inat_splits)
   1.158  
   1.159  lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   1.160 -  apply (induct_tac k)
   1.161 -   apply (simp (no_asm) only: Fin_0)
   1.162 -   apply (fast intro: ile_iless_trans i0_lb)
   1.163 -  apply (erule exE)
   1.164 -  apply (drule spec)
   1.165 -  apply (erule exE)
   1.166 -  apply (drule ileI1)
   1.167 -  apply (rule iSuc_Fin [THEN subst])
   1.168 -  apply (rule exI)
   1.169 -  apply (erule (1) ile_iless_trans)
   1.170 -  done
   1.171 +apply (induct_tac k)
   1.172 + apply (simp (no_asm) only: Fin_0)
   1.173 + apply (fast intro: ile_iless_trans i0_lb)
   1.174 +apply (erule exE)
   1.175 +apply (drule spec)
   1.176 +apply (erule exE)
   1.177 +apply (drule ileI1)
   1.178 +apply (rule iSuc_Fin [THEN subst])
   1.179 +apply (rule exI)
   1.180 +apply (erule (1) ile_iless_trans)
   1.181 +done
   1.182  
   1.183  end