--- a/src/HOLCF/Algebraic.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Algebraic.thy Wed Nov 03 15:56:15 2010 +0100
@@ -191,7 +191,7 @@
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
apply (rule iffI)
apply (simp only: compact_def cast_below_cast [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
apply (erule compact_cast)
done
--- a/src/HOLCF/Cfun.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Cfun.thy Wed Nov 03 15:56:15 2010 +0100
@@ -13,28 +13,28 @@
subsection {* Definition of continuous function type *}
-cpodef (CFun) ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
+cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
by (auto intro: cont_const adm_cont)
type_notation (xsymbols)
cfun ("(_ \<rightarrow>/ _)" [1, 0] 0)
notation
- Rep_CFun ("(_$/_)" [999,1000] 999)
+ Rep_cfun ("(_$/_)" [999,1000] 999)
notation (xsymbols)
- Rep_CFun ("(_\<cdot>/_)" [999,1000] 999)
+ Rep_cfun ("(_\<cdot>/_)" [999,1000] 999)
notation (HTML output)
- Rep_CFun ("(_\<cdot>/_)" [999,1000] 999)
+ Rep_cfun ("(_\<cdot>/_)" [999,1000] 999)
subsection {* Syntax for continuous lambda abstraction *}
syntax "_cabs" :: "'a"
parse_translation {*
-(* rewrite (_cabs x t) => (Abs_CFun (%x. t)) *)
- [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_CFun})];
+(* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
+ [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
*}
text {* To avoid eta-contraction of body: *}
@@ -50,7 +50,7 @@
val (x,t') = atomic_abs_tr' abs';
in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
- in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
+ in [(@{const_syntax Abs_cfun}, cabs_tr')] end;
*}
text {* Syntax for nested abstractions *}
@@ -88,32 +88,32 @@
text {* Dummy patterns for continuous abstraction *}
translations
- "\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
+ "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
subsection {* Continuous function space is pointed *}
-lemma UU_CFun: "\<bottom> \<in> CFun"
-by (simp add: CFun_def inst_fun_pcpo)
+lemma UU_cfun: "\<bottom> \<in> cfun"
+by (simp add: cfun_def inst_fun_pcpo)
instance cfun :: (cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
+by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
instance cfun :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
+by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
-lemmas Rep_CFun_strict =
- typedef_Rep_strict [OF type_definition_CFun below_CFun_def UU_CFun]
+lemmas Rep_cfun_strict =
+ typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
-lemmas Abs_CFun_strict =
- typedef_Abs_strict [OF type_definition_CFun below_CFun_def UU_CFun]
+lemmas Abs_cfun_strict =
+ typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
text {* function application is strict in its first argument *}
-lemma Rep_CFun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
-by (simp add: Rep_CFun_strict)
+lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
+by (simp add: Rep_cfun_strict)
lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
-by (simp add: inst_fun_pcpo [symmetric] Abs_CFun_strict)
+by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)
text {* for compatibility with old HOLCF-Version *}
lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
@@ -123,11 +123,11 @@
text {* Beta-equality for continuous functions *}
-lemma Abs_CFun_inverse2: "cont f \<Longrightarrow> Rep_CFun (Abs_CFun f) = f"
-by (simp add: Abs_CFun_inverse CFun_def)
+lemma Abs_cfun_inverse2: "cont f \<Longrightarrow> Rep_cfun (Abs_cfun f) = f"
+by (simp add: Abs_cfun_inverse cfun_def)
lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
-by (simp add: Abs_CFun_inverse2)
+by (simp add: Abs_cfun_inverse2)
text {* Beta-reduction simproc *}
@@ -144,7 +144,7 @@
that would otherwise be caused by large continuity side conditions.
*}
-simproc_setup beta_cfun_proc ("Abs_CFun f\<cdot>x") = {*
+simproc_setup beta_cfun_proc ("Abs_cfun f\<cdot>x") = {*
fn phi => fn ss => fn ct =>
let
val dest = Thm.dest_comb;
@@ -160,12 +160,12 @@
text {* Eta-equality for continuous functions *}
lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"
-by (rule Rep_CFun_inverse)
+by (rule Rep_cfun_inverse)
text {* Extensionality for continuous functions *}
lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
-by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff)
+by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)
lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
by (simp add: cfun_eq_iff)
@@ -173,7 +173,7 @@
text {* Extensionality wrt. ordering for continuous functions *}
lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)"
-by (simp add: below_CFun_def fun_below_iff)
+by (simp add: below_cfun_def fun_below_iff)
lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
by (simp add: cfun_below_iff)
@@ -191,32 +191,32 @@
subsection {* Continuity of application *}
-lemma cont_Rep_CFun1: "cont (\<lambda>f. f\<cdot>x)"
-by (rule cont_Rep_CFun [THEN cont2cont_fun])
+lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
+by (rule cont_Rep_cfun [THEN cont2cont_fun])
-lemma cont_Rep_CFun2: "cont (\<lambda>x. f\<cdot>x)"
-apply (cut_tac x=f in Rep_CFun)
-apply (simp add: CFun_def)
+lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
+apply (cut_tac x=f in Rep_cfun)
+apply (simp add: cfun_def)
done
-lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono]
+lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
-lemmas monofun_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2mono, standard]
-lemmas monofun_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2mono, standard]
+lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono, standard]
+lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono, standard]
-text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
+text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
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])
+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])
+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])
+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])
+by (rule cont_Rep_cfun1 [THEN contE])
text {* monotonicity of application *}
@@ -224,7 +224,7 @@
by (simp add: cfun_below_iff)
lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
-by (rule monofun_Rep_CFun2 [THEN monofunE])
+by (rule monofun_Rep_cfun2 [THEN monofunE])
lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
@@ -232,15 +232,15 @@
text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (erule monofun_Rep_CFun2 [THEN ch2ch_monofun])
+by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])
-lemma ch2ch_Rep_CFunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
+lemma ch2ch_Rep_cfunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
+by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun])
-lemma ch2ch_Rep_CFunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
-by (rule monofun_Rep_CFun1 [THEN ch2ch_monofun])
+lemma ch2ch_Rep_cfunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
+by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun])
-lemma ch2ch_Rep_CFun [simp]:
+lemma ch2ch_Rep_cfun [simp]:
"\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
by (simp add: chain_def monofun_cfun)
@@ -248,7 +248,7 @@
"\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
by (simp add: chain_def cfun_below_iff)
-text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
+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))"
@@ -257,15 +257,15 @@
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: ch2ch_Rep_cfun)
apply (simp only: contlub_cfun)
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: thelub_CFun)
-apply (simp add: Abs_CFun_inverse2)
+apply (simp add: thelub_cfun)
+apply (simp add: Abs_cfun_inverse2)
apply (simp add: thelub_fun ch2ch_lambda)
done
@@ -291,17 +291,17 @@
subsection {* Continuity simplification procedure *}
-text {* cont2cont lemma for @{term Rep_CFun} *}
+text {* cont2cont lemma for @{term Rep_cfun} *}
-lemma cont2cont_Rep_CFun [simp, cont2cont]:
+lemma cont2cont_APP [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes t: "cont (\<lambda>x. t x)"
shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
proof -
have 1: "\<And>y. cont (\<lambda>x. (f x)\<cdot>y)"
- using cont_Rep_CFun1 f by (rule cont_compose)
+ using cont_Rep_cfun1 f by (rule cont_compose)
show "cont (\<lambda>x. (f x)\<cdot>(t x))"
- using t cont_Rep_CFun2 1 by (rule cont_apply)
+ using t cont_Rep_cfun2 1 by (rule cont_apply)
qed
text {*
@@ -309,11 +309,11 @@
These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
*}
-lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
+lemma cont_APP_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
+by (rule cont2cont_APP [THEN cont2cont_fun])
-lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
-by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
+lemma cont_APP_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
+by (rule cont_APP_app [THEN cont2cont_fun])
text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
@@ -334,9 +334,9 @@
assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
-proof (rule cont_Abs_CFun)
+proof (rule cont_Abs_cfun)
fix x
- from f1 show "f x \<in> CFun" by (simp add: CFun_def)
+ from f1 show "f x \<in> cfun" by (simp add: cfun_def)
from f2 show "cont f" by (rule cont2cont_lambda)
qed
@@ -356,24 +356,24 @@
by (simp add: cont2cont_LAM)
lemmas cont_lemmas1 =
- cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
+ cont_const cont_id cont_Rep_cfun2 cont2cont_APP cont2cont_LAM
subsection {* Miscellaneous *}
-text {* Monotonicity of @{term Abs_CFun} *}
+text {* Monotonicity of @{term Abs_cfun} *}
-lemma semi_monofun_Abs_CFun:
- "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
-by (simp add: below_CFun_def Abs_CFun_inverse2)
+lemma semi_monofun_Abs_cfun:
+ "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_cfun f \<sqsubseteq> Abs_cfun g"
+by (simp add: below_cfun_def Abs_cfun_inverse2)
text {* some lemmata for functions with flat/chfin domain/range types *}
-lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)
+lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)
==> !s. ? n. (LUB i. Y i)$s = Y n$s"
apply (rule allI)
apply (subst contlub_cfun_fun)
apply assumption
-apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_CFunL)
+apply (fast intro!: thelubI 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/ConvexPD.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy Wed Nov 03 15:56:15 2010 +0100
@@ -256,7 +256,7 @@
using convex_unit_Rep_compact_basis [of compact_bot]
by (simp add: inst_convex_pd_pcpo)
-lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma convex_unit_bottom_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
lemma compact_convex_unit: "compact x \<Longrightarrow> compact {x}\<natural>"
@@ -265,7 +265,7 @@
lemma compact_convex_unit_iff [simp]: "compact {x}\<natural> \<longleftrightarrow> compact x"
apply (safe elim!: compact_convex_unit)
apply (simp only: compact_def convex_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
done
lemma compact_convex_plus [simp]:
--- a/src/HOLCF/Deflation.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Deflation.thy Wed Nov 03 15:56:15 2010 +0100
@@ -207,7 +207,7 @@
proof -
assume "compact (e\<cdot>x)"
hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
- hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
+ hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
thus "compact x" by (rule compactI)
qed
@@ -216,7 +216,7 @@
proof -
assume "compact x"
hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
- hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
+ hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
thus "compact (e\<cdot>x)" by (rule compactI)
qed
@@ -392,7 +392,7 @@
finally show "e\<cdot>\<bottom> = \<bottom>" by simp
qed
-lemma e_defined_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
--- a/src/HOLCF/Domain.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Domain.thy Wed Nov 03 15:56:15 2010 +0100
@@ -22,25 +22,25 @@
text {* Lemmas for proving nchotomy rule: *}
-lemma ex_one_defined_iff:
+lemma ex_one_bottom_iff:
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
by simp
-lemma ex_up_defined_iff:
+lemma ex_up_bottom_iff:
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
by (safe, case_tac x, auto)
-lemma ex_sprod_defined_iff:
+lemma ex_sprod_bottom_iff:
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
(\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
by (safe, case_tac y, auto)
-lemma ex_sprod_up_defined_iff:
+lemma ex_sprod_up_bottom_iff:
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
(\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
by (safe, case_tac y, simp, case_tac x, auto)
-lemma ex_ssum_defined_iff:
+lemma ex_ssum_bottom_iff:
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
(\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
@@ -49,12 +49,12 @@
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
by auto
-lemmas ex_defined_iffs =
- ex_ssum_defined_iff
- ex_sprod_up_defined_iff
- ex_sprod_defined_iff
- ex_up_defined_iff
- ex_one_defined_iff
+lemmas ex_bottom_iffs =
+ ex_ssum_bottom_iff
+ ex_sprod_up_bottom_iff
+ ex_sprod_bottom_iff
+ ex_up_bottom_iff
+ ex_one_bottom_iff
text {* Rules for turning nchotomy into exhaust: *}
@@ -78,14 +78,14 @@
lemmas con_strict_rules =
sinl_strict sinr_strict spair_strict1 spair_strict2
-lemmas con_defined_iff_rules =
- sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
+lemmas con_bottom_iff_rules =
+ sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
lemmas con_below_iff_rules =
- sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_defined_iff_rules
+ sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
lemmas con_eq_iff_rules =
- sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
+ sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
lemmas sel_strict_rules =
cfcomp2 sscase1 sfst_strict ssnd_strict fup1
@@ -102,8 +102,8 @@
sel_strict_rules sel_app_extra_rules
ssnd_spair sfst_spair up_defined spair_defined
-lemmas sel_defined_iff_rules =
- cfcomp2 sfst_defined_iff ssnd_defined_iff
+lemmas sel_bottom_iff_rules =
+ cfcomp2 sfst_bottom_iff ssnd_bottom_iff
lemmas take_con_rules =
ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
--- a/src/HOLCF/Domain_Aux.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Domain_Aux.thy Wed Nov 03 15:56:15 2010 +0100
@@ -71,19 +71,19 @@
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
-lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (auto elim: abs_defin' intro: abs_strict)
-lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
- by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
+lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
+ by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)
lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
- by (simp add: rep_defined_iff)
+ by (simp add: rep_bottom_iff)
lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
proof (unfold compact_def)
assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
- with cont_Rep_CFun2
+ with cont_Rep_cfun2
have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
qed
--- a/src/HOLCF/Fix.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Fix.thy Wed Nov 03 15:56:15 2010 +0100
@@ -119,7 +119,7 @@
text {* strictness of @{term fix} *}
-lemma fix_defined_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
+lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
apply (rule iffI)
apply (erule subst)
apply (rule fix_eq [symmetric])
@@ -127,10 +127,10 @@
done
lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
text {* @{term fix} applied to identity and constant functions *}
--- a/src/HOLCF/Fixrec.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Fixrec.thy Wed Nov 03 15:56:15 2010 +0100
@@ -150,12 +150,12 @@
definition
match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where
- "match_TT = (\<Lambda> x k. If x then k else fail fi)"
+ "match_TT = (\<Lambda> x k. If x then k else fail)"
definition
match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where
- "match_FF = (\<Lambda> x k. If x then fail else k fi)"
+ "match_FF = (\<Lambda> x k. If x then fail else k)"
lemma match_UU_simps [simp]:
"match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
@@ -222,11 +222,11 @@
by simp
lemma def_cont_fix_eq:
- "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
+ "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
by (simp, subst fix_eq, simp)
lemma def_cont_fix_ind:
- "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
+ "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
by (simp add: fix_ind)
text {* lemma for proving rewrite rules *}
--- a/src/HOLCF/HOLCF.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/HOLCF.thy Wed Nov 03 15:56:15 2010 +0100
@@ -11,7 +11,7 @@
Powerdomains
begin
-default_sort pcpo
+default_sort bifinite
ML {* path_add "~~/src/HOLCF/Library" *}
@@ -27,6 +27,9 @@
lemmas monofun_fun_arg = monofunE
lemmas monofun_lub_fun = adm_monofun [THEN admD]
lemmas cont_lub_fun = adm_cont [THEN admD]
+lemmas cont2cont_Rep_CFun = cont2cont_APP
+lemmas cont_Rep_CFun_app = cont_APP_app
+lemmas cont_Rep_CFun_app_app = cont_APP_app_app
text {* Older legacy theorem names: *}
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Nov 03 15:56:15 2010 +0100
@@ -39,7 +39,7 @@
| x##xs => (flift1
(%p.(If Def ((fst p)~:actions sig)
then Def (s=(snd p))
- else TT fi)
+ else TT)
andalso (h$xs) (snd p))
$x)
)))"
@@ -137,7 +137,7 @@
| x##xs => (flift1
(%p.(If Def ((fst p)~:actions sig)
then Def (s=(snd p))
- else TT fi)
+ else TT)
andalso (stutter2 sig$xs) (snd p))
$x)
))"
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed Nov 03 15:56:15 2010 +0100
@@ -8,7 +8,9 @@
imports HOLCF
begin
-domain 'a seq = nil ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65)
+default_sort pcpo
+
+domain (unsafe) 'a seq = nil ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65)
(*
sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -70,7 +72,7 @@
sfilter_nil: "sfilter$P$nil=nil"
| sfilter_cons:
"x~=UU ==> sfilter$P$(x##xs)=
- (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
+ (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"
lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
by fixrec_simp
@@ -98,7 +100,7 @@
stakewhile_nil: "stakewhile$P$nil=nil"
| stakewhile_cons:
"x~=UU ==> stakewhile$P$(x##xs) =
- (If P$x then x##(stakewhile$P$xs) else nil fi)"
+ (If P$x then x##(stakewhile$P$xs) else nil)"
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
by fixrec_simp
@@ -111,7 +113,7 @@
sdropwhile_nil: "sdropwhile$P$nil=nil"
| sdropwhile_cons:
"x~=UU ==> sdropwhile$P$(x##xs) =
- (If P$x then sdropwhile$P$xs else x##xs fi)"
+ (If P$x then sdropwhile$P$xs else x##xs)"
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
by fixrec_simp
@@ -123,7 +125,7 @@
where
slast_nil: "slast$nil=UU"
| slast_cons:
- "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"
+ "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"
lemma slast_UU [simp]: "slast$UU=UU"
by fixrec_simp
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Nov 03 15:56:15 2010 +0100
@@ -901,8 +901,8 @@
apply (rule_tac t="s1" in seq.reach [THEN subst])
apply (rule_tac t="s2" in seq.reach [THEN subst])
apply (rule lub_mono)
-apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
-apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
apply (rule assms)
done
--- a/src/HOLCF/Library/Stream.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Library/Stream.thy Wed Nov 03 15:56:15 2010 +0100
@@ -8,7 +8,9 @@
imports HOLCF Nat_Infinity
begin
-domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
+default_sort pcpo
+
+domain (unsafe) 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
definition
smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
@@ -17,7 +19,7 @@
definition
sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream" where
"sfilter = fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
- If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
+ If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs)"
definition
slen :: "'a stream \<Rightarrow> inat" ("#_" [1000] 1000) where
@@ -504,7 +506,7 @@
lemma sfilter_unfold:
"sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
- If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
+ If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs)"
by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
@@ -518,7 +520,7 @@
lemma sfilter_scons [simp]:
"x ~= \<bottom> ==> sfilter\<cdot>f\<cdot>(x && xs) =
- If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs fi"
+ If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs"
by (subst sfilter_unfold, force)
@@ -921,7 +923,7 @@
by (rule monofun_cfun_arg,simp)
lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
-by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric])
+by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric])
lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
(LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
--- a/src/HOLCF/Lift.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Lift.thy Wed Nov 03 15:56:15 2010 +0100
@@ -95,6 +95,11 @@
flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where
"flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
+translations
+ "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"
+ "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
+ "\<Lambda>(CONST Def x). t" <= "FLIFT x. t"
+
definition
flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
"flift2 f = (FLIFT x. Def (f x))"
@@ -114,7 +119,7 @@
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
by (erule lift_definedE, simp)
-lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cases x, simp_all)
lemma FLIFT_mono:
--- a/src/HOLCF/LowerPD.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Wed Nov 03 15:56:15 2010 +0100
@@ -229,10 +229,10 @@
using lower_unit_Rep_compact_basis [of compact_bot]
by (simp add: inst_lower_pd_pcpo)
-lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma lower_unit_bottom_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
-lemma lower_plus_strict_iff [simp]:
+lemma lower_plus_bottom_iff [simp]:
"xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
apply safe
apply (rule UU_I, erule subst, rule lower_plus_below1)
@@ -256,7 +256,7 @@
lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
apply (safe elim!: compact_lower_unit)
apply (simp only: compact_def lower_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
done
lemma compact_lower_plus [simp]:
--- a/src/HOLCF/Pcpodef.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Pcpodef.thy Wed Nov 03 15:56:15 2010 +0100
@@ -152,13 +152,9 @@
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
and f_in_A: "\<And>x. f x \<in> A"
- and cont_f: "cont f"
- shows "cont (\<lambda>x. Abs (f x))"
- apply (rule contI)
- apply (rule typedef_is_lubI [OF below])
- apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
- apply (erule cont_f [THEN contE])
-done
+ shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
+unfolding cont_def is_lub_def is_ub_def ball_simps below
+by (simp add: type_definition.Abs_inverse [OF type f_in_A])
subsection {* Proving subtype elements are compact *}
@@ -235,7 +231,7 @@
apply (rule type_definition.Abs_inverse [OF type UU_in_A])
done
-theorem typedef_Abs_strict_iff:
+theorem typedef_Abs_bottom_iff:
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"
@@ -244,7 +240,7 @@
apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
done
-theorem typedef_Rep_strict_iff:
+theorem typedef_Rep_bottom_iff:
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"
@@ -258,14 +254,14 @@
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_strict_iff [OF type below UU_in_A])
+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_strict_iff [OF type below UU_in_A])
+by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
subsection {* Proving a subtype is flat *}
--- a/src/HOLCF/Product_Cpo.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Product_Cpo.thy Wed Nov 03 15:56:15 2010 +0100
@@ -173,7 +173,7 @@
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
by (rule minimal_cprod [THEN UU_I, symmetric])
-lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
unfolding inst_cprod_pcpo by simp
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
--- a/src/HOLCF/Sprod.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Sprod.thy Wed Nov 03 15:56:15 2010 +0100
@@ -80,7 +80,7 @@
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
by (simp add: Rep_sprod_simps)
-lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
+lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
by (simp add: Rep_sprod_simps strict_conv_if)
lemma spair_below_iff:
@@ -136,10 +136,10 @@
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
-lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
+lemma sfst_bottom_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
by (cases p, simp_all)
-lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
+lemma ssnd_bottom_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
by (cases p, simp_all)
lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
--- a/src/HOLCF/Ssum.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Ssum.thy Wed Nov 03 15:56:15 2010 +0100
@@ -98,10 +98,10 @@
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
by (simp add: Rep_ssum_simps)
-lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma sinl_bottom_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
using sinl_eq [of "x" "\<bottom>"] by simp
-lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma sinr_bottom_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
using sinr_eq [of "x" "\<bottom>"] by simp
lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
@@ -120,11 +120,11 @@
lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinl]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)
lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x"
unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinr]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)
lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x"
by (safe elim!: compact_sinl compact_sinlD)
@@ -160,7 +160,7 @@
definition
sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
- "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s))"
+ "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))"
translations
"case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
@@ -170,7 +170,7 @@
"\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
lemma beta_sscase:
- "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s)"
+ "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose])
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
--- a/src/HOLCF/Tools/Domain/domain.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain.ML Wed Nov 03 15:56:15 2010 +0100
@@ -221,6 +221,7 @@
(** outer syntax **)
val _ = Keyword.keyword "lazy";
+val _ = Keyword.keyword "unsafe";
val dest_decl : (bool * binding option * string) parser =
Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
@@ -237,11 +238,12 @@
(Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
val domains_decl =
- Parse.and_list1 domain_decl;
+ Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
+ Parse.and_list1 domain_decl;
fun mk_domain
- (definitional : bool)
- (doms : ((((string * string option) list * binding) * mixfix) *
+ (unsafe : bool,
+ doms : ((((string * string option) list * binding) * mixfix) *
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
let
val specs : ((string * string option) list * binding * mixfix *
@@ -249,17 +251,13 @@
map (fn (((vs, t), mx), cons) =>
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
in
- if definitional
- then add_new_domain_cmd specs
- else add_domain_cmd specs
+ if unsafe
+ then add_domain_cmd specs
+ else add_new_domain_cmd specs
end;
val _ =
Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
- Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
-
-val _ =
- Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
- Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
+ Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain));
end;
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Nov 03 15:56:15 2010 +0100
@@ -67,7 +67,7 @@
val simple_ss = HOL_basic_ss addsimps simp_thms;
val beta_rules =
- @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
@@ -210,7 +210,7 @@
in (n2, mk_ssumT (t1, t2)) end;
val ct = ctyp_of thy (snd (cons2typ 1 spec'));
val thm1 = instantiate' [SOME ct] [] @{thm exh_start};
- val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
+ val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1;
val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
val y = Free ("y", lhsT);
@@ -279,8 +279,8 @@
val lhs = mk_undef (list_ccomb (con, vs));
val rhss = map mk_undef nonlazy;
val goal = mk_trp (iff_disj (lhs, rhss));
- val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
- val rules = rule1 :: @{thms con_defined_iff_rules};
+ val rule1 = iso_locale RS @{thm iso.abs_bottom_iff};
+ val rules = rule1 :: @{thms con_bottom_iff_rules};
val tacs = [simp_tac (HOL_ss addsimps rules) 1];
in prove thy con_betas goal (K tacs) end;
in
@@ -453,7 +453,7 @@
fun argvars n args = map_index (argvar n) args;
fun app s (l, r) = mk_appl (Constant s) [l, r];
val cabs = app "_cabs";
- val capp = app @{const_syntax Rep_CFun};
+ val capp = app @{const_syntax Rep_cfun};
val capps = Library.foldl capp
fun con1 authentic n (con,args) =
Library.foldl capp (c_ast authentic con, argvars n args);
@@ -506,7 +506,7 @@
val goal = Logic.list_implies (assms, concl);
val defs = case_beta :: con_betas;
val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
- val rules2 = @{thms con_defined_iff_rules};
+ val rules2 = @{thms con_bottom_iff_rules};
val rules3 = @{thms cfcomp2 one_case2};
val rules = abs_inverse :: rules1 @ rules2 @ rules3;
val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
@@ -528,7 +528,7 @@
(rep_const : term)
(abs_inv : thm)
(rep_strict : thm)
- (rep_strict_iff : thm)
+ (rep_bottom_iff : thm)
(con_betas : thm list)
(thy : theory)
: thm list * theory =
@@ -637,7 +637,7 @@
(* prove selector definedness rules *)
val sel_defins : thm list =
let
- val rules = rep_strict_iff :: @{thms sel_defined_iff_rules};
+ val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules};
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
fun sel_defin sel =
let
@@ -868,8 +868,8 @@
val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
val rep_strict = iso_locale RS @{thm iso.rep_strict};
val abs_strict = iso_locale RS @{thm iso.abs_strict};
- val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
- val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
+ val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff};
+ val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff};
val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict];
(* qualify constants and theorems with domain name *)
@@ -908,7 +908,7 @@
map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
in
add_selectors sel_spec rep_const
- abs_iso_thm rep_strict rep_defined_iff con_betas thy
+ abs_iso_thm rep_strict rep_bottom_iff con_betas thy
end;
(* define and prove theorems for discriminator functions *)
--- a/src/HOLCF/Tools/Domain/domain_induction.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML Wed Nov 03 15:56:15 2010 +0100
@@ -132,7 +132,7 @@
mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons;
val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos);
- val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
+ val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews);
fun quant_tac ctxt i = EVERY
(map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names);
@@ -317,7 +317,7 @@
end;
val goal =
mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)));
- val rules = @{thm Rep_CFun_strict1} :: take_0_thms;
+ val rules = @{thm Rep_cfun_strict1} :: take_0_thms;
fun tacf {prems, context} =
let
val prem' = rewrite_rule [bisim_def_thm] (hd prems);
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 03 15:56:15 2010 +0100
@@ -38,7 +38,7 @@
struct
val beta_rules =
- @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'};
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
@@ -155,7 +155,7 @@
(* convert parameters to lambda abstractions *)
fun mk_eqn (lhs, rhs) =
case lhs of
- Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
+ Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) =>
mk_eqn (f, big_lambda x rhs)
| f $ Const (@{const_name TYPE}, T) =>
mk_eqn (f, Abs ("t", T, rhs))
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Nov 03 15:56:15 2010 +0100
@@ -106,7 +106,7 @@
};
val beta_rules =
- @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
--- a/src/HOLCF/Tools/cont_consts.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Wed Nov 03 15:56:15 2010 +0100
@@ -28,7 +28,7 @@
in
[Syntax.ParsePrintRule
(Syntax.mk_appl (Constant name2) (map Variable vnames),
- fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_CFun}) [t, Variable a])
+ fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
vnames (Constant name1))] @
(case mx of
Infix _ => [extra_parse_rule]
--- a/src/HOLCF/Tools/cont_proc.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML Wed Nov 03 15:56:15 2010 +0100
@@ -19,19 +19,19 @@
val cont_K = @{thm cont_const};
val cont_I = @{thm cont_id};
-val cont_A = @{thm cont2cont_Rep_CFun};
+val cont_A = @{thm cont2cont_APP};
val cont_L = @{thm cont2cont_LAM};
-val cont_R = @{thm cont_Rep_CFun2};
+val cont_R = @{thm cont_Rep_cfun2};
(* checks whether a term contains no dangling bound variables *)
fun is_closed_term t = not (Term.loose_bvar (t, 0));
(* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const (@{const_name Rep_CFun}, _) $ t $ u) =
+fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
is_lcf_term t andalso is_lcf_term u
- | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+ | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
is_lcf_term t
- | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ t) =
+ | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
| is_lcf_term (Bound _) = true
| is_lcf_term t = is_closed_term t;
@@ -67,17 +67,17 @@
(* first list: cont thm for each dangling bound variable *)
(* second list: cont thm for each LAM in t *)
(* if b = false, only return cont thm for outermost LAMs *)
- fun cont_thms1 b (Const (@{const_name Rep_CFun}, _) $ f $ t) =
+ fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) =
let
val (cs1,ls1) = cont_thms1 b f;
val (cs2,ls2) = cont_thms1 b t;
in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
- | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+ | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
let
val (cs, ls) = cont_thms1 b t;
val (cs', l) = lam cs;
in (cs', l::ls) end
- | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ t) =
+ | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) =
let
val t' = Term.incr_boundvars 1 t $ Bound 0;
val (cs, ls) = cont_thms1 b t';
@@ -109,7 +109,7 @@
fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
let
- val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
+ val f' = Const (@{const_name Abs_cfun}, dummyT) $ f;
in
if is_lcf_term f'
then new_cont_tac f'
--- a/src/HOLCF/Tools/fixrec.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Wed Nov 03 15:56:15 2010 +0100
@@ -65,7 +65,7 @@
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
(* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
+fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
| chead_of u = u;
infix 0 ==; val (op ==) = Logic.mk_equals;
@@ -82,7 +82,7 @@
val run = Const(@{const_name Fixrec.run}, mT ->> T)
in
case t of
- Const(@{const_name Rep_CFun}, _) $
+ Const(@{const_name Rep_cfun}, _) $
Const(@{const_name Fixrec.succeed}, _) $ u => u
| _ => run ` t
end;
@@ -226,7 +226,7 @@
(* compiles a monadic term for a constructor pattern *)
and comp_con T p rhs vs taken =
case p of
- Const(@{const_name Rep_CFun},_) $ f $ x =>
+ Const(@{const_name Rep_cfun},_) $ f $ x =>
let val (rhs', v, taken') = comp_pat x rhs taken
in comp_con T f rhs' (v::vs) taken' end
| f $ x =>
@@ -250,7 +250,7 @@
(* returns (constant, (vars, matcher)) *)
fun compile_lhs match_name pat rhs vs taken =
case pat of
- Const(@{const_name Rep_CFun}, _) $ f $ x =>
+ Const(@{const_name Rep_cfun}, _) $ f $ x =>
let val (rhs', v, taken') = compile_pat match_name x rhs taken;
in compile_lhs match_name f rhs' (v::vs) taken' end
| Free(_,_) => (pat, (vs, rhs))
--- a/src/HOLCF/Tools/holcf_library.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/holcf_library.ML Wed Nov 03 15:56:15 2010 +0100
@@ -76,10 +76,10 @@
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
fun capply_const (S, T) =
- Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+ Const(@{const_name Rep_cfun}, (S ->> T) --> (S --> T));
fun cabs_const (S, T) =
- Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+ Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T));
fun mk_cabs t =
let val T = fastype_of t
--- a/src/HOLCF/Tools/pcpodef.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Wed Nov 03 15:56:15 2010 +0100
@@ -11,7 +11,7 @@
{ below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
lub: thm, thelub: thm, compact: thm }
type pcpo_info =
- { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+ { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
Rep_defined: thm, Abs_defined: thm }
val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
@@ -48,7 +48,7 @@
lub: thm, thelub: thm, compact: thm }
type pcpo_info =
- { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+ { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
Rep_defined: thm, Abs_defined: thm }
(* building terms *)
@@ -136,8 +136,8 @@
fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
val Rep_strict = make @{thm typedef_Rep_strict};
val Abs_strict = make @{thm typedef_Abs_strict};
- val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
- val Abs_strict_iff = make @{thm typedef_Abs_strict_iff};
+ 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) =
@@ -146,14 +146,14 @@
|> Global_Theory.add_thms
([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []),
((Binding.suffix_name "_strict" Abs_name, Abs_strict), []),
- ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
- ((Binding.suffix_name "_strict_iff" Abs_name, Abs_strict_iff), []),
+ ((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), [])])
||> Sign.parent_path;
val pcpo_info =
{ Rep_strict = Rep_strict, Abs_strict = Abs_strict,
- Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
+ Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
Rep_defined = Rep_defined, Abs_defined = Abs_defined };
in
(pcpo_info, thy)
--- a/src/HOLCF/Tr.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tr.thy Wed Nov 03 15:56:15 2010 +0100
@@ -64,36 +64,37 @@
default_sort pcpo
-definition
- trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
- ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
+definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" where
+ "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
+
abbreviation
- cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) where
- "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
+ cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
+where
+ "If b then e1 else e2 == tr_case\<cdot>e1\<cdot>e2\<cdot>b"
translations
- "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
- "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
+ "\<Lambda> (XCONST TT). t" == "CONST tr_case\<cdot>t\<cdot>\<bottom>"
+ "\<Lambda> (XCONST FF). t" == "CONST tr_case\<cdot>\<bottom>\<cdot>t"
lemma ifte_thms [simp]:
- "If \<bottom> then e1 else e2 fi = \<bottom>"
- "If FF then e1 else e2 fi = e2"
- "If TT then e1 else e2 fi = e1"
-by (simp_all add: ifte_def TT_def FF_def)
+ "If \<bottom> then e1 else e2 = \<bottom>"
+ "If FF then e1 else e2 = e2"
+ "If TT then e1 else e2 = e1"
+by (simp_all add: tr_case_def TT_def FF_def)
subsection {* Boolean connectives *}
definition
trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
- andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
+ andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
abbreviation
andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where
"x andalso y == trand\<cdot>x\<cdot>y"
definition
tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
- orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)"
+ orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
abbreviation
orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where
"x orelse y == tror\<cdot>x\<cdot>y"
@@ -104,11 +105,11 @@
definition
If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
- "If2 Q x y = (If Q then x else y fi)"
+ "If2 Q x y = (If Q then x else y)"
text {* tactic for tr-thms with case split *}
-lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
+lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def
text {* lemmas about andalso, orelse, neg and if *}
@@ -182,7 +183,7 @@
by (simp add: TT_def)
lemma If_and_if:
- "(If Def P then A else B fi) = (if P then A else B)"
+ "(If Def P then A else B) = (if P then A else B)"
apply (rule_tac p = "Def P" in trE)
apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
done
--- a/src/HOLCF/Tutorial/Domain_ex.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tutorial/Domain_ex.thy Wed Nov 03 15:56:15 2010 +0100
@@ -105,19 +105,21 @@
text {* Lazy constructor arguments may have unpointed types. *}
-domain natlist = nnil | ncons (lazy "nat discr") natlist
+domain (unsafe) natlist = nnil | ncons (lazy "nat discr") natlist
text {* Class constraints may be given for type parameters on the LHS. *}
-domain ('a::cpo) box = Box (lazy 'a)
+domain (unsafe) ('a::cpo) box = Box (lazy 'a)
+
+domain (unsafe) ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
subsection {* Generated constants and theorems *}
domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
-lemmas tree_abs_defined_iff =
- iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
+lemmas tree_abs_bottom_iff =
+ iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
text {* Rules about ismorphism *}
term tree_rep
@@ -196,11 +198,4 @@
-- "Inner syntax error: unexpected end of input"
*)
-text {*
- Non-cpo type parameters currently do not work.
-*}
-(*
-domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
-*)
-
end
--- a/src/HOLCF/Tutorial/New_Domain.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Tutorial/New_Domain.thy Wed Nov 03 15:56:15 2010 +0100
@@ -9,8 +9,8 @@
begin
text {*
- The definitional domain package only works with bifinite domains,
- i.e. types in class @{text bifinite}.
+ UPDATE: The definitional back-end is now the default mode of the domain
+ package. This file should be merged with @{text Domain_ex.thy}.
*}
default_sort bifinite
@@ -21,7 +21,7 @@
domain package.
*}
-new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
text {*
The difference is that the new domain package is completely
@@ -38,7 +38,7 @@
indirect recursion through the lazy list type constructor.
*}
-new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
text {*
For indirect-recursive definitions, the domain package is not able to
--- a/src/HOLCF/Up.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/Up.thy Wed Nov 03 15:56:15 2010 +0100
@@ -237,7 +237,7 @@
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
by (safe elim!: compact_up compact_upD)
--- a/src/HOLCF/UpperPD.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Wed Nov 03 15:56:15 2010 +0100
@@ -233,10 +233,10 @@
lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
by (rule UU_I, rule upper_plus_below2)
-lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
-lemma upper_plus_strict_iff [simp]:
+lemma upper_plus_bottom_iff [simp]:
"xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
apply (rule iffI)
apply (erule rev_mp)
@@ -252,7 +252,7 @@
lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
apply (safe elim!: compact_upper_unit)
apply (simp only: compact_def upper_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
done
lemma compact_upper_plus [simp]:
--- a/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 03 15:56:15 2010 +0100
@@ -31,7 +31,7 @@
foo_bar_baz_deflF ::
"defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
where
- "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3).
+ "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
, u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
@@ -269,7 +269,7 @@
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
where
- "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
+ "foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3).
(
foo_abs oo
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
--- a/src/HOLCF/ex/Hoare.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/ex/Hoare.thy Wed Nov 03 15:56:15 2010 +0100
@@ -30,11 +30,11 @@
definition
p :: "'a -> 'a" where
- "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)"
+ "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)"
definition
q :: "'a -> 'a" where
- "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)"
+ "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x)"
(* --------- pure HOLCF logic, some little lemmas ------ *)
@@ -102,13 +102,13 @@
(* ----- access to definitions ----- *)
-lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
+lemma p_def3: "p$x = If b1$x then p$(g$x) else x"
apply (rule trans)
apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
apply simp
done
-lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
+lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x"
apply (rule trans)
apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
apply simp
--- a/src/HOLCF/ex/Loop.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/ex/Loop.thy Wed Nov 03 15:56:15 2010 +0100
@@ -10,23 +10,23 @@
definition
step :: "('a -> tr)->('a -> 'a)->'a->'a" where
- "step = (LAM b g x. If b$x then g$x else x fi)"
+ "step = (LAM b g x. If b$x then g$x else x)"
definition
while :: "('a -> tr)->('a -> 'a)->'a->'a" where
- "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
+ "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x))"
(* ------------------------------------------------------------------------- *)
(* access to definitions *)
(* ------------------------------------------------------------------------- *)
-lemma step_def2: "step$b$g$x = If b$x then g$x else x fi"
+lemma step_def2: "step$b$g$x = If b$x then g$x else x"
apply (unfold step_def)
apply simp
done
-lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)"
+lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x)"
apply (unfold while_def)
apply simp
done
@@ -36,7 +36,7 @@
(* rekursive properties of while *)
(* ------------------------------------------------------------------------- *)
-lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x fi"
+lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x"
apply (rule trans)
apply (rule while_def2 [THEN fix_eq5])
apply simp
--- a/src/HOLCF/ex/Pattern_Match.thy Wed Nov 03 13:54:23 2010 +0100
+++ b/src/HOLCF/ex/Pattern_Match.thy Wed Nov 03 15:56:15 2010 +0100
@@ -8,6 +8,8 @@
imports HOLCF
begin
+default_sort pcpo
+
text {* FIXME: Find a proper way to un-hide constants. *}
abbreviation fail :: "'a match"
@@ -115,9 +117,9 @@
parse_translation {*
(* rewrite (_pat x) => (succeed) *)
-(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
+(* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
[(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
- mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
+ mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
*}
text {* Printing Case expressions *}
@@ -127,14 +129,14 @@
print_translation {*
let
- fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
+ fun dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax unit_when},_) $ t) =
(Syntax.const @{syntax_const "_noargs"}, t)
- | dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
+ | dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax csplit},_) $ t) =
let
val (v1, t1) = dest_LAM t;
val (v2, t2) = dest_LAM t1;
in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
- | dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
+ | dest_LAM (Const (@{const_syntax Abs_cfun},_) $ t) =
let
val abs =
case t of Abs abs => abs
@@ -149,7 +151,7 @@
(Syntax.const @{syntax_const "_match"} $ p $ v) $ t
end;
- in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
+ in [(@{const_syntax Rep_cfun}, Case1_tr')] end;
*}
translations
@@ -184,11 +186,11 @@
definition
TT_pat :: "(tr, unit) pat" where
- "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail fi)"
+ "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail)"
definition
FF_pat :: "(tr, unit) pat" where
- "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>() fi)"
+ "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>())"
definition
ONE_pat :: "(one, unit) pat" where
@@ -363,7 +365,7 @@
infix 9 ` ;
val beta_rules =
- @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
@@ -485,7 +487,7 @@
open Syntax
fun syntax c = Syntax.mark_const (fst (dest_Const c));
fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
- val capp = app @{const_syntax Rep_CFun};
+ val capp = app @{const_syntax Rep_cfun};
val capps = Library.foldl capp
fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];
--- a/src/Tools/Code/code_runtime.ML Wed Nov 03 13:54:23 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Nov 03 15:56:15 2010 +0100
@@ -418,8 +418,7 @@
(0, Path.implode filepath) false (File.read filepath);
val thy'' = (Context.the_theory o the) (Context.thread_data ());
val names = Loaded_Values.get thy'';
- val thy''' = Thy_Load.provide_file filepath thy'';
- in (names, thy''') end;
+ in (names, thy'') end;
end;