--- a/NEWS Sun Aug 10 12:38:26 2008 +0200
+++ b/NEWS Mon Aug 11 14:49:53 2008 +0200
@@ -40,6 +40,10 @@
*** HOL ***
+* HOL/Orderings: class "wellorder" moved here, with explicit induction rule
+"less_induct" as assumption. For instantiation of "wellorder" by means
+of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY.
+
* HOL/Orderings: added class "preorder" as superclass of "order".
INCOMPATIBILITY: Instantiation proofs for order, linorder
etc. slightly changed. Some theorems named order_class.* now named
@@ -5671,4 +5675,5 @@
:mode=text:wrap=hard:maxLineLen=72:
+
$Id$
--- a/src/HOL/Datatype.thy Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Datatype.thy Mon Aug 11 14:49:53 2008 +0200
@@ -9,14 +9,9 @@
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
theory Datatype
-imports Finite_Set Wellfounded
+imports Finite_Set
begin
-lemma size_bool [code func]:
- "size (b\<Colon>bool) = 0" by (cases b) auto
-
-declare "prod.size" [noatp]
-
typedef (Node)
('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
--{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
--- a/src/HOL/Library/Nat_Infinity.thy Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Aug 11 14:49:53 2008 +0200
@@ -317,13 +317,9 @@
instance inat :: wellorder
proof
- show "wf {(x::inat, y::inat). x < y}"
- proof (rule wfUNIVI)
- fix P and x :: inat
- assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x"
- hence 1: "!!x::inat. ALL y. y < x --> P y ==> P x" by fast
- thus "P x" by (rule inat_less_induct)
- qed
+ fix P and n
+ assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
+ show "P n" by (blast intro: inat_less_induct hyp)
qed
--- a/src/HOL/Nat.thy Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Nat.thy Mon Aug 11 14:49:53 2008 +0200
@@ -733,31 +733,66 @@
text {* Complete induction, aka course-of-values induction *}
-lemma less_induct [case_names less]:
- fixes P :: "nat \<Rightarrow> bool"
- assumes step: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
- shows "P a"
-proof -
- have "\<And>z. z\<le>a \<Longrightarrow> P z"
- proof (induct a)
- case (0 z)
+instance nat :: wellorder proof
+ fix P and n :: nat
+ assume step: "\<And>n::nat. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n"
+ have "\<And>q. q \<le> n \<Longrightarrow> P q"
+ proof (induct n)
+ case (0 n)
have "P 0" by (rule step) auto
thus ?case using 0 by auto
next
- case (Suc x z)
- then have "z \<le> x \<or> z = Suc x" by (simp add: le_Suc_eq)
+ case (Suc m n)
+ then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq)
thus ?case
proof
- assume "z \<le> x" thus "P z" by (rule Suc(1))
+ assume "n \<le> m" thus "P n" by (rule Suc(1))
next
- assume z: "z = Suc x"
- show "P z"
- by (rule step) (rule Suc(1), simp add: z le_simps)
+ assume n: "n = Suc m"
+ show "P n"
+ by (rule step) (rule Suc(1), simp add: n le_simps)
qed
qed
- thus ?thesis by auto
+ then show "P n" by auto
qed
+lemma Least_Suc:
+ "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
+ apply (case_tac "n", auto)
+ apply (frule LeastI)
+ apply (drule_tac P = "%x. P (Suc x) " in LeastI)
+ apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
+ apply (erule_tac [2] Least_le)
+ apply (case_tac "LEAST x. P x", auto)
+ apply (drule_tac P = "%x. P (Suc x) " in Least_le)
+ apply (blast intro: order_antisym)
+ done
+
+lemma Least_Suc2:
+ "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
+ apply (erule (1) Least_Suc [THEN ssubst])
+ apply simp
+ done
+
+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)"
+ apply (cases n)
+ apply blast
+ apply (rule_tac x="LEAST k. P(k)" in exI)
+ apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
+ done
+
+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)"
+ apply (cases n)
+ apply blast
+ apply (frule (1) ex_least_nat_le)
+ apply (erule exE)
+ apply (case_tac k)
+ apply simp
+ apply (rename_tac k1)
+ apply (rule_tac x=k1 in exI)
+ apply (auto simp add: less_eq_Suc_le)
+ done
+
lemma nat_less_induct:
assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
using assms less_induct by blast
--- a/src/HOL/Orderings.thy Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Orderings.thy Mon Aug 11 14:49:53 2008 +0200
@@ -1109,4 +1109,71 @@
apply (blast intro: order_antisym)
done
+
+subsection {* Dense orders *}
+
+class dense_linear_order = linorder +
+ assumes gt_ex: "\<exists>y. x < y"
+ and lt_ex: "\<exists>y. y < x"
+ and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+ (*see further theory Dense_Linear_Order*)
+
+
+subsection {* Wellorders *}
+
+class wellorder = linorder +
+ assumes less_induct [case_names less]: "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
+begin
+
+lemma wellorder_Least_lemma:
+ fixes k :: 'a
+ assumes "P k"
+ shows "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k"
+proof -
+ have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
+ using assms proof (induct k rule: less_induct)
+ case (less x) then have "P x" by simp
+ show ?case proof (rule classical)
+ assume assm: "\<not> (P (LEAST a. P a) \<and> (LEAST a. P a) \<le> x)"
+ have "\<And>y. P y \<Longrightarrow> x \<le> y"
+ proof (rule classical)
+ fix y
+ assume "P y" and "\<not> x \<le> y"
+ with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
+ by (auto simp add: not_le)
+ with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
+ by auto
+ then show "x \<le> y" by auto
+ qed
+ with `P x` have Least: "(LEAST a. P a) = x"
+ by (rule Least_equality)
+ with `P x` show ?thesis by simp
+ qed
+ qed
+ then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
+qed
+
+lemmas LeastI = wellorder_Least_lemma(1)
+lemmas Least_le = wellorder_Least_lemma(2)
+
+-- "The following 3 lemmas are due to Brian Huffman"
+lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
+ by (erule exE) (erule LeastI)
+
+lemma LeastI2:
+ "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
+ by (blast intro: LeastI)
+
+lemma LeastI2_ex:
+ "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
+ by (blast intro: LeastI_ex)
+
+lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
+apply (simp (no_asm_use) add: not_le [symmetric])
+apply (erule contrapos_nn)
+apply (erule Least_le)
+done
+
+end
+
end
--- a/src/HOL/Wellfounded.thy Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Wellfounded.thy Mon Aug 11 14:49:53 2008 +0200
@@ -45,10 +45,6 @@
abbreviation acyclicP :: "('a => 'a => bool) => bool" where
"acyclicP r == acyclic {(x, y). r x y}"
-class wellorder = linorder +
- assumes wf: "wf {(x, y). x < y}"
-
-
lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
by (simp add: wfP_def)
@@ -90,6 +86,18 @@
(* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *)
lemmas wf_irrefl = wf_not_refl [elim_format]
+lemma wf_wellorderI:
+ assumes wf: "wf {(x::'a::ord, y). x < y}"
+ assumes lin: "OFCLASS('a::ord, linorder_class)"
+ shows "OFCLASS('a::ord, wellorder_class)"
+using lin by (rule wellorder_class.intro)
+ (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+
+lemma (in wellorder) wf:
+ "wf {(x, y). x < y}"
+unfolding wf_def by (blast intro: less_induct)
+
+
subsection {* Basic Results *}
text{*transitive closure of a well-founded relation is well-founded! *}
@@ -460,43 +468,6 @@
*}
-subsection {*LEAST and wellorderings*}
-
-text{* See also @{text wf_linord_ex_has_least} and its consequences in
- @{text Wellfounded_Relations.ML}*}
-
-lemma wellorder_Least_lemma [rule_format]:
- "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
-apply (rule_tac a = k in wf [THEN wf_induct])
-apply (rule impI)
-apply (rule classical)
-apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
-apply (auto simp add: linorder_not_less [symmetric])
-done
-
-lemmas LeastI = wellorder_Least_lemma [THEN conjunct1, standard]
-lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
-
--- "The following 3 lemmas are due to Brian Huffman"
-lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
-apply (erule exE)
-apply (erule LeastI)
-done
-
-lemma LeastI2:
- "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
-by (blast intro: LeastI)
-
-lemma LeastI2_ex:
- "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
-by (blast intro: LeastI_ex)
-
-lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
-apply (simp (no_asm_use) add: linorder_not_le [symmetric])
-apply (erule contrapos_nn)
-apply (erule Least_le)
-done
-
subsection {* @{typ nat} is well-founded *}
lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
@@ -550,52 +521,6 @@
lemma wf_less: "wf {(x, y::nat). x < y}"
using wf_less_than by (simp add: less_than_def less_eq [symmetric])
-text {* Type @{typ nat} is a wellfounded order *}
-
-instance nat :: wellorder
- by intro_classes
- (assumption |
- rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
-
-text {* @{text LEAST} theorems for type @{typ nat}*}
-
-lemma Least_Suc:
- "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
- apply (case_tac "n", auto)
- apply (frule LeastI)
- apply (drule_tac P = "%x. P (Suc x) " in LeastI)
- apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
- apply (erule_tac [2] Least_le)
- apply (case_tac "LEAST x. P x", auto)
- apply (drule_tac P = "%x. P (Suc x) " in Least_le)
- apply (blast intro: order_antisym)
- done
-
-lemma Least_Suc2:
- "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
- apply (erule (1) Least_Suc [THEN ssubst])
- apply simp
- done
-
-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)"
- apply (cases n)
- apply blast
- apply (rule_tac x="LEAST k. P(k)" in exI)
- apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
- done
-
-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)"
- apply (cases n)
- apply blast
- apply (frule (1) ex_least_nat_le)
- apply (erule exE)
- apply (case_tac k)
- apply simp
- apply (rename_tac k1)
- apply (rule_tac x=k1 in exI)
- apply fastsimp
- done
-
subsection {* Accessible Part *}
@@ -914,8 +839,12 @@
setup Size.setup
+lemma size_bool [code func]:
+ "size (b\<Colon>bool) = 0" by (cases b) auto
+
lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
by (induct n) simp_all
+declare "prod.size" [noatp]
end