src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
 changeset 62622 7c56e4a1ad0c parent 62390 842917225d56 child 62647 3cf0edded065
```     1.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Mon Mar 14 21:37:49 2016 +0100
1.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Mar 15 08:34:04 2016 +0100
1.3 @@ -22,6 +22,9 @@
1.4  lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
1.5  by(auto simp add: Chains_def intro: FieldI1 FieldI2)
1.6
1.7 +lemma in_Chains_conv_chain: "M \<in> Chains r \<longleftrightarrow> Complete_Partial_Order.chain (\<lambda>x y. (x, y) \<in> r) M"
1.9 +
1.10  lemma partial_order_on_trans:
1.11    "\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r"
1.12  by(auto simp add: order_on_defs dest: transD)
1.13 @@ -218,24 +221,6 @@
1.14  lemma fixp_iterates_above: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> iterates_above a"
1.15  unfolding fixp_above_def by(rule iterates_above.Sup)(blast intro: chain_iterates_above)+
1.16
1.17 -lemma
1.18 -  assumes b: "b \<in> iterates_above a"
1.19 -  and fb: "f b = b"
1.20 -  and x: "x \<in> iterates_above a"
1.21 -  and a: "a \<in> Field leq"
1.22 -  shows "b \<in> iterates_above x"
1.23 -using x
1.24 -proof(induction)
1.25 -  case base show ?case using b by simp
1.26 -next
1.27 -  case (step x)
1.28 -  from step.hyps a have "x \<in> Field leq" by(rule iterates_above_Field)
1.29 -  from iterates_above_successor[OF step.IH this] fb
1.30 -  show ?case by(auto)
1.31 -next
1.32 -  case (Sup M)
1.33 -  oops
1.34 -
1.35  lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
1.36  using fixp_iterates_above by(rule iterates_above_Field)
1.37
1.38 @@ -251,6 +236,20 @@
1.39
1.40  end
1.41
1.42 +lemma fixp_induct [case_names adm closed base step]:
1.43 +  assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
1.44 +  and a: "a \<in> Field leq"
1.45 +  and base: "P a"
1.46 +  and step: "\<And>x. P x \<Longrightarrow> P (f x)"
1.47 +  shows "P (fixp_above a)"
1.48 +using adm chain_iterates_above[OF a] unfolding fixp_above_def in_Chains_conv_chain