# HG changeset patch
# User Andreas Lochbihler
# Date 1458201405 -3600
# Node ID 3cf0edded065b0ddb0e92136a5d52dc2e55dcd1f
# Parent  28b75a9b044362747528bedd57291c83ac270244
less preconditions

diff -r 28b75a9b0443 -r 3cf0edded065 src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Wed Mar 16 22:42:15 2016 +0100
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Thu Mar 17 08:56:45 2016 +0100
@@ -57,7 +57,13 @@
 | 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)"
+where "fixp_above a = (if a \<in> Field leq then lub (iterates_above a) else a)"
+
+lemma fixp_above_outside: "a \<notin> Field leq \<Longrightarrow> fixp_above a = a"
+by(simp add: fixp_above_def)
+
+lemma fixp_above_inside: "a \<in> Field leq \<Longrightarrow> fixp_above a = lub (iterates_above a)"
+by(simp add: fixp_above_def)
 
 context 
   notes leq_refl [intro!, simp]
@@ -218,8 +224,8 @@
   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 fixp_iterates_above: "fixp_above a \<in> iterates_above a"
+by(auto intro: chain_iterates_above simp add: fixp_above_def)
 
 lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
 using fixp_iterates_above by(rule iterates_above_Field)
@@ -230,25 +236,29 @@
 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)
+  have "f ?a \<in> iterates_above a" using fixp_iterates_above by(rule iterates_above.step)
+  with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq"
+    by(simp add: fixp_above_inside assms lub_upper)
 qed
 
 end
 
-lemma fixp_induct [case_names adm closed base step]:
+lemma fixp_induct [case_names adm 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
+proof(cases "a \<in> Field leq")
+  case True
+  from adm chain_iterates_above[OF True]
+  show ?thesis unfolding fixp_above_inside[OF True] 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
+qed(simp add: fixp_above_outside base)
 
 end