# HG changeset patch
# User huffman
# Date 1287752931 25200
# Node ID 49b9d301fadb8bb2eb439bc554f59fd14b0fbe6d
# Parent  1b5f394866d9862506f9b774f561a4b5c633b6ce
simplify proofs about flift; remove unneeded lemmas

diff -r 1b5f394866d9 -r 49b9d301fadb src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Fri Oct 22 05:54:54 2010 -0700
+++ b/src/HOLCF/Lift.thy	Fri Oct 22 06:08:51 2010 -0700
@@ -80,6 +80,18 @@
     by (induct x) auto
 qed
 
+subsection {* Continuity of @{const lift_case} *}
+
+lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
+apply (induct x, unfold lift.cases)
+apply (simp add: Rep_lift_strict)
+apply (simp add: Def_def Abs_lift_inverse)
+done
+
+lemma cont2cont_lift_case [simp]:
+  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
+unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose])
+
 subsection {* Further operations *}
 
 definition
@@ -90,59 +102,14 @@
   flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
   "flift2 f = (FLIFT x. Def (f x))"
 
-subsection {* Continuity Proofs for flift1, flift2 *}
-
-text {* Need the instance of @{text flat}. *}
-
-lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
-apply (induct x)
-apply simp
-apply simp
-apply (rule cont_id [THEN cont2cont_fun])
-done
-
-lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
-apply (rule flatdom_strict2cont)
-apply simp
-done
-
-lemma cont_flift1: "cont flift1"
-unfolding flift1_def
-apply (rule cont2cont_LAM)
-apply (rule cont_lift_case2)
-apply (rule cont_lift_case1)
-done
-
-lemma FLIFT_mono:
-  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
-apply (rule monofunE [where f=flift1])
-apply (rule cont2mono [OF cont_flift1])
-apply (simp add: fun_below_iff)
-done
-
-lemma cont2cont_flift1 [simp, cont2cont]:
-  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
-apply (rule cont_flift1 [THEN cont_compose])
-apply simp
-done
-
-lemma cont2cont_lift_case [simp]:
-  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
-apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
-apply (simp add: flift1_def cont_lift_case2)
-apply simp
-done
-
-text {* rewrites for @{term flift1}, @{term flift2} *}
-
 lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
-by (simp add: flift1_def cont_lift_case2)
+by (simp add: flift1_def)
 
 lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
 by (simp add: flift2_def)
 
 lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
-by (simp add: flift1_def cont_lift_case2)
+by (simp add: flift1_def)
 
 lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
 by (simp add: flift2_def)
@@ -153,4 +120,12 @@
 lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
 by (cases x, simp_all)
 
+lemma FLIFT_mono:
+  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
+by (rule cfun_belowI, case_tac x, simp_all)
+
+lemma cont2cont_flift1 [simp, cont2cont]:
+  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
+by (simp add: flift1_def cont2cont_LAM)
+
 end