--- a/src/HOLCF/Lift.ML Sat Nov 03 01:36:19 2001 +0100
+++ b/src/HOLCF/Lift.ML Sat Nov 03 01:38:11 2001 +0100
@@ -1,108 +1,53 @@
-(* Title: HOLCF/Lift.ML
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 Technische Universitaet Muenchen
-Theorems for Lift.thy
-*)
-
-
-(* ---------------------------------------------------------- *)
- section"Continuity Proofs for flift1, flift2, if";
-(* ---------------------------------------------------------- *)
-(* need the instance into flat *)
-
-
-(* flift1 is continuous in its argument itself*)
-Goal "cont (lift_case UU f)";
-by (rtac flatdom_strict2cont 1);
-by (Simp_tac 1);
-qed"cont_flift1_arg";
-
-(* flift1 is continuous in a variable that occurs only
- in the Def branch *)
+(* legacy ML bindings *)
-Goal "!!f. [| !! a. cont (%y. (f y) a) |] ==> \
-\ cont (%y. lift_case UU (f y))";
-by (rtac cont2cont_CF1L_rev 1);
-by (strip_tac 1);
-by (res_inst_tac [("x","y")] Lift_cases 1);
-by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed"cont_flift1_not_arg";
-
-(* flift1 is continuous in a variable that occurs either
- in the Def branch or in the argument *)
-
-Goal "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
-\ cont (%y. lift_case UU (f y) (g y))";
-by (res_inst_tac [("tt","g")] cont2cont_app 1);
-by (rtac cont_flift1_not_arg 1);
-by Auto_tac;
-by (rtac cont_flift1_arg 1);
-qed"cont_flift1_arg_and_not_arg";
-
-(* flift2 is continuous in its argument itself *)
-
-Goal "cont (lift_case UU (%y. Def (f y)))";
-by (rtac flatdom_strict2cont 1);
-by (Simp_tac 1);
-qed"cont_flift2_arg";
-
+structure lift =
+struct
+ val distinct = thms "lift.distinct";
+ val inject = thms "lift.inject";
+ val exhaust = thm "lift.exhaust";
+ val cases = thms "lift.cases";
+ val split = thm "lift.split";
+ val split_asm = thm "lift.split_asm";
+ val induct = thm "lift.induct";
+ val recs = thms "lift.recs";
+ val simps = thms "lift.simps";
+ val size = thms "lift.size";
+end;
-(* ---------------------------------------------------------- *)
-(* Extension of cont_tac and installation of simplifier *)
-(* ---------------------------------------------------------- *)
-
-bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev);
-
-val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
- cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2,
- cont_Rep_CFun_app,cont_Rep_CFun_app_app,cont_if];
-
-val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext;
-
-Addsimps cont_lemmas_ext;
-
-fun cont_tac i = resolve_tac cont_lemmas2 i;
-fun cont_tacR i = REPEAT (cont_tac i);
-
-fun cont_tacRs i = simp_tac (simpset() addsimps [flift1_def,flift2_def]) i THEN
- REPEAT (cont_tac i);
-
-
-simpset_ref() := simpset() addSolver
- (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
-
-
-
-(* ---------------------------------------------------------- *)
- section"flift1, flift2";
-(* ---------------------------------------------------------- *)
-
-
-Goal "flift1 f$(Def x) = (f x)";
-by (simp_tac (simpset() addsimps [flift1_def]) 1);
-qed"flift1_Def";
-
-Goal "flift2 f$(Def x) = Def (f x)";
-by (simp_tac (simpset() addsimps [flift2_def]) 1);
-qed"flift2_Def";
-
-Goal "flift1 f$UU = UU";
-by (simp_tac (simpset() addsimps [flift1_def]) 1);
-qed"flift1_UU";
-
-Goal "flift2 f$UU = UU";
-by (simp_tac (simpset() addsimps [flift2_def]) 1);
-qed"flift2_UU";
-
-Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
-
-Goal "x~=UU ==> (flift2 f)$x~=UU";
-by (def_tac 1);
-qed"flift2_nUU";
-
-Addsimps [flift2_nUU];
-
-
+val Def_not_UU = thm "Def_not_UU";
+val DefE = thm "DefE";
+val DefE2 = thm "DefE2";
+val Def_inject_less_eq = thm "Def_inject_less_eq";
+val Def_less_is_eq = thm "Def_less_is_eq";
+val Lift_cases = thm "Lift_cases";
+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";
+val cont_flift1_arg = thm "cont_flift1_arg";
+val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg";
+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";
+val flift1_def = thm "flift1_def";
+val flift2_Def = thm "flift2_Def";
+val flift2_UU = thm "flift2_UU";
+val flift2_def = thm "flift2_def";
+val flift2_nUU = thm "flift2_nUU";
+val inst_lift_pcpo = thm "inst_lift_pcpo";
+val inst_lift_po = thm "inst_lift_po";
+val least_lift = thm "least_lift";
+val less_lift = thm "less_lift";
+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";
--- a/src/HOLCF/Lift.thy Sat Nov 03 01:36:19 2001 +0100
+++ b/src/HOLCF/Lift.thy Sat Nov 03 01:38:11 2001 +0100
@@ -1,16 +1,339 @@
(* Title: HOLCF/Lift.thy
ID: $Id$
- Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
+ Author: Olaf Mueller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-Lift = Lift3 +
+header {* Lifting types of class term to flat pcpo's *}
+
+theory Lift = Cprod3:
+
+defaultsort "term"
+
+
+typedef 'a lift = "UNIV :: 'a option set" ..
+
+constdefs
+ Undef :: "'a lift"
+ "Undef == Abs_lift None"
+ Def :: "'a => 'a lift"
+ "Def x == Abs_lift (Some x)"
+
+instance lift :: ("term") sq_ord ..
+
+defs (overloaded)
+ less_lift_def: "x << y == (x=y | x=Undef)"
+
+instance lift :: ("term") po
+proof
+ fix x y z :: "'a lift"
+ show "x << x" by (unfold less_lift_def) blast
+ { assume "x << y" and "y << x" thus "x = y" by (unfold less_lift_def) blast }
+ { assume "x << y" and "y << z" thus "x << z" by (unfold less_lift_def) blast }
+qed
+
+lemma inst_lift_po: "(op <<) = (\<lambda>x y. x = y | x = Undef)"
+ -- {* For compatibility with old HOLCF-Version. *}
+ by (simp only: less_lift_def [symmetric])
+
+
+subsection {* Type lift is pointed *}
+
+lemma minimal_lift [iff]: "Undef << x"
+ by (simp add: inst_lift_po)
+
+lemma UU_lift_def: "(SOME u. \<forall>y. u \<sqsubseteq> y) = Undef"
+ apply (rule minimal2UU [symmetric])
+ apply (rule minimal_lift)
+ done
+
+lemma least_lift: "EX x::'a lift. ALL y. x << y"
+ apply (rule_tac x = Undef in exI)
+ apply (rule minimal_lift [THEN allI])
+ done
+
+
+subsection {* Type lift is a cpo *}
+
+text {*
+ The following lemmas have already been proved in @{text Pcpo.ML} and
+ @{text Fix.ML}, but there class @{text pcpo} is assumed, although
+ only @{text po} is necessary and a least element. Therefore they are
+ redone here for the @{text po} lift with least element @{text
+ 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
+ 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)
+ done
+
+instance lift :: ("term") pcpo
+ apply intro_classes
+ apply (erule cpo_lift)
+ apply (rule least_lift)
+ done
+
+lemma inst_lift_pcpo: "UU = Undef"
+ -- {* For compatibility with old HOLCF-Version. *}
+ by (simp add: UU_def UU_lift_def)
+
+
+subsection {* Lift as a datatype *}
+
+lemma lift_distinct1: "UU ~= Def x"
+ by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
+
+lemma lift_distinct2: "Def x ~= UU"
+ by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
+
+lemma Def_inject: "(Def x = Def x') = (x = x')"
+ by (simp add: Def_def Abs_lift_inject lift_def)
+
+lemma lift_induct: "P UU ==> (!!x. P (Def x)) ==> P y"
+ apply (induct y)
+ apply (induct_tac y)
+ apply (simp_all add: Undef_def Def_def inst_lift_pcpo)
+ done
+
+rep_datatype lift
+ distinct lift_distinct1 lift_distinct2
+ inject Def_inject
+ induction lift_induct
+
+lemma Def_not_UU: "Def a ~= UU"
+ by simp
+
+
+subsection {* Further operations *}
+
+consts
+ flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"
+ flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
+ liftpair ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
-instance lift :: (term)flat (ax_flat_lift)
+defs
+ flift1_def:
+ "flift1 f == (LAM x. (case x of
+ UU => UU
+ | Def y => (f y)))"
+ flift2_def:
+ "flift2 f == (LAM x. (case x of
+ UU => UU
+ | Def y => Def (f y)))"
+ liftpair_def:
+ "liftpair x == (case (cfst$x) of
+ UU => UU
+ | Def x1 => (case (csnd$x) of
+ UU => UU
+ | Def x2 => Def (x1,x2)))"
+
+
+declare inst_lift_pcpo [symmetric, simp]
+
+
+lemma less_lift: "(x::'a lift) << y = (x=y | x=UU)"
+ by (simp add: inst_lift_po)
+
+
+text {* @{text UU} and @{text Def} *}
+
+lemma Lift_exhaust: "x = UU | (EX y. x = Def y)"
+ by (induct x) simp_all
+
+lemma Lift_cases: "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"
+ by (insert Lift_exhaust) blast
+
+lemma not_Undef_is_Def: "(x ~= UU) = (EX y. x = Def y)"
+ by (cases x) simp_all
+
+text {*
+ For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
+ x} by @{text "Def a"} in conclusion. *}
+
+ML {*
+ local val not_Undef_is_Def = thm "not_Undef_is_Def"
+ in val def_tac = SIMPSET' (fn ss =>
+ etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss)
+ end;
+*}
+
+lemma Undef_eq_UU: "Undef = UU"
+ by (rule inst_lift_pcpo [symmetric])
+
+lemma DefE: "Def x = UU ==> R"
+ by simp
+
+lemma DefE2: "[| x = Def s; x = UU |] ==> R"
+ by simp
+
+lemma Def_inject_less_eq: "Def x << Def y = (x = y)"
+ by (simp add: less_lift_def)
+
+lemma Def_less_is_eq [simp]: "Def x << y = (Def x = y)"
+ by (simp add: less_lift)
+
+
+subsection {* Lift is flat *}
+
+instance lift :: ("term") flat
+proof
+ show "ALL x y::'a lift. x << y --> x = UU | x = y"
+ by (simp add: less_lift)
+qed
+
+defaultsort pcpo
+
+
+text {*
+ \medskip Two specific lemmas for the combination of LCF and HOL
+ terms.
+*}
+
+lemma cont_Rep_CFun_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)"
+ apply (rule cont2cont_CF1L)
+ apply (tactic "resolve_tac cont_lemmas1 1")+
+ apply auto
+ done
+
+lemma cont_Rep_CFun_app_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)"
+ apply (rule cont2cont_CF1L)
+ apply (erule cont_Rep_CFun_app)
+ apply assumption
+ done
-default pcpo
+text {* Continuity of if-then-else. *}
+
+lemma cont_if: "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)"
+ by (cases b) simp_all
+
+
+subsection {* Continuity Proofs for flift1, flift2, if *}
+
+text {* Need the instance of @{text flat}. *}
+
+lemma cont_flift1_arg: "cont (lift_case UU f)"
+ -- {* @{text flift1} is continuous in its argument itself. *}
+ apply (rule flatdom_strict2cont)
+ apply simp
+ done
+
+lemma cont_flift1_not_arg: "!!f. [| !! a. cont (%y. (f y) a) |] ==>
+ cont (%y. lift_case UU (f y))"
+ -- {* @{text flift1} is continuous in a variable that occurs only
+ in the @{text Def} branch. *}
+ apply (rule cont2cont_CF1L_rev)
+ apply (intro strip)
+ apply (case_tac y)
+ apply simp
+ apply simp
+ done
+
+lemma cont_flift1_arg_and_not_arg: "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==>
+ cont (%y. lift_case UU (f y) (g y))"
+ -- {* @{text flift1} is continuous in a variable that occurs either
+ in the @{text Def} branch or in the argument. *}
+ apply (rule_tac tt = g in cont2cont_app)
+ apply (rule cont_flift1_not_arg)
+ apply auto
+ apply (rule cont_flift1_arg)
+ done
+
+lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))"
+ -- {* @{text flift2} is continuous in its argument itself. *}
+ apply (rule flatdom_strict2cont)
+ apply simp
+ done
+
+text {*
+ \medskip Extension of cont_tac and installation of simplifier.
+*}
+
+lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1"
+ apply (rule cont2cont_CF1L_rev)
+ apply simp
+ done
+
+lemmas cont_lemmas_ext [simp] =
+ cont_flift1_arg cont_flift2_arg
+ cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2
+ cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
+
+ML_setup {*
+val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
+
+fun cont_tac i = resolve_tac cont_lemmas2 i;
+fun cont_tacR i = REPEAT (cont_tac i);
+
+local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def"
+in fun cont_tacRs i =
+ simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN
+ REPEAT (cont_tac i)
+end;
+
+simpset_ref() := simpset() addSolver
+ (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
+*}
+
+
+subsection {* flift1, flift2 *}
+
+lemma flift1_Def [simp]: "flift1 f$(Def x) = (f x)"
+ by (simp add: flift1_def)
+
+lemma flift2_Def [simp]: "flift2 f$(Def x) = Def (f x)"
+ by (simp add: flift2_def)
+
+lemma flift1_UU [simp]: "flift1 f$UU = UU"
+ by (simp add: flift1_def)
+
+lemma flift2_UU [simp]: "flift2 f$UU = UU"
+ by (simp add: flift2_def)
+
+lemma flift2_nUU [simp]: "x~=UU ==> (flift2 f)$x~=UU"
+ by (tactic "def_tac 1")
end
-
-
-
--- a/src/HOLCF/Lift1.ML Sat Nov 03 01:36:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOLCF/Lift1.ML
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 Technische Universitaet Muenchen
-
-Theorems for Lift1.thy
-*)
-
-
-open Lift1;
-
-(* ------------------------------------------------------------------------ *)
-(* less_lift is a partial order on type 'a -> 'b *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [less_lift_def] "(x::'a lift) << x";
-by (fast_tac HOL_cs 1);
-qed"refl_less_lift";
-
-Goalw [less_lift_def]
- "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
-by (fast_tac HOL_cs 1);
-qed"antisym_less_lift";
-
-Goalw [less_lift_def]
- "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
-by (fast_tac HOL_cs 1);
-qed"trans_less_lift";
--- a/src/HOLCF/Lift1.thy Sat Nov 03 01:36:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: HOLCF/Lift1.thy
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 Technische Universitaet Muenchen
-
-Lifting types of class term to flat pcpo's
-*)
-
-Lift1 = Cprod3 + Datatype +
-
-default term
-
-datatype 'a lift = Undef | Def 'a
-
-instance lift :: (term)sq_ord
-defs
-
- less_lift_def "x << y == (x=y | x=Undef)"
-
-end
--- a/src/HOLCF/Lift2.ML Sat Nov 03 01:36:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-(* Title: HOLCF/Lift2.ML
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 Technische Universitaet Muenchen
-
-Class Instance lift::(term)po
-*)
-
-(* for compatibility with old HOLCF-Version *)
-Goal "(op <<)=(%x y. x=y|x=Undef)";
-by (fold_goals_tac [less_lift_def]);
-by (rtac refl 1);
-qed "inst_lift_po";
-
-(* -------------------------------------------------------------------------*)
-(* type ('a)lift is pointed *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "Undef << x";
-by (simp_tac (simpset() addsimps [inst_lift_po]) 1);
-qed"minimal_lift";
-
-bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
-
-AddIffs [minimal_lift];
-
-Goal "EX x::'a lift. ALL y. x<<y";
-by (res_inst_tac [("x","Undef")] exI 1);
-by (rtac (minimal_lift RS allI) 1);
-qed "least_lift";
-
-(* ------------------------------------------------------------------------ *)
-(* ('a)lift is a cpo *)
-(* ------------------------------------------------------------------------ *)
-
-(* The following Lemmata have already been proved in Pcpo.ML and Fix.ML,
- but there class pcpo is assumed, although only po is necessary and a
- least element. Therefore they are redone here for the po lift with
- least element Undef. *)
-
-(* Tailoring notUU_I of Pcpo.ML to Undef *)
-
-Goal "[| x<<y; ~x=Undef |] ==> ~y=Undef";
-by (blast_tac (claset() addIs [antisym_less]) 1);
-qed"notUndef_I";
-
-
-(* Tailoring chain_mono2 of Pcpo.ML to Undef *)
-
-Goal "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] \
-\ ==> EX j. ALL i. j<i-->~Y(i)=Undef";
-by Safe_tac;
-by (Step_tac 1);
-by (strip_tac 1);
-by (rtac notUndef_I 1);
-by (atac 2);
-by (etac (chain_mono) 1);
-by (atac 1);
-qed"chain_mono2_po";
-
-
-(* Tailoring flat_imp_chfin of Fix.ML to lift *)
-
-Goal "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))";
-by (rewtac max_in_chain_def);
-by (strip_tac 1);
-by (res_inst_tac [("P","ALL i. Y(i)=Undef")] case_split_thm 1);
-by (res_inst_tac [("x","0")] exI 1);
-by (strip_tac 1);
-by (rtac trans 1);
-by (etac spec 1);
-by (rtac sym 1);
-by (etac spec 1);
-by (subgoal_tac "ALL x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
-by (simp_tac (simpset() addsimps [inst_lift_po]) 2);
-by (rtac (chain_mono2_po RS exE) 1);
-by (Fast_tac 1);
-by (atac 1);
-by (res_inst_tac [("x","Suc(x)")] exI 1);
-by (strip_tac 1);
-by (rtac disjE 1);
-by (atac 3);
-by (rtac mp 1);
-by (dtac spec 1);
-by (etac spec 1);
-by (etac (le_imp_less_or_eq RS disjE) 1);
-by (etac (chain_mono) 1);
-by Auto_tac;
-qed"flat_imp_chfin_poo";
-
-
-(* Main Lemma: cpo_lift *)
-
-Goal "chain(Y::nat=>('a)lift) ==> EX x. range(Y) <<|x";
-by (cut_inst_tac [] flat_imp_chfin_poo 1);
-by (blast_tac (claset() addIs [lub_finch1]) 1);
-qed"cpo_lift";
-
-
-
--- a/src/HOLCF/Lift2.thy Sat Nov 03 01:36:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: HOLCF/Lift2.thy
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 Technische Universitaet Muenchen
-
-Class Instance lift::(term)po
-*)
-
-Lift2 = Lift1 +
-
-instance "lift" :: (term)po (refl_less_lift,antisym_less_lift,trans_less_lift)
-
-end
-
-
--- a/src/HOLCF/Lift3.ML Sat Nov 03 01:36:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,155 +0,0 @@
-(* Title: HOLCF/Lift3.ML
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 Technische Universitaet Muenchen
-
-Class Instance lift::(term)pcpo
-*)
-
-
-(* for compatibility with old HOLCF-Version *)
-Goal "UU = Undef";
-by (simp_tac (HOL_ss addsimps [UU_def,UU_lift_def]) 1);
-qed "inst_lift_pcpo";
-
-(* ----------------------------------------------------------- *)
-(* In lift.simps Undef is replaced by UU *)
-(* Undef should be invisible from now on *)
-(* ----------------------------------------------------------- *)
-
-
-Addsimps [inst_lift_pcpo];
-
-local
-
-val case1' = prove_goal thy "lift_case f1 f2 UU = f1"
- (fn _ => [simp_tac (simpset() addsimps lift.simps) 1]);
-val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a"
- (fn _ => [Simp_tac 1]);
-val distinct1' = prove_goal thy "UU ~= Def a"
- (fn _ => [Simp_tac 1]);
-val distinct2' = prove_goal thy "Def a ~= UU"
- (fn _ => [Simp_tac 1]);
-val inject' = prove_goal thy "(Def a = Def aa) = (a = aa)"
- (fn _ => [Simp_tac 1]);
-val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1"
- (fn _ => [Simp_tac 1]);
-val rec2' = prove_goal thy "lift_rec f1 f2 (Def a) = f2 a"
- (fn _ => [Simp_tac 1]);
-val induct' = prove_goal thy "[| P UU; !a. P (Def a) |] ==> P lift"
- (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1,
- etac Lift1.lift.induct 1,fast_tac HOL_cs 1]);
-
-in
-
-val Def_not_UU = distinct2';
-
-structure lift =
-struct
-val cases = [case1',case2'];
-val distinct = [distinct1',distinct2'];
-val inject = [inject'];
-val induct = allI RSN(2,induct');
-val recs = [rec1',rec2'];
-val simps = cases@distinct@inject@recs;
-fun induct_tac (s:string) (i:int) =
- (res_inst_tac [("lift",s)] induct i);
-end;
-
-end; (* local *)
-
-Delsimps Lift1.lift.simps;
-Delsimps [inst_lift_pcpo];
-Addsimps [inst_lift_pcpo RS sym];
-Addsimps lift.simps;
-
-
-(* --------------------------------------------------------*)
- section"less_lift";
-(* --------------------------------------------------------*)
-
-Goal "(x::'a lift) << y = (x=y | x=UU)";
-by (stac inst_lift_po 1);
-by (Simp_tac 1);
-qed"less_lift";
-
-
-(* ---------------------------------------------------------- *)
- section"UU and Def";
-(* ---------------------------------------------------------- *)
-
-Goal "x=UU | (? y. x=Def y)";
-by (lift.induct_tac "x" 1);
-by (Asm_simp_tac 1);
-by (rtac disjI2 1);
-by (rtac exI 1);
-by (Asm_simp_tac 1);
-qed"Lift_exhaust";
-
-val prems = Goal "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P";
-by (cut_facts_tac [Lift_exhaust] 1);
-by (fast_tac (HOL_cs addSEs prems) 1);
-qed"Lift_cases";
-
-Goal "(x~=UU)=(? y. x=Def y)";
-by (rtac iffI 1);
-by (rtac Lift_cases 1);
-by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
-qed"not_Undef_is_Def";
-
-(* For x~=UU in assumptions def_tac replaces x by (Def a) in conclusion *)
-val def_tac = etac (not_Undef_is_Def RS iffD1 RS exE) THEN' Asm_simp_tac;
-
-bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym);
-
-Goal "Def x = UU ==> R";
-by (asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1);
-qed "DefE";
-
-Goal "[| x = Def s; x = UU |] ==> R";
-by (fast_tac (HOL_cs addSDs [DefE]) 1);
-qed"DefE2";
-
-Goal "Def x << Def y = (x = y)";
-by (stac (hd lift.inject RS sym) 1);
-back();
-by (rtac iffI 1);
-by (asm_full_simp_tac (simpset() addsimps [inst_lift_po] ) 1);
-by (etac (antisym_less_inverse RS conjunct1) 1);
-qed"Def_inject_less_eq";
-
-Goal "Def x << y = (Def x = y)";
-by (simp_tac (simpset() addsimps [less_lift]) 1);
-qed"Def_less_is_eq";
-
-Addsimps [Def_less_is_eq];
-
-(* ---------------------------------------------------------- *)
- section"Lift is flat";
-(* ---------------------------------------------------------- *)
-
-Goal "! x y::'a lift. x << y --> x = UU | x = y";
-by (simp_tac (simpset() addsimps [less_lift]) 1);
-qed"ax_flat_lift";
-
-(* Two specific lemmas for the combination of LCF and HOL terms *)
-
-Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)";
-by (rtac cont2cont_CF1L 1);
-by (REPEAT (resolve_tac cont_lemmas1 1));
-by Auto_tac;
-qed"cont_Rep_CFun_app";
-
-Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)";
-by (rtac cont2cont_CF1L 1);
-by (etac cont_Rep_CFun_app 1);
-by (assume_tac 1);
-qed"cont_Rep_CFun_app_app";
-
-
-(* continuity of if then else *)
-Goal "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)";
-by (case_tac "b" 1);
-by Auto_tac;
-qed"cont_if";
-
--- a/src/HOLCF/Lift3.thy Sat Nov 03 01:36:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title: HOLCF/Lift3.thy
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 Technische Universitaet Muenchen
-
-Class Instance lift::(term)pcpo
-*)
-
-Lift3 = Lift2 +
-
-instance lift :: (term)pcpo (cpo_lift,least_lift)
-
-consts
- flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"
- flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
-
- liftpair ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
-
-translations
- "UU" <= "Undef"
-
-defs
- flift1_def
- "flift1 f == (LAM x. (case x of
- Undef => UU
- | Def y => (f y)))"
- flift2_def
- "flift2 f == (LAM x. (case x of
- Undef => UU
- | Def y => Def (f y)))"
- liftpair_def
- "liftpair x == (case (cfst$x) of
- Undef => UU
- | Def x1 => (case (csnd$x) of
- Undef => UU
- | Def x2 => Def (x1,x2)))"
-
-end
-