src/HOL/Library/Nat_Infinity.thy
changeset 23315 df3a7e9ebadb
parent 21404 eb85850d3eb7
child 25112 98824cc791c0
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Jun 11 11:06:00 2007 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Jun 11 11:06:04 2007 +0200
     1.3 @@ -51,120 +51,120 @@
     1.4  subsection "Constructors"
     1.5  
     1.6  lemma Fin_0: "Fin 0 = 0"
     1.7 -  by (simp add: inat_defs split:inat_splits, arith?)
     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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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: inat_defs split:inat_splits, arith?)
    1.71 +  by (simp add: 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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
    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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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, arith?)
   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)