author Andreas Lochbihler Tue, 15 Mar 2016 08:34:04 +0100 changeset 62622 7c56e4a1ad0c parent 62621 a1e73be79c0b child 62623 dbc62f86a1a9
```--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Mon Mar 14 21:37:49 2016 +0100
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Mar 15 08:34:04 2016 +0100
@@ -22,6 +22,9 @@
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 in_Chains_conv_chain: "M \<in> Chains r \<longleftrightarrow> Complete_Partial_Order.chain (\<lambda>x y. (x, y) \<in> r) M"
+
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)
@@ -218,24 +221,6 @@
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)

@@ -251,6 +236,20 @@

end

+lemma fixp_induct [case_names adm closed base step]:
+  assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
+  and a: "a \<in> Field leq"
+  and base: "P a"
+  and step: "\<And>x. P x \<Longrightarrow> P (f x)"
+  shows "P (fixp_above a)"
+using adm chain_iterates_above[OF a] unfolding fixp_above_def in_Chains_conv_chain