--- a/CONTRIBUTORS Tue Dec 01 14:19:25 2015 +0000
+++ b/CONTRIBUTORS Tue Dec 01 17:18:34 2015 +0100
@@ -6,6 +6,10 @@
Contributions to this Isabelle version
--------------------------------------
+* Autumn 2015: Andreas Lochbihler
+ Bourbaki-Witt fixpoint theorem for increasing functions on
+ chain-complete partial orders.
+
* Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
A large number of additional binomial identities.
--- a/NEWS Tue Dec 01 14:19:25 2015 +0000
+++ b/NEWS Tue Dec 01 17:18:34 2015 +0100
@@ -581,6 +581,10 @@
less_eq_multiset_def
INCOMPATIBILITY
+* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt
+fixpoint theorem for increasing functions in chain-complete partial
+orders.
+
* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Tue Dec 01 17:18:34 2015 +0100
@@ -0,0 +1,252 @@
+(* Title: Bourbaki_Witt_Fixpoint.thy
+ Author: Andreas Lochbihler, ETH Zurich *)
+
+section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
+
+theory Bourbaki_Witt_Fixpoint imports Main begin
+
+lemma ChainsI [intro?]:
+ "(\<And>a b. \<lbrakk> a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> (a, b) \<in> r \<or> (b, a) \<in> r) \<Longrightarrow> Y \<in> Chains r"
+unfolding Chains_def by blast
+
+lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
+by(auto simp add: Chains_def)
+
+lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
+ unfolding Field_def by auto
+
+lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
+by(auto simp add: Chains_def intro: FieldI1 FieldI2)
+
+lemma partial_order_on_trans:
+ "\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r"
+by(auto simp add: order_on_defs dest: transD)
+
+locale bourbaki_witt_fixpoint =
+ fixes lub :: "'a set \<Rightarrow> 'a"
+ and leq :: "('a \<times> 'a) set"
+ and f :: "'a \<Rightarrow> 'a"
+ assumes po: "Partial_order leq"
+ and lub_least: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> (x, z) \<in> leq \<rbrakk> \<Longrightarrow> (lub M, z) \<in> leq"
+ and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq"
+ and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq"
+ and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq"
+begin
+
+lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq"
+by(rule partial_order_on_trans[OF po])
+
+lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq"
+using po by(simp add: order_on_defs refl_on_def)
+
+lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y"
+using po by(simp add: order_on_defs antisym_def)
+
+inductive_set iterates_above :: "'a \<Rightarrow> 'a set"
+ for a
+where
+ base: "a \<in> iterates_above a"
+| step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a"
+| Sup: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above a \<rbrakk> \<Longrightarrow> lub M \<in> iterates_above a"
+
+definition fixp_above :: "'a \<Rightarrow> 'a"
+where "fixp_above a = lub (iterates_above a)"
+
+context
+ notes leq_refl [intro!, simp]
+ and base [intro]
+ and step [intro]
+ and Sup [intro]
+ and leq_trans [trans]
+begin
+
+lemma iterates_above_le_f: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq"
+by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+
+
+lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq"
+by(drule (1) iterates_above_le_f)(rule FieldI1)
+
+lemma iterates_above_ge:
+ assumes y: "y \<in> iterates_above a"
+ and a: "a \<in> Field leq"
+ shows "(a, y) \<in> leq"
+using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])
+
+lemma iterates_above_lub:
+ assumes M: "M \<in> Chains leq"
+ and nempty: "M \<noteq> {}"
+ and upper: "\<And>y. y \<in> M \<Longrightarrow> \<exists>z \<in> M. (y, z) \<in> leq \<and> z \<in> iterates_above a"
+ shows "lub M \<in> iterates_above a"
+proof -
+ let ?M = "M \<inter> iterates_above a"
+ from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp
+ have "?M \<noteq> {}" using nempty by(auto dest: upper)
+ with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast
+ also have "lub ?M = lub M" using nempty
+ by(intro leq_antisym)(blast intro!: lub_least[OF M] lub_least[OF M'] intro: lub_upper[OF M'] lub_upper[OF M] leq_trans dest: upper)+
+ finally show ?thesis .
+qed
+
+lemma iterates_above_successor:
+ assumes y: "y \<in> iterates_above a"
+ and a: "a \<in> Field leq"
+ shows "y = a \<or> y \<in> iterates_above (f a)"
+using y
+proof induction
+ case base thus ?case by simp
+next
+ case (step x) thus ?case by auto
+next
+ case (Sup M)
+ show ?case
+ proof(cases "\<exists>x. M \<subseteq> {x}")
+ case True
+ with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto
+ have "lub M = y"
+ by(rule leq_antisym)(auto intro!: lub_upper Sup lub_least ChainsI simp add: a M Sup.hyps(3)[of y, THEN iterates_above_Field] dest: iterates_above_Field)
+ with Sup.IH[of y] M show ?thesis by simp
+ next
+ case False
+ from Sup(1-2) have "lub M \<in> iterates_above (f a)"
+ proof(rule iterates_above_lub)
+ fix y
+ assume y: "y \<in> M"
+ from Sup.IH[OF this] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (f a)"
+ proof
+ assume "y = a"
+ from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI)
+ with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
+ show ?thesis by(auto dest: iterates_above_ge intro: a)
+ next
+ assume "y \<in> iterates_above (f a)"
+ moreover with increasing[OF a] have "y \<in> Field leq"
+ by(auto dest!: iterates_above_Field intro: FieldI2)
+ ultimately show ?thesis using y by(auto)
+ qed
+ qed
+ thus ?thesis by simp
+ qed
+qed
+
+lemma iterates_above_Sup_aux:
+ assumes M: "M \<in> Chains leq" "M \<noteq> {}"
+ and M': "M' \<in> Chains leq" "M' \<noteq> {}"
+ and comp: "\<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x"
+ shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
+proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')")
+ case True
+ then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast
+ have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field)
+ have "lub M \<in> iterates_above (lub M')" using M
+ proof(rule iterates_above_lub)
+ fix y
+ assume y: "y \<in> M"
+ from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')"
+ proof
+ assume "y \<in> iterates_above (lub M')"
+ from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
+ next
+ assume "lub M' \<in> iterates_above y"
+ hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
+ also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge)
+ finally show ?thesis using x by blast
+ qed
+ qed
+ thus ?thesis ..
+next
+ case False
+ have "(lub M, lub M') \<in> leq" using M
+ proof(rule lub_least)
+ fix x
+ assume x: "x \<in> M"
+ from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto
+ moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD)
+ ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge)
+ qed
+ thus ?thesis ..
+qed
+
+lemma iterates_above_triangle:
+ assumes x: "x \<in> iterates_above a"
+ and y: "y \<in> iterates_above a"
+ and a: "a \<in> Field leq"
+ shows "x \<in> iterates_above y \<or> y \<in> iterates_above x"
+using x y
+proof(induction arbitrary: y)
+ case base then show ?case by simp
+next
+ case (step x) thus ?case using a
+ by(auto dest: iterates_above_successor intro: iterates_above_Field)
+next
+ case x: (Sup M)
+ hence lub: "lub M \<in> iterates_above a" by blast
+ from \<open>y \<in> iterates_above a\<close> show ?case
+ proof(induction)
+ case base show ?case using lub by simp
+ next
+ case (step y) thus ?case using a
+ by(auto dest: iterates_above_successor intro: iterates_above_Field)
+ next
+ case y: (Sup M')
+ hence lub': "lub M' \<in> iterates_above a" by blast
+ have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x
+ using that lub' by(rule x.IH)
+ with x(1-2) y(1-2) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
+ by(rule iterates_above_Sup_aux)
+ moreover from y(1-2) x(1-2) have "(lub M', lub M) \<in> leq \<or> lub M' \<in> iterates_above (lub M)"
+ by(rule iterates_above_Sup_aux)(blast dest: y.IH)
+ ultimately show ?case by(auto 4 3 dest: leq_antisym)
+ qed
+qed
+
+lemma chain_iterates_above:
+ assumes a: "a \<in> Field leq"
+ shows "iterates_above a \<in> Chains leq" (is "?C \<in> _")
+proof (rule ChainsI)
+ fix x y
+ assume "x \<in> ?C" "y \<in> ?C"
+ hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle)
+ moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field)
+ moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field)
+ ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge)
+qed
+
+lemma fixp_iterates_above: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> iterates_above a"
+unfolding fixp_above_def by(rule iterates_above.Sup)(blast intro: chain_iterates_above)+
+
+lemma
+ assumes b: "b \<in> iterates_above a"
+ and fb: "f b = b"
+ and x: "x \<in> iterates_above a"
+ and a: "a \<in> Field leq"
+ shows "b \<in> iterates_above x"
+using x
+proof(induction)
+ case base show ?case using b by simp
+next
+ case (step x)
+ from step.hyps a have "x \<in> Field leq" by(rule iterates_above_Field)
+ from iterates_above_successor[OF step.IH this] fb
+ show ?case by(auto)
+next
+ case (Sup M)
+ oops
+
+lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
+using fixp_iterates_above by(rule iterates_above_Field)
+
+lemma fixp_above_unfold:
+ assumes a: "a \<in> Field leq"
+ shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
+proof(rule leq_antisym)
+ show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing)
+
+ have "f ?a \<in> iterates_above a" using fixp_iterates_above[OF a] by(rule iterates_above.step)
+ with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq" unfolding fixp_above_def by(rule lub_upper)
+qed
+
+end
+
+end
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Library.thy Tue Dec 01 14:19:25 2015 +0000
+++ b/src/HOL/Library/Library.thy Tue Dec 01 17:18:34 2015 +0100
@@ -6,6 +6,7 @@
Bit
BNF_Axiomatization
Boolean_Algebra
+ Bourbaki_Witt_Fixpoint
Char_ord
Code_Test
ContNotDenum
--- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Dec 01 14:19:25 2015 +0000
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Dec 01 17:18:34 2015 +0100
@@ -93,14 +93,14 @@
lemma rtrancl_path_distinct:
assumes xy: "rtrancl_path r x xs y"
- obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')"
+ obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs"
using xy
proof (induct xs rule: measure_induct_rule [of length])
case (less xs)
show ?case
proof (cases "distinct (x # xs)")
case True
- with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less)
+ with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp
next
case False
then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
@@ -112,11 +112,11 @@
case Nil
with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
by auto
- from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y"
+ from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs"
by (auto elim: rtrancl_path_appendE)
from xs have "length cs < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: cs less(2))+
+ by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+
next
case (Cons d ds)
with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
@@ -127,9 +127,10 @@
from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
by (rule rtrancl_path_trans)
+ from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto
from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: xy less(2))+
+ by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+
qed
qed
qed
@@ -206,4 +207,23 @@
code_pred rtranclp
using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
+lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> RangeP R z"
+by(induction rule: rtrancl_path.induct) auto
+
+lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> RangeP R y"
+by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
+
+lemma rtrancl_path_nth:
+ "\<lbrakk> rtrancl_path R x xs y; i < length xs \<rbrakk> \<Longrightarrow> R ((x # xs) ! i) (xs ! i)"
+proof(induction arbitrary: i rule: rtrancl_path.induct)
+ case step thus ?case by(cases i) simp_all
+qed simp
+
+lemma rtrancl_path_last: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> last xs = y"
+by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
+
+lemma rtrancl_path_mono:
+ "\<lbrakk> rtrancl_path R x p y; \<And>x y. R x y \<Longrightarrow> S x y \<rbrakk> \<Longrightarrow> rtrancl_path S x p y"
+by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros)
+
end
\ No newline at end of file