--- a/src/HOLCF/Algebraic.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Algebraic.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Cfun.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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,7 +291,7 @@
subsection {* Continuity simplification procedure *}
-text {* cont2cont lemma for @{term Rep_CFun} *}
+text {* cont2cont lemma for @{term Rep_cfun} *}
lemma cont2cont_APP [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
@@ -299,9 +299,9 @@
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 {*
@@ -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_APP 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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Deflation.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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
--- a/src/HOLCF/Domain_Aux.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Domain_Aux.thy Fri Oct 29 17:15:28 2010 -0700
@@ -83,7 +83,7 @@
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/Fixrec.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Fixrec.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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/IOA/meta_theory/Sequence.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Library/Stream.thy Fri Oct 29 17:15:28 2010 -0700
@@ -921,7 +921,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/LowerPD.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/LowerPD.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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/Ssum.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Ssum.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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)
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Oct 29 17:15:28 2010 -0700
@@ -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);
--- a/src/HOLCF/Tools/Domain/domain_induction.ML Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 29 17:15:28 2010 -0700
@@ -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/cont_consts.ML Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/cont_consts.ML Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/cont_proc.ML Fri Oct 29 17:15:28 2010 -0700
@@ -21,17 +21,17 @@
val cont_I = @{thm cont_id};
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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/holcf_library.ML Fri Oct 29 17:15:28 2010 -0700
@@ -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/Up.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Up.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/UpperPD.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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 Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy Fri Oct 29 17:15:28 2010 -0700
@@ -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/Pattern_Match.thy Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy Fri Oct 29 17:15:28 2010 -0700
@@ -115,9 +115,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 +127,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 +149,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
@@ -485,7 +485,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"];