--- a/src/HOLCF/Cfun.thy Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Cfun.thy Fri Oct 29 16:51:40 2010 -0700
@@ -293,7 +293,7 @@
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))"
@@ -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)"} *}
@@ -356,7 +356,7 @@
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 *}
--- a/src/HOLCF/HOLCF.thy Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/HOLCF.thy Fri Oct 29 16:51:40 2010 -0700
@@ -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/Tools/Domain/domain_constructors.ML Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Oct 29 16:51:40 2010 -0700
@@ -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);
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 29 16:51:40 2010 -0700
@@ -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);
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Oct 29 16:51:40 2010 -0700
@@ -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_proc.ML Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/cont_proc.ML Fri Oct 29 16:51:40 2010 -0700
@@ -19,7 +19,7 @@
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};
--- a/src/HOLCF/ex/Pattern_Match.thy Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy Fri Oct 29 16:51:40 2010 -0700
@@ -363,7 +363,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);