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.8 +by(simp add: Chains_def chain_def)
     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
    1.49 +proof(rule ccpo.admissibleD)
    1.50 +  have "a \<in> iterates_above a" ..
    1.51 +  then show "iterates_above a \<noteq> {}" by(auto)
    1.52 +  show "P x" if "x \<in> iterates_above a" for x using that
    1.53 +    by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm])
    1.54 +qed
    1.55 +
    1.56  end
    1.57  
    1.58  end