proved linorder and wellorder class instances
authorhuffman
Mon Feb 18 02:10:55 2008 +0100 (2008-02-18)
changeset 26089373221497340
parent 26088 9b48d0264ffd
child 26090 ec111fa4f8c5
proved linorder and wellorder class instances
src/HOL/Library/Nat_Infinity.thy
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sun Feb 17 19:04:50 2008 +0100
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Feb 18 02:10:55 2008 +0100
     1.3 @@ -41,7 +41,9 @@
     1.4      | \<infinity>  => False"
     1.5  
     1.6  definition
     1.7 -  ile_def: "(m::inat) \<le> n == \<not> (n < m)"
     1.8 +  ile_def: "m \<le> n ==
     1.9 +    case n of Fin n1 => (case m of Fin m1 => m1 \<le> n1 | \<infinity> => False)
    1.10 +    | \<infinity>  => True"
    1.11  
    1.12  instance ..
    1.13  
    1.14 @@ -83,20 +85,43 @@
    1.15  
    1.16  subsection "Ordering relations"
    1.17  
    1.18 +instance inat :: linorder
    1.19 +proof
    1.20 +  fix x :: inat
    1.21 +  show "x \<le> x"
    1.22 +    by (simp add: inat_defs split: inat_splits)
    1.23 +next
    1.24 +  fix x y :: inat
    1.25 +  assume "x \<le> y" and "y \<le> x" thus "x = y"
    1.26 +    by (simp add: inat_defs split: inat_splits)
    1.27 +next
    1.28 +  fix x y z :: inat
    1.29 +  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
    1.30 +    by (simp add: inat_defs split: inat_splits)
    1.31 +next
    1.32 +  fix x y :: inat
    1.33 +  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
    1.34 +    by (simp add: inat_defs order_less_le split: inat_splits)
    1.35 +next
    1.36 +  fix x y :: inat
    1.37 +  show "x \<le> y \<or> y \<le> x"
    1.38 +    by (simp add: inat_defs linorder_linear split: inat_splits)
    1.39 +qed
    1.40 +
    1.41  lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
    1.42  by (simp add: inat_defs split:inat_splits)
    1.43  
    1.44  lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
    1.45 -by (simp add: inat_defs split:inat_splits, arith)
    1.46 +by (rule linorder_less_linear)
    1.47  
    1.48 -lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
    1.49 -by (simp add: inat_defs split:inat_splits)
    1.50 +lemma iless_not_refl: "\<not> n < (n::inat)"
    1.51 +by (rule order_less_irrefl)
    1.52  
    1.53  lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
    1.54 -by (simp add: inat_defs split:inat_splits)
    1.55 +by (rule order_less_trans)
    1.56  
    1.57  lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
    1.58 -by (simp add: inat_defs split:inat_splits)
    1.59 +by (rule order_less_not_sym)
    1.60  
    1.61  lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
    1.62  by (simp add: inat_defs split:inat_splits)
    1.63 @@ -125,19 +150,19 @@
    1.64  
    1.65  
    1.66  lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
    1.67 -by (simp add: inat_defs split:inat_splits, arith)
    1.68 +by (rule order_le_less)
    1.69  
    1.70  lemma ile_refl [simp]: "n \<le> (n::inat)"
    1.71 -by (simp add: inat_defs split:inat_splits)
    1.72 +by (rule order_refl)
    1.73  
    1.74  lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
    1.75 -by (simp add: inat_defs split:inat_splits)
    1.76 +by (rule order_trans)
    1.77  
    1.78  lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
    1.79 -by (simp add: inat_defs split:inat_splits)
    1.80 +by (rule order_le_less_trans)
    1.81  
    1.82  lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
    1.83 -by (simp add: inat_defs split:inat_splits)
    1.84 +by (rule order_less_le_trans)
    1.85  
    1.86  lemma Infty_ub [simp]: "n \<le> \<infinity>"
    1.87  by (simp add: inat_defs split:inat_splits)
    1.88 @@ -149,10 +174,10 @@
    1.89  by (simp add: inat_defs split:inat_splits)
    1.90  
    1.91  lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
    1.92 -by (simp add: inat_defs split:inat_splits, arith)
    1.93 +by (simp add: inat_defs split:inat_splits)
    1.94  
    1.95  lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
    1.96 -by (simp add: inat_defs split:inat_splits)
    1.97 +by (rule order_le_neq_trans)
    1.98  
    1.99  lemma ileI1: "m < n ==> iSuc m \<le> n"
   1.100  by (simp add: inat_defs split:inat_splits)
   1.101 @@ -178,7 +203,7 @@
   1.102  lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   1.103  apply (induct_tac k)
   1.104   apply (simp (no_asm) only: Fin_0)
   1.105 - apply (fast intro: ile_iless_trans i0_lb)
   1.106 + apply (fast intro: ile_iless_trans [OF i0_lb])
   1.107  apply (erule exE)
   1.108  apply (drule spec)
   1.109  apply (erule exE)
   1.110 @@ -188,4 +213,47 @@
   1.111  apply (erule (1) ile_iless_trans)
   1.112  done
   1.113  
   1.114 +
   1.115 +subsection "Well-ordering"
   1.116 +
   1.117 +lemma less_FinE:
   1.118 +  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
   1.119 +by (induct n) auto
   1.120 +
   1.121 +lemma less_InftyE:
   1.122 +  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
   1.123 +by (induct n) auto
   1.124 +
   1.125 +lemma inat_less_induct:
   1.126 +  assumes prem: "!!n. \<forall>m::inat. m < n --> P m ==> P n" shows "P n"
   1.127 +proof -
   1.128 +  have P_Fin: "!!k. P (Fin k)"
   1.129 +    apply (rule nat_less_induct)
   1.130 +    apply (rule prem, clarify)
   1.131 +    apply (erule less_FinE, simp)
   1.132 +    done
   1.133 +  show ?thesis
   1.134 +  proof (induct n)
   1.135 +    fix nat
   1.136 +    show "P (Fin nat)" by (rule P_Fin)
   1.137 +  next
   1.138 +    show "P Infty"
   1.139 +      apply (rule prem, clarify)
   1.140 +      apply (erule less_InftyE)
   1.141 +      apply (simp add: P_Fin)
   1.142 +      done
   1.143 +  qed
   1.144 +qed
   1.145 +
   1.146 +instance inat :: wellorder
   1.147 +proof
   1.148 +  show "wf {(x::inat, y::inat). x < y}"
   1.149 +  proof (rule wfUNIVI)
   1.150 +    fix P and x :: inat
   1.151 +    assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x"
   1.152 +    hence 1: "!!x::inat. ALL y. y < x --> P y ==> P x" by fast
   1.153 +    thus "P x" by (rule inat_less_induct)
   1.154 +  qed
   1.155 +qed
   1.156 +
   1.157  end