src/HOL/Complete_Partial_Order.thy
changeset 53361 1cb7d3c0cf31
parent 46041 1e3ff542e83e
child 54630 9061af4d5ebc
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Sun Sep 01 14:00:05 2013 +0200
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Mon Sep 02 16:28:11 2013 +0200
     1.3 @@ -155,67 +155,72 @@
     1.4    qed (auto intro: ccpo_Sup_least)
     1.5  qed
     1.6  
     1.7 +end
     1.8  
     1.9  subsection {* Fixpoint induction *}
    1.10  
    1.11 -definition
    1.12 -  admissible :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.13 -where
    1.14 -  "admissible P = (\<forall>A. chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    1.15 +setup {* Sign.map_naming (Name_Space.mandatory_path "ccpo") *}
    1.16 +
    1.17 +definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.18 +where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
    1.19  
    1.20  lemma admissibleI:
    1.21 -  assumes "\<And>A. chain (op \<le>) A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (Sup A)"
    1.22 -  shows "admissible P"
    1.23 -using assms unfolding admissible_def by fast
    1.24 +  assumes "\<And>A. chain ord A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
    1.25 +  shows "ccpo.admissible lub ord P"
    1.26 +using assms unfolding ccpo.admissible_def by fast
    1.27  
    1.28  lemma admissibleD:
    1.29 -  assumes "admissible P"
    1.30 -  assumes "chain (op \<le>) A"
    1.31 +  assumes "ccpo.admissible lub ord P"
    1.32 +  assumes "chain ord A"
    1.33    assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
    1.34 -  shows "P (Sup A)"
    1.35 -using assms by (auto simp: admissible_def)
    1.36 +  shows "P (lub A)"
    1.37 +using assms by (auto simp: ccpo.admissible_def)
    1.38  
    1.39 -lemma fixp_induct:
    1.40 -  assumes adm: "admissible P"
    1.41 +setup {* Sign.map_naming Name_Space.parent_path *}
    1.42 +
    1.43 +lemma (in ccpo) fixp_induct:
    1.44 +  assumes adm: "ccpo.admissible Sup (op \<le>) P"
    1.45    assumes mono: "monotone (op \<le>) (op \<le>) f"
    1.46    assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
    1.47    shows "P (fixp f)"
    1.48  unfolding fixp_def using adm chain_iterates[OF mono]
    1.49 -proof (rule admissibleD)
    1.50 +proof (rule ccpo.admissibleD)
    1.51    fix x assume "x \<in> iterates f"
    1.52    thus "P x"
    1.53      by (induct rule: iterates.induct)
    1.54 -      (auto intro: step admissibleD adm)
    1.55 +      (auto intro: step ccpo.admissibleD adm)
    1.56  qed
    1.57  
    1.58 -lemma admissible_True: "admissible (\<lambda>x. True)"
    1.59 -unfolding admissible_def by simp
    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> admissible (\<lambda>x. False)"
    1.64 -unfolding admissible_def chain_def by simp
    1.65 +lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
    1.66 +unfolding ccpo.admissible_def chain_def by simp
    1.67  
    1.68 -lemma admissible_const: "admissible (\<lambda>x. t) = t"
    1.69 +lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t) = t"
    1.70  by (cases t, simp_all add: admissible_True admissible_False)
    1.71  
    1.72  lemma admissible_conj:
    1.73 -  assumes "admissible (\<lambda>x. P x)"
    1.74 -  assumes "admissible (\<lambda>x. Q x)"
    1.75 -  shows "admissible (\<lambda>x. P x \<and> Q x)"
    1.76 -using assms unfolding admissible_def by simp
    1.77 +  assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
    1.78 +  assumes "ccpo.admissible lub ord (\<lambda>x. Q x)"
    1.79 +  shows "ccpo.admissible lub ord (\<lambda>x. P x \<and> Q x)"
    1.80 +using assms unfolding ccpo.admissible_def by simp
    1.81  
    1.82  lemma admissible_all:
    1.83 -  assumes "\<And>y. admissible (\<lambda>x. P x y)"
    1.84 -  shows "admissible (\<lambda>x. \<forall>y. P x y)"
    1.85 -using assms unfolding admissible_def by fast
    1.86 +  assumes "\<And>y. ccpo.admissible lub ord (\<lambda>x. P x y)"
    1.87 +  shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y. P x y)"
    1.88 +using assms unfolding ccpo.admissible_def by fast
    1.89  
    1.90  lemma admissible_ball:
    1.91 -  assumes "\<And>y. y \<in> A \<Longrightarrow> admissible (\<lambda>x. P x y)"
    1.92 -  shows "admissible (\<lambda>x. \<forall>y\<in>A. P x y)"
    1.93 -using assms unfolding admissible_def by fast
    1.94 +  assumes "\<And>y. y \<in> A \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x y)"
    1.95 +  shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y\<in>A. P x y)"
    1.96 +using assms unfolding ccpo.admissible_def by fast
    1.97  
    1.98 -lemma chain_compr: "chain (op \<le>) A \<Longrightarrow> chain (op \<le>) {x \<in> A. P x}"
    1.99 +lemma chain_compr: "chain ord A \<Longrightarrow> chain ord {x \<in> A. P x}"
   1.100  unfolding chain_def by fast
   1.101  
   1.102 +context ccpo begin
   1.103 +
   1.104  lemma admissible_disj_lemma:
   1.105    assumes A: "chain (op \<le>)A"
   1.106    assumes P: "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y"
   1.107 @@ -238,10 +243,10 @@
   1.108  
   1.109  lemma admissible_disj:
   1.110    fixes P Q :: "'a \<Rightarrow> bool"
   1.111 -  assumes P: "admissible (\<lambda>x. P x)"
   1.112 -  assumes Q: "admissible (\<lambda>x. Q x)"
   1.113 -  shows "admissible (\<lambda>x. P x \<or> Q x)"
   1.114 -proof (rule admissibleI)
   1.115 +  assumes P: "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x)"
   1.116 +  assumes Q: "ccpo.admissible Sup (op \<le>) (\<lambda>x. Q x)"
   1.117 +  shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
   1.118 +proof (rule ccpo.admissibleI)
   1.119    fix A :: "'a set" assume A: "chain (op \<le>) A"
   1.120    assume "\<forall>x\<in>A. P x \<or> Q x"
   1.121    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.122 @@ -250,8 +255,8 @@
   1.123      using admissible_disj_lemma [OF A] by fast
   1.124    thus "P (Sup A) \<or> Q (Sup A)"
   1.125      apply (rule disjE, simp_all)
   1.126 -    apply (rule disjI1, rule admissibleD [OF P chain_compr [OF A]], simp)
   1.127 -    apply (rule disjI2, rule admissibleD [OF Q chain_compr [OF A]], simp)
   1.128 +    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp)
   1.129 +    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp)
   1.130      done
   1.131  qed
   1.132  
   1.133 @@ -271,6 +276,6 @@
   1.134      by (rule fixp_lowerbound [OF f'], subst lfp_unfold [OF f], rule order_refl)
   1.135  qed
   1.136  
   1.137 -hide_const (open) iterates fixp admissible
   1.138 +hide_const (open) iterates fixp
   1.139  
   1.140  end