1.1 --- a/src/HOLCF/HOLCF.thy	Mon Dec 09 19:13:13 1996 +0100
     1.2 +++ b/src/HOLCF/HOLCF.thy	Mon Dec 09 19:16:20 1996 +0100
     1.3 @@ -8,5 +8,9 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -HOLCF = Tr2
     1.8 +HOLCF = Lift3 +
     1.9  
    1.10 +default pcpo
    1.11 +
    1.12 +end
    1.13 +

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/Lift1.ML	Mon Dec 09 19:16:20 1996 +0100
     2.3 @@ -0,0 +1,21 @@
     2.4 +(* Lift1.ML *)
     2.5 +
     2.6 +open Lift1;
     2.7 +
     2.8 +(* ------------------------------------------------------------------------ *)
     2.9 +(* less_lift is a partial order on type 'a -> 'b                            *)
    2.10 +(* ------------------------------------------------------------------------ *)
    2.11 +
    2.12 +goalw Lift1.thy [less_lift_def] "less_lift x x";
    2.13 +by (fast_tac HOL_cs 1);
    2.14 +qed"refl_less_lift";
    2.15 +
    2.16 +goalw Lift1.thy [less_lift_def] 
    2.17 +  "less_lift x1 x2 & less_lift x2 x1 --> x1 = x2";
    2.18 +by (fast_tac HOL_cs 1);
    2.19 +qed"antisym_less_lift";
    2.20 +
    2.21 +goalw Lift1.thy [less_lift_def] 
    2.22 +  "less_lift x1 x2 & less_lift x2 x3 --> less_lift x1 x3";
    2.23 +by (fast_tac HOL_cs 1);
    2.24 +qed"trans_less_lift";

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/Lift1.thy	Mon Dec 09 19:16:20 1996 +0100
     3.3 @@ -0,0 +1,18 @@
     3.4 +Lift1 = Tr2 + 
     3.5 +
     3.6 +default term
     3.7 +
     3.8 +datatype 'a lift  = Undef | Def('a)
     3.9 +
    3.10 +arities "lift" :: (term)term
    3.11 +
    3.12 +consts less_lift    :: "['a lift, 'a lift] => bool"
    3.13 +       UU_lift      :: "'a lift"
    3.14 +
    3.15 +defs 
    3.16 + 
    3.17 + less_lift_def  "less_lift x y == (x=y | x=Undef)"
    3.18 +
    3.19 +
    3.20 +end
    3.21 +

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/Lift2.ML	Mon Dec 09 19:16:20 1996 +0100
     4.3 @@ -0,0 +1,106 @@
     4.4 + (* Lift2.ML *)
     4.5 +
     4.6 +open Lift2;
     4.7 +Addsimps [less_lift_def];
     4.8 +
     4.9 +
    4.10 +(* -------------------------------------------------------------------------*)
    4.11 +(* type ('a)lift is pointed                                                *)
    4.12 +(* ------------------------------------------------------------------------ *)
    4.13 + 
    4.14 +
    4.15 +goal Lift2.thy  "Undef << x";
    4.16 +by (simp_tac (!simpset addsimps [inst_lift_po]) 1);
    4.17 +qed"minimal_lift";
    4.18 +
    4.19 +
    4.20 +(* ------------------------------------------------------------------------ *)
    4.21 +(* ('a)lift is a cpo                                                       *)
    4.22 +(* ------------------------------------------------------------------------ *)
    4.23 +
    4.24 +(* The following Lemmata have already been proved in Pcpo.ML and Fix.ML, 
    4.25 +   but there class pcpo is assumed, although only po is necessary and a
    4.26 +   least element. Therefore they are redone here for the po lift with 
    4.27 +   least element Undef.   *)
    4.28 +
    4.29 +(* Tailoring notUU_I of Pcpo.ML to Undef *)
    4.30 +
    4.31 +goal Lift2.thy "!!x. [| x<<y; ~x=Undef |] ==> ~y=Undef";
    4.32 +by (etac contrapos 1);
    4.33 +by (hyp_subst_tac 1);
    4.34 +by (rtac antisym_less 1);
    4.35 +by (atac 1);
    4.36 +by (rtac minimal_lift 1);
    4.37 +qed"notUndef_I";
    4.38 +
    4.39 +
    4.40 +(* Tailoring chain_mono2 of Pcpo.ML to Undef *)
    4.41 +
    4.42 +goal Lift2.thy
    4.43 +"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
    4.44 +\ ==> ? j.!i.j<i-->~Y(i)=Undef";
    4.45 +by (safe_tac HOL_cs);
    4.46 +by (step_tac HOL_cs 1);
    4.47 +by (strip_tac 1);
    4.48 +by (rtac notUndef_I 1);
    4.49 +by (atac 2);
    4.50 +by (etac (chain_mono RS mp) 1);
    4.51 +by (atac 1);
    4.52 +qed"chain_mono2_po";
    4.53 +
    4.54 +
    4.55 +(* Tailoring flat_imp_chain_finite of Fix.ML to lift *)
    4.56 +
    4.57 +goal Lift2.thy
    4.58 +        "(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
    4.59 +by (rewtac max_in_chain_def);  
    4.60 +by (strip_tac 1);
    4.61 +by (res_inst_tac [("P","!i.Y(i)=Undef")] case_split_thm  1);
    4.62 +by (res_inst_tac [("x","0")] exI 1);
    4.63 +by (strip_tac 1);
    4.64 +by (rtac trans 1);
    4.65 +by (etac spec 1);
    4.66 +by (rtac sym 1);
    4.67 +by (etac spec 1); 
    4.68 +
    4.69 +by (subgoal_tac "!x y.x<<(y::('a)lift) --> x=Undef | x=y" 1);
    4.70 +by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
    4.71 +by (rtac (chain_mono2_po RS exE) 1); 
    4.72 +by (fast_tac HOL_cs 1); 
    4.73 +by (atac 1); 
    4.74 +by (res_inst_tac [("x","Suc(x)")] exI 1); 
    4.75 +by (strip_tac 1); 
    4.76 +by (rtac disjE 1); 
    4.77 +by (atac 3); 
    4.78 +by (rtac mp 1); 
    4.79 +by (dtac spec 1);
    4.80 +by (etac spec 1); 
    4.81 +by (etac (le_imp_less_or_eq RS disjE) 1); 
    4.82 +by (etac (chain_mono RS mp) 1); 
    4.83 +by (atac 1); 
    4.84 +by (hyp_subst_tac 1); 
    4.85 +by (rtac refl_less 1); 
    4.86 +by (res_inst_tac [("P","Y(Suc(x)) = Undef")] notE 1); 
    4.87 +by (atac 2); 
    4.88 +by (rtac mp 1); 
    4.89 +by (etac spec 1); 
    4.90 +by (Asm_simp_tac 1);
    4.91 +qed"flat_imp_chain_finite_poo";
    4.92 +
    4.93 +
    4.94 +(* Main Lemma: cpo_lift *)
    4.95 +
    4.96 +goal Lift2.thy  
    4.97 +  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x";
    4.98 +by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
    4.99 +by (step_tac HOL_cs 1);
   4.100 +by (safe_tac HOL_cs);
   4.101 +by (step_tac HOL_cs 1); 
   4.102 +by (rtac exI 1);
   4.103 +by (rtac lub_finch1 1);
   4.104 +by (atac 1);
   4.105 +by (atac 1);
   4.106 +qed"cpo_lift";
   4.107 +
   4.108 +
   4.109 +

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/Lift2.thy	Mon Dec 09 19:16:20 1996 +0100
     5.3 @@ -0,0 +1,12 @@
     5.4 +Lift2 = Lift1 + 
     5.5 +
     5.6 +default term
     5.7 +
     5.8 +arities "lift" :: (term)po
     5.9 +
    5.10 +rules
    5.11 +
    5.12 + inst_lift_po   "((op <<)::['a lift,'a lift]=>bool) = less_lift"
    5.13 +
    5.14 +end
    5.15 +

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/Lift3.ML	Mon Dec 09 19:16:20 1996 +0100
     6.3 @@ -0,0 +1,324 @@
     6.4 +(* Lift3.ML *)
     6.5 +
     6.6 +open Lift3;
     6.7 +
     6.8 +
     6.9 +
    6.10 +
    6.11 +
    6.12 +(* ----------------------------------------------------------- *)
    6.13 +(*                        From Undef to UU		       *)
    6.14 +(* ----------------------------------------------------------- *)
    6.15 +
    6.16 +Addsimps [inst_lift_pcpo];
    6.17 +
    6.18 +local
    6.19 +
    6.20 +val case1' = prove_goal Lift3.thy "lift_case f1 f2 UU = f1"
    6.21 +	     (fn _ => [simp_tac (!simpset addsimps lift.simps) 1]);
    6.22 +
    6.23 +val case2' = prove_goal Lift3.thy "lift_case f1 f2 (Def a) = f2 a"
    6.24 +	     (fn _ => [Simp_tac 1]);
    6.25 +
    6.26 +val distinct1' = prove_goal Lift3.thy "UU ~= Def a" 
    6.27 +		 (fn _ => [Simp_tac 1]);
    6.28 +
    6.29 +val distinct2' = prove_goal Lift3.thy "Def a ~= UU"
    6.30 +		 (fn _ => [Simp_tac 1]);
    6.31 +
    6.32 +val inject' = prove_goal Lift3.thy "Def a = Def aa = (a = aa)"
    6.33 +	       (fn _ => [Simp_tac 1]);
    6.34 +
    6.35 +val rec1' = prove_goal Lift3.thy "lift_rec f1 f2 UU = f1"
    6.36 +	    (fn _ => [Simp_tac 1]);
    6.37 +
    6.38 +val rec2' = prove_goal Lift3.thy "lift_rec f1 f2 (Def a) = f2 a"
    6.39 +	    (fn _ => [Simp_tac 1]);
    6.40 +
    6.41 +val induct' = prove_goal Lift3.thy "[| P UU; !a. P (Def a) |] ==> P lift"
    6.42 +	    (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1,
    6.43 +		      etac Lift1.lift.induct 1,fast_tac HOL_cs 1]);
    6.44 +
    6.45 +in 
    6.46 +
    6.47 +val Def_not_UU = distinct1' RS not_sym;
    6.48 +
    6.49 +structure lift =
    6.50 +struct
    6.51 +val cases = [case1',case2'];
    6.52 +val distinct = [distinct1',distinct2'];
    6.53 +val inject = [inject'];
    6.54 +val induct = allI RSN(2,induct');
    6.55 +val recs = [rec1',rec2'];
    6.56 +val simps = cases@distinct@inject@recs;
    6.57 +fun induct_tac (s:string) (i:int) = 
    6.58 +    (res_inst_tac [("lift",s)] induct i);
    6.59 +end;
    6.60 +
    6.61 +end; (* local *)
    6.62 +
    6.63 +Delsimps [inst_lift_pcpo];
    6.64 +Delsimps lift.simps;
    6.65 +
    6.66 +Addsimps [inst_lift_pcpo RS sym];
    6.67 +Addsimps lift.simps;
    6.68 +
    6.69 +
    6.70 +(* -------------------------------------------------------------------------*)
    6.71 +(* rewrite_rule for less_lift 						    *)
    6.72 +(* -------------------------------------------------------------------------*)
    6.73 +
    6.74 +goal Lift3.thy "(x::'a lift) << y = (x=y | x=UU)";
    6.75 +br (inst_lift_po RS ssubst) 1;
    6.76 +by (Simp_tac 1);
    6.77 +val less_lift = result();
    6.78 +
    6.79 +
    6.80 +
    6.81 +
    6.82 +(* ---------------------------------------------------------- *)
    6.83 +(*                  Relating UU and Undef                     *)
    6.84 +(* ---------------------------------------------------------- *)
    6.85 +
    6.86 +goal Lift3.thy "x=UU | (? y.x=Def y)"; 
    6.87 +by (lift.induct_tac "x" 1);
    6.88 +by (Asm_simp_tac 1);
    6.89 +by (rtac disjI2 1);
    6.90 +by (rtac exI 1);
    6.91 +by (Asm_simp_tac 1);
    6.92 +qed"Lift_exhaust";
    6.93 +
    6.94 +val prems = goal Lift3.thy 
    6.95 +  "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P";
    6.96 +by (cut_facts_tac [Lift_exhaust] 1);
    6.97 +by (fast_tac (HOL_cs addSEs prems) 1);
    6.98 +qed"Lift_cases";
    6.99 +
   6.100 +goal Lift3.thy "(x~=UU)=(? y.x=Def y)";
   6.101 +br iffI 1;
   6.102 + br Lift_cases 1;
   6.103 +  by (fast_tac HOL_cs 1);
   6.104 + by (fast_tac HOL_cs 1);
   6.105 +by (fast_tac (HOL_cs addSIs lift.distinct) 1);
   6.106 +qed"not_Undef_is_Def";
   6.107 +
   6.108 +val Undef_eq_UU = inst_lift_pcpo RS sym;
   6.109 +
   6.110 +val DefE = prove_goal Lift3.thy "Def x = UU ==> R" 
   6.111 +    (fn prems => [
   6.112 +        cut_facts_tac prems 1,
   6.113 +        asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1]);
   6.114 +
   6.115 +val prems = goal Lift3.thy "[| x = Def s; x = UU |] ==> R";
   6.116 +by (cut_facts_tac prems 1);
   6.117 +by (fast_tac (HOL_cs addSDs [DefE]) 1);
   6.118 +val DefE2 = result();
   6.119 +
   6.120 +
   6.121 +
   6.122 +(* ---------------------------------------------------------- *)
   6.123 +(*                          Lift is flat                     *)
   6.124 +(* ---------------------------------------------------------- *)
   6.125 +
   6.126 +goalw Lift3.thy [flat_def] "flat (x::'a lift)";
   6.127 +by (simp_tac (!simpset addsimps [less_lift]) 1);
   6.128 +val flat_lift = result();
   6.129 +
   6.130 +
   6.131 +
   6.132 +
   6.133 +(* ---------------------------------------------------------- *)
   6.134 +(*       More Continuity Proofs and Extended Tactic           *)
   6.135 +(* ---------------------------------------------------------- *)
   6.136 +
   6.137 +goal Lift3.thy "cont (%x. case x of Undef => UU | Def a => f a)";
   6.138 +
   6.139 +br flatdom_strict2cont 1;
   6.140 + br flat_lift 1;
   6.141 +by (Simp_tac 1);
   6.142 +
   6.143 +val cont_flift1_arg = result();
   6.144 +
   6.145 +
   6.146 +
   6.147 +goal Lift3.thy "cont (%x. case x of Undef => UU | Def a => Def (f a))";
   6.148 +
   6.149 +br flatdom_strict2cont 1;
   6.150 + br flat_lift 1;
   6.151 +by (Simp_tac 1);
   6.152 +
   6.153 +val cont_flift2_arg = result();
   6.154 +
   6.155 +
   6.156 +
   6.157 +goal Lift3.thy "!!f. [|! a.cont (%y. (f y) a)|] ==> \
   6.158 +\   cont (%y. case x of Undef => UU | Def a => (f y) a)";
   6.159 +
   6.160 +by (res_inst_tac [("x","x")] Lift_cases 1);
   6.161 + by (Asm_simp_tac 1);
   6.162 +by (fast_tac (HOL_cs addss !simpset) 1);
   6.163 +
   6.164 +qed"cont_flift1_not_arg";
   6.165 +
   6.166 +val cont_flift1_not_arg2 = (allI RS cont_flift1_not_arg);
   6.167 +
   6.168 +
   6.169 +
   6.170 +
   6.171 +(* zusammenfassen zu cont(%y. ((f y)`(g y)) s)     *)
   6.172 +
   6.173 +goal Lift3.thy "!!f.cont g ==> cont(%x. (f`(g x)) s)";
   6.174 +by (rtac monocontlub2cont 1);
   6.175 +(* monotone *)
   6.176 + by (rtac monofunI 1);
   6.177 + by (strip_tac 1);
   6.178 + by (rtac (monofun_cfun_arg RS monofun_fun_fun) 1);
   6.179 + by (etac (cont2mono RS monofunE RS spec RS spec RS mp) 1); 
   6.180 + by (atac 1);
   6.181 +(* contlub *)
   6.182 +by (rtac contlubI 1);
   6.183 +by (strip_tac 1);
   6.184 +by ((rtac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1) THEN (atac 1));
   6.185 + ba 1;
   6.186 +by (stac (contlub_cfun_arg RS fun_cong) 1);
   6.187 + be (cont2mono RS ch2ch_monofun) 1;
   6.188 + ba 1;
   6.189 +by (stac thelub_fun 1);
   6.190 + by (fast_tac ((HOL_cs addSIs [ch2ch_fappR]) 
   6.191 +		       addSEs [cont2mono RS ch2ch_monofun]) 1);
   6.192 +br refl 1;
   6.193 +qed"cont_fapp_app1";
   6.194 +
   6.195 +
   6.196 +goal Lift3.thy "cont(%y. (y`x) s)";
   6.197 +by (rtac monocontlub2cont 1);
   6.198 + (* monotone *)
   6.199 + by (rtac monofunI 1);
   6.200 + by (strip_tac 1); 
   6.201 + be (monofun_cfun_fun RS monofun_fun_fun) 1;
   6.202 +(* continuous *)
   6.203 +by (rtac contlubI 1);
   6.204 +by (strip_tac 1);
   6.205 +by (stac (contlub_cfun_fun RS fun_cong) 1);
   6.206 + by (atac 1);
   6.207 +by (stac thelub_fun 1);
   6.208 + be ch2ch_fappL 1;
   6.209 +br refl 1;
   6.210 +qed"cont_fapp_app2";
   6.211 +
   6.212 +
   6.213 +
   6.214 +val prems = goal Lift3.thy "[| cont f1; cont f2 |] ==> \
   6.215 +\   cont (%x. if b then f1 x else f2 x)";
   6.216 +
   6.217 +by (cut_facts_tac prems 1);
   6.218 +by (case_tac "b" 1);
   6.219 +by (TRYALL (fast_tac (HOL_cs addss HOL_ss)));
   6.220 +
   6.221 +val cont_if = result();
   6.222 +
   6.223 +
   6.224 +
   6.225 +val cont2cont_CF1L_rev2 = (allI RS cont2cont_CF1L_rev);
   6.226 +
   6.227 +val cont_lemmas =  cont_lemmas@
   6.228 +		   [cont_flift1_arg,cont_flift2_arg,
   6.229 +                    cont_flift1_not_arg2,cont2cont_CF1L_rev2, 
   6.230 +                    cont_fapp_app1,cont_fapp_app2,cont_if];
   6.231 +
   6.232 +
   6.233 +val cont_tac = (fn i => ((resolve_tac cont_lemmas i)));
   6.234 + 
   6.235 +val cont_tacR = (fn i => ((simp_tac (!simpset 
   6.236 +                                addsimps [flift1_def,flift2_def]) i)
   6.237 +                           THEN REPEAT (cont_tac i) ));
   6.238 +
   6.239 +(* --------------------------------------------------------- *)
   6.240 +(*                Admissibility tactic and tricks            *)
   6.241 +(* --------------------------------------------------------- *)
   6.242 +
   6.243 +
   6.244 +goal Lift3.thy "x~=FF = (x=TT|x=UU)";
   6.245 +by (res_inst_tac [("p","x")] trE 1);
   6.246 +  by (TRYALL (Asm_full_simp_tac));
   6.247 +qed"adm_trick_1";
   6.248 +
   6.249 +goal Lift3.thy "x~=TT = (x=FF|x=UU)";
   6.250 +by (res_inst_tac [("p","x")] trE 1);
   6.251 +  by (TRYALL (Asm_full_simp_tac));
   6.252 +qed"adm_trick_2";
   6.253 +
   6.254 +
   6.255 +val adm_tricks = [adm_trick_1,adm_trick_2];
   6.256 +val adm_tac = (fn i => ((resolve_tac adm_thms i)));
   6.257 +val adm_tacR = (fn i => (REPEAT (adm_tac i)));
   6.258 +val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i)));
   6.259 +
   6.260 +
   6.261 +(* ----------------------------------------------------------------- *)
   6.262 +(*     Relations between domains and terms using lift constructs     *)
   6.263 +(* ----------------------------------------------------------------- *)
   6.264 +
   6.265 +goal Lift3.thy
   6.266 +"!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
   6.267 +by (rtac iffI 1);
   6.268 +(* 1 *)
   6.269 +by (res_inst_tac [("p","t")] trE 1);
   6.270 +by (fast_tac HOL_cs 1);
   6.271 +by (res_inst_tac [("p","s")] trE 1);
   6.272 +by (Asm_full_simp_tac 1);
   6.273 +by (Asm_full_simp_tac 1);
   6.274 +by (subgoal_tac "(t andalso s) = FF" 1);
   6.275 +by (fast_tac HOL_cs 1);
   6.276 +by (Asm_full_simp_tac 1);
   6.277 +by (res_inst_tac [("p","s")] trE 1);
   6.278 +by (subgoal_tac "(t andalso s) = FF" 1);
   6.279 +by (fast_tac HOL_cs 1);
   6.280 +by (Asm_full_simp_tac 1);
   6.281 +by (subgoal_tac "(t andalso s) = FF" 1);
   6.282 +by (fast_tac HOL_cs 1);
   6.283 +by (Asm_full_simp_tac 1);
   6.284 +by (subgoal_tac "(t andalso s) = FF" 1);
   6.285 +by (fast_tac HOL_cs 1);
   6.286 +by (Asm_full_simp_tac 1);
   6.287 +(* 2*)
   6.288 +by (res_inst_tac [("p","t")] trE 1);
   6.289 +by (fast_tac HOL_cs 1);
   6.290 +by (Asm_full_simp_tac 1);
   6.291 +by (fast_tac HOL_cs 1);
   6.292 +qed"andalso_and";
   6.293 +
   6.294 +
   6.295 +goal Lift3.thy "blift x ~=UU";
   6.296 +by (simp_tac (!simpset addsimps [blift_def])1);
   6.297 +by (case_tac "x" 1);
   6.298 + by (Asm_full_simp_tac 1);
   6.299 +by (Asm_full_simp_tac 1);
   6.300 +qed"blift_not_UU";
   6.301 +
   6.302 +goal Lift3.thy "(blift x ~=FF)= x";
   6.303 +by (simp_tac (!simpset addsimps [blift_def]) 1);
   6.304 +by (case_tac "x" 1); 
   6.305 + by (Asm_full_simp_tac 1);
   6.306 +by (Asm_full_simp_tac 1);
   6.307 +qed"blift_and_bool";
   6.308 +
   6.309 +goal Lift3.thy "plift P`(Def y) = blift (P y)";
   6.310 +by (simp_tac (!simpset addsimps [plift_def,flift1_def]) 1);
   6.311 +by (stac beta_cfun 1);
   6.312 +by (cont_tacR 1);
   6.313 +by (Simp_tac 1);
   6.314 +qed"plift2blift";
   6.315 +
   6.316 +goal Lift3.thy 
   6.317 +  "(If blift P then A else B fi)= (if P then A else B)";
   6.318 +by (simp_tac (!simpset addsimps [blift_def]) 1);
   6.319 +by (res_inst_tac [("P","P"),("Q","P")] impCE 1);
   6.320 +by (fast_tac HOL_cs 1);
   6.321 +by (REPEAT (Asm_full_simp_tac 1));
   6.322 +qed"If_and_if";
   6.323 +
   6.324 +
   6.325 +Addsimps [plift2blift,If_and_if,blift_not_UU,blift_and_bool];
   6.326 +
   6.327 +simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));
   6.328 \ No newline at end of file

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOLCF/Lift3.thy	Mon Dec 09 19:16:20 1996 +0100
     7.3 @@ -0,0 +1,39 @@
     7.4 +Lift3 = Lift2 + 
     7.5 +
     7.6 +default term
     7.7 +
     7.8 +arities 
     7.9 + "lift" :: (term)pcpo
    7.10 +
    7.11 +consts 
    7.12 + flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
    7.13 + blift        :: "bool => tr"  
    7.14 + plift        :: "('a => bool) => 'a lift -> tr"   
    7.15 + flift2      :: "('a => 'b) => ('a lift -> 'b lift)"
    7.16 +
    7.17 +translations
    7.18 + "UU" <= "Undef"
    7.19 +
    7.20 +defs
    7.21 + blift_def
    7.22 +  "blift b == (if b then TT else FF)"
    7.23 +
    7.24 + flift1_def
    7.25 +  "flift1 f  == (LAM x. (case x of 
    7.26 +                   Undef => UU
    7.27 +                 | Def y => (f y)))"
    7.28 +
    7.29 + flift2_def
    7.30 +  "flift2 f == (LAM x. (case x of 
    7.31 +                              Undef => Undef
    7.32 +                            | Def y => Def (f y)))"
    7.33 +
    7.34 + plift_def
    7.35 +  "plift p == (LAM x. flift1 (%a. blift (p a))`x)"
    7.36 +
    7.37 +
    7.38 +rules
    7.39 + inst_lift_pcpo "(UU::'a lift) = Undef"
    7.40 +
    7.41 +end
    7.42 +