# HG changeset patch
# User huffman
# Date 1131223837 -3600
# Node ID 2c5d5da79a1eb823a08e2d4643ef9f25d98c732c
# Parent  820cfb3da6d3847ad5aaa138290d365d42991922
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM

diff -r 820cfb3da6d3 -r 2c5d5da79a1e src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Cfun.thy	Sat Nov 05 21:50:37 2005 +0100
@@ -166,12 +166,11 @@
 subsection {* Continuity of application *}
 
 lemma cont_Rep_CFun1: "cont (\<lambda>f. f\<cdot>x)"
-by (rule cont_Rep_CFun [THEN cont2cont_CF1L])
+by (rule cont_Rep_CFun [THEN cont2cont_fun])
 
 lemma cont_Rep_CFun2: "cont (\<lambda>x. f\<cdot>x)"
-apply (rule_tac P = "cont" in CollectD)
-apply (fold CFun_def)
-apply (rule Rep_CFun)
+apply (cut_tac x=f in Rep_CFun)
+apply (simp add: CFun_def)
 done
 
 lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono]
@@ -226,6 +225,10 @@
 apply (erule chainE)
 done
 
+lemma ch2ch_LAM: "\<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 expand_cfun_less)
+
 text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
 
 lemma contlub_cfun: 
@@ -239,6 +242,14 @@
 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 ch2ch_LAM)
+apply (simp add: Abs_CFun_inverse2)
+apply (simp add: thelub_fun ch2ch_lambda)
+done
+
 text {* strictness *}
 
 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
diff -r 820cfb3da6d3 -r 2c5d5da79a1e src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Cont.ML	Sat Nov 05 21:50:37 2005 +0100
@@ -8,8 +8,7 @@
 val cont2cont_app2 = thm "cont2cont_app2";
 val cont2cont_app3 = thm "cont2cont_app3";
 val cont2cont_app = thm "cont2cont_app";
-val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev";
-val cont2cont_CF1L = thm "cont2cont_CF1L";
+val cont2cont_fun = thm "cont2cont_fun";
 val cont2cont_lambda = thm "cont2cont_lambda";
 val cont2contlub_app = thm "cont2contlub_app";
 val cont2contlubE = thm "cont2contlubE";
@@ -31,8 +30,8 @@
 val flatdom_strict2cont = thm "flatdom_strict2cont";
 val flatdom_strict2mono = thm "flatdom_strict2mono";
 val mono2mono_app = thm "mono2mono_app";
-val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev";
-val mono2mono_MF1L = thm "mono2mono_MF1L";
+val mono2mono_fun = thm "mono2mono_fun";
+val mono2mono_lambda = thm "mono2mono_lambda";
 val monocontlub2cont = thm "monocontlub2cont";
 val monofun_def = thm "monofun_def";
 val monofunE = thm "monofunE";
diff -r 820cfb3da6d3 -r 2c5d5da79a1e src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Cont.thy	Sat Nov 05 21:50:37 2005 +0100
@@ -194,14 +194,14 @@
   "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
 by (simp add: thelub_fun [symmetric] cont_lub_fun)
 
-lemma mono2mono_MF1L: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
+lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
 apply (rule monofunI)
 apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
 done
 
-lemma cont2cont_CF1L: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
+lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
 apply (rule monocontlub2cont)
-apply (erule cont2mono [THEN mono2mono_MF1L])
+apply (erule cont2mono [THEN mono2mono_fun])
 apply (rule contlubI)
 apply (simp add: cont2contlubE)
 apply (simp add: thelub_fun ch2ch_cont)
@@ -209,13 +209,13 @@
 
 text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
 
-lemma mono2mono_MF1L_rev: "\<forall>y. monofun (\<lambda>x. f x y) \<Longrightarrow> monofun f"
+lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f"
 apply (rule monofunI)
 apply (rule less_fun_ext)
 apply (blast dest: monofunE)
 done
 
-lemma cont2cont_CF1L_rev: "\<forall>y. cont (\<lambda>x. f x y) \<Longrightarrow> cont f"
+lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
 apply (subgoal_tac "monofun f")
 apply (rule monocontlub2cont)
 apply assumption
@@ -223,20 +223,23 @@
 apply (rule ext)
 apply (simp add: thelub_fun ch2ch_monofun)
 apply (blast dest: cont2contlubE)
-apply (simp add: mono2mono_MF1L_rev cont2mono)
+apply (simp add: mono2mono_lambda cont2mono)
 done
 
-lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. (\<lambda>y. f x y))"
-by (rule cont2cont_CF1L_rev, simp)
+text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
 
-text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
+lemma contlub_lambda:
+  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
+    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
+by (simp add: thelub_fun ch2ch_lambda)
 
 lemma contlub_abstraction:
   "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
     (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
-apply (drule cont2cont_CF1L_rev)
 apply (rule thelub_fun [symmetric])
-apply (erule (1) ch2ch_cont)
+apply (rule ch2ch_cont)
+apply (simp add: cont2cont_lambda)
+apply assumption
 done
 
 lemma mono2mono_app:
diff -r 820cfb3da6d3 -r 2c5d5da79a1e src/HOLCF/Ffun.ML
--- a/src/HOLCF/Ffun.ML	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Ffun.ML	Sat Nov 05 21:50:37 2005 +0100
@@ -4,7 +4,7 @@
 val antisym_less_fun = thm "antisym_less_fun";
 val app_strict = thm "app_strict";
 val ch2ch_fun = thm "ch2ch_fun";
-val ch2ch_fun_rev = thm "ch2ch_fun_rev";
+val ch2ch_lambda = thm "ch2ch_lambda";
 val cpo_fun = thm "cpo_fun";
 val expand_fun_less = thm "expand_fun_less";
 val inst_fun_pcpo = thm "inst_fun_pcpo";
diff -r 820cfb3da6d3 -r 2c5d5da79a1e src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Ffun.thy	Sat Nov 05 21:50:37 2005 +0100
@@ -55,7 +55,7 @@
 lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
 by (simp add: chain_def less_fun_def)
 
-lemma ch2ch_fun_rev: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
+lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
 by (simp add: chain_def less_fun_def)
 
 
diff -r 820cfb3da6d3 -r 2c5d5da79a1e src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Fix.thy	Sat Nov 05 21:50:37 2005 +0100
@@ -71,7 +71,7 @@
 apply (unfold fix_def)
 apply (rule beta_cfun)
 apply (rule cont2cont_lub)
-apply (rule ch2ch_fun_rev)
+apply (rule ch2ch_lambda)
 apply (rule chain_iterate)
 apply simp
 done
diff -r 820cfb3da6d3 -r 2c5d5da79a1e src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Lift.thy	Sat Nov 05 21:50:37 2005 +0100
@@ -103,10 +103,10 @@
 *}
 
 lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_Rep_CFun [THEN cont2cont_CF1L])
+by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
 
 lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
-by (rule cont_Rep_CFun_app [THEN cont2cont_CF1L])
+by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
 
 subsection {* Further operations *}
 
@@ -128,7 +128,7 @@
 apply (induct x)
 apply simp
 apply simp
-apply (rule cont_id [THEN cont2cont_CF1L])
+apply (rule cont_id [THEN cont2cont_fun])
 done
 
 lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"