# HG changeset patch
# User mueller
# Date 861897034 -7200
# Node ID 5230c37ad29f55f8440b56aebcc3569a91209ff5
# Parent  9c44acc3c6fa67424c41d091c5f9b5d06215b6dd
Complete Redesign of Theory, main points are:

- Extension of the continuity prover:
  * Lemmas about continuity of flift1 and flift2 are generalized
  * Lemmas about continuity of mixed definitions of HOL and LCF terms generalized
  Pay attention: Sometimes proofs are shorter now!
- a number of new lemmas concerning flift1, flift2, Def and Undef,
  Def_less_is_eq (Def x << y = (Def x = y)) and lemmas characterizing flift1 and flift2
  are added to !simpset
  Pay attention: Sometimes proofs are shorter now!
- added tactic def_tac for eliminating x~=UU in assumptions

diff -r 9c44acc3c6fa -r 5230c37ad29f src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Thu Apr 24 17:40:30 1997 +0200
+++ b/src/HOLCF/Lift3.ML	Thu Apr 24 17:50:34 1997 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOLCF/Lift3.ML
     ID:         $Id$
-    Author:     Olaf Mueller, Robert Sandner
+    Author:     Olaf Mueller
     Copyright   1996 Technische Universitaet Muenchen
 
 Theorems for Lift3.thy
@@ -15,41 +15,36 @@
         ]);
 
 (* ----------------------------------------------------------- *)
-(*                        From Undef to UU		       *)
+(*           In lift.simps Undef is replaced by UU             *)
+(*           Undef should be invisible from now on             *)
 (* ----------------------------------------------------------- *)
 
+
 Addsimps [inst_lift_pcpo];
 
 local
 
-val case1' = prove_goal Lift3.thy "lift_case f1 f2 UU = f1"
+val case1' = prove_goal 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"
+val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a"
 	     (fn _ => [Simp_tac 1]);
-
-val distinct1' = prove_goal Lift3.thy "UU ~= Def a" 
+val distinct1' = prove_goal thy "UU ~= Def a" 
 		 (fn _ => [Simp_tac 1]);
-
-val distinct2' = prove_goal Lift3.thy "Def a ~= UU"
+val distinct2' = prove_goal thy "Def a ~= UU"
 		 (fn _ => [Simp_tac 1]);
-
-val inject' = prove_goal Lift3.thy "Def a = Def aa = (a = aa)"
+val inject' = prove_goal thy "Def a = Def aa = (a = aa)"
 	       (fn _ => [Simp_tac 1]);
-
-val rec1' = prove_goal Lift3.thy "lift_rec f1 f2 UU = f1"
+val rec1' = prove_goal 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"
+val rec2' = prove_goal 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"
+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 = distinct1' RS not_sym;
+val Def_not_UU = distinct2';
 
 structure lift =
 struct
@@ -65,30 +60,27 @@
 
 end; (* local *)
 
+Delsimps lift.simps;
 Delsimps [inst_lift_pcpo];
-Delsimps lift.simps;
-
 Addsimps [inst_lift_pcpo RS sym];
 Addsimps lift.simps;
 
 
-(* -------------------------------------------------------------------------*)
-(* rewrite_rule for less_lift 						    *)
-(* -------------------------------------------------------------------------*)
+(* --------------------------------------------------------*)
+              section"less_lift";
+(* --------------------------------------------------------*)
 
-goal Lift3.thy "(x::'a lift) << y = (x=y | x=UU)";
+goal thy "(x::'a lift) << y = (x=y | x=UU)";
 br (inst_lift_po RS ssubst) 1;
 by (Simp_tac 1);
-val less_lift = result();
-
-
+qed"less_lift";
 
 
 (* ---------------------------------------------------------- *)
-(*                  Relating UU and Undef                     *)
+                 section"UU and Def";             
 (* ---------------------------------------------------------- *)
 
-goal Lift3.thy "x=UU | (? y.x=Def y)"; 
+goal thy "x=UU | (? y.x=Def y)"; 
 by (lift.induct_tac "x" 1);
 by (Asm_simp_tac 1);
 by (rtac disjI2 1);
@@ -96,7 +88,7 @@
 by (Asm_simp_tac 1);
 qed"Lift_exhaust";
 
-val prems = goal Lift3.thy 
+val prems = goal 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);
@@ -108,142 +100,173 @@
 by(ALLGOALS Asm_simp_tac);
 qed "expand_lift_case";
 
-goal Lift3.thy "(x~=UU)=(? y.x=Def y)";
+goal 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);
+br Lift_cases 1;
+by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
 qed"not_Undef_is_Def";
 
-val Undef_eq_UU = inst_lift_pcpo RS sym;
+(* 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;
 
-val DefE = prove_goal Lift3.thy "Def x = UU ==> R" 
+bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym);
+
+val DefE = prove_goal 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";
+val prems = goal thy "[| x = Def s; x = UU |] ==> R";
 by (cut_facts_tac prems 1);
 by (fast_tac (HOL_cs addSDs [DefE]) 1);
-val DefE2 = result();
+qed"DefE2";
+
+goal thy "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);
+be (antisym_less_inverse RS conjunct1) 1;
+qed"Def_inject_less_eq";
+
+goal thy "Def x << y = (Def x = y)";
+by (simp_tac (!simpset addsimps [less_lift]) 1);
+qed"Def_less_is_eq";
+
+Addsimps [Def_less_is_eq];
 
 (* ---------------------------------------------------------- *)
-(*                          Lift is flat                     *)
+              section"Lift is flat";
 (* ---------------------------------------------------------- *)
 
-goalw Lift3.thy [flat_def] "flat (x::'a lift)";
+goalw thy [flat_def] "flat (x::'a lift)";
 by (simp_tac (!simpset addsimps [less_lift]) 1);
-val flat_lift = result();
+qed"flat_lift";
 
 bind_thm("ax_flat_lift",flat_lift RS flatE);
 
 
 (* ---------------------------------------------------------- *)
-(*       More Continuity Proofs and Extended Tactic           *)
+    section"Continuity Proofs for flift1, flift2, if";
 (* ---------------------------------------------------------- *)
 
-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)     *)
+(* flift1 is continuous in its argument itself*)
+
+goal thy "cont (lift_case UU f)"; 
+br flatdom_strict2cont 1;
+br flat_lift 1;
+by (Simp_tac 1);
+qed"cont_flift1_arg";
+
+(* flift1 is continuous in a variable that occurs only 
+   in the Def branch *)
+
+goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
+\          cont (%y. lift_case UU (f y))";
+br 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 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 thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
+\   cont (%y. lift_case UU (f y) (g y))";
+br cont2cont_app 1;
+back();
+by (safe_tac set_cs);
+br cont_flift1_not_arg 1;
+auto();
+br cont_flift1_arg 1;
+qed"cont_flift1_arg_and_not_arg";
+
+(* flift2 is continuous in its argument itself *)
+
+goal thy "cont (lift_case UU (%y. Def (f y)))";
+br flatdom_strict2cont 1;
+br flat_lift 1;
+by (Simp_tac 1);
+qed"cont_flift2_arg";
+
+(* Two specific lemmas for the combination of LCF and HOL terms *)
+
+goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
+br cont2cont_CF1L 1;
+by (REPEAT (resolve_tac cont_lemmas1 1));
+auto();
+qed"cont_fapp_app";
+
+goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
+br cont2cont_CF1L 1;
+be cont_fapp_app 1;
+ba 1;
+qed"cont_fapp_app_app";
 
 
-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";
+(* continuity of if then else *)
 
-
-
-val prems = goal Lift3.thy "[| cont f1; cont f2 |] ==> \
+val prems = goal 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)));
+qed"cont_if";
 
-val cont_if = result();
+
+(* ---------------------------------------------------------- *)
+(*    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_fapp_app,cont_fapp_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);
 
 
-val cont2cont_CF1L_rev2 = (allI RS cont2cont_CF1L_rev);
+simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+
+(* ---------------------------------------------------------- *)
+              section"flift1, flift2";
+(* ---------------------------------------------------------- *)
+
 
-val cont_lemmas2 =  cont_lemmas1@
-		   [cont_flift1_arg,cont_flift2_arg,
-                    cont_flift1_not_arg2,cont2cont_CF1L_rev2, 
-                    cont_fapp_app1,cont_fapp_app2,cont_if];
+goal thy "flift1 f`(Def x) = (f x)";
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"flift1_Def";
+
+goal thy "flift2 f`(Def x) = Def (f x)";
+by (simp_tac (!simpset addsimps [flift2_def]) 1);
+qed"flift2_Def";
 
-Addsimps 	   [cont_flift1_arg,cont_flift2_arg,
-                    cont_flift1_not_arg2,cont2cont_CF1L_rev2, 
-                    cont_fapp_app1,cont_fapp_app2,cont_if];
+goal thy "flift1 f`UU = UU";
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"flift1_UU";
+
+goal thy "flift2 f`UU = UU";
+by (simp_tac (!simpset addsimps [flift2_def]) 1);
+qed"flift2_UU";
 
-fun cont_tac  i = resolve_tac cont_lemmas2 i;
-fun cont_tacR i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
-		  REPEAT (cont_tac i);
+Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
 
-simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+goal thy "!!x. x~=UU ==> (flift2 f)`x~=UU";
+by (def_tac 1);
+qed"flift2_nUU";
+
+Addsimps [flift2_nUU];
+
+