--- a/src/HOLCF/Pcpo.thy Fri May 08 10:59:11 2009 +0200
+++ b/src/HOLCF/Pcpo.thy Fri May 08 13:34:27 2009 +0200
@@ -13,28 +13,28 @@
text {* The class cpo of chain complete partial orders *}
class cpo = po +
- -- {* class axiom: *}
- assumes cpo: "chain S \<Longrightarrow> \<exists>x :: 'a::po. range S <<| x"
+ assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
+begin
text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
-lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
-by (fast dest: cpo elim: lubI)
+lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
+ by (fast dest: cpo elim: lubI)
-lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l"
-by (blast dest: cpo intro: lubI)
+lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
+ by (blast dest: cpo intro: lubI)
text {* Properties of the lub *}
-lemma is_ub_thelub: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
-by (blast dest: cpo intro: lubI [THEN is_ub_lub])
+lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
+ by (blast dest: cpo intro: lubI [THEN is_ub_lub])
lemma is_lub_thelub:
- "\<lbrakk>chain (S::nat \<Rightarrow> 'a::cpo); range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
-by (blast dest: cpo intro: lubI [THEN is_lub_lub])
+ "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
+ by (blast dest: cpo intro: lubI [THEN is_lub_lub])
lemma lub_range_mono:
- "\<lbrakk>range X \<subseteq> range Y; chain Y; chain (X::nat \<Rightarrow> 'a::cpo)\<rbrakk>
+ "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
apply (erule is_lub_thelub)
apply (rule ub_rangeI)
@@ -45,7 +45,7 @@
done
lemma lub_range_shift:
- "chain (Y::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
+ "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
apply (rule antisym_less)
apply (rule lub_range_mono)
apply fast
@@ -62,7 +62,7 @@
done
lemma maxinch_is_thelub:
- "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = ((Y i)::'a::cpo))"
+ "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
apply (rule iffI)
apply (fast intro!: thelubI lub_finch1)
apply (unfold max_in_chain_def)
@@ -75,7 +75,7 @@
text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
lemma lub_mono:
- "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk>
+ "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
apply (erule is_lub_thelub)
apply (rule ub_rangeI)
@@ -87,14 +87,14 @@
text {* the = relation between two chains is preserved by their lubs *}
lemma lub_equal:
- "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<forall>k. X k = Y k\<rbrakk>
+ "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
-by (simp only: expand_fun_eq [symmetric])
+ by (simp only: expand_fun_eq [symmetric])
text {* more results about mono and = of lubs of chains *}
lemma lub_mono2:
- "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain (X::nat \<Rightarrow> 'a::cpo); chain Y\<rbrakk>
+ "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
apply (erule exE)
apply (subgoal_tac "(\<Squnion>i. X (i + Suc j)) \<sqsubseteq> (\<Squnion>i. Y (i + Suc j))")
@@ -104,12 +104,12 @@
done
lemma lub_equal2:
- "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain (X::nat \<Rightarrow> 'a::cpo); chain Y\<rbrakk>
+ "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
-by (blast intro: antisym_less lub_mono2 sym)
+ by (blast intro: antisym_less lub_mono2 sym)
lemma lub_mono3:
- "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
+ "\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
\<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)"
apply (erule is_lub_thelub)
apply (rule ub_rangeI)
@@ -120,7 +120,6 @@
done
lemma ch2ch_lub:
- fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo"
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
@@ -130,7 +129,6 @@
done
lemma diag_lub:
- fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo"
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
@@ -159,12 +157,12 @@
qed
lemma ex_lub:
- fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo"
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)"
-by (simp add: diag_lub 1 2)
+ by (simp add: diag_lub 1 2)
+end
subsection {* Pointed cpos *}
@@ -172,9 +170,9 @@
class pcpo = cpo +
assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
+begin
-definition
- UU :: "'a::pcpo" where
+definition UU :: 'a where
"UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
notation (xsymbols)
@@ -193,6 +191,8 @@
lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
by (rule UU_least [THEN spec])
+end
+
text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
setup {*
@@ -202,6 +202,9 @@
simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
+context pcpo
+begin
+
text {* useful lemmas about @{term \<bottom>} *}
lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
@@ -213,9 +216,6 @@
lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
by (subst eq_UU_iff)
-lemma not_less2not_eq: "\<not> (x::'a::po) \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
-by auto
-
lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
apply (rule allI)
apply (rule UU_I)
@@ -230,49 +230,53 @@
done
lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>"
-by (blast intro: chain_UU_I_inverse)
+ by (blast intro: chain_UU_I_inverse)
lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
-by (blast intro: UU_I)
+ by (blast intro: UU_I)
lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
-by (blast dest: notUU_I chain_mono_less)
+ by (blast dest: notUU_I chain_mono_less)
+
+end
subsection {* Chain-finite and flat cpos *}
text {* further useful classes for HOLCF domains *}
-class finite_po = finite + po
+class chfin = po +
+ assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
+begin
-class chfin = po +
- assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n (Y :: nat => 'a::po)"
+subclass cpo
+apply default
+apply (frule chfin)
+apply (blast intro: lub_finch1)
+done
-class flat = pcpo +
- assumes ax_flat: "(x :: 'a::pcpo) \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
+lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y"
+ by (simp add: chfin finite_chain_def)
+
+end
-text {* finite partial orders are chain-finite *}
+class finite_po = finite + po
+begin
-instance finite_po < chfin
-apply intro_classes
+subclass chfin
+apply default
apply (drule finite_range_imp_finch)
apply (rule finite)
apply (simp add: finite_chain_def)
done
-text {* some properties for chfin and flat *}
-
-text {* chfin types are cpo *}
+end
-instance chfin < cpo
-apply intro_classes
-apply (frule chfin)
-apply (blast intro: lub_finch1)
-done
+class flat = pcpo +
+ assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
+begin
-text {* flat types are chfin *}
-
-instance flat < chfin
-apply intro_classes
+subclass chfin
+apply default
apply (unfold max_in_chain_def)
apply (case_tac "\<forall>i. Y i = \<bottom>")
apply simp
@@ -283,31 +287,28 @@
apply (blast dest: chain_mono ax_flat)
done
-text {* flat subclass of chfin; @{text adm_flat} not needed *}
-
lemma flat_less_iff:
- fixes x y :: "'a::flat"
shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
-by (safe dest!: ax_flat)
+ by (safe dest!: ax_flat)
-lemma flat_eq: "(a::'a::flat) \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
-by (safe dest!: ax_flat)
+lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
+ by (safe dest!: ax_flat)
-lemma chfin2finch: "chain (Y::nat \<Rightarrow> 'a::chfin) \<Longrightarrow> finite_chain Y"
-by (simp add: chfin finite_chain_def)
+end
text {* Discrete cpos *}
class discrete_cpo = sq_ord +
assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
+begin
-subclass (in discrete_cpo) po
+subclass po
proof qed simp_all
text {* In a discrete cpo, every chain is constant *}
lemma discrete_chain_const:
- assumes S: "chain (S::nat \<Rightarrow> 'a::discrete_cpo)"
+ assumes S: "chain S"
shows "\<exists>x. S = (\<lambda>i. x)"
proof (intro exI ext)
fix i :: nat
@@ -316,7 +317,7 @@
thus "S i = S 0" by (rule sym)
qed
-instance discrete_cpo < cpo
+subclass cpo
proof
fix S :: "nat \<Rightarrow> 'a"
assume S: "chain S"
@@ -326,31 +327,6 @@
by (fast intro: lub_const)
qed
-text {* lemmata for improved admissibility introdution rule *}
-
-lemma infinite_chain_adm_lemma:
- "\<lbrakk>chain Y; \<forall>i. P (Y i);
- \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
- \<Longrightarrow> P (\<Squnion>i. Y i)"
-apply (case_tac "finite_chain Y")
-prefer 2 apply fast
-apply (unfold finite_chain_def)
-apply safe
-apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
-apply assumption
-apply (erule spec)
-done
-
-lemma increasing_chain_adm_lemma:
- "\<lbrakk>chain Y; \<forall>i. P (Y i); \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i);
- \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
- \<Longrightarrow> P (\<Squnion>i. Y i)"
-apply (erule infinite_chain_adm_lemma)
-apply assumption
-apply (erule thin_rl)
-apply (unfold finite_chain_def)
-apply (unfold max_in_chain_def)
-apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
-done
+end
end
--- a/src/HOLCF/Porder.thy Fri May 08 10:59:11 2009 +0200
+++ b/src/HOLCF/Porder.thy Fri May 08 13:34:27 2009 +0200
@@ -12,6 +12,7 @@
class sq_ord =
fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+begin
notation
sq_le (infixl "<<" 55)
@@ -19,35 +20,43 @@
notation (xsymbols)
sq_le (infixl "\<sqsubseteq>" 55)
+lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+ by (rule subst)
+
+lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+ by (rule ssubst)
+
+end
+
class po = sq_ord +
assumes refl_less [iff]: "x \<sqsubseteq> x"
- assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
- assumes antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
+ assumes trans_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+ assumes antisym_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+begin
text {* minimal fixes least element *}
-lemma minimal2UU[OF allI] : "\<forall>x::'a::po. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)"
-by (blast intro: theI2 antisym_less)
+lemma minimal2UU[OF allI] : "\<forall>x. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)"
+ by (blast intro: theI2 antisym_less)
text {* the reverse law of anti-symmetry of @{term "op <<"} *}
-lemma antisym_less_inverse: "(x::'a::po) = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
-by simp
+lemma antisym_less_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
+ by simp
-lemma box_less: "\<lbrakk>(a::'a::po) \<sqsubseteq> b; c \<sqsubseteq> a; b \<sqsubseteq> d\<rbrakk> \<Longrightarrow> c \<sqsubseteq> d"
-by (rule trans_less [OF trans_less])
-
-lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)"
-by (fast elim!: antisym_less_inverse intro!: antisym_less)
+lemma box_less: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
+ by (rule trans_less [OF trans_less])
-lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-by (rule trans_less)
+lemma po_eq_conv: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
+ by (fast elim!: antisym_less_inverse intro!: antisym_less)
-lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
-by (rule subst)
+lemma rev_trans_less: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
+ by (rule trans_less)
-lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
-by (rule ssubst)
+lemma not_less2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
+ by auto
+
+end
lemmas HOLCF_trans_rules [trans] =
trans_less
@@ -55,49 +64,51 @@
sq_ord_less_eq_trans
sq_ord_eq_less_trans
+context po
+begin
+
subsection {* Upper bounds *}
-definition
- is_ub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<|" 55) where
- "(S <| x) = (\<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x)"
+definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<|" 55) where
+ "S <| x \<longleftrightarrow> (\<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x)"
lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u"
-by (simp add: is_ub_def)
+ by (simp add: is_ub_def)
lemma is_ubD: "\<lbrakk>S <| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
-by (simp add: is_ub_def)
+ by (simp add: is_ub_def)
lemma ub_imageI: "(\<And>x. x \<in> S \<Longrightarrow> f x \<sqsubseteq> u) \<Longrightarrow> (\<lambda>x. f x) ` S <| u"
-unfolding is_ub_def by fast
+ unfolding is_ub_def by fast
lemma ub_imageD: "\<lbrakk>f ` S <| u; x \<in> S\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> u"
-unfolding is_ub_def by fast
+ unfolding is_ub_def by fast
lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x"
-unfolding is_ub_def by fast
+ unfolding is_ub_def by fast
lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x"
-unfolding is_ub_def by fast
+ unfolding is_ub_def by fast
lemma is_ub_empty [simp]: "{} <| u"
-unfolding is_ub_def by fast
+ unfolding is_ub_def by fast
lemma is_ub_insert [simp]: "(insert x A) <| y = (x \<sqsubseteq> y \<and> A <| y)"
-unfolding is_ub_def by fast
+ unfolding is_ub_def by fast
lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y"
-unfolding is_ub_def by (fast intro: trans_less)
+ unfolding is_ub_def by (fast intro: trans_less)
subsection {* Least upper bounds *}
-definition
- is_lub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<<|" 55) where
- "(S <<| x) = (S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u))"
+definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<|" 55) where
+ "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
-definition
- lub :: "'a set \<Rightarrow> 'a::po" where
+definition lub :: "'a set \<Rightarrow> 'a" where
"lub S = (THE x. S <<| x)"
+end
+
syntax
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3LUB _:_./ _)" [0,0, 10] 10)
@@ -107,6 +118,9 @@
translations
"LUB x:A. t" == "CONST lub ((%x. t) ` A)"
+context po
+begin
+
abbreviation
Lub (binder "LUB " 10) where
"LUB n. t n == lub (range t)"
@@ -117,13 +131,13 @@
text {* access to some definition as inference rule *}
lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
-unfolding is_lub_def by fast
+ unfolding is_lub_def by fast
lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
-unfolding is_lub_def by fast
+ unfolding is_lub_def by fast
lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
-unfolding is_lub_def by fast
+ unfolding is_lub_def by fast
text {* lubs are unique *}
@@ -142,54 +156,53 @@
done
lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
-by (rule unique_lub [OF lubI])
+ by (rule unique_lub [OF lubI])
lemma is_lub_singleton: "{x} <<| x"
-by (simp add: is_lub_def)
+ by (simp add: is_lub_def)
lemma lub_singleton [simp]: "lub {x} = x"
-by (rule thelubI [OF is_lub_singleton])
+ by (rule thelubI [OF is_lub_singleton])
lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
-by (simp add: is_lub_def)
+ by (simp add: is_lub_def)
lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
-by (rule is_lub_bin [THEN thelubI])
+ by (rule is_lub_bin [THEN thelubI])
lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
-by (erule is_lubI, erule (1) is_ubD)
+ by (erule is_lubI, erule (1) is_ubD)
lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
-by (rule is_lub_maximal [THEN thelubI])
+ by (rule is_lub_maximal [THEN thelubI])
subsection {* Countable chains *}
-definition
+definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
-- {* Here we use countable chains and I prefer to code them as functions! *}
- chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
"chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))"
lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y"
-unfolding chain_def by fast
+ unfolding chain_def by fast
lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)"
-unfolding chain_def by fast
+ unfolding chain_def by fast
text {* chains are monotone functions *}
lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
-by (erule less_Suc_induct, erule chainE, erule trans_less)
+ by (erule less_Suc_induct, erule chainE, erule trans_less)
lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
-by (cases "i = j", simp, simp add: chain_mono_less)
+ by (cases "i = j", simp, simp add: chain_mono_less)
lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
-by (rule chainI, simp, erule chainE)
+ by (rule chainI, simp, erule chainE)
text {* technical lemmas about (least) upper bounds of chains *}
lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
-by (rule is_lubD1 [THEN ub_rangeD])
+ by (rule is_lubD1 [THEN ub_rangeD])
lemma is_ub_range_shift:
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
@@ -205,45 +218,43 @@
lemma is_lub_range_shift:
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
-by (simp add: is_lub_def is_ub_range_shift)
+ by (simp add: is_lub_def is_ub_range_shift)
text {* the lub of a constant chain is the constant *}
lemma chain_const [simp]: "chain (\<lambda>i. c)"
-by (simp add: chainI)
+ by (simp add: chainI)
lemma lub_const: "range (\<lambda>x. c) <<| c"
by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
-by (rule lub_const [THEN thelubI])
+ by (rule lub_const [THEN thelubI])
subsection {* Finite chains *}
-definition
+definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" where
-- {* finite chains, needed for monotony of continuous functions *}
- max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool" where
- "max_in_chain i C = (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
+ "max_in_chain i C \<longleftrightarrow> (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
-definition
- finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
+definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
"finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
text {* results about finite chains *}
lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y"
-unfolding max_in_chain_def by fast
+ unfolding max_in_chain_def by fast
lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j"
-unfolding max_in_chain_def by fast
+ unfolding max_in_chain_def by fast
lemma finite_chainI:
"\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> finite_chain C"
-unfolding finite_chain_def by fast
+ unfolding finite_chain_def by fast
lemma finite_chainE:
"\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-unfolding finite_chain_def by fast
+ unfolding finite_chain_def by fast
lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i"
apply (rule is_lubI)
@@ -311,11 +322,11 @@
done
lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)"
-by (rule chainI, simp)
+ by (rule chainI, simp)
lemma bin_chainmax:
"x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
-unfolding max_in_chain_def by simp
+ unfolding max_in_chain_def by simp
lemma lub_bin_chain:
"x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
@@ -328,36 +339,35 @@
text {* the maximal element in a chain is its lub *}
lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
-by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
+ by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
subsection {* Directed sets *}
-definition
- directed :: "'a::po set \<Rightarrow> bool" where
- "directed S = ((\<exists>x. x \<in> S) \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z))"
+definition directed :: "'a set \<Rightarrow> bool" where
+ "directed S \<longleftrightarrow> (\<exists>x. x \<in> S) \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
lemma directedI:
assumes 1: "\<exists>z. z \<in> S"
assumes 2: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
shows "directed S"
-unfolding directed_def using prems by fast
+ unfolding directed_def using prems by fast
lemma directedD1: "directed S \<Longrightarrow> \<exists>z. z \<in> S"
-unfolding directed_def by fast
+ unfolding directed_def by fast
lemma directedD2: "\<lbrakk>directed S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-unfolding directed_def by fast
+ unfolding directed_def by fast
lemma directedE1:
assumes S: "directed S"
obtains z where "z \<in> S"
-by (insert directedD1 [OF S], fast)
+ by (insert directedD1 [OF S], fast)
lemma directedE2:
assumes S: "directed S"
assumes x: "x \<in> S" and y: "y \<in> S"
obtains z where "z \<in> S" "x \<sqsubseteq> z" "y \<sqsubseteq> z"
-by (insert directedD2 [OF S x y], fast)
+ by (insert directedD2 [OF S x y], fast)
lemma directed_finiteI:
assumes U: "\<And>U. \<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. U <| z"
@@ -395,13 +405,13 @@
qed
lemma not_directed_empty [simp]: "\<not> directed {}"
-by (rule notI, drule directedD1, simp)
+ by (rule notI, drule directedD1, simp)
lemma directed_singleton: "directed {x}"
-by (rule directedI, auto)
+ by (rule directedI, auto)
lemma directed_bin: "x \<sqsubseteq> y \<Longrightarrow> directed {x, y}"
-by (rule directedI, auto)
+ by (rule directedI, auto)
lemma directed_chain: "chain S \<Longrightarrow> directed (range S)"
apply (rule directedI)
@@ -412,4 +422,33 @@
apply simp
done
+text {* lemmata for improved admissibility introdution rule *}
+
+lemma infinite_chain_adm_lemma:
+ "\<lbrakk>chain Y; \<forall>i. P (Y i);
+ \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
+ \<Longrightarrow> P (\<Squnion>i. Y i)"
+apply (case_tac "finite_chain Y")
+prefer 2 apply fast
+apply (unfold finite_chain_def)
+apply safe
+apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
+apply assumption
+apply (erule spec)
+done
+
+lemma increasing_chain_adm_lemma:
+ "\<lbrakk>chain Y; \<forall>i. P (Y i); \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i);
+ \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
+ \<Longrightarrow> P (\<Squnion>i. Y i)"
+apply (erule infinite_chain_adm_lemma)
+apply assumption
+apply (erule thin_rl)
+apply (unfold finite_chain_def)
+apply (unfold max_in_chain_def)
+apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
+done
+
end
+
+end
\ No newline at end of file