src/HOL/Complete_Partial_Order.thy
changeset 54630 9061af4d5ebc
parent 53361 1cb7d3c0cf31
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Tue Dec 03 02:51:20 2013 +0100
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Thu Dec 05 09:20:32 2013 +0100
     1.3 @@ -50,6 +50,9 @@
     1.4    obtains "ord x y" | "ord y x"
     1.5  using assms unfolding chain_def by fast
     1.6  
     1.7 +lemma chain_empty: "chain ord {}"
     1.8 +by(simp add: chain_def)
     1.9 +
    1.10  subsection {* Chain-complete partial orders *}
    1.11  
    1.12  text {*
    1.13 @@ -119,6 +122,9 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 +lemma bot_in_iterates: "Sup {} \<in> iterates f"
    1.18 +by(auto intro: iterates.Sup simp add: chain_empty)
    1.19 +
    1.20  subsection {* Fixpoint combinator *}
    1.21  
    1.22  definition
    1.23 @@ -162,16 +168,17 @@
    1.24  setup {* Sign.map_naming (Name_Space.mandatory_path "ccpo") *}
    1.25  
    1.26  definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.27 -where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
    1.28 +where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (A \<noteq> {}) \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
    1.29  
    1.30  lemma admissibleI:
    1.31 -  assumes "\<And>A. chain ord A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
    1.32 +  assumes "\<And>A. chain ord A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
    1.33    shows "ccpo.admissible lub ord P"
    1.34  using assms unfolding ccpo.admissible_def by fast
    1.35  
    1.36  lemma admissibleD:
    1.37    assumes "ccpo.admissible lub ord P"
    1.38    assumes "chain ord A"
    1.39 +  assumes "A \<noteq> {}"
    1.40    assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
    1.41    shows "P (lub A)"
    1.42  using assms by (auto simp: ccpo.admissible_def)
    1.43 @@ -181,24 +188,26 @@
    1.44  lemma (in ccpo) fixp_induct:
    1.45    assumes adm: "ccpo.admissible Sup (op \<le>) P"
    1.46    assumes mono: "monotone (op \<le>) (op \<le>) f"
    1.47 +  assumes bot: "P (Sup {})"
    1.48    assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
    1.49    shows "P (fixp f)"
    1.50  unfolding fixp_def using adm chain_iterates[OF mono]
    1.51  proof (rule ccpo.admissibleD)
    1.52 +  show "iterates f \<noteq> {}" using bot_in_iterates by auto
    1.53    fix x assume "x \<in> iterates f"
    1.54    thus "P x"
    1.55      by (induct rule: iterates.induct)
    1.56 -      (auto intro: step ccpo.admissibleD adm)
    1.57 +      (case_tac "M = {}", auto intro: step bot ccpo.admissibleD adm)
    1.58  qed
    1.59  
    1.60  lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
    1.61  unfolding ccpo.admissible_def by simp
    1.62  
    1.63 -lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
    1.64 +(*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
    1.65  unfolding ccpo.admissible_def chain_def by simp
    1.66 -
    1.67 -lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t) = t"
    1.68 -by (cases t, simp_all add: admissible_True admissible_False)
    1.69 +*)
    1.70 +lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t)"
    1.71 +by(auto intro: ccpo.admissibleI)
    1.72  
    1.73  lemma admissible_conj:
    1.74    assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
    1.75 @@ -248,15 +257,16 @@
    1.76    shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
    1.77  proof (rule ccpo.admissibleI)
    1.78    fix A :: "'a set" assume A: "chain (op \<le>) A"
    1.79 -  assume "\<forall>x\<in>A. P x \<or> Q x"
    1.80 -  hence "(\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
    1.81 +  assume "A \<noteq> {}"
    1.82 +    and "\<forall>x\<in>A. P x \<or> Q x"
    1.83 +  hence "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
    1.84      using chainD[OF A] by blast
    1.85 -  hence "Sup A = Sup {x \<in> A. P x} \<or> Sup A = Sup {x \<in> A. Q x}"
    1.86 -    using admissible_disj_lemma [OF A] by fast
    1.87 +  hence "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
    1.88 +    using admissible_disj_lemma [OF A] by blast
    1.89    thus "P (Sup A) \<or> Q (Sup A)"
    1.90      apply (rule disjE, simp_all)
    1.91 -    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp)
    1.92 -    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp)
    1.93 +    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp, simp)
    1.94 +    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp, simp)
    1.95      done
    1.96  qed
    1.97