moved class wellorder to theory Orderings
authorhaftmann
Mon Aug 11 14:49:53 2008 +0200 (2008-08-11)
changeset 2782352971512d1a2
parent 27822 a6319699e517
child 27824 97d2a3797ce0
moved class wellorder to theory Orderings
NEWS
src/HOL/Datatype.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Sun Aug 10 12:38:26 2008 +0200
     1.2 +++ b/NEWS	Mon Aug 11 14:49:53 2008 +0200
     1.3 @@ -40,6 +40,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL/Orderings: class "wellorder" moved here, with explicit induction rule
     1.8 +"less_induct" as assumption.  For instantiation of "wellorder" by means
     1.9 +of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
    1.10 +
    1.11  * HOL/Orderings: added class "preorder" as superclass of "order".
    1.12  INCOMPATIBILITY: Instantiation proofs for order, linorder
    1.13  etc. slightly changed.  Some theorems named order_class.* now named
    1.14 @@ -5671,4 +5675,5 @@
    1.15  
    1.16  :mode=text:wrap=hard:maxLineLen=72:
    1.17  
    1.18 +
    1.19  $Id$
     2.1 --- a/src/HOL/Datatype.thy	Sun Aug 10 12:38:26 2008 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Mon Aug 11 14:49:53 2008 +0200
     2.3 @@ -9,14 +9,9 @@
     2.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     2.5  
     2.6  theory Datatype
     2.7 -imports Finite_Set Wellfounded
     2.8 +imports Finite_Set
     2.9  begin
    2.10  
    2.11 -lemma size_bool [code func]:
    2.12 -  "size (b\<Colon>bool) = 0" by (cases b) auto
    2.13 -
    2.14 -declare "prod.size" [noatp]
    2.15 -
    2.16  typedef (Node)
    2.17    ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    2.18      --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
     3.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sun Aug 10 12:38:26 2008 +0200
     3.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 11 14:49:53 2008 +0200
     3.3 @@ -317,13 +317,9 @@
     3.4  
     3.5  instance inat :: wellorder
     3.6  proof
     3.7 -  show "wf {(x::inat, y::inat). x < y}"
     3.8 -  proof (rule wfUNIVI)
     3.9 -    fix P and x :: inat
    3.10 -    assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x"
    3.11 -    hence 1: "!!x::inat. ALL y. y < x --> P y ==> P x" by fast
    3.12 -    thus "P x" by (rule inat_less_induct)
    3.13 -  qed
    3.14 +  fix P and n
    3.15 +  assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
    3.16 +  show "P n" by (blast intro: inat_less_induct hyp)
    3.17  qed
    3.18  
    3.19  
     4.1 --- a/src/HOL/Nat.thy	Sun Aug 10 12:38:26 2008 +0200
     4.2 +++ b/src/HOL/Nat.thy	Mon Aug 11 14:49:53 2008 +0200
     4.3 @@ -733,31 +733,66 @@
     4.4  
     4.5  text {* Complete induction, aka course-of-values induction *}
     4.6  
     4.7 -lemma less_induct [case_names less]:
     4.8 -  fixes P :: "nat \<Rightarrow> bool"
     4.9 -  assumes step: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
    4.10 -  shows "P a"
    4.11 -proof - 
    4.12 -  have "\<And>z. z\<le>a \<Longrightarrow> P z"
    4.13 -  proof (induct a)
    4.14 -    case (0 z)
    4.15 +instance nat :: wellorder proof
    4.16 +  fix P and n :: nat
    4.17 +  assume step: "\<And>n::nat. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n"
    4.18 +  have "\<And>q. q \<le> n \<Longrightarrow> P q"
    4.19 +  proof (induct n)
    4.20 +    case (0 n)
    4.21      have "P 0" by (rule step) auto
    4.22      thus ?case using 0 by auto
    4.23    next
    4.24 -    case (Suc x z)
    4.25 -    then have "z \<le> x \<or> z = Suc x" by (simp add: le_Suc_eq)
    4.26 +    case (Suc m n)
    4.27 +    then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq)
    4.28      thus ?case
    4.29      proof
    4.30 -      assume "z \<le> x" thus "P z" by (rule Suc(1))
    4.31 +      assume "n \<le> m" thus "P n" by (rule Suc(1))
    4.32      next
    4.33 -      assume z: "z = Suc x"
    4.34 -      show "P z"
    4.35 -        by (rule step) (rule Suc(1), simp add: z le_simps)
    4.36 +      assume n: "n = Suc m"
    4.37 +      show "P n"
    4.38 +        by (rule step) (rule Suc(1), simp add: n le_simps)
    4.39      qed
    4.40    qed
    4.41 -  thus ?thesis by auto
    4.42 +  then show "P n" by auto
    4.43  qed
    4.44  
    4.45 +lemma Least_Suc:
    4.46 +     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    4.47 +  apply (case_tac "n", auto)
    4.48 +  apply (frule LeastI)
    4.49 +  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
    4.50 +  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
    4.51 +  apply (erule_tac [2] Least_le)
    4.52 +  apply (case_tac "LEAST x. P x", auto)
    4.53 +  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
    4.54 +  apply (blast intro: order_antisym)
    4.55 +  done
    4.56 +
    4.57 +lemma Least_Suc2:
    4.58 +   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
    4.59 +  apply (erule (1) Least_Suc [THEN ssubst])
    4.60 +  apply simp
    4.61 +  done
    4.62 +
    4.63 +lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
    4.64 +  apply (cases n)
    4.65 +   apply blast
    4.66 +  apply (rule_tac x="LEAST k. P(k)" in exI)
    4.67 +  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
    4.68 +  done
    4.69 +
    4.70 +lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
    4.71 +  apply (cases n)
    4.72 +   apply blast
    4.73 +  apply (frule (1) ex_least_nat_le)
    4.74 +  apply (erule exE)
    4.75 +  apply (case_tac k)
    4.76 +   apply simp
    4.77 +  apply (rename_tac k1)
    4.78 +  apply (rule_tac x=k1 in exI)
    4.79 +  apply (auto simp add: less_eq_Suc_le)
    4.80 +  done
    4.81 +
    4.82  lemma nat_less_induct:
    4.83    assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
    4.84    using assms less_induct by blast
     5.1 --- a/src/HOL/Orderings.thy	Sun Aug 10 12:38:26 2008 +0200
     5.2 +++ b/src/HOL/Orderings.thy	Mon Aug 11 14:49:53 2008 +0200
     5.3 @@ -1109,4 +1109,71 @@
     5.4  apply (blast intro: order_antisym)
     5.5  done
     5.6  
     5.7 +
     5.8 +subsection {* Dense orders *}
     5.9 +
    5.10 +class dense_linear_order = linorder + 
    5.11 +  assumes gt_ex: "\<exists>y. x < y" 
    5.12 +  and lt_ex: "\<exists>y. y < x"
    5.13 +  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
    5.14 +  (*see further theory Dense_Linear_Order*)
    5.15 +
    5.16 +
    5.17 +subsection {* Wellorders *}
    5.18 +
    5.19 +class wellorder = linorder +
    5.20 +  assumes less_induct [case_names less]: "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
    5.21 +begin
    5.22 +
    5.23 +lemma wellorder_Least_lemma:
    5.24 +  fixes k :: 'a
    5.25 +  assumes "P k"
    5.26 +  shows "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k"
    5.27 +proof -
    5.28 +  have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
    5.29 +  using assms proof (induct k rule: less_induct)
    5.30 +    case (less x) then have "P x" by simp
    5.31 +    show ?case proof (rule classical)
    5.32 +      assume assm: "\<not> (P (LEAST a. P a) \<and> (LEAST a. P a) \<le> x)"
    5.33 +      have "\<And>y. P y \<Longrightarrow> x \<le> y"
    5.34 +      proof (rule classical)
    5.35 +        fix y
    5.36 +        assume "P y" and "\<not> x \<le> y" 
    5.37 +        with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    5.38 +          by (auto simp add: not_le)
    5.39 +        with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    5.40 +          by auto
    5.41 +        then show "x \<le> y" by auto
    5.42 +      qed
    5.43 +      with `P x` have Least: "(LEAST a. P a) = x"
    5.44 +        by (rule Least_equality)
    5.45 +      with `P x` show ?thesis by simp
    5.46 +    qed
    5.47 +  qed
    5.48 +  then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
    5.49 +qed
    5.50 +
    5.51 +lemmas LeastI   = wellorder_Least_lemma(1)
    5.52 +lemmas Least_le = wellorder_Least_lemma(2)
    5.53 +
    5.54 +-- "The following 3 lemmas are due to Brian Huffman"
    5.55 +lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
    5.56 +  by (erule exE) (erule LeastI)
    5.57 +
    5.58 +lemma LeastI2:
    5.59 +  "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
    5.60 +  by (blast intro: LeastI)
    5.61 +
    5.62 +lemma LeastI2_ex:
    5.63 +  "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
    5.64 +  by (blast intro: LeastI_ex)
    5.65 +
    5.66 +lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
    5.67 +apply (simp (no_asm_use) add: not_le [symmetric])
    5.68 +apply (erule contrapos_nn)
    5.69 +apply (erule Least_le)
    5.70 +done
    5.71 +
    5.72 +end  
    5.73 +
    5.74  end
     6.1 --- a/src/HOL/Wellfounded.thy	Sun Aug 10 12:38:26 2008 +0200
     6.2 +++ b/src/HOL/Wellfounded.thy	Mon Aug 11 14:49:53 2008 +0200
     6.3 @@ -45,10 +45,6 @@
     6.4  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
     6.5    "acyclicP r == acyclic {(x, y). r x y}"
     6.6  
     6.7 -class wellorder = linorder +
     6.8 -  assumes wf: "wf {(x, y). x < y}"
     6.9 -
    6.10 -
    6.11  lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
    6.12    by (simp add: wfP_def)
    6.13  
    6.14 @@ -90,6 +86,18 @@
    6.15  (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
    6.16  lemmas wf_irrefl = wf_not_refl [elim_format]
    6.17  
    6.18 +lemma wf_wellorderI:
    6.19 +  assumes wf: "wf {(x::'a::ord, y). x < y}"
    6.20 +  assumes lin: "OFCLASS('a::ord, linorder_class)"
    6.21 +  shows "OFCLASS('a::ord, wellorder_class)"
    6.22 +using lin by (rule wellorder_class.intro)
    6.23 +  (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
    6.24 +
    6.25 +lemma (in wellorder) wf:
    6.26 +  "wf {(x, y). x < y}"
    6.27 +unfolding wf_def by (blast intro: less_induct)
    6.28 +
    6.29 +
    6.30  subsection {* Basic Results *}
    6.31  
    6.32  text{*transitive closure of a well-founded relation is well-founded! *}
    6.33 @@ -460,43 +468,6 @@
    6.34  *}
    6.35  
    6.36  
    6.37 -subsection {*LEAST and wellorderings*}
    6.38 -
    6.39 -text{* See also @{text wf_linord_ex_has_least} and its consequences in
    6.40 - @{text Wellfounded_Relations.ML}*}
    6.41 -
    6.42 -lemma wellorder_Least_lemma [rule_format]:
    6.43 -     "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
    6.44 -apply (rule_tac a = k in wf [THEN wf_induct])
    6.45 -apply (rule impI)
    6.46 -apply (rule classical)
    6.47 -apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
    6.48 -apply (auto simp add: linorder_not_less [symmetric])
    6.49 -done
    6.50 -
    6.51 -lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
    6.52 -lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
    6.53 -
    6.54 --- "The following 3 lemmas are due to Brian Huffman"
    6.55 -lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
    6.56 -apply (erule exE)
    6.57 -apply (erule LeastI)
    6.58 -done
    6.59 -
    6.60 -lemma LeastI2:
    6.61 -  "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
    6.62 -by (blast intro: LeastI)
    6.63 -
    6.64 -lemma LeastI2_ex:
    6.65 -  "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
    6.66 -by (blast intro: LeastI_ex)
    6.67 -
    6.68 -lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
    6.69 -apply (simp (no_asm_use) add: linorder_not_le [symmetric])
    6.70 -apply (erule contrapos_nn)
    6.71 -apply (erule Least_le)
    6.72 -done
    6.73 -
    6.74  subsection {* @{typ nat} is well-founded *}
    6.75  
    6.76  lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
    6.77 @@ -550,52 +521,6 @@
    6.78  lemma wf_less: "wf {(x, y::nat). x < y}"
    6.79    using wf_less_than by (simp add: less_than_def less_eq [symmetric])
    6.80  
    6.81 -text {* Type @{typ nat} is a wellfounded order *}
    6.82 -
    6.83 -instance nat :: wellorder
    6.84 -  by intro_classes
    6.85 -    (assumption |
    6.86 -      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
    6.87 -
    6.88 -text {* @{text LEAST} theorems for type @{typ nat}*}
    6.89 -
    6.90 -lemma Least_Suc:
    6.91 -     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    6.92 -  apply (case_tac "n", auto)
    6.93 -  apply (frule LeastI)
    6.94 -  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
    6.95 -  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
    6.96 -  apply (erule_tac [2] Least_le)
    6.97 -  apply (case_tac "LEAST x. P x", auto)
    6.98 -  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
    6.99 -  apply (blast intro: order_antisym)
   6.100 -  done
   6.101 -
   6.102 -lemma Least_Suc2:
   6.103 -   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   6.104 -  apply (erule (1) Least_Suc [THEN ssubst])
   6.105 -  apply simp
   6.106 -  done
   6.107 -
   6.108 -lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
   6.109 -  apply (cases n)
   6.110 -   apply blast
   6.111 -  apply (rule_tac x="LEAST k. P(k)" in exI)
   6.112 -  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   6.113 -  done
   6.114 -
   6.115 -lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
   6.116 -  apply (cases n)
   6.117 -   apply blast
   6.118 -  apply (frule (1) ex_least_nat_le)
   6.119 -  apply (erule exE)
   6.120 -  apply (case_tac k)
   6.121 -   apply simp
   6.122 -  apply (rename_tac k1)
   6.123 -  apply (rule_tac x=k1 in exI)
   6.124 -  apply fastsimp
   6.125 -  done
   6.126 -
   6.127  
   6.128  subsection {* Accessible Part *}
   6.129  
   6.130 @@ -914,8 +839,12 @@
   6.131  
   6.132  setup Size.setup
   6.133  
   6.134 +lemma size_bool [code func]:
   6.135 +  "size (b\<Colon>bool) = 0" by (cases b) auto
   6.136 +
   6.137  lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   6.138    by (induct n) simp_all
   6.139  
   6.140 +declare "prod.size" [noatp]
   6.141  
   6.142  end