# HG changeset patch
# User Andreas Lochbihler
# Date 1458027244 -3600
# Node ID 7c56e4a1ad0c160e0b9c9b314790823584405274
# Parent  a1e73be79c0b15451208db0363818d773bfa45af
add fixpoint induction principle

diff -r a1e73be79c0b -r 7c56e4a1ad0c src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- 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"
+by(simp add: Chains_def chain_def)
+
 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
+proof(rule ccpo.admissibleD)
+  have "a \<in> iterates_above a" ..
+  then show "iterates_above a \<noteq> {}" by(auto)
+  show "P x" if "x \<in> iterates_above a" for x using that
+    by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm])
+qed
+
 end
 
 end