# HG changeset patch
# User sandnerr
# Date 850155380 -3600
# Node ID 125260ef480cd09de8bb54da22fca9bb6764917e
# Parent  ee9bdbe2ac8a3e23292218ba6992614b029f1f8d
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy

diff -r ee9bdbe2ac8a -r 125260ef480c src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Mon Dec 09 19:13:13 1996 +0100
+++ b/src/HOLCF/HOLCF.thy	Mon Dec 09 19:16:20 1996 +0100
@@ -8,5 +8,9 @@
 
 *)
 
-HOLCF = Tr2
+HOLCF = Lift3 +
 
+default pcpo
+
+end
+
diff -r ee9bdbe2ac8a -r 125260ef480c src/HOLCF/Lift1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift1.ML	Mon Dec 09 19:16:20 1996 +0100
@@ -0,0 +1,21 @@
+(* Lift1.ML *)
+
+open Lift1;
+
+(* ------------------------------------------------------------------------ *)
+(* less_lift is a partial order on type 'a -> 'b                            *)
+(* ------------------------------------------------------------------------ *)
+
+goalw Lift1.thy [less_lift_def] "less_lift x x";
+by (fast_tac HOL_cs 1);
+qed"refl_less_lift";
+
+goalw Lift1.thy [less_lift_def] 
+  "less_lift x1 x2 & less_lift x2 x1 --> x1 = x2";
+by (fast_tac HOL_cs 1);
+qed"antisym_less_lift";
+
+goalw Lift1.thy [less_lift_def] 
+  "less_lift x1 x2 & less_lift x2 x3 --> less_lift x1 x3";
+by (fast_tac HOL_cs 1);
+qed"trans_less_lift";
diff -r ee9bdbe2ac8a -r 125260ef480c src/HOLCF/Lift1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift1.thy	Mon Dec 09 19:16:20 1996 +0100
@@ -0,0 +1,18 @@
+Lift1 = Tr2 + 
+
+default term
+
+datatype 'a lift  = Undef | Def('a)
+
+arities "lift" :: (term)term
+
+consts less_lift    :: "['a lift, 'a lift] => bool"
+       UU_lift      :: "'a lift"
+
+defs 
+ 
+ less_lift_def  "less_lift x y == (x=y | x=Undef)"
+
+
+end
+
diff -r ee9bdbe2ac8a -r 125260ef480c src/HOLCF/Lift2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift2.ML	Mon Dec 09 19:16:20 1996 +0100
@@ -0,0 +1,106 @@
+ (* Lift2.ML *)
+
+open Lift2;
+Addsimps [less_lift_def];
+
+
+(* -------------------------------------------------------------------------*)
+(* type ('a)lift is pointed                                                *)
+(* ------------------------------------------------------------------------ *)
+ 
+
+goal Lift2.thy  "Undef << x";
+by (simp_tac (!simpset addsimps [inst_lift_po]) 1);
+qed"minimal_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 Lift2.thy "!!x. [| x<<y; ~x=Undef |] ==> ~y=Undef";
+by (etac contrapos 1);
+by (hyp_subst_tac 1);
+by (rtac antisym_less 1);
+by (atac 1);
+by (rtac minimal_lift 1);
+qed"notUndef_I";
+
+
+(* Tailoring chain_mono2 of Pcpo.ML to Undef *)
+
+goal Lift2.thy
+"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
+\ ==> ? j.!i.j<i-->~Y(i)=Undef";
+by (safe_tac HOL_cs);
+by (step_tac HOL_cs 1);
+by (strip_tac 1);
+by (rtac notUndef_I 1);
+by (atac 2);
+by (etac (chain_mono RS mp) 1);
+by (atac 1);
+qed"chain_mono2_po";
+
+
+(* Tailoring flat_imp_chain_finite of Fix.ML to lift *)
+
+goal Lift2.thy
+        "(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
+by (rewtac max_in_chain_def);  
+by (strip_tac 1);
+by (res_inst_tac [("P","!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 "!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 HOL_cs 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 RS mp) 1); 
+by (atac 1); 
+by (hyp_subst_tac 1); 
+by (rtac refl_less 1); 
+by (res_inst_tac [("P","Y(Suc(x)) = Undef")] notE 1); 
+by (atac 2); 
+by (rtac mp 1); 
+by (etac spec 1); 
+by (Asm_simp_tac 1);
+qed"flat_imp_chain_finite_poo";
+
+
+(* Main Lemma: cpo_lift *)
+
+goal Lift2.thy  
+  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x";
+by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
+by (step_tac HOL_cs 1);
+by (safe_tac HOL_cs);
+by (step_tac HOL_cs 1); 
+by (rtac exI 1);
+by (rtac lub_finch1 1);
+by (atac 1);
+by (atac 1);
+qed"cpo_lift";
+
+
+
diff -r ee9bdbe2ac8a -r 125260ef480c src/HOLCF/Lift2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift2.thy	Mon Dec 09 19:16:20 1996 +0100
@@ -0,0 +1,12 @@
+Lift2 = Lift1 + 
+
+default term
+
+arities "lift" :: (term)po
+
+rules
+
+ inst_lift_po   "((op <<)::['a lift,'a lift]=>bool) = less_lift"
+
+end
+
diff -r ee9bdbe2ac8a -r 125260ef480c src/HOLCF/Lift3.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift3.ML	Mon Dec 09 19:16:20 1996 +0100
@@ -0,0 +1,324 @@
+(* Lift3.ML *)
+
+open Lift3;
+
+
+
+
+
+(* ----------------------------------------------------------- *)
+(*                        From Undef to UU		       *)
+(* ----------------------------------------------------------- *)
+
+Addsimps [inst_lift_pcpo];
+
+local
+
+val case1' = prove_goal Lift3.thy "lift_case f1 f2 UU = f1"
+	     (fn _ => [simp_tac (!simpset addsimps lift.simps) 1]);
+
+val case2' = prove_goal Lift3.thy "lift_case f1 f2 (Def a) = f2 a"
+	     (fn _ => [Simp_tac 1]);
+
+val distinct1' = prove_goal Lift3.thy "UU ~= Def a" 
+		 (fn _ => [Simp_tac 1]);
+
+val distinct2' = prove_goal Lift3.thy "Def a ~= UU"
+		 (fn _ => [Simp_tac 1]);
+
+val inject' = prove_goal Lift3.thy "Def a = Def aa = (a = aa)"
+	       (fn _ => [Simp_tac 1]);
+
+val rec1' = prove_goal Lift3.thy "lift_rec f1 f2 UU = f1"
+	    (fn _ => [Simp_tac 1]);
+
+val rec2' = prove_goal Lift3.thy "lift_rec f1 f2 (Def a) = f2 a"
+	    (fn _ => [Simp_tac 1]);
+
+val induct' = prove_goal Lift3.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 = distinct1' RS not_sym;
+
+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 [inst_lift_pcpo];
+Delsimps lift.simps;
+
+Addsimps [inst_lift_pcpo RS sym];
+Addsimps lift.simps;
+
+
+(* -------------------------------------------------------------------------*)
+(* rewrite_rule for less_lift 						    *)
+(* -------------------------------------------------------------------------*)
+
+goal Lift3.thy "(x::'a lift) << y = (x=y | x=UU)";
+br (inst_lift_po RS ssubst) 1;
+by (Simp_tac 1);
+val less_lift = result();
+
+
+
+
+(* ---------------------------------------------------------- *)
+(*                  Relating UU and Undef                     *)
+(* ---------------------------------------------------------- *)
+
+goal Lift3.thy "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 Lift3.thy 
+  "[| 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 Lift3.thy "(x~=UU)=(? y.x=Def y)";
+br iffI 1;
+ br Lift_cases 1;
+  by (fast_tac HOL_cs 1);
+ by (fast_tac HOL_cs 1);
+by (fast_tac (HOL_cs addSIs lift.distinct) 1);
+qed"not_Undef_is_Def";
+
+val Undef_eq_UU = inst_lift_pcpo RS sym;
+
+val DefE = prove_goal Lift3.thy "Def x = UU ==> R" 
+    (fn prems => [
+        cut_facts_tac prems 1,
+        asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1]);
+
+val prems = goal Lift3.thy "[| x = Def s; x = UU |] ==> R";
+by (cut_facts_tac prems 1);
+by (fast_tac (HOL_cs addSDs [DefE]) 1);
+val DefE2 = result();
+
+
+
+(* ---------------------------------------------------------- *)
+(*                          Lift is flat                     *)
+(* ---------------------------------------------------------- *)
+
+goalw Lift3.thy [flat_def] "flat (x::'a lift)";
+by (simp_tac (!simpset addsimps [less_lift]) 1);
+val flat_lift = result();
+
+
+
+
+(* ---------------------------------------------------------- *)
+(*       More Continuity Proofs and Extended Tactic           *)
+(* ---------------------------------------------------------- *)
+
+goal Lift3.thy "cont (%x. case x of Undef => UU | Def a => f a)";
+
+br flatdom_strict2cont 1;
+ br flat_lift 1;
+by (Simp_tac 1);
+
+val cont_flift1_arg = result();
+
+
+
+goal Lift3.thy "cont (%x. case x of Undef => UU | Def a => Def (f a))";
+
+br flatdom_strict2cont 1;
+ br flat_lift 1;
+by (Simp_tac 1);
+
+val cont_flift2_arg = result();
+
+
+
+goal Lift3.thy "!!f. [|! a.cont (%y. (f y) a)|] ==> \
+\   cont (%y. case x of Undef => UU | Def a => (f y) a)";
+
+by (res_inst_tac [("x","x")] Lift_cases 1);
+ by (Asm_simp_tac 1);
+by (fast_tac (HOL_cs addss !simpset) 1);
+
+qed"cont_flift1_not_arg";
+
+val cont_flift1_not_arg2 = (allI RS cont_flift1_not_arg);
+
+
+
+
+(* zusammenfassen zu cont(%y. ((f y)`(g y)) s)     *)
+
+goal Lift3.thy "!!f.cont g ==> cont(%x. (f`(g x)) s)";
+by (rtac monocontlub2cont 1);
+(* monotone *)
+ by (rtac monofunI 1);
+ by (strip_tac 1);
+ by (rtac (monofun_cfun_arg RS monofun_fun_fun) 1);
+ by (etac (cont2mono RS monofunE RS spec RS spec RS mp) 1); 
+ by (atac 1);
+(* contlub *)
+by (rtac contlubI 1);
+by (strip_tac 1);
+by ((rtac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1) THEN (atac 1));
+ ba 1;
+by (stac (contlub_cfun_arg RS fun_cong) 1);
+ be (cont2mono RS ch2ch_monofun) 1;
+ ba 1;
+by (stac thelub_fun 1);
+ by (fast_tac ((HOL_cs addSIs [ch2ch_fappR]) 
+		       addSEs [cont2mono RS ch2ch_monofun]) 1);
+br refl 1;
+qed"cont_fapp_app1";
+
+
+goal Lift3.thy "cont(%y. (y`x) s)";
+by (rtac monocontlub2cont 1);
+ (* monotone *)
+ by (rtac monofunI 1);
+ by (strip_tac 1); 
+ be (monofun_cfun_fun RS monofun_fun_fun) 1;
+(* continuous *)
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (stac (contlub_cfun_fun RS fun_cong) 1);
+ by (atac 1);
+by (stac thelub_fun 1);
+ be ch2ch_fappL 1;
+br refl 1;
+qed"cont_fapp_app2";
+
+
+
+val prems = goal Lift3.thy "[| cont f1; cont f2 |] ==> \
+\   cont (%x. if b then f1 x else f2 x)";
+
+by (cut_facts_tac prems 1);
+by (case_tac "b" 1);
+by (TRYALL (fast_tac (HOL_cs addss HOL_ss)));
+
+val cont_if = result();
+
+
+
+val cont2cont_CF1L_rev2 = (allI RS cont2cont_CF1L_rev);
+
+val cont_lemmas =  cont_lemmas@
+		   [cont_flift1_arg,cont_flift2_arg,
+                    cont_flift1_not_arg2,cont2cont_CF1L_rev2, 
+                    cont_fapp_app1,cont_fapp_app2,cont_if];
+
+
+val cont_tac = (fn i => ((resolve_tac cont_lemmas i)));
+ 
+val cont_tacR = (fn i => ((simp_tac (!simpset 
+                                addsimps [flift1_def,flift2_def]) i)
+                           THEN REPEAT (cont_tac i) ));
+
+(* --------------------------------------------------------- *)
+(*                Admissibility tactic and tricks            *)
+(* --------------------------------------------------------- *)
+
+
+goal Lift3.thy "x~=FF = (x=TT|x=UU)";
+by (res_inst_tac [("p","x")] trE 1);
+  by (TRYALL (Asm_full_simp_tac));
+qed"adm_trick_1";
+
+goal Lift3.thy "x~=TT = (x=FF|x=UU)";
+by (res_inst_tac [("p","x")] trE 1);
+  by (TRYALL (Asm_full_simp_tac));
+qed"adm_trick_2";
+
+
+val adm_tricks = [adm_trick_1,adm_trick_2];
+val adm_tac = (fn i => ((resolve_tac adm_thms i)));
+val adm_tacR = (fn i => (REPEAT (adm_tac i)));
+val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i)));
+
+
+(* ----------------------------------------------------------------- *)
+(*     Relations between domains and terms using lift constructs     *)
+(* ----------------------------------------------------------------- *)
+
+goal Lift3.thy
+"!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
+by (rtac iffI 1);
+(* 1 *)
+by (res_inst_tac [("p","t")] trE 1);
+by (fast_tac HOL_cs 1);
+by (res_inst_tac [("p","s")] trE 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (res_inst_tac [("p","s")] trE 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+(* 2*)
+by (res_inst_tac [("p","t")] trE 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed"andalso_and";
+
+
+goal Lift3.thy "blift x ~=UU";
+by (simp_tac (!simpset addsimps [blift_def])1);
+by (case_tac "x" 1);
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed"blift_not_UU";
+
+goal Lift3.thy "(blift x ~=FF)= x";
+by (simp_tac (!simpset addsimps [blift_def]) 1);
+by (case_tac "x" 1); 
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed"blift_and_bool";
+
+goal Lift3.thy "plift P`(Def y) = blift (P y)";
+by (simp_tac (!simpset addsimps [plift_def,flift1_def]) 1);
+by (stac beta_cfun 1);
+by (cont_tacR 1);
+by (Simp_tac 1);
+qed"plift2blift";
+
+goal Lift3.thy 
+  "(If blift P then A else B fi)= (if P then A else B)";
+by (simp_tac (!simpset addsimps [blift_def]) 1);
+by (res_inst_tac [("P","P"),("Q","P")] impCE 1);
+by (fast_tac HOL_cs 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"If_and_if";
+
+
+Addsimps [plift2blift,If_and_if,blift_not_UU,blift_and_bool];
+
+simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));
\ No newline at end of file
diff -r ee9bdbe2ac8a -r 125260ef480c src/HOLCF/Lift3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift3.thy	Mon Dec 09 19:16:20 1996 +0100
@@ -0,0 +1,39 @@
+Lift3 = Lift2 + 
+
+default term
+
+arities 
+ "lift" :: (term)pcpo
+
+consts 
+ flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
+ blift        :: "bool => tr"  
+ plift        :: "('a => bool) => 'a lift -> tr"   
+ flift2      :: "('a => 'b) => ('a lift -> 'b lift)"
+
+translations
+ "UU" <= "Undef"
+
+defs
+ blift_def
+  "blift b == (if b then TT else FF)"
+
+ 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 => Undef
+                            | Def y => Def (f y)))"
+
+ plift_def
+  "plift p == (LAM x. flift1 (%a. blift (p a))`x)"
+
+
+rules
+ inst_lift_pcpo "(UU::'a lift) = Undef"
+
+end
+