1.1 --- a/NEWS Sat Nov 27 12:55:12 2010 -0800
1.2 +++ b/NEWS Sat Nov 27 13:12:10 2010 -0800
1.3 @@ -461,6 +461,22 @@
1.4 * Case combinators generated by the domain package for type 'foo'
1.5 are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
1.6
1.7 +* Several theorems have been renamed to more accurately reflect the
1.8 +names of constants and types involved. INCOMPATIBILITY.
1.9 + thelub_const ~> lub_const
1.10 + lub_const ~> is_lub_const
1.11 + thelubI ~> lub_eqI
1.12 + is_lub_lub ~> is_lubD2
1.13 + lubI ~> is_lub_lub
1.14 + unique_lub ~> is_lub_unique
1.15 + is_ub_lub ~> is_lub_rangeD1
1.16 + lub_bin_chain ~> is_lub_bin_chain
1.17 + thelub_Pair ~> lub_Pair
1.18 + lub_cprod ~> is_lub_prod
1.19 + thelub_cprod ~> lub_prod
1.20 + minimal_cprod ~> minimal_prod
1.21 + inst_cprod_pcpo ~> inst_prod_pcpo
1.22 +
1.23 * Many legacy theorem names have been discontinued. INCOMPATIBILITY.
1.24 sq_ord_less_eq_trans ~> below_eq_trans
1.25 sq_ord_eq_less_trans ~> eq_below_trans
2.1 --- a/src/HOLCF/Bifinite.thy Sat Nov 27 12:55:12 2010 -0800
2.2 +++ b/src/HOLCF/Bifinite.thy Sat Nov 27 13:12:10 2010 -0800
2.3 @@ -642,7 +642,7 @@
2.4 apply (simp add: contlub_cfun_fun)
2.5 apply (simp add: discr_approx_def)
2.6 apply (case_tac x, simp)
2.7 -apply (rule thelubI)
2.8 +apply (rule lub_eqI)
2.9 apply (rule is_lubI)
2.10 apply (rule ub_rangeI, simp)
2.11 apply (drule ub_rangeD)
3.1 --- a/src/HOLCF/Cfun.thy Sat Nov 27 12:55:12 2010 -0800
3.2 +++ b/src/HOLCF/Cfun.thy Sat Nov 27 13:12:10 2010 -0800
3.3 @@ -209,15 +209,9 @@
3.4 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
3.5 by (rule cont_Rep_cfun2 [THEN cont2contlubE])
3.6
3.7 -lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
3.8 -by (rule cont_Rep_cfun2 [THEN contE])
3.9 -
3.10 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
3.11 by (rule cont_Rep_cfun1 [THEN cont2contlubE])
3.12
3.13 -lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
3.14 -by (rule cont_Rep_cfun1 [THEN contE])
3.15 -
3.16 text {* monotonicity of application *}
3.17
3.18 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
3.19 @@ -287,7 +281,7 @@
3.20 by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
3.21
3.22 lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
3.23 -by (rule lub_cfun [THEN thelubI])
3.24 +by (rule lub_cfun [THEN lub_eqI])
3.25
3.26 subsection {* Continuity simplification procedure *}
3.27
3.28 @@ -370,7 +364,7 @@
3.29 apply (rule allI)
3.30 apply (subst contlub_cfun_fun)
3.31 apply assumption
3.32 -apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
3.33 +apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
3.34 done
3.35
3.36 lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
4.1 --- a/src/HOLCF/Completion.thy Sat Nov 27 12:55:12 2010 -0800
4.2 +++ b/src/HOLCF/Completion.thy Sat Nov 27 13:12:10 2010 -0800
4.3 @@ -55,7 +55,7 @@
4.4 lemma lub_image_principal:
4.5 assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
4.6 shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
4.7 -apply (rule thelubI)
4.8 +apply (rule lub_eqI)
4.9 apply (rule is_lub_maximal)
4.10 apply (rule ub_imageI)
4.11 apply (simp add: f)
4.12 @@ -117,7 +117,7 @@
4.13 apply (simp add: below 2 is_ub_def, fast)
4.14 done
4.15 hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
4.16 - by (rule thelubI)
4.17 + by (rule lub_eqI)
4.18 show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
4.19 by (simp add: 4 2)
4.20 qed
4.21 @@ -140,13 +140,13 @@
4.22 subsection {* Lemmas about least upper bounds *}
4.23
4.24 lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
4.25 -apply (erule exE, drule lubI)
4.26 +apply (erule exE, drule is_lub_lub)
4.27 apply (drule is_lubD1)
4.28 apply (erule (1) is_ubD)
4.29 done
4.30
4.31 lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
4.32 -by (erule exE, drule lubI, erule is_lub_lub)
4.33 +by (erule exE, drule is_lub_lub, erule is_lubD2)
4.34
4.35 subsection {* Locale for ideal completion *}
4.36
4.37 @@ -163,7 +163,7 @@
4.38 lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
4.39 apply (frule bin_chain)
4.40 apply (drule rep_lub)
4.41 -apply (simp only: thelubI [OF lub_bin_chain])
4.42 +apply (simp only: lub_eqI [OF is_lub_bin_chain])
4.43 apply (rule subsetI, rule UN_I [where a=0], simp_all)
4.44 done
4.45
5.1 --- a/src/HOLCF/Cont.thy Sat Nov 27 12:55:12 2010 -0800
5.2 +++ b/src/HOLCF/Cont.thy Sat Nov 27 13:12:10 2010 -0800
5.3 @@ -72,7 +72,7 @@
5.4 apply (erule contE)
5.5 apply (erule bin_chain)
5.6 apply (rule_tac f=f in arg_cong)
5.7 -apply (erule lub_bin_chain [THEN thelubI])
5.8 +apply (erule is_lub_bin_chain [THEN lub_eqI])
5.9 done
5.10
5.11 text {* continuity implies monotonicity *}
5.12 @@ -80,7 +80,7 @@
5.13 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
5.14 apply (rule monofunI)
5.15 apply (drule (1) binchain_cont)
5.16 -apply (drule_tac i=0 in is_ub_lub)
5.17 +apply (drule_tac i=0 in is_lub_rangeD1)
5.18 apply simp
5.19 done
5.20
5.21 @@ -92,7 +92,7 @@
5.22
5.23 lemma cont2contlubE:
5.24 "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
5.25 -apply (rule thelubI [symmetric])
5.26 +apply (rule lub_eqI [symmetric])
5.27 apply (erule (1) contE)
5.28 done
5.29
5.30 @@ -142,9 +142,7 @@
5.31 text {* constant functions are continuous *}
5.32
5.33 lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
5.34 -apply (rule contI)
5.35 -apply (rule lub_const)
5.36 -done
5.37 + using is_lub_const by (rule contI)
5.38
5.39 text {* application of functions is continuous *}
5.40
5.41 @@ -235,7 +233,7 @@
5.42 lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
5.43 apply (rule contI)
5.44 apply (drule discrete_chain_const, clarify)
5.45 -apply (simp add: lub_const)
5.46 +apply (simp add: is_lub_const)
5.47 done
5.48
5.49 end
6.1 --- a/src/HOLCF/FOCUS/Fstream.thy Sat Nov 27 12:55:12 2010 -0800
6.2 +++ b/src/HOLCF/FOCUS/Fstream.thy Sat Nov 27 13:12:10 2010 -0800
6.3 @@ -225,7 +225,7 @@
6.4 lemma fstream_lub_lemma1:
6.5 "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
6.6 apply (case_tac "max_in_chain i Y")
6.7 -apply (drule (1) lub_finch1 [THEN thelubI, THEN sym])
6.8 +apply (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
6.9 apply (force)
6.10 apply (unfold max_in_chain_def)
6.11 apply auto
6.12 @@ -254,7 +254,7 @@
6.13 apply (rule chainI)
6.14 apply (fast)
6.15 apply (erule chain_shift)
6.16 -apply (subst lub_const [THEN thelubI])
6.17 +apply (subst lub_const)
6.18 apply (subst lub_range_shift)
6.19 apply (assumption)
6.20 apply (simp)
7.1 --- a/src/HOLCF/FOCUS/Fstreams.thy Sat Nov 27 12:55:12 2010 -0800
7.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy Sat Nov 27 13:12:10 2010 -0800
7.3 @@ -246,7 +246,7 @@
7.4 apply (drule fstreams_lub_lemma1, auto)
7.5 apply (rule_tac x="j" in exI, auto)
7.6 apply (case_tac "max_in_chain j Y")
7.7 -apply (frule lub_finch1 [THEN thelubI], auto)
7.8 +apply (frule lub_finch1 [THEN lub_eqI], auto)
7.9 apply (rule_tac x="j" in exI)
7.10 apply (erule subst) back back
7.11 apply (simp add: below_prod_def sconc_mono)
7.12 @@ -266,7 +266,7 @@
7.13 lemma lub_Pair_not_UU_lemma:
7.14 "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |]
7.15 ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
7.16 -apply (frule thelub_cprod, clarsimp)
7.17 +apply (frule lub_prod, clarsimp)
7.18 apply (drule chain_UU_I_inverse2, clarsimp)
7.19 apply (case_tac "Y i", clarsimp)
7.20 apply (case_tac "max_in_chain i Y")
7.21 @@ -298,7 +298,7 @@
7.22 apply (drule fstreams_lub_lemma2, auto)
7.23 apply (rule_tac x="j" in exI, auto)
7.24 apply (case_tac "max_in_chain j Y")
7.25 -apply (frule lub_finch1 [THEN thelubI], auto)
7.26 +apply (frule lub_finch1 [THEN lub_eqI], auto)
7.27 apply (rule_tac x="j" in exI)
7.28 apply (erule subst) back back
7.29 apply (simp add: sconc_mono)
7.30 @@ -312,7 +312,7 @@
7.31 apply (rule sconc_mono)
7.32 apply (subgoal_tac "tt ~= tta" "tta << ms")
7.33 apply (blast intro: fstreams_chain_lemma)
7.34 -apply (frule lub_cprod [THEN thelubI], auto)
7.35 +apply (frule lub_prod, auto)
7.36 apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
7.37 apply (drule fstreams_mono, simp)
7.38 apply (rule is_ub_thelub chainI)
8.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy Sat Nov 27 12:55:12 2010 -0800
8.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy Sat Nov 27 13:12:10 2010 -0800
8.3 @@ -37,7 +37,7 @@
8.4 prefer 2 apply fast
8.5 apply (unfold finite_chain_def)
8.6 apply safe
8.7 -apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
8.8 +apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst])
8.9 apply assumption
8.10 apply (erule spec)
8.11 done
9.1 --- a/src/HOLCF/Fix.thy Sat Nov 27 12:55:12 2010 -0800
9.2 +++ b/src/HOLCF/Fix.thy Sat Nov 27 13:12:10 2010 -0800
9.3 @@ -183,7 +183,7 @@
9.4 hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
9.5 by - (rule admD [OF adm'], simp, assumption)
9.6 hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
9.7 - by (simp add: thelub_Pair)
9.8 + by (simp add: lub_Pair)
9.9 hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
9.10 by simp
9.11 thus "P (fix\<cdot>F) (fix\<cdot>G)"
10.1 --- a/src/HOLCF/Fun_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
10.2 +++ b/src/HOLCF/Fun_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
10.3 @@ -80,7 +80,7 @@
10.4 lemma thelub_fun:
10.5 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
10.6 \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
10.7 -by (rule lub_fun [THEN thelubI])
10.8 +by (rule lub_fun [THEN lub_eqI])
10.9
10.10 instance "fun" :: (type, cpo) cpo
10.11 by intro_classes (rule exI, erule lub_fun)
11.1 --- a/src/HOLCF/HOLCF.thy Sat Nov 27 12:55:12 2010 -0800
11.2 +++ b/src/HOLCF/HOLCF.thy Sat Nov 27 13:12:10 2010 -0800
11.3 @@ -30,5 +30,10 @@
11.4 lemmas cont2cont_Rep_CFun = cont2cont_APP
11.5 lemmas cont_Rep_CFun_app = cont_APP_app
11.6 lemmas cont_Rep_CFun_app_app = cont_APP_app_app
11.7 +lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
11.8 +lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
11.9 +(*
11.10 +lemmas thelubI = lub_eqI
11.11 +*)
11.12
11.13 end
12.1 --- a/src/HOLCF/Library/List_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
12.2 +++ b/src/HOLCF/Library/List_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
12.3 @@ -141,7 +141,7 @@
12.4 fix S :: "nat \<Rightarrow> 'a list"
12.5 assume "chain S" thus "\<exists>x. range S <<| x"
12.6 proof (induct rule: list_chain_induct)
12.7 - case Nil thus ?case by (auto intro: lub_const)
12.8 + case Nil thus ?case by (auto intro: is_lub_const)
12.9 next
12.10 case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
12.11 qed
12.12 @@ -163,7 +163,7 @@
12.13 fixes A :: "nat \<Rightarrow> 'a::cpo"
12.14 assumes A: "chain A" and B: "chain B"
12.15 shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
12.16 -by (intro thelubI is_lub_Cons cpo_lubI A B)
12.17 +by (intro lub_eqI is_lub_Cons cpo_lubI A B)
12.18
12.19 lemma cont2cont_list_case:
12.20 assumes f: "cont (\<lambda>x. f x)"
12.21 @@ -175,7 +175,7 @@
12.22 apply (rule cont_apply [OF f])
12.23 apply (rule contI)
12.24 apply (erule list_chain_cases)
12.25 -apply (simp add: lub_const)
12.26 +apply (simp add: is_lub_const)
12.27 apply (simp add: lub_Cons)
12.28 apply (simp add: cont2contlubE [OF h2])
12.29 apply (simp add: cont2contlubE [OF h3])
13.1 --- a/src/HOLCF/Library/Sum_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
13.2 +++ b/src/HOLCF/Library/Sum_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
13.3 @@ -98,10 +98,10 @@
13.4 lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
13.5 apply (rule is_lubI)
13.6 apply (rule ub_rangeI)
13.7 - apply (simp add: is_ub_lub)
13.8 + apply (simp add: is_lub_rangeD1)
13.9 apply (frule ub_rangeD [where i=arbitrary])
13.10 apply (erule Inl_belowE, simp)
13.11 - apply (erule is_lub_lub)
13.12 + apply (erule is_lubD2)
13.13 apply (rule ub_rangeI)
13.14 apply (drule ub_rangeD, simp)
13.15 done
13.16 @@ -109,10 +109,10 @@
13.17 lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
13.18 apply (rule is_lubI)
13.19 apply (rule ub_rangeI)
13.20 - apply (simp add: is_ub_lub)
13.21 + apply (simp add: is_lub_rangeD1)
13.22 apply (frule ub_rangeD [where i=arbitrary])
13.23 apply (erule Inr_belowE, simp)
13.24 - apply (erule is_lub_lub)
13.25 + apply (erule is_lubD2)
13.26 apply (rule ub_rangeI)
13.27 apply (drule ub_rangeD, simp)
13.28 done
14.1 --- a/src/HOLCF/Pcpo.thy Sat Nov 27 12:55:12 2010 -0800
14.2 +++ b/src/HOLCF/Pcpo.thy Sat Nov 27 13:12:10 2010 -0800
14.3 @@ -19,19 +19,19 @@
14.4 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
14.5
14.6 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
14.7 - by (fast dest: cpo elim: lubI)
14.8 + by (fast dest: cpo elim: is_lub_lub)
14.9
14.10 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
14.11 - by (blast dest: cpo intro: lubI)
14.12 + by (blast dest: cpo intro: is_lub_lub)
14.13
14.14 text {* Properties of the lub *}
14.15
14.16 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
14.17 - by (blast dest: cpo intro: lubI [THEN is_ub_lub])
14.18 + by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
14.19
14.20 lemma is_lub_thelub:
14.21 "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
14.22 - by (blast dest: cpo intro: lubI [THEN is_lub_lub])
14.23 + by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])
14.24
14.25 lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
14.26 by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
14.27 @@ -70,7 +70,7 @@
14.28 lemma maxinch_is_thelub:
14.29 "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
14.30 apply (rule iffI)
14.31 -apply (fast intro!: thelubI lub_finch1)
14.32 +apply (fast intro!: lub_eqI lub_finch1)
14.33 apply (unfold max_in_chain_def)
14.34 apply (safe intro!: below_antisym)
14.35 apply (fast elim!: chain_mono)
15.1 --- a/src/HOLCF/Pcpodef.thy Sat Nov 27 12:55:12 2010 -0800
15.2 +++ b/src/HOLCF/Pcpodef.thy Sat Nov 27 13:12:10 2010 -0800
15.3 @@ -107,7 +107,7 @@
15.4 by (rule typedef_is_lubI [OF below])
15.5 qed
15.6
15.7 -lemmas typedef_lub = typedef_is_lub [THEN thelubI, standard]
15.8 +lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
15.9
15.10 theorem typedef_cpo:
15.11 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
16.1 --- a/src/HOLCF/Porder.thy Sat Nov 27 12:55:12 2010 -0800
16.2 +++ b/src/HOLCF/Porder.thy Sat Nov 27 13:12:10 2010 -0800
16.3 @@ -126,7 +126,7 @@
16.4 lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
16.5 unfolding is_lub_def by fast
16.6
16.7 -lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
16.8 +lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
16.9 unfolding is_lub_def by fast
16.10
16.11 lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
16.12 @@ -137,40 +137,34 @@
16.13
16.14 text {* lubs are unique *}
16.15
16.16 -lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
16.17 -apply (unfold is_lub_def is_ub_def)
16.18 -apply (blast intro: below_antisym)
16.19 -done
16.20 +lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
16.21 + unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
16.22
16.23 text {* technical lemmas about @{term lub} and @{term is_lub} *}
16.24
16.25 -lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
16.26 -apply (unfold lub_def)
16.27 -apply (rule theI)
16.28 -apply assumption
16.29 -apply (erule (1) unique_lub)
16.30 -done
16.31 +lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
16.32 + unfolding lub_def by (rule theI [OF _ is_lub_unique])
16.33
16.34 -lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
16.35 - by (rule unique_lub [OF lubI])
16.36 +lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l"
16.37 + by (rule is_lub_unique [OF is_lub_lub])
16.38
16.39 lemma is_lub_singleton: "{x} <<| x"
16.40 by (simp add: is_lub_def)
16.41
16.42 lemma lub_singleton [simp]: "lub {x} = x"
16.43 - by (rule thelubI [OF is_lub_singleton])
16.44 + by (rule is_lub_singleton [THEN lub_eqI])
16.45
16.46 lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
16.47 by (simp add: is_lub_def)
16.48
16.49 lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
16.50 - by (rule is_lub_bin [THEN thelubI])
16.51 + by (rule is_lub_bin [THEN lub_eqI])
16.52
16.53 lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
16.54 by (erule is_lubI, erule (1) is_ubD)
16.55
16.56 lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
16.57 - by (rule is_lub_maximal [THEN thelubI])
16.58 + by (rule is_lub_maximal [THEN lub_eqI])
16.59
16.60 subsection {* Countable chains *}
16.61
16.62 @@ -197,7 +191,7 @@
16.63
16.64 text {* technical lemmas about (least) upper bounds of chains *}
16.65
16.66 -lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
16.67 +lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
16.68 by (rule is_lubD1 [THEN ub_rangeD])
16.69
16.70 lemma is_ub_range_shift:
16.71 @@ -221,11 +215,11 @@
16.72 lemma chain_const [simp]: "chain (\<lambda>i. c)"
16.73 by (simp add: chainI)
16.74
16.75 -lemma lub_const: "range (\<lambda>x. c) <<| c"
16.76 +lemma is_lub_const: "range (\<lambda>x. c) <<| c"
16.77 by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
16.78
16.79 -lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
16.80 - by (rule lub_const [THEN thelubI])
16.81 +lemma lub_const [simp]: "(\<Squnion>i. c) = c"
16.82 + by (rule is_lub_const [THEN lub_eqI])
16.83
16.84 subsection {* Finite chains *}
16.85
16.86 @@ -324,7 +318,7 @@
16.87 "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
16.88 unfolding max_in_chain_def by simp
16.89
16.90 -lemma lub_bin_chain:
16.91 +lemma is_lub_bin_chain:
16.92 "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
16.93 apply (frule bin_chain)
16.94 apply (drule bin_chainmax)
16.95 @@ -335,7 +329,7 @@
16.96 text {* the maximal element in a chain is its lub *}
16.97
16.98 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
16.99 - by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
16.100 + by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)
16.101
16.102 end
16.103
17.1 --- a/src/HOLCF/Product_Cpo.thy Sat Nov 27 12:55:12 2010 -0800
17.2 +++ b/src/HOLCF/Product_Cpo.thy Sat Nov 27 13:12:10 2010 -0800
17.3 @@ -111,46 +111,30 @@
17.4
17.5 lemma is_lub_Pair:
17.6 "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
17.7 -apply (rule is_lubI [OF ub_rangeI])
17.8 -apply (simp add: is_ub_lub)
17.9 -apply (frule ub2ub_monofun [OF monofun_fst])
17.10 -apply (drule ub2ub_monofun [OF monofun_snd])
17.11 -apply (simp add: below_prod_def is_lub_lub)
17.12 -done
17.13 +unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
17.14
17.15 -lemma thelub_Pair:
17.16 +lemma lub_Pair:
17.17 "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
17.18 \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
17.19 -by (fast intro: thelubI is_lub_Pair elim: thelubE)
17.20 +by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
17.21
17.22 -lemma lub_cprod:
17.23 +lemma is_lub_prod:
17.24 fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
17.25 assumes S: "chain S"
17.26 shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
17.27 -proof -
17.28 - from `chain S` have "chain (\<lambda>i. fst (S i))"
17.29 - by (rule ch2ch_fst)
17.30 - hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
17.31 - by (rule cpo_lubI)
17.32 - from `chain S` have "chain (\<lambda>i. snd (S i))"
17.33 - by (rule ch2ch_snd)
17.34 - hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
17.35 - by (rule cpo_lubI)
17.36 - show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
17.37 - using is_lub_Pair [OF 1 2] by simp
17.38 -qed
17.39 +using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
17.40
17.41 -lemma thelub_cprod:
17.42 +lemma lub_prod:
17.43 "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
17.44 \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
17.45 -by (rule lub_cprod [THEN thelubI])
17.46 +by (rule is_lub_prod [THEN lub_eqI])
17.47
17.48 instance prod :: (cpo, cpo) cpo
17.49 proof
17.50 fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
17.51 assume "chain S"
17.52 hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
17.53 - by (rule lub_cprod)
17.54 + by (rule is_lub_prod)
17.55 thus "\<exists>x. range S <<| x" ..
17.56 qed
17.57
17.58 @@ -164,23 +148,23 @@
17.59
17.60 subsection {* Product type is pointed *}
17.61
17.62 -lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
17.63 +lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
17.64 by (simp add: below_prod_def)
17.65
17.66 instance prod :: (pcpo, pcpo) pcpo
17.67 -by intro_classes (fast intro: minimal_cprod)
17.68 +by intro_classes (fast intro: minimal_prod)
17.69
17.70 -lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
17.71 -by (rule minimal_cprod [THEN UU_I, symmetric])
17.72 +lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
17.73 +by (rule minimal_prod [THEN UU_I, symmetric])
17.74
17.75 lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
17.76 -unfolding inst_cprod_pcpo by simp
17.77 +unfolding inst_prod_pcpo by simp
17.78
17.79 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
17.80 -unfolding inst_cprod_pcpo by (rule fst_conv)
17.81 +unfolding inst_prod_pcpo by (rule fst_conv)
17.82
17.83 lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
17.84 -unfolding inst_cprod_pcpo by (rule snd_conv)
17.85 +unfolding inst_prod_pcpo by (rule snd_conv)
17.86
17.87 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
17.88 by simp
17.89 @@ -194,25 +178,25 @@
17.90 apply (rule contI)
17.91 apply (rule is_lub_Pair)
17.92 apply (erule cpo_lubI)
17.93 -apply (rule lub_const)
17.94 +apply (rule is_lub_const)
17.95 done
17.96
17.97 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
17.98 apply (rule contI)
17.99 apply (rule is_lub_Pair)
17.100 -apply (rule lub_const)
17.101 +apply (rule is_lub_const)
17.102 apply (erule cpo_lubI)
17.103 done
17.104
17.105 lemma cont_fst: "cont fst"
17.106 apply (rule contI)
17.107 -apply (simp add: thelub_cprod)
17.108 +apply (simp add: lub_prod)
17.109 apply (erule cpo_lubI [OF ch2ch_fst])
17.110 done
17.111
17.112 lemma cont_snd: "cont snd"
17.113 apply (rule contI)
17.114 -apply (simp add: thelub_cprod)
17.115 +apply (simp add: lub_prod)
17.116 apply (erule cpo_lubI [OF ch2ch_snd])
17.117 done
17.118
18.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 12:55:12 2010 -0800
18.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 13:12:10 2010 -0800
18.3 @@ -711,7 +711,7 @@
18.4 val goal = mk_trp (mk_eq (lhs, rhs));
18.5 val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
18.6 val start_rules =
18.7 - @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
18.8 + @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
18.9 @ @{thms pair_collapse split_def}
18.10 @ map_apply_thms @ map_ID_thms;
18.11 val rules0 =
19.1 --- a/src/HOLCF/Up.thy Sat Nov 27 12:55:12 2010 -0800
19.2 +++ b/src/HOLCF/Up.thy Sat Nov 27 13:12:10 2010 -0800
19.3 @@ -111,7 +111,7 @@
19.4 proof (rule up_chain_lemma)
19.5 assume "\<forall>i. S i = Ibottom"
19.6 hence "range (\<lambda>i. S i) <<| Ibottom"
19.7 - by (simp add: lub_const)
19.8 + by (simp add: is_lub_const)
19.9 thus ?thesis ..
19.10 next
19.11 fix A :: "nat \<Rightarrow> 'a"
19.12 @@ -160,7 +160,7 @@
19.13 assume A: "\<forall>i. Iup (A i) = Y (i + k)"
19.14 assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
19.15 hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
19.16 - by (simp add: thelubI contlub_cfun_arg)
19.17 + by (simp add: lub_eqI contlub_cfun_arg)
19.18 also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
19.19 by (simp add: A)
19.20 also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
19.21 @@ -223,7 +223,7 @@
19.22 assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
19.23 | 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)"
19.24 apply (rule up_chain_lemma [OF Y])
19.25 -apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
19.26 +apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
19.27 done
19.28
19.29 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
20.1 --- a/src/HOLCF/ex/Domain_Proofs.thy Sat Nov 27 12:55:12 2010 -0800
20.2 +++ b/src/HOLCF/ex/Domain_Proofs.thy Sat Nov 27 13:12:10 2010 -0800
20.3 @@ -467,7 +467,7 @@
20.4 lemma lub_take_lemma:
20.5 "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
20.6 = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
20.7 -apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
20.8 +apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
20.9 apply (simp only: map_apply_thms pair_collapse)
20.10 apply (simp only: fix_def2)
20.11 apply (rule lub_eq)