merged

--- a/NEWS	Mon Dec 06 19:54:56 2010 +0100
+++ b/NEWS	Mon Dec 06 13:43:05 2010 -0800
@@ -524,6 +524,9 @@
   unique_lub      ~> is_lub_unique
   is_ub_lub       ~> is_lub_rangeD1
   lub_bin_chain   ~> is_lub_bin_chain
+  lub_fun         ~> is_lub_fun
+  thelub_fun      ~> lub_fun
+  thelub_cfun     ~> lub_cfun
   thelub_Pair     ~> lub_Pair
   lub_cprod       ~> is_lub_prod
   thelub_cprod    ~> lub_prod

--- a/src/HOL/HOLCF/Bifinite.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -618,6 +618,42 @@
   "LIFTDEFL('a::predomain \<times> 'b::predomain) = DEFL('a u \<otimes> 'b u)"
 by (rule liftdefl_prod_def)
 
+subsubsection {* Unit type *}
+
+instantiation unit :: liftdomain
+begin
+
+definition
+  "emb = (\<bottom> :: unit \<rightarrow> udom)"
+
+definition
+  "prj = (\<bottom> :: udom \<rightarrow> unit)"
+
+definition
+  "defl (t::unit itself) = \<bottom>"
+
+definition
+  "(liftemb :: unit u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> unit u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl (t::unit itself) = u_defl\<cdot>DEFL(unit)"
+
+instance
+using liftemb_unit_def liftprj_unit_def liftdefl_unit_def
+proof (rule liftdomain_class_intro)
+  show "ep_pair emb (prj :: udom \<rightarrow> unit)"
+    unfolding emb_unit_def prj_unit_def
+    by (simp add: ep_pair.intro)
+next
+  show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)"
+    unfolding emb_unit_def prj_unit_def defl_unit_def by simp
+qed
+
+end
+
 subsubsection {* Discrete cpo *}
 
 definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"

--- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -244,28 +244,19 @@
 
 text {* contlub, cont properties of @{term Rep_cfun} in both arguments *}
 
-lemma contlub_cfun: 
-  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"
+lemma lub_APP:
+  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
 by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
 
-lemma cont_cfun: 
-  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
-apply (rule thelubE)
-apply (simp only: ch2ch_Rep_cfun)
-apply (simp only: contlub_cfun)
+lemma lub_LAM:
+  "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
+    \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
+apply (simp add: lub_cfun)
+apply (simp add: Abs_cfun_inverse2)
+apply (simp add: lub_fun ch2ch_lambda)
 done
 
-lemma contlub_LAM:
-  "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
-    \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
-apply (simp add: lub_cfun)
-apply (simp add: Abs_cfun_inverse2)
-apply (simp add: thelub_fun ch2ch_lambda)
-done
-
-lemmas lub_distribs = 
-  contlub_cfun [symmetric]
-  contlub_LAM [symmetric]
+lemmas lub_distribs = lub_APP lub_LAM
 
 text {* strictness *}
 
@@ -277,11 +268,8 @@
 
 text {* type @{typ "'a -> 'b"} is chain complete *}
 
-lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
-by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
-
-lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
-by (rule lub_cfun [THEN lub_eqI])
+lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
+by (simp add: lub_cfun lub_fun ch2ch_lambda)
 
 subsection {* Continuity simplification procedure *}
 

--- a/src/HOL/HOLCF/Completion.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -52,17 +52,6 @@
 lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
 by (fast intro: ideal_principal)
 
-lemma lub_image_principal:
-  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-  shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
-apply (rule lub_eqI)
-apply (rule is_lub_maximal)
-apply (rule ub_imageI)
-apply (simp add: f)
-apply (rule imageI)
-apply (simp add: r_refl)
-done
-
 text {* The set of ideals is a cpo *}
 
 lemma ideal_UN:
@@ -156,7 +145,7 @@
   assumes ideal_rep: "\<And>x. ideal (rep x)"
   assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
   assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
-  assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
+  assumes belowI: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
   assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
 begin
 
@@ -168,20 +157,11 @@
 done
 
 lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
-by (rule iffI [OF rep_mono subset_repD])
-
-lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
-unfolding below_def rep_principal
-apply safe
-apply (erule (1) idealD3 [OF ideal_rep])
-apply (erule subsetD, simp add: r_refl)
-done
-
-lemma mem_rep_iff_principal_below: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
-by (simp add: rep_eq)
+by (rule iffI [OF rep_mono belowI])
 
 lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
-by (simp add: rep_eq)
+unfolding below_def rep_principal
+by (auto intro: r_refl elim: idealD3 [OF ideal_rep])
 
 lemma principal_below_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
 by (simp add: principal_below_iff_mem_rep rep_principal)
@@ -192,9 +172,6 @@
 lemma eq_iff: "x = y \<longleftrightarrow> rep x = rep y"
 unfolding po_eq_conv below_def by auto
 
-lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
-by (simp add: rep_eq)
-
 lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
 by (simp only: principal_below_iff)
 
@@ -202,16 +179,6 @@
   "\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
 by (simp add: chainI principal_mono)
 
-lemma lub_principal_rep: "principal ` rep x <<| x"
-apply (rule is_lubI)
-apply (rule ub_imageI)
-apply (erule repD)
-apply (subst below_def)
-apply (rule subsetI)
-apply (drule (1) ub_imageD)
-apply (simp add: rep_eq)
-done
-
 subsubsection {* Principal ideals approximate all elements *}
 
 lemma compact_principal [simp]: "compact (principal a)"
@@ -321,13 +288,6 @@
 apply (drule (2) admD2, fast, simp)
 done
 
-lemma obtain_compact_chain:
-  obtains Y :: "nat \<Rightarrow> 'b"
-  where "chain Y" and "\<forall>i. compact (Y i)" and "x = (\<Squnion>i. Y i)"
-apply (rule obtain_principal_chain [of x])
-apply (rule_tac Y="\<lambda>i. principal (Y i)" in that, simp_all)
-done
-
 subsection {* Defining functions in terms of basis elements *}
 
 definition
@@ -387,7 +347,12 @@
   shows "basis_fun f\<cdot>(principal a) = f a"
 apply (subst basis_fun_beta, erule f_mono)
 apply (subst rep_principal)
-apply (rule lub_image_principal, erule f_mono)
+apply (rule lub_eqI)
+apply (rule is_lub_maximal)
+apply (rule ub_imageI)
+apply (simp add: f_mono)
+apply (rule imageI)
+apply (simp add: r_refl)
 done
 
 lemma basis_fun_mono:

--- a/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -250,20 +250,6 @@
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
-theorem typedef_Abs_defined:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
-
-theorem typedef_Rep_defined:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
-
 subsection {* Proving a subtype is flat *}
 
 theorem typedef_flat:

--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -250,7 +250,7 @@
 apply  (rule_tac x="i+j" in exI)
 apply  (drule fstream_prefix)
 apply  (clarsimp)
-apply  (subst contlub_cfun [symmetric])
+apply  (subst lub_APP)
 apply   (rule chainI)
 apply   (fast)
 apply  (erule chain_shift)

--- a/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -36,10 +36,10 @@
 done
 
 lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>"
-by (simp add: succeed_def cont_Abs_match Abs_match_defined)
+by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff)
 
 lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
-by (simp add: fail_def Abs_match_defined)
+by (simp add: fail_def Abs_match_bottom_iff)
 
 lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)"
 by (simp add: succeed_def cont_Abs_match Abs_match_inject)

--- a/src/HOL/HOLCF/Fun_Cpo.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Fun_Cpo.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -57,19 +57,13 @@
 lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
 by (simp add: chain_def below_fun_def)
 
-text {* upper bounds of function chains yield upper bound in the po range *}
-
-lemma ub2ub_fun:
-  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
-by (auto simp add: is_ub_def below_fun_def)
-
 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
 
 lemma is_lub_lambda:
   "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
 unfolding is_lub_def is_ub_def below_fun_def by simp
 
-lemma lub_fun:
+lemma is_lub_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
     \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
 apply (rule is_lub_lambda)
@@ -77,33 +71,13 @@
 apply (erule ch2ch_fun)
 done
 
-lemma thelub_fun:
+lemma lub_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
     \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-by (rule lub_fun [THEN lub_eqI])
+by (rule is_lub_fun [THEN lub_eqI])
 
 instance "fun"  :: (type, cpo) cpo
-by intro_classes (rule exI, erule lub_fun)
-
-subsection {* Chain-finiteness of function space *}
-
-lemma maxinch2maxinch_lambda:
-  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
-unfolding max_in_chain_def fun_eq_iff by simp
-
-lemma maxinch_mono:
-  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
-unfolding max_in_chain_def
-proof (intro allI impI)
-  fix k
-  assume Y: "\<forall>n\<ge>i. Y i = Y n"
-  assume ij: "i \<le> j"
-  assume jk: "j \<le> k"
-  from ij jk have ik: "i \<le> k" by simp
-  from Y ij have Yij: "Y i = Y j" by simp
-  from Y ik have Yik: "Y i = Y k" by simp
-  from Yij Yik show "Y j = Y k" by auto
-qed
+by intro_classes (rule exI, erule is_lub_fun)
 
 instance "fun" :: (type, discrete_cpo) discrete_cpo
 proof
@@ -135,12 +109,12 @@
 text {* The lub of a chain of monotone functions is monotone. *}
 
 lemma adm_monofun: "adm monofun"
-by (rule admI, simp add: thelub_fun fun_chain_iff monofun_def lub_mono)
+by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono)
 
 text {* The lub of a chain of continuous functions is continuous. *}
 
 lemma adm_cont: "adm cont"
-by (rule admI, simp add: thelub_fun fun_chain_iff)
+by (rule admI, simp add: lub_fun fun_chain_iff)
 
 text {* Function application preserves monotonicity and continuity. *}
 
@@ -150,7 +124,7 @@
 lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
 apply (rule contI2)
 apply (erule cont2mono [THEN mono2mono_fun])
-apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
+apply (simp add: cont2contlubE lub_fun ch2ch_cont)
 done
 
 lemma cont_fun: "cont (\<lambda>f. f x)"
@@ -174,6 +148,6 @@
 lemma contlub_lambda:
   "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
     \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
-by (simp add: thelub_fun ch2ch_lambda)
+by (simp add: lub_fun ch2ch_lambda)
 
 end

--- a/src/HOL/HOLCF/HOLCF.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/HOLCF.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -32,8 +32,8 @@
 lemmas cont_Rep_CFun_app_app = cont_APP_app_app
 lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
 lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
-(*
+lemmas contlub_cfun = lub_APP [symmetric]
+lemmas contlub_LAM = lub_LAM [symmetric]
 lemmas thelubI = lub_eqI
-*)
 
 end

--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Dec 06 13:43:05 2010 -0800
@@ -228,7 +228,7 @@
     apply (induct rule: list_chain_induct)
     apply simp
     apply (simp add: lub_Cons f h)
-    apply (simp add: contlub_cfun [symmetric] ch2ch_monofun [OF mono])
+    apply (simp add: lub_APP ch2ch_monofun [OF mono])
     apply (simp add: monofun_cfun)
     done
 qed

--- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 19:54:56 2010 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 13:43:05 2010 -0800
@@ -9,10 +9,10 @@
 sig
   type cpo_info =
     { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-      is_lub: thm, lub: thm, compact: thm }
+      lub: thm, compact: thm }
   type pcpo_info =
-    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
-      Rep_defined: thm, Abs_defined: thm }
+    { Rep_strict: thm, Abs_strict: thm,
+      Rep_bottom_iff: thm, Abs_bottom_iff: thm }
 
   val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> theory ->
@@ -45,11 +45,11 @@
 
 type cpo_info =
   { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-    is_lub: thm, lub: thm, compact: thm }
+    lub: thm, compact: thm }
 
 type pcpo_info =
-  { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
-    Rep_defined: thm, Abs_defined: thm }
+  { Rep_strict: thm, Abs_strict: thm,
+    Rep_bottom_iff: thm, Abs_bottom_iff: thm }
 
 (* building terms *)
 
@@ -94,7 +94,6 @@
     fun make thm = Drule.zero_var_indexes (thm OF cpo_thms')
     val cont_Rep = make @{thm typedef_cont_Rep}
     val cont_Abs = make @{thm typedef_cont_Abs}
-    val is_lub = make @{thm typedef_is_lub}
     val lub = make @{thm typedef_lub}
     val compact = make @{thm typedef_compact}
     val (_, thy) =
@@ -104,13 +103,12 @@
         ([((Binding.prefix_name "adm_"      name, admissible'), []),
           ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
           ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
-          ((Binding.prefix_name "is_lub_"   name, is_lub     ), []),
           ((Binding.prefix_name "lub_"      name, lub        ), []),
           ((Binding.prefix_name "compact_"  name, compact    ), [])])
       ||> Sign.parent_path
     val cpo_info : cpo_info =
       { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
-        cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact }
+        cont_Abs = cont_Abs, lub = lub, compact = compact }
   in
     (cpo_info, thy)
   end
@@ -138,8 +136,6 @@
     val Abs_strict = make @{thm typedef_Abs_strict}
     val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff}
     val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff}
-    val Rep_defined = make @{thm typedef_Rep_defined}
-    val Abs_defined = make @{thm typedef_Abs_defined}
     val (_, thy) =
       thy
       |> Sign.add_path (Binding.name_of name)
@@ -147,14 +143,11 @@
         ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
           ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
           ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
-          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
-          ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
-          ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
+          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), [])])
       ||> Sign.parent_path
     val pcpo_info =
       { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
-        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
-        Rep_defined = Rep_defined, Abs_defined = Abs_defined }
+        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff }
   in
     (pcpo_info, thy)
   end