# HG changeset patch
# User huffman
# Date 1128911906 -7200
# Node ID ccf54e3cabfa1f6d040c9e51c31e7eaf416e4301
# Parent  21183d6f62b82d49f4cbde1d0352c57c6748e499
removed Istrictify; simplified some proofs

diff -r 21183d6f62b8 -r ccf54e3cabfa src/HOLCF/Cfun.ML
--- a/src/HOLCF/Cfun.ML	Mon Oct 10 04:12:31 2005 +0200
+++ b/src/HOLCF/Cfun.ML	Mon Oct 10 04:38:26 2005 +0200
@@ -22,14 +22,14 @@
 val cont_cfun_arg = thm "cont_cfun_arg";
 val cont_cfun_fun = thm "cont_cfun_fun";
 val cont_cfun = thm "cont_cfun";
-val cont_Istrictify1 = thm "cont_Istrictify1";
-val cont_Istrictify2 = thm "cont_Istrictify2";
+val cont_strictify1 = thm "cont_strictify1";
+val cont_strictify2 = thm "cont_strictify2";
 val cont_lemmas1 = thms "cont_lemmas1";
 val contlub_cfun_arg = thm "contlub_cfun_arg";
 val contlub_cfun_fun = thm "contlub_cfun_fun";
 val cont_lub_cfun = thm "cont_lub_cfun";
 val contlub_cfun = thm "contlub_cfun";
-val contlub_Istrictify2 = thm "contlub_Istrictify2";
+val contlub_strictify2 = thm "contlub_strictify2";
 val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1";
 val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2";
 val cont_Rep_CFun1 = thm "cont_Rep_CFun1";
@@ -49,9 +49,6 @@
 val injection_eq = thm "injection_eq";
 val injection_less = thm "injection_less";
 val inst_cfun_pcpo = thm "inst_cfun_pcpo";
-val Istrictify1 = thm "Istrictify1";
-val Istrictify2 = thm "Istrictify2";
-val Istrictify_def = thm "Istrictify_def";
 val less_cfun_def = thm "less_CFun_def";
 val less_cfun_ext = thm "less_cfun_ext";
 val lub_cfun_mono = thm "lub_cfun_mono";
@@ -59,7 +56,7 @@
 val monofun_cfun_arg = thm "monofun_cfun_arg";
 val monofun_cfun_fun = thm "monofun_cfun_fun";
 val monofun_cfun = thm "monofun_cfun";
-val monofun_Istrictify2 = thm "monofun_Istrictify2";
+val monofun_strictify2 = thm "monofun_strictify2";
 val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1";
 val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2";
 val oo_def = thm "oo_def";
@@ -77,7 +74,6 @@
 structure Cfun =
 struct
   val thy = the_context ();
-  val Istrictify_def = Istrictify_def;
   val strictify_def = strictify_def;
   val ID_def = ID_def;
   val oo_def = oo_def;
diff -r 21183d6f62b8 -r ccf54e3cabfa src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Oct 10 04:12:31 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Mon Oct 10 04:38:26 2005 +0200
@@ -405,67 +405,47 @@
 
 defaultsort pcpo
 
-consts  
-  Istrictify :: "('a \<rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+constdefs
   strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b"
-
-defs
-  Istrictify_def: "Istrictify f x \<equiv> if x = \<bottom> then \<bottom> else f\<cdot>x"    
-  strictify_def:  "strictify \<equiv> (\<Lambda> f x. Istrictify f x)"
+  "strictify \<equiv> (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
 
 text {* results about strictify *}
 
-lemma Istrictify1: "Istrictify f \<bottom> = \<bottom>"
-by (simp add: Istrictify_def)
+lemma cont_strictify1: "cont (\<lambda>f. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+by (simp add: cont_if)
 
-lemma Istrictify2: "x \<noteq> \<bottom> \<Longrightarrow> Istrictify f x = f\<cdot>x"
-by (simp add: Istrictify_def)
-
-lemma cont_Istrictify1: "cont (\<lambda>f. Istrictify f x)"
-apply (case_tac "x = \<bottom>")
-apply (simp add: Istrictify1)
-apply (simp add: Istrictify2)
+lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+apply (rule monofunI)
+apply (auto simp add: monofun_cfun_arg eq_UU_iff [symmetric])
 done
 
-lemma monofun_Istrictify2: "monofun (\<lambda>x. Istrictify f x)"
-apply (rule monofunI)
-apply (simp add: Istrictify_def monofun_cfun_arg)
-apply clarify
-apply (simp add: eq_UU_iff)
-done
-
-lemma contlub_Istrictify2: "contlub (\<lambda>x. Istrictify f x)"
+(*FIXME: long proof*)
+lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
 apply (rule contlubI)
 apply (case_tac "lub (range Y) = \<bottom>")
 apply (drule (1) chain_UU_I)
-apply (simp add: Istrictify1 thelub_const)
-apply (simp add: Istrictify2)
-apply (simp add: contlub_cfun_arg)
+apply (simp add: thelub_const)
+apply (simp del: if_image_distrib)
+apply (simp only: contlub_cfun_arg)
 apply (rule lub_equal2)
 apply (rule chain_mono2 [THEN exE])
 apply (erule chain_UU_I_inverse2)
 apply (assumption)
-apply (blast intro: Istrictify2 [symmetric])
+apply (rule_tac x=x in exI, clarsimp)
 apply (erule chain_monofun)
-apply (erule monofun_Istrictify2 [THEN ch2ch_monofun])
+apply (erule monofun_strictify2 [THEN ch2ch_monofun])
 done
 
-lemmas cont_Istrictify2 =
-  monocontlub2cont [OF monofun_Istrictify2 contlub_Istrictify2, standard]
+lemmas cont_strictify2 =
+  monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard]
+
+lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
+by (unfold strictify_def, simp add: cont_strictify1 cont_strictify2)
 
 lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
-apply (unfold strictify_def)
-apply (simp add: cont_Istrictify1 cont_Istrictify2)
-apply (rule Istrictify1)
-done
+by (simp add: strictify_conv_if)
 
 lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
-apply (unfold strictify_def)
-apply (simp add: cont_Istrictify1 cont_Istrictify2)
-apply (erule Istrictify2)
-done
-
-lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
-by simp
+by (simp add: strictify_conv_if)
 
 end