src/HOLCF/Sprod3.ML

-(*  Title:      HOLCF/sprod3.thy
+(*  Title:      HOLCF/Sprod3.thy
     ID:         $Id$
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Lemmas for Sprod3.thy 
+Lemmas for Sprod.thy 
 *)
 
 open Sprod3;
 
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_sprod_pcpo" thy "UU = Ispair UU UU"
+ (fn prems => 
+        [
+        (simp_tac (HOL_ss addsimps [UU_def,UU_sprod_def]) 1)
+        ]);
 (* ------------------------------------------------------------------------ *)
 (* continuity of Ispair, Isfst, Issnd                                       *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "sprod3_lemma1" Sprod3.thy 
+qed_goal "sprod3_lemma1" thy 
 "[| is_chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
 \ Ispair (lub(range Y)) x =\
 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
 \        (lub(range(%i. Issnd(Ispair(Y i) x))))"
  (fn prems =>

         (etac sym 1),
         (asm_simp_tac Sprod0_ss  1),
         (rtac minimal 1)
         ]);
 
-qed_goal "sprod3_lemma2" Sprod3.thy 
+qed_goal "sprod3_lemma2" thy 
 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
 \   Ispair (lub(range Y)) x =\
 \   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
 \          (lub(range(%i. Issnd(Ispair(Y i) x))))"
  (fn prems =>

         (etac (chain_UU_I RS spec) 1),
         (atac 1)
         ]);
 
 
-qed_goal "sprod3_lemma3" Sprod3.thy 
+qed_goal "sprod3_lemma3" thy 
 "[| is_chain(Y); x = UU |] ==>\
 \          Ispair (lub(range Y)) x =\
 \          Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
 \                 (lub(range(%i. Issnd(Ispair (Y i) x))))"
  (fn prems =>

         (rtac allI 1),
         (simp_tac Sprod0_ss  1)
         ]);
 
 
-qed_goal "contlub_Ispair1" Sprod3.thy "contlub(Ispair)"
+qed_goal "contlub_Ispair1" thy "contlub(Ispair)"
 (fn prems =>
         [
         (rtac contlubI 1),
         (strip_tac 1),
         (rtac (expand_fun_eq RS iffD2) 1),

         (atac 1),
         (etac sprod3_lemma3 1),
         (atac 1)
         ]);
 
-qed_goal "sprod3_lemma4" Sprod3.thy 
+qed_goal "sprod3_lemma4" thy 
 "[| is_chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
 \         Ispair x (lub(range Y)) =\
 \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
 \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
  (fn prems =>

         (atac 1),
         (rtac allI 1),
         (asm_simp_tac Sprod0_ss 1)
         ]);
 
-qed_goal "sprod3_lemma5" Sprod3.thy 
+qed_goal "sprod3_lemma5" thy 
 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
 \         Ispair x (lub(range Y)) =\
 \         Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
 \                (lub(range(%i. Issnd(Ispair x (Y i)))))"
  (fn prems =>

         (asm_simp_tac Sprod0_ss  1),
         (etac (chain_UU_I RS spec) 1),
         (atac 1)
         ]);
 
-qed_goal "sprod3_lemma6" Sprod3.thy 
+qed_goal "sprod3_lemma6" thy 
 "[| is_chain(Y); x = UU |] ==>\
 \         Ispair x (lub(range Y)) =\
 \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
 \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
 (fn prems =>

         (rtac chain_UU_I_inverse 1),
         (rtac allI 1),
         (simp_tac Sprod0_ss  1)
         ]);
 
-qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
+qed_goal "contlub_Ispair2" thy "contlub(Ispair(x))"
 (fn prems =>
         [
         (rtac contlubI 1),
         (strip_tac 1),
         (rtac trans 1),

         (etac sprod3_lemma6 1),
         (atac 1)
         ]);
 
 
-qed_goal "cont_Ispair1" Sprod3.thy "cont(Ispair)"
+qed_goal "cont_Ispair1" thy "cont(Ispair)"
 (fn prems =>
         [
         (rtac monocontlub2cont 1),
         (rtac monofun_Ispair1 1),
         (rtac contlub_Ispair1 1)
         ]);
 
 
-qed_goal "cont_Ispair2" Sprod3.thy "cont(Ispair(x))"
+qed_goal "cont_Ispair2" thy "cont(Ispair(x))"
 (fn prems =>
         [
         (rtac monocontlub2cont 1),
         (rtac monofun_Ispair2 1),
         (rtac contlub_Ispair2 1)
         ]);
 
-qed_goal "contlub_Isfst" Sprod3.thy "contlub(Isfst)"
+qed_goal "contlub_Isfst" thy "contlub(Isfst)"
  (fn prems =>
         [
         (rtac contlubI 1),
         (strip_tac 1),
         (stac (lub_sprod RS thelubI) 1),

         (etac (defined_IsfstIssnd RS conjunct2) 2),
         (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS 
                                   chain_UU_I RS spec]) 1)
         ]);
 
-qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)"
+qed_goal "contlub_Issnd" thy "contlub(Issnd)"
 (fn prems =>
         [
         (rtac contlubI 1),
         (strip_tac 1),
         (stac (lub_sprod RS thelubI) 1),

         (etac (defined_IsfstIssnd RS conjunct1) 2),
         (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS
                                   chain_UU_I RS spec]) 1)
         ]);
 
-qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)"
+qed_goal "cont_Isfst" thy "cont(Isfst)"
 (fn prems =>
         [
         (rtac monocontlub2cont 1),
         (rtac monofun_Isfst 1),
         (rtac contlub_Isfst 1)
         ]);
 
-qed_goal "cont_Issnd" Sprod3.thy "cont(Issnd)"
+qed_goal "cont_Issnd" thy "cont(Issnd)"
 (fn prems =>
         [
         (rtac monocontlub2cont 1),
         (rtac monofun_Issnd 1),
         (rtac contlub_Issnd 1)
         ]);
 
-(* 
- -------------------------------------------------------------------------- 
- more lemmas for Sprod3.thy 
- 
- -------------------------------------------------------------------------- 
-*)
-
-qed_goal "spair_eq" Sprod3.thy "[|x1=x2;y1=y2|] ==> (|x1,y1|) = (|x2,y2|)"
+qed_goal "spair_eq" thy "[|x1=x2;y1=y2|] ==> (|x1,y1|) = (|x2,y2|)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (fast_tac HOL_cs 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
 (* convert all lemmas to the continuous versions                            *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "beta_cfun_sprod" Sprod3.thy [spair_def]
+qed_goalw "beta_cfun_sprod" thy [spair_def]
         "(LAM x y.Ispair x y)`a`b = Ispair a b"
  (fn prems =>
         [
         (stac beta_cfun 1),
         (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1,

         (stac beta_cfun 1),
         (rtac cont_Ispair2 1),
         (rtac refl 1)
         ]);
 
-qed_goalw "inject_spair" Sprod3.thy [spair_def]
+qed_goalw "inject_spair" thy [spair_def]
         "[| aa~=UU ; ba~=UU ; (|a,b|)=(|aa,ba|) |] ==> a=aa & b=ba"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (etac inject_Ispair 1),

         (etac box_equals 1),
         (rtac beta_cfun_sprod 1),
         (rtac beta_cfun_sprod 1)
         ]);
 
-qed_goalw "inst_sprod_pcpo2" Sprod3.thy [spair_def] "UU = (|UU,UU|)"
+qed_goalw "inst_sprod_pcpo2" thy [spair_def] "UU = (|UU,UU|)"
  (fn prems =>
         [
         (rtac sym 1),
         (rtac trans 1),
         (rtac beta_cfun_sprod 1),
         (rtac sym 1),
         (rtac inst_sprod_pcpo 1)
         ]);
 
-qed_goalw "strict_spair" Sprod3.thy [spair_def] 
+qed_goalw "strict_spair" thy [spair_def] 
         "(a=UU | b=UU) ==> (|a,b|)=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac trans 1),

         (rtac trans 1),
         (rtac (inst_sprod_pcpo RS sym) 2),
         (etac strict_Ispair 1)
         ]);
 
-qed_goalw "strict_spair1" Sprod3.thy [spair_def] "(|UU,b|) = UU"
+qed_goalw "strict_spair1" thy [spair_def] "(|UU,b|) = UU"
  (fn prems =>
         [
         (stac beta_cfun_sprod 1),
         (rtac trans 1),
         (rtac (inst_sprod_pcpo RS sym) 2),
         (rtac strict_Ispair1 1)
         ]);
 
-qed_goalw "strict_spair2" Sprod3.thy [spair_def] "(|a,UU|) = UU"
+qed_goalw "strict_spair2" thy [spair_def] "(|a,UU|) = UU"
  (fn prems =>
         [
         (stac beta_cfun_sprod 1),
         (rtac trans 1),
         (rtac (inst_sprod_pcpo RS sym) 2),
         (rtac strict_Ispair2 1)
         ]);
 
-qed_goalw "strict_spair_rev" Sprod3.thy [spair_def]
+qed_goalw "strict_spair_rev" thy [spair_def]
         "(|x,y|)~=UU ==> ~x=UU & ~y=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac strict_Ispair_rev 1),
         (rtac (beta_cfun_sprod RS subst) 1),
         (rtac (inst_sprod_pcpo RS subst) 1),
         (atac 1)
         ]);
 
-qed_goalw "defined_spair_rev" Sprod3.thy [spair_def]
+qed_goalw "defined_spair_rev" thy [spair_def]
  "(|a,b|) = UU ==> (a = UU | b = UU)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac defined_Ispair_rev 1),
         (rtac (beta_cfun_sprod RS subst) 1),
         (rtac (inst_sprod_pcpo RS subst) 1),
         (atac 1)
         ]);
 
-qed_goalw "defined_spair" Sprod3.thy [spair_def]
+qed_goalw "defined_spair" thy [spair_def]
         "[|a~=UU; b~=UU|] ==> (|a,b|) ~= UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun_sprod 1),
         (stac inst_sprod_pcpo 1),
         (etac defined_Ispair 1),
         (atac 1)
         ]);
 
-qed_goalw "Exh_Sprod2" Sprod3.thy [spair_def]
+qed_goalw "Exh_Sprod2" thy [spair_def]
         "z=UU | (? a b. z=(|a,b|) & a~=UU & b~=UU)"
  (fn prems =>
         [
         (rtac (Exh_Sprod RS disjE) 1),
         (rtac disjI1 1),

         (fast_tac HOL_cs 1),
         (fast_tac HOL_cs 1)
         ]);
 
 
-qed_goalw "sprodE" Sprod3.thy [spair_def]
+qed_goalw "sprodE" thy [spair_def]
 "[|p=UU ==> Q;!!x y. [|p=(|x,y|);x~=UU ; y~=UU|] ==> Q|] ==> Q"
 (fn prems =>
         [
         (rtac IsprodE 1),
         (resolve_tac prems 1),

         (stac beta_cfun_sprod 1),
         (atac 1)
         ]);
 
 
-qed_goalw "strict_sfst" Sprod3.thy [sfst_def] 
+qed_goalw "strict_sfst" thy [sfst_def] 
         "p=UU==>sfst`p=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun 1),

         (rtac strict_Isfst 1),
         (rtac (inst_sprod_pcpo RS subst) 1),
         (atac 1)
         ]);
 
-qed_goalw "strict_sfst1" Sprod3.thy [sfst_def,spair_def] 
+qed_goalw "strict_sfst1" thy [sfst_def,spair_def] 
         "sfst`(|UU,y|) = UU"
  (fn prems =>
         [
         (stac beta_cfun_sprod 1),
         (stac beta_cfun 1),
         (rtac cont_Isfst 1),
         (rtac strict_Isfst1 1)
         ]);
  
-qed_goalw "strict_sfst2" Sprod3.thy [sfst_def,spair_def] 
+qed_goalw "strict_sfst2" thy [sfst_def,spair_def] 
         "sfst`(|x,UU|) = UU"
  (fn prems =>
         [
         (stac beta_cfun_sprod 1),
         (stac beta_cfun 1),
         (rtac cont_Isfst 1),
         (rtac strict_Isfst2 1)
         ]);
 
-qed_goalw "strict_ssnd" Sprod3.thy [ssnd_def] 
+qed_goalw "strict_ssnd" thy [ssnd_def] 
         "p=UU==>ssnd`p=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun 1),

         (rtac strict_Issnd 1),
         (rtac (inst_sprod_pcpo RS subst) 1),
         (atac 1)
         ]);
 
-qed_goalw "strict_ssnd1" Sprod3.thy [ssnd_def,spair_def] 
+qed_goalw "strict_ssnd1" thy [ssnd_def,spair_def] 
         "ssnd`(|UU,y|) = UU"
  (fn prems =>
         [
         (stac beta_cfun_sprod 1),
         (stac beta_cfun 1),
         (rtac cont_Issnd 1),
         (rtac strict_Issnd1 1)
         ]);
 
-qed_goalw "strict_ssnd2" Sprod3.thy [ssnd_def,spair_def] 
+qed_goalw "strict_ssnd2" thy [ssnd_def,spair_def] 
         "ssnd`(|x,UU|) = UU"
  (fn prems =>
         [
         (stac beta_cfun_sprod 1),
         (stac beta_cfun 1),
         (rtac cont_Issnd 1),
         (rtac strict_Issnd2 1)
         ]);
 
-qed_goalw "sfst2" Sprod3.thy [sfst_def,spair_def] 
+qed_goalw "sfst2" thy [sfst_def,spair_def] 
         "y~=UU ==>sfst`(|x,y|)=x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun_sprod 1),
         (stac beta_cfun 1),
         (rtac cont_Isfst 1),
         (etac Isfst2 1)
         ]);
 
-qed_goalw "ssnd2" Sprod3.thy [ssnd_def,spair_def] 
+qed_goalw "ssnd2" thy [ssnd_def,spair_def] 
         "x~=UU ==>ssnd`(|x,y|)=y"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun_sprod 1),

         (rtac cont_Issnd 1),
         (etac Issnd2 1)
         ]);
 
 
-qed_goalw "defined_sfstssnd" Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "defined_sfstssnd" thy [sfst_def,ssnd_def,spair_def]
         "p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun 1),

         (rtac (inst_sprod_pcpo RS subst) 1),
         (atac 1)
         ]);
  
 
-qed_goalw "surjective_pairing_Sprod2" Sprod3.thy 
+qed_goalw "surjective_pairing_Sprod2" thy 
         [sfst_def,ssnd_def,spair_def] "(|sfst`p , ssnd`p|) = p"
  (fn prems =>
         [
         (stac beta_cfun_sprod 1),
         (stac beta_cfun 1),

         (rtac cont_Isfst 1),
         (rtac (surjective_pairing_Sprod RS sym) 1)
         ]);
 
 
-qed_goalw "less_sprod5b" Sprod3.thy [sfst_def,ssnd_def,spair_def]
- "p1~=UU ==> (p1<<p2) = (sfst`p1<<sfst`p2 & ssnd`p1<<ssnd`p2)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (stac beta_cfun 1),
-        (rtac cont_Issnd 1),
-        (stac beta_cfun 1),
-        (rtac cont_Issnd 1),
-        (stac beta_cfun 1),
-        (rtac cont_Isfst 1),
-        (stac beta_cfun 1),
-        (rtac cont_Isfst 1),
-        (rtac less_sprod3b 1),
-        (rtac (inst_sprod_pcpo RS subst) 1),
-        (atac 1)
-        ]);
-
- 
-qed_goalw "less_sprod5c" Sprod3.thy [sfst_def,ssnd_def,spair_def]
- "[|(|xa,ya|) << (|x,y|);xa~=UU;ya~=UU;x~=UU;y~=UU|] ==>xa<<x & ya << y"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac less_sprod4c 1),
-        (REPEAT (atac 2)),
-        (rtac (beta_cfun_sprod RS subst) 1),
-        (rtac (beta_cfun_sprod RS subst) 1),
-        (atac 1)
-        ]);
-
-qed_goalw "lub_sprod2" Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
 "[|is_chain(S)|] ==> range(S) <<| \
 \ (| lub(range(%i.sfst`(S i))), lub(range(%i.ssnd`(S i))) |)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),

  "is_chain ?S1 ==>
  lub (range ?S1) =
  (|lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i)))|)" : thm
 *)
 
-qed_goalw "ssplit1" Sprod3.thy [ssplit_def]
+qed_goalw "ssplit1" thy [ssplit_def]
         "ssplit`f`UU=UU"
  (fn prems =>
         [
         (stac beta_cfun 1),
         (Simp_tac 1),
         (stac strictify1 1),
         (rtac refl 1)
         ]);
 
-qed_goalw "ssplit2" Sprod3.thy [ssplit_def]
+qed_goalw "ssplit2" thy [ssplit_def]
         "[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y"
  (fn prems =>
         [
         (stac beta_cfun 1),
         (Simp_tac 1),

         (resolve_tac prems 1),
         (rtac refl 1)
         ]);
 
 
-qed_goalw "ssplit3" Sprod3.thy [ssplit_def]
+qed_goalw "ssplit3" thy [ssplit_def]
   "ssplit`spair`z=z"
  (fn prems =>
         [
         (stac beta_cfun 1),
         (Simp_tac 1),

         (stac beta_cfun 1),
         (Simp_tac 1),
         (rtac surjective_pairing_Sprod2 1)
         ]);
 
-
 (* ------------------------------------------------------------------------ *)
 (* install simplifier for Sprod                                             *)
 (* ------------------------------------------------------------------------ *)
 
 val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
                 strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
                 ssplit1,ssplit2];
-
-Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
-          strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
-          ssplit1,ssplit2];
+Addsimps Sprod_rews;
+