# HG changeset patch
# User haftmann
# Date 1241782467 -7200
# Node ID 845a6acd3bf363fb04b4572847e63e8a988b3ed3
# Parent  ee1ebd405a37e880d5a862dbdbe61e08de16c7ca
localized (complete) partial order classes

diff -r ee1ebd405a37 -r 845a6acd3bf3 src/HOLCF/Pcpo.thy
--- 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
diff -r ee1ebd405a37 -r 845a6acd3bf3 src/HOLCF/Porder.thy
--- 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