# HG changeset patch
# User huffman
# Date 1116982186 -7200
# Node ID c57725e8055a4f5f570f1e05e48034524d9fd3c8
# Parent  c2257f8a73bb5ec770b598ef3a749e8bfab08886
shorted proof that lift is chfin

diff -r c2257f8a73bb -r c57725e8055a src/HOLCF/Lift.ML
--- a/src/HOLCF/Lift.ML	Wed May 25 01:47:11 2005 +0200
+++ b/src/HOLCF/Lift.ML	Wed May 25 02:49:46 2005 +0200
@@ -24,7 +24,6 @@
 val Lift_exhaust = thm "Lift_exhaust";
 val UU_lift_def = thm "UU_lift_def";
 val Undef_eq_UU = thm "Undef_eq_UU";
-val chain_mono2_po = thm "chain_mono2_po";
 val cont2cont_CF1L_rev2 = thm "cont2cont_CF1L_rev2";
 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
 val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
@@ -33,7 +32,6 @@
 val cont_flift1_not_arg = thm "cont_flift1_not_arg";
 val cont_flift2_arg = thm "cont_flift2_arg";
 val cont_if = thm "cont_if";
-val cpo_lift = thm "cpo_lift";
 val flat_imp_chfin_poo = thm "flat_imp_chfin_poo";
 val flift1_Def = thm "flift1_Def";
 val flift1_UU = thm "flift1_UU";
@@ -49,5 +47,4 @@
 val less_lift_def = thm "less_lift_def";
 val liftpair_def = thm "liftpair_def";
 val minimal_lift = thm "minimal_lift";
-val notUndef_I = thm "notUndef_I";
 val not_Undef_is_Def = thm "not_Undef_is_Def";
diff -r c2257f8a73bb -r c57725e8055a src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Wed May 25 01:47:11 2005 +0200
+++ b/src/HOLCF/Lift.thy	Wed May 25 02:49:46 2005 +0200
@@ -64,57 +64,27 @@
   Undef}.
 *}
 
-lemma notUndef_I: "[| x<<y; x ~= Undef |] ==> y ~= Undef"
-  -- {* Tailoring @{text notUU_I} of @{text Pcpo.ML} to @{text Undef} *}
-  by (blast intro: antisym_less)
-
-lemma chain_mono2_po: "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |]
-         ==> EX j. ALL i. j<i-->~Y(i)=Undef"
-  -- {* Tailoring @{text chain_mono2} of @{text Pcpo.ML} to @{text Undef} *}
-  apply safe
-  apply (rule exI)
-  apply (intro strip)
-  apply (rule notUndef_I)
-   apply (erule (1) chain_mono)
-  apply assumption
-  done
-
 lemma flat_imp_chfin_poo: "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))"
   -- {* Tailoring @{text flat_imp_chfin} of @{text Fix.ML} to @{text lift} *}
   apply (unfold max_in_chain_def)
-  apply (intro strip)
-  apply (rule_tac P = "ALL i. Y (i) = Undef" in case_split)
-   apply (rule_tac x = 0 in exI)
-   apply (intro strip)
-   apply (rule trans)
-    apply (erule spec)
-   apply (rule sym)
-   apply (erule spec)
-  apply (subgoal_tac "ALL x y. x << (y:: ('a) lift) --> x=Undef | x=y")
-   prefer 2 apply (simp add: inst_lift_po)
-  apply (rule chain_mono2_po [THEN exE])
-    apply fast
-   apply assumption
-  apply (rule_tac x = "Suc x" in exI)
-  apply (intro strip)
-  apply (rule disjE)
-    prefer 3 apply assumption
-   apply (rule mp)
-    apply (drule spec)
-    apply (erule spec)
-   apply (erule le_imp_less_or_eq [THEN disjE])
-    apply (erule chain_mono)
-    apply auto
+  apply clarify
+  apply (case_tac "ALL i. Y i = Undef")
+   apply simp
+  apply simp
+  apply (erule exE)
+  apply (rule_tac x=i in exI)
+  apply clarify
+  apply (drule chain_mono3, assumption)
+  apply (simp add: less_lift_def)
   done
 
-theorem cpo_lift: "chain (Y::nat => 'a lift) ==> EX x. range Y <<| x"
-  apply (cut_tac flat_imp_chfin_poo)
-  apply (blast intro: lub_finch1)
+instance lift :: (type) chfin
+  apply intro_classes
+  apply (rule flat_imp_chfin_poo)
   done
 
 instance lift :: (type) pcpo
   apply intro_classes
-   apply (erule cpo_lift)
   apply (rule least_lift)
   done