--- a/NEWS Sat Nov 27 12:55:12 2010 -0800
+++ b/NEWS Sat Nov 27 13:12:10 2010 -0800
@@ -461,6 +461,22 @@
* Case combinators generated by the domain package for type 'foo'
are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
+* Several theorems have been renamed to more accurately reflect the
+names of constants and types involved. INCOMPATIBILITY.
+ thelub_const ~> lub_const
+ lub_const ~> is_lub_const
+ thelubI ~> lub_eqI
+ is_lub_lub ~> is_lubD2
+ lubI ~> is_lub_lub
+ unique_lub ~> is_lub_unique
+ is_ub_lub ~> is_lub_rangeD1
+ lub_bin_chain ~> is_lub_bin_chain
+ thelub_Pair ~> lub_Pair
+ lub_cprod ~> is_lub_prod
+ thelub_cprod ~> lub_prod
+ minimal_cprod ~> minimal_prod
+ inst_cprod_pcpo ~> inst_prod_pcpo
+
* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
sq_ord_less_eq_trans ~> below_eq_trans
sq_ord_eq_less_trans ~> eq_below_trans
--- a/src/HOLCF/Bifinite.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Bifinite.thy Sat Nov 27 13:12:10 2010 -0800
@@ -642,7 +642,7 @@
apply (simp add: contlub_cfun_fun)
apply (simp add: discr_approx_def)
apply (case_tac x, simp)
-apply (rule thelubI)
+apply (rule lub_eqI)
apply (rule is_lubI)
apply (rule ub_rangeI, simp)
apply (drule ub_rangeD)
--- a/src/HOLCF/Cfun.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Cfun.thy Sat Nov 27 13:12:10 2010 -0800
@@ -209,15 +209,9 @@
lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
by (rule cont_Rep_cfun2 [THEN cont2contlubE])
-lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
-by (rule cont_Rep_cfun2 [THEN contE])
-
lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
by (rule cont_Rep_cfun1 [THEN cont2contlubE])
-lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
-by (rule cont_Rep_cfun1 [THEN contE])
-
text {* monotonicity of application *}
lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
@@ -287,7 +281,7 @@
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 thelubI])
+by (rule lub_cfun [THEN lub_eqI])
subsection {* Continuity simplification procedure *}
@@ -370,7 +364,7 @@
apply (rule allI)
apply (subst contlub_cfun_fun)
apply assumption
-apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
+apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
done
lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
--- a/src/HOLCF/Completion.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Completion.thy Sat Nov 27 13:12:10 2010 -0800
@@ -55,7 +55,7 @@
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 thelubI)
+apply (rule lub_eqI)
apply (rule is_lub_maximal)
apply (rule ub_imageI)
apply (simp add: f)
@@ -117,7 +117,7 @@
apply (simp add: below 2 is_ub_def, fast)
done
hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
- by (rule thelubI)
+ by (rule lub_eqI)
show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
by (simp add: 4 2)
qed
@@ -140,13 +140,13 @@
subsection {* Lemmas about least upper bounds *}
lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
-apply (erule exE, drule lubI)
+apply (erule exE, drule is_lub_lub)
apply (drule is_lubD1)
apply (erule (1) is_ubD)
done
lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
-by (erule exE, drule lubI, erule is_lub_lub)
+by (erule exE, drule is_lub_lub, erule is_lubD2)
subsection {* Locale for ideal completion *}
@@ -163,7 +163,7 @@
lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
apply (frule bin_chain)
apply (drule rep_lub)
-apply (simp only: thelubI [OF lub_bin_chain])
+apply (simp only: lub_eqI [OF is_lub_bin_chain])
apply (rule subsetI, rule UN_I [where a=0], simp_all)
done
--- a/src/HOLCF/Cont.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Cont.thy Sat Nov 27 13:12:10 2010 -0800
@@ -72,7 +72,7 @@
apply (erule contE)
apply (erule bin_chain)
apply (rule_tac f=f in arg_cong)
-apply (erule lub_bin_chain [THEN thelubI])
+apply (erule is_lub_bin_chain [THEN lub_eqI])
done
text {* continuity implies monotonicity *}
@@ -80,7 +80,7 @@
lemma cont2mono: "cont f \<Longrightarrow> monofun f"
apply (rule monofunI)
apply (drule (1) binchain_cont)
-apply (drule_tac i=0 in is_ub_lub)
+apply (drule_tac i=0 in is_lub_rangeD1)
apply simp
done
@@ -92,7 +92,7 @@
lemma cont2contlubE:
"\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
-apply (rule thelubI [symmetric])
+apply (rule lub_eqI [symmetric])
apply (erule (1) contE)
done
@@ -142,9 +142,7 @@
text {* constant functions are continuous *}
lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
-apply (rule contI)
-apply (rule lub_const)
-done
+ using is_lub_const by (rule contI)
text {* application of functions is continuous *}
@@ -235,7 +233,7 @@
lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
apply (rule contI)
apply (drule discrete_chain_const, clarify)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
done
end
--- a/src/HOLCF/FOCUS/Fstream.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstream.thy Sat Nov 27 13:12:10 2010 -0800
@@ -225,7 +225,7 @@
lemma fstream_lub_lemma1:
"\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
apply (case_tac "max_in_chain i Y")
-apply (drule (1) lub_finch1 [THEN thelubI, THEN sym])
+apply (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
apply (force)
apply (unfold max_in_chain_def)
apply auto
@@ -254,7 +254,7 @@
apply (rule chainI)
apply (fast)
apply (erule chain_shift)
-apply (subst lub_const [THEN thelubI])
+apply (subst lub_const)
apply (subst lub_range_shift)
apply (assumption)
apply (simp)
--- a/src/HOLCF/FOCUS/Fstreams.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstreams.thy Sat Nov 27 13:12:10 2010 -0800
@@ -246,7 +246,7 @@
apply (drule fstreams_lub_lemma1, auto)
apply (rule_tac x="j" in exI, auto)
apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
apply (rule_tac x="j" in exI)
apply (erule subst) back back
apply (simp add: below_prod_def sconc_mono)
@@ -266,7 +266,7 @@
lemma lub_Pair_not_UU_lemma:
"[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |]
==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
-apply (frule thelub_cprod, clarsimp)
+apply (frule lub_prod, clarsimp)
apply (drule chain_UU_I_inverse2, clarsimp)
apply (case_tac "Y i", clarsimp)
apply (case_tac "max_in_chain i Y")
@@ -298,7 +298,7 @@
apply (drule fstreams_lub_lemma2, auto)
apply (rule_tac x="j" in exI, auto)
apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
apply (rule_tac x="j" in exI)
apply (erule subst) back back
apply (simp add: sconc_mono)
@@ -312,7 +312,7 @@
apply (rule sconc_mono)
apply (subgoal_tac "tt ~= tta" "tta << ms")
apply (blast intro: fstreams_chain_lemma)
-apply (frule lub_cprod [THEN thelubI], auto)
+apply (frule lub_prod, auto)
apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub chainI)
--- a/src/HOLCF/FOCUS/Stream_adm.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Sat Nov 27 13:12:10 2010 -0800
@@ -37,7 +37,7 @@
prefer 2 apply fast
apply (unfold finite_chain_def)
apply safe
-apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
+apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst])
apply assumption
apply (erule spec)
done
--- a/src/HOLCF/Fix.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Fix.thy Sat Nov 27 13:12:10 2010 -0800
@@ -183,7 +183,7 @@
hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
by - (rule admD [OF adm'], simp, assumption)
hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
- by (simp add: thelub_Pair)
+ by (simp add: lub_Pair)
hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
by simp
thus "P (fix\<cdot>F) (fix\<cdot>G)"
--- a/src/HOLCF/Fun_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Fun_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
@@ -80,7 +80,7 @@
lemma thelub_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 thelubI])
+by (rule lub_fun [THEN lub_eqI])
instance "fun" :: (type, cpo) cpo
by intro_classes (rule exI, erule lub_fun)
--- a/src/HOLCF/HOLCF.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/HOLCF.thy Sat Nov 27 13:12:10 2010 -0800
@@ -30,5 +30,10 @@
lemmas cont2cont_Rep_CFun = cont2cont_APP
lemmas cont_Rep_CFun_app = cont_APP_app
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 thelubI = lub_eqI
+*)
end
--- a/src/HOLCF/Library/List_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Library/List_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
@@ -141,7 +141,7 @@
fix S :: "nat \<Rightarrow> 'a list"
assume "chain S" thus "\<exists>x. range S <<| x"
proof (induct rule: list_chain_induct)
- case Nil thus ?case by (auto intro: lub_const)
+ case Nil thus ?case by (auto intro: is_lub_const)
next
case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
qed
@@ -163,7 +163,7 @@
fixes A :: "nat \<Rightarrow> 'a::cpo"
assumes A: "chain A" and B: "chain B"
shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
-by (intro thelubI is_lub_Cons cpo_lubI A B)
+by (intro lub_eqI is_lub_Cons cpo_lubI A B)
lemma cont2cont_list_case:
assumes f: "cont (\<lambda>x. f x)"
@@ -175,7 +175,7 @@
apply (rule cont_apply [OF f])
apply (rule contI)
apply (erule list_chain_cases)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
apply (simp add: lub_Cons)
apply (simp add: cont2contlubE [OF h2])
apply (simp add: cont2contlubE [OF h3])
--- a/src/HOLCF/Library/Sum_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Library/Sum_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
@@ -98,10 +98,10 @@
lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
apply (rule is_lubI)
apply (rule ub_rangeI)
- apply (simp add: is_ub_lub)
+ apply (simp add: is_lub_rangeD1)
apply (frule ub_rangeD [where i=arbitrary])
apply (erule Inl_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
apply (rule ub_rangeI)
apply (drule ub_rangeD, simp)
done
@@ -109,10 +109,10 @@
lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
apply (rule is_lubI)
apply (rule ub_rangeI)
- apply (simp add: is_ub_lub)
+ apply (simp add: is_lub_rangeD1)
apply (frule ub_rangeD [where i=arbitrary])
apply (erule Inr_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
apply (rule ub_rangeI)
apply (drule ub_rangeD, simp)
done
--- a/src/HOLCF/Pcpo.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Pcpo.thy Sat Nov 27 13:12:10 2010 -0800
@@ -19,19 +19,19 @@
text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
- by (fast dest: cpo elim: lubI)
+ by (fast dest: cpo elim: is_lub_lub)
lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
- by (blast dest: cpo intro: lubI)
+ by (blast dest: cpo intro: is_lub_lub)
text {* Properties of the 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])
+ by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
lemma is_lub_thelub:
"\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
- by (blast dest: cpo intro: lubI [THEN is_lub_lub])
+ by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])
lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
@@ -70,7 +70,7 @@
lemma maxinch_is_thelub:
"chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
apply (rule iffI)
-apply (fast intro!: thelubI lub_finch1)
+apply (fast intro!: lub_eqI lub_finch1)
apply (unfold max_in_chain_def)
apply (safe intro!: below_antisym)
apply (fast elim!: chain_mono)
--- a/src/HOLCF/Pcpodef.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Pcpodef.thy Sat Nov 27 13:12:10 2010 -0800
@@ -107,7 +107,7 @@
by (rule typedef_is_lubI [OF below])
qed
-lemmas typedef_lub = typedef_is_lub [THEN thelubI, standard]
+lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
theorem typedef_cpo:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
--- a/src/HOLCF/Porder.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Porder.thy Sat Nov 27 13:12:10 2010 -0800
@@ -126,7 +126,7 @@
lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
unfolding is_lub_def by fast
-lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
+lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
unfolding is_lub_def by fast
lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
@@ -137,40 +137,34 @@
text {* lubs are unique *}
-lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
-apply (unfold is_lub_def is_ub_def)
-apply (blast intro: below_antisym)
-done
+lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
+ unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
text {* technical lemmas about @{term lub} and @{term is_lub} *}
-lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
-apply (unfold lub_def)
-apply (rule theI)
-apply assumption
-apply (erule (1) unique_lub)
-done
+lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
+ unfolding lub_def by (rule theI [OF _ is_lub_unique])
-lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
- by (rule unique_lub [OF lubI])
+lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l"
+ by (rule is_lub_unique [OF is_lub_lub])
lemma is_lub_singleton: "{x} <<| x"
by (simp add: is_lub_def)
lemma lub_singleton [simp]: "lub {x} = x"
- by (rule thelubI [OF is_lub_singleton])
+ by (rule is_lub_singleton [THEN lub_eqI])
lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
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 lub_eqI])
lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
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 lub_eqI])
subsection {* Countable chains *}
@@ -197,7 +191,7 @@
text {* technical lemmas about (least) upper bounds of chains *}
-lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
+lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
by (rule is_lubD1 [THEN ub_rangeD])
lemma is_ub_range_shift:
@@ -221,11 +215,11 @@
lemma chain_const [simp]: "chain (\<lambda>i. c)"
by (simp add: chainI)
-lemma lub_const: "range (\<lambda>x. c) <<| c"
+lemma is_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])
+lemma lub_const [simp]: "(\<Squnion>i. c) = c"
+ by (rule is_lub_const [THEN lub_eqI])
subsection {* Finite chains *}
@@ -324,7 +318,7 @@
"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
-lemma lub_bin_chain:
+lemma is_lub_bin_chain:
"x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
apply (frule bin_chain)
apply (drule bin_chainmax)
@@ -335,7 +329,7 @@
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: lub_eqI is_lubI ub_rangeI)
end
--- a/src/HOLCF/Product_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Product_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
@@ -111,46 +111,30 @@
lemma is_lub_Pair:
"\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
-apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: is_ub_lub)
-apply (frule ub2ub_monofun [OF monofun_fst])
-apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: below_prod_def is_lub_lub)
-done
+unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
-lemma thelub_Pair:
+lemma lub_Pair:
"\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
\<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
-by (fast intro: thelubI is_lub_Pair elim: thelubE)
+by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
-lemma lub_cprod:
+lemma is_lub_prod:
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
assumes S: "chain S"
shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-proof -
- from `chain S` have "chain (\<lambda>i. fst (S i))"
- by (rule ch2ch_fst)
- hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
- by (rule cpo_lubI)
- from `chain S` have "chain (\<lambda>i. snd (S i))"
- by (rule ch2ch_snd)
- hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
- by (rule cpo_lubI)
- show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
- using is_lub_Pair [OF 1 2] by simp
-qed
+using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
-lemma thelub_cprod:
+lemma lub_prod:
"chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-by (rule lub_cprod [THEN thelubI])
+by (rule is_lub_prod [THEN lub_eqI])
instance prod :: (cpo, cpo) cpo
proof
fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
assume "chain S"
hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
- by (rule lub_cprod)
+ by (rule is_lub_prod)
thus "\<exists>x. range S <<| x" ..
qed
@@ -164,23 +148,23 @@
subsection {* Product type is pointed *}
-lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
+lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
by (simp add: below_prod_def)
instance prod :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_cprod)
+by intro_classes (fast intro: minimal_prod)
-lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_cprod [THEN UU_I, symmetric])
+lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
+by (rule minimal_prod [THEN UU_I, symmetric])
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-unfolding inst_cprod_pcpo by simp
+unfolding inst_prod_pcpo by simp
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule fst_conv)
+unfolding inst_prod_pcpo by (rule fst_conv)
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule snd_conv)
+unfolding inst_prod_pcpo by (rule snd_conv)
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
by simp
@@ -194,25 +178,25 @@
apply (rule contI)
apply (rule is_lub_Pair)
apply (erule cpo_lubI)
-apply (rule lub_const)
+apply (rule is_lub_const)
done
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
apply (rule contI)
apply (rule is_lub_Pair)
-apply (rule lub_const)
+apply (rule is_lub_const)
apply (erule cpo_lubI)
done
lemma cont_fst: "cont fst"
apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
apply (erule cpo_lubI [OF ch2ch_fst])
done
lemma cont_snd: "cont snd"
apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
apply (erule cpo_lubI [OF ch2ch_snd])
done
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 13:12:10 2010 -0800
@@ -711,7 +711,7 @@
val goal = mk_trp (mk_eq (lhs, rhs));
val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
val start_rules =
- @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
+ @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
@ @{thms pair_collapse split_def}
@ map_apply_thms @ map_ID_thms;
val rules0 =
--- a/src/HOLCF/Up.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Up.thy Sat Nov 27 13:12:10 2010 -0800
@@ -111,7 +111,7 @@
proof (rule up_chain_lemma)
assume "\<forall>i. S i = Ibottom"
hence "range (\<lambda>i. S i) <<| Ibottom"
- by (simp add: lub_const)
+ by (simp add: is_lub_const)
thus ?thesis ..
next
fix A :: "nat \<Rightarrow> 'a"
@@ -160,7 +160,7 @@
assume A: "\<forall>i. Iup (A i) = Y (i + k)"
assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
- by (simp add: thelubI contlub_cfun_arg)
+ by (simp add: lub_eqI contlub_cfun_arg)
also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
by (simp add: A)
also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
@@ -223,7 +223,7 @@
assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
| A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
apply (rule up_chain_lemma [OF Y])
-apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
+apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
done
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
--- a/src/HOLCF/ex/Domain_Proofs.thy Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy Sat Nov 27 13:12:10 2010 -0800
@@ -467,7 +467,7 @@
lemma lub_take_lemma:
"(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
= (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
-apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
+apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
apply (simp only: map_apply_thms pair_collapse)
apply (simp only: fix_def2)
apply (rule lub_eq)