huffman@15576: (*  Title:      HOLCF/Sprod0.thy
huffman@15576:     ID:         $Id$
huffman@15576:     Author:     Franz Regensburger
huffman@15576:     License:    GPL (GNU GENERAL PUBLIC LICENSE)
huffman@15576: 
huffman@15576: Strict product with typedef.
huffman@15576: *)
huffman@15576: 
huffman@15576: header {* The type of strict products *}
huffman@15576: 
huffman@15577: theory Sprod
huffman@15577: imports Cfun
huffman@15577: begin
huffman@15576: 
huffman@15576: constdefs
huffman@15576:   Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
huffman@15576:  "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
huffman@15576: 
huffman@15576: typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
huffman@15576: by auto
huffman@15576: 
huffman@15576: syntax (xsymbols)
huffman@15576:   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
huffman@15576: syntax (HTML output)
huffman@15576:   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
huffman@15576: 
huffman@15576: subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *}
huffman@15576: 
huffman@15576: consts
huffman@15576:   Ispair        :: "['a,'b] => ('a ** 'b)"
huffman@15576:   Isfst         :: "('a ** 'b) => 'a"
huffman@15576:   Issnd         :: "('a ** 'b) => 'b"  
huffman@15576: 
huffman@15576: defs
huffman@15576:    (*defining the abstract constants*)
huffman@15576: 
huffman@15576:   Ispair_def:    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
huffman@15576: 
huffman@15576:   Isfst_def:     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
huffman@15576:                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
huffman@15576: 
huffman@15576:   Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
huffman@15576:                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* A non-emptyness result for Sprod                                         *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma SprodI: "(Spair_Rep a b):Sprod"
huffman@15576: apply (unfold Sprod_def)
huffman@15576: apply (rule CollectI, rule exI, rule exI, rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
huffman@15576: apply (rule inj_on_inverseI)
huffman@15576: apply (erule Abs_Sprod_inverse)
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* Strictness and definedness of Spair_Rep                                  *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma strict_Spair_Rep: 
huffman@15576:  "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
huffman@15576: apply (unfold Spair_Rep_def)
huffman@15576: apply (rule ext)
huffman@15576: apply (rule ext)
huffman@15576: apply (rule iffI)
huffman@15576: apply fast
huffman@15576: apply fast
huffman@15576: done
huffman@15576: 
huffman@15576: lemma defined_Spair_Rep_rev: 
huffman@15576:  "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
huffman@15576: apply (unfold Spair_Rep_def)
huffman@15576: apply (case_tac "a=UU|b=UU")
huffman@15576: apply assumption
huffman@15576: apply (fast dest: fun_cong)
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* injectivity of Spair_Rep and Ispair                                      *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma inject_Spair_Rep: 
huffman@15576: "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
huffman@15576: 
huffman@15576: apply (unfold Spair_Rep_def)
huffman@15576: apply (drule fun_cong)
huffman@15576: apply (drule fun_cong)
huffman@15576: apply (erule iffD1 [THEN mp])
huffman@15576: apply auto
huffman@15576: done
huffman@15576: 
huffman@15576: lemma inject_Ispair: 
huffman@15576:         "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
huffman@15576: apply (unfold Ispair_def)
huffman@15576: apply (erule inject_Spair_Rep)
huffman@15576: apply assumption
huffman@15576: apply (erule inj_on_Abs_Sprod [THEN inj_onD])
huffman@15576: apply (rule SprodI)
huffman@15576: apply (rule SprodI)
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* strictness and definedness of Ispair                                     *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma strict_Ispair: 
huffman@15576:  "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
huffman@15576: apply (unfold Ispair_def)
huffman@15576: apply (erule strict_Spair_Rep [THEN arg_cong])
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Ispair1: 
huffman@15576:         "Ispair UU b  = Ispair UU UU"
huffman@15576: apply (unfold Ispair_def)
huffman@15576: apply (rule strict_Spair_Rep [THEN arg_cong])
huffman@15576: apply (rule disjI1)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Ispair2: 
huffman@15576:         "Ispair a UU = Ispair UU UU"
huffman@15576: apply (unfold Ispair_def)
huffman@15576: apply (rule strict_Spair_Rep [THEN arg_cong])
huffman@15576: apply (rule disjI2)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
huffman@15576: apply (rule de_Morgan_disj [THEN subst])
huffman@15576: apply (erule contrapos_nn)
huffman@15576: apply (erule strict_Ispair)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma defined_Ispair_rev: 
huffman@15576:         "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
huffman@15576: apply (unfold Ispair_def)
huffman@15576: apply (rule defined_Spair_Rep_rev)
huffman@15576: apply (rule inj_on_Abs_Sprod [THEN inj_onD])
huffman@15576: apply assumption
huffman@15576: apply (rule SprodI)
huffman@15576: apply (rule SprodI)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"
huffman@15576: apply (rule contrapos_nn)
huffman@15576: apply (erule_tac [2] defined_Ispair_rev)
huffman@15576: apply (rule de_Morgan_disj [THEN iffD2])
huffman@15576: apply (erule conjI)
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* Exhaustion of the strict product **                                      *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma Exh_Sprod:
huffman@15576:         "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
huffman@15576: apply (unfold Ispair_def)
huffman@15576: apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
huffman@15576: apply (erule exE)
huffman@15576: apply (erule exE)
huffman@15576: apply (rule excluded_middle [THEN disjE])
huffman@15576: apply (rule disjI2)
huffman@15576: apply (rule exI)
huffman@15576: apply (rule exI)
huffman@15576: apply (rule conjI)
huffman@15576: apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
huffman@15576: apply (erule arg_cong)
huffman@15576: apply (rule de_Morgan_disj [THEN subst])
huffman@15576: apply assumption
huffman@15576: apply (rule disjI1)
huffman@15576: apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
huffman@15576: apply (rule_tac f = "Abs_Sprod" in arg_cong)
huffman@15576: apply (erule trans)
huffman@15576: apply (erule strict_Spair_Rep)
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* general elimination rule for strict product                              *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma IsprodE:
huffman@15576: assumes prem1: "p=Ispair UU UU ==> Q"
huffman@15576: assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q"
huffman@15576: shows "Q"
huffman@15576: apply (rule Exh_Sprod [THEN disjE])
huffman@15576: apply (erule prem1)
huffman@15576: apply (erule exE)
huffman@15576: apply (erule exE)
huffman@15576: apply (erule conjE)
huffman@15576: apply (erule conjE)
huffman@15576: apply (erule prem2)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* some results about the selectors Isfst, Issnd                            *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
huffman@15576: apply (unfold Isfst_def)
huffman@15576: apply (rule some_equality)
huffman@15576: apply (rule conjI)
huffman@15576: apply fast
huffman@15576: apply (intro strip)
huffman@15576: apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
huffman@15576: apply (rule not_sym)
huffman@15576: apply (rule defined_Ispair)
huffman@15576: apply (fast+)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU"
huffman@15576: apply (subst strict_Ispair1)
huffman@15576: apply (rule strict_Isfst)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU"
huffman@15576: apply (subst strict_Ispair2)
huffman@15576: apply (rule strict_Isfst)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
huffman@15576: apply (unfold Issnd_def)
huffman@15576: apply (rule some_equality)
huffman@15576: apply (rule conjI)
huffman@15576: apply fast
huffman@15576: apply (intro strip)
huffman@15576: apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
huffman@15576: apply (rule not_sym)
huffman@15576: apply (rule defined_Ispair)
huffman@15576: apply (fast+)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU"
huffman@15576: apply (subst strict_Ispair1)
huffman@15576: apply (rule strict_Issnd)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU"
huffman@15576: apply (subst strict_Ispair2)
huffman@15576: apply (rule strict_Issnd)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
huffman@15576: apply (unfold Isfst_def)
huffman@15576: apply (rule some_equality)
huffman@15576: apply (rule conjI)
huffman@15576: apply (intro strip)
huffman@15576: apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
huffman@15576: apply (erule defined_Ispair)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: apply (intro strip)
huffman@15576: apply (rule inject_Ispair [THEN conjunct1])
huffman@15576: prefer 3 apply fast
huffman@15576: apply (fast+)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
huffman@15576: apply (unfold Issnd_def)
huffman@15576: apply (rule some_equality)
huffman@15576: apply (rule conjI)
huffman@15576: apply (intro strip)
huffman@15576: apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
huffman@15576: apply (erule defined_Ispair)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: apply (intro strip)
huffman@15576: apply (rule inject_Ispair [THEN conjunct2])
huffman@15576: prefer 3 apply fast
huffman@15576: apply (fast+)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
huffman@15576: apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (erule Isfst)
huffman@15576: apply assumption
huffman@15576: apply (erule ssubst)
huffman@15576: apply (rule strict_Isfst1)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
huffman@15576: apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (erule Issnd)
huffman@15576: apply assumption
huffman@15576: apply (erule ssubst)
huffman@15576: apply (rule strict_Issnd2)
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* instantiate the simplifier                                               *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
huffman@15576:                  Isfst2 Issnd2
huffman@15576: 
huffman@15576: declare Isfst2 [simp] Issnd2 [simp]
huffman@15576: 
huffman@15576: lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
huffman@15576: apply (rule_tac p = "p" in IsprodE)
huffman@15576: apply simp
huffman@15576: apply (erule ssubst)
huffman@15576: apply (rule conjI)
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* Surjective pairing: equivalent to Exh_Sprod                              *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
huffman@15576: apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: apply (erule exE)
huffman@15576: apply (erule exE)
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
huffman@15576: apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
huffman@15576: apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
huffman@15576: apply simp
huffman@15576: done
huffman@15576: 
huffman@15576: subsection {* The strict product is a partial order *}
huffman@15576: 
huffman@15576: instance "**"::(sq_ord,sq_ord)sq_ord ..
huffman@15576: 
huffman@15576: defs (overloaded)
huffman@15576:   less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* less_sprod is a partial order on Sprod                                   *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma refl_less_sprod: "(p::'a ** 'b) << p"
huffman@15576: apply (unfold less_sprod_def)
huffman@15576: apply (fast intro: refl_less)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma antisym_less_sprod: 
huffman@15576:         "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
huffman@15576: apply (unfold less_sprod_def)
huffman@15576: apply (rule Sel_injective_Sprod)
huffman@15576: apply (fast intro: antisym_less)
huffman@15576: apply (fast intro: antisym_less)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma trans_less_sprod: 
huffman@15576:         "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
huffman@15576: apply (unfold less_sprod_def)
huffman@15576: apply (blast intro: trans_less)
huffman@15576: done
huffman@15576: 
huffman@15576: instance "**"::(pcpo,pcpo)po
huffman@15576: by intro_classes
huffman@15576:   (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
huffman@15576: 
huffman@15576: (* for compatibility with old HOLCF-Version *)
huffman@15576: lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
huffman@15576: apply (fold less_sprod_def)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: subsection {* The strict product is pointed *}
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* type sprod is pointed                                                    *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (*
huffman@15576: lemma minimal_sprod: "Ispair UU UU << p"
huffman@15576: apply (simp add: inst_sprod_po minimal)
huffman@15576: done
huffman@15576: 
huffman@15576: lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
huffman@15576: 
huffman@15576: lemma least_sprod: "? x::'a**'b.!y. x<<y"
huffman@15576: apply (rule_tac x = "Ispair UU UU" in exI)
huffman@15576: apply (rule minimal_sprod [THEN allI])
huffman@15576: done
huffman@15576: *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* Ispair is monotone in both arguments                                     *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma monofun_Ispair1: "monofun(Ispair)"
huffman@15576: apply (unfold monofun)
huffman@15576: apply (intro strip)
huffman@15576: apply (rule less_fun [THEN iffD2])
huffman@15576: apply (intro strip)
huffman@15576: apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (frule notUU_I)
huffman@15576: apply assumption
huffman@15576: apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma monofun_Ispair2: "monofun(Ispair(x))"
huffman@15576: apply (unfold monofun)
huffman@15576: apply (intro strip)
huffman@15576: apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (frule notUU_I)
huffman@15576: apply assumption
huffman@15576: apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
huffman@15576: apply (rule trans_less)
huffman@15576: apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
huffman@15576: prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* Isfst and Issnd are monotone                                             *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma monofun_Isfst: "monofun(Isfst)"
huffman@15576: apply (unfold monofun)
huffman@15576: apply (simp add: inst_sprod_po)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma monofun_Issnd: "monofun(Issnd)"
huffman@15576: apply (unfold monofun)
huffman@15576: apply (simp add: inst_sprod_po)
huffman@15576: done
huffman@15576: 
huffman@15576: subsection {* The strict product is a cpo *}
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* the type 'a ** 'b is a cpo                                               *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma lub_sprod: 
huffman@15576: "[|chain(S)|] ==> range(S) <<|  
huffman@15576:   Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
huffman@15576: apply (rule is_lubI)
huffman@15576: apply (rule ub_rangeI)
huffman@15576: apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
huffman@15576: apply (rule monofun_Ispair)
huffman@15576: apply (rule is_ub_thelub)
huffman@15576: apply (erule monofun_Isfst [THEN ch2ch_monofun])
huffman@15576: apply (rule is_ub_thelub)
huffman@15576: apply (erule monofun_Issnd [THEN ch2ch_monofun])
huffman@15576: apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
huffman@15576: apply (rule monofun_Ispair)
huffman@15576: apply (rule is_lub_thelub)
huffman@15576: apply (erule monofun_Isfst [THEN ch2ch_monofun])
huffman@15576: apply (erule monofun_Isfst [THEN ub2ub_monofun])
huffman@15576: apply (rule is_lub_thelub)
huffman@15576: apply (erule monofun_Issnd [THEN ch2ch_monofun])
huffman@15576: apply (erule monofun_Issnd [THEN ub2ub_monofun])
huffman@15576: done
huffman@15576: 
huffman@15576: lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
huffman@15576: 
huffman@15576: lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
huffman@15576: apply (rule exI)
huffman@15576: apply (erule lub_sprod)
huffman@15576: done
huffman@15576: 
huffman@15576: instance "**" :: (pcpo, pcpo) cpo
huffman@15576: by intro_classes (rule cpo_sprod)
huffman@15576: 
huffman@15576: 
huffman@15576: subsection {* The strict product is a pcpo *}
huffman@15576: 
huffman@15576: lemma minimal_sprod: "Ispair UU UU << p"
huffman@15576: apply (simp add: inst_sprod_po minimal)
huffman@15576: done
huffman@15576: 
huffman@15576: lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
huffman@15576: 
huffman@15576: lemma least_sprod: "? x::'a**'b.!y. x<<y"
huffman@15576: apply (rule_tac x = "Ispair UU UU" in exI)
huffman@15576: apply (rule minimal_sprod [THEN allI])
huffman@15576: done
huffman@15576: 
huffman@15576: instance "**" :: (pcpo, pcpo) pcpo
huffman@15576: by intro_classes (rule least_sprod)
huffman@15576: 
huffman@15576: 
huffman@15576: subsection {* Other constants *}
huffman@15576: 
huffman@15576: consts  
huffman@15576:   spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
huffman@15576:   sfst		:: "('a**'b)->'a"
huffman@15576:   ssnd		:: "('a**'b)->'b"
huffman@15576:   ssplit	:: "('a->'b->'c)->('a**'b)->'c"
huffman@15576: 
huffman@15576: syntax  
huffman@15576:   "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
huffman@15576: 
huffman@15576: translations
huffman@15576:         "(:x, y, z:)"   == "(:x, (:y, z:):)"
huffman@15576:         "(:x, y:)"      == "spair$x$y"
huffman@15576: 
huffman@15576: defs
huffman@15576: spair_def:       "spair  == (LAM x y. Ispair x y)"
huffman@15576: sfst_def:        "sfst   == (LAM p. Isfst p)"
huffman@15576: ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
huffman@15576: ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
huffman@15576: 
huffman@15576: (* for compatibility with old HOLCF-Version *)
huffman@15576: lemma inst_sprod_pcpo: "UU = Ispair UU UU"
huffman@15576: apply (simp add: UU_def UU_sprod_def)
huffman@15576: done
huffman@15576: 
huffman@15576: declare inst_sprod_pcpo [symmetric, simp]
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* continuity of Ispair, Isfst, Issnd                                       *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma sprod3_lemma1: 
huffman@15576: "[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
huffman@15576:   Ispair (lub(range Y)) x = 
huffman@15576:   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))  
huffman@15576:          (lub(range(%i. Issnd(Ispair(Y i) x))))"
huffman@15576: apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
huffman@15576: apply (rule lub_equal)
huffman@15576: apply assumption
huffman@15576: apply (rule monofun_Isfst [THEN ch2ch_monofun])
huffman@15576: apply (rule ch2ch_fun)
huffman@15576: apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
huffman@15576: apply assumption
huffman@15576: apply (rule allI)
huffman@15576: apply (simp (no_asm_simp))
huffman@15576: apply (rule sym)
huffman@15576: apply (drule chain_UU_I_inverse2)
huffman@15576: apply (erule exE)
huffman@15576: apply (rule lub_chain_maxelem)
huffman@15576: apply (erule Issnd2)
huffman@15576: apply (rule allI)
huffman@15576: apply (rename_tac "j")
huffman@15576: apply (case_tac "Y (j) =UU")
huffman@15576: apply auto
huffman@15576: done
huffman@15576: 
huffman@15576: lemma sprod3_lemma2: 
huffman@15576: "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
huffman@15576:     Ispair (lub(range Y)) x = 
huffman@15576:     Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) 
huffman@15576:            (lub(range(%i. Issnd(Ispair(Y i) x))))"
huffman@15576: apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
huffman@15576: apply assumption
huffman@15576: apply (rule trans)
huffman@15576: apply (rule strict_Ispair1)
huffman@15576: apply (rule strict_Ispair [symmetric])
huffman@15576: apply (rule disjI1)
huffman@15576: apply (rule chain_UU_I_inverse)
huffman@15576: apply auto
huffman@15576: apply (erule chain_UU_I [THEN spec])
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: lemma sprod3_lemma3: 
huffman@15576: "[| chain(Y); x = UU |] ==> 
huffman@15576:            Ispair (lub(range Y)) x = 
huffman@15576:            Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) 
huffman@15576:                   (lub(range(%i. Issnd(Ispair (Y i) x))))"
huffman@15576: apply (erule ssubst)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule strict_Ispair2)
huffman@15576: apply (rule strict_Ispair [symmetric])
huffman@15576: apply (rule disjI1)
huffman@15576: apply (rule chain_UU_I_inverse)
huffman@15576: apply (rule allI)
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma contlub_Ispair1: "contlub(Ispair)"
huffman@15576: apply (rule contlubI)
huffman@15576: apply (intro strip)
huffman@15576: apply (rule expand_fun_eq [THEN iffD2])
huffman@15576: apply (intro strip)
huffman@15576: apply (subst lub_fun [THEN thelubI])
huffman@15576: apply (erule monofun_Ispair1 [THEN ch2ch_monofun])
huffman@15576: apply (rule trans)
huffman@15576: apply (rule_tac [2] thelub_sprod [symmetric])
huffman@15576: apply (rule_tac [2] ch2ch_fun)
huffman@15576: apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
huffman@15576: apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (erule sprod3_lemma1)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: apply (erule sprod3_lemma2)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: apply (erule sprod3_lemma3)
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: lemma sprod3_lemma4: 
huffman@15576: "[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> 
huffman@15576:           Ispair x (lub(range Y)) = 
huffman@15576:           Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
huffman@15576:                  (lub(range(%i. Issnd (Ispair x (Y i)))))"
huffman@15576: apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
huffman@15576: apply (rule sym)
huffman@15576: apply (drule chain_UU_I_inverse2)
huffman@15576: apply (erule exE)
huffman@15576: apply (rule lub_chain_maxelem)
huffman@15576: apply (erule Isfst2)
huffman@15576: apply (rule allI)
huffman@15576: apply (rename_tac "j")
huffman@15576: apply (case_tac "Y (j) =UU")
huffman@15576: apply auto
huffman@15576: done
huffman@15576: 
huffman@15576: lemma sprod3_lemma5: 
huffman@15576: "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
huffman@15576:           Ispair x (lub(range Y)) = 
huffman@15576:           Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) 
huffman@15576:                  (lub(range(%i. Issnd(Ispair x (Y i)))))"
huffman@15576: apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
huffman@15576: apply assumption
huffman@15576: apply (rule trans)
huffman@15576: apply (rule strict_Ispair2)
huffman@15576: apply (rule strict_Ispair [symmetric])
huffman@15576: apply (rule disjI2)
huffman@15576: apply (rule chain_UU_I_inverse)
huffman@15576: apply (rule allI)
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: apply (erule chain_UU_I [THEN spec])
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: lemma sprod3_lemma6: 
huffman@15576: "[| chain(Y); x = UU |] ==> 
huffman@15576:           Ispair x (lub(range Y)) = 
huffman@15576:           Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
huffman@15576:                  (lub(range(%i. Issnd (Ispair x (Y i)))))"
huffman@15576: apply (rule_tac s = "UU" and t = "x" in ssubst)
huffman@15576: apply assumption
huffman@15576: apply (rule trans)
huffman@15576: apply (rule strict_Ispair1)
huffman@15576: apply (rule strict_Ispair [symmetric])
huffman@15576: apply (rule disjI1)
huffman@15576: apply (rule chain_UU_I_inverse)
huffman@15576: apply (rule allI)
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma contlub_Ispair2: "contlub(Ispair(x))"
huffman@15576: apply (rule contlubI)
huffman@15576: apply (intro strip)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule_tac [2] thelub_sprod [symmetric])
huffman@15576: apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
huffman@15576: apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (erule sprod3_lemma4)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: apply (erule sprod3_lemma5)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: apply (erule sprod3_lemma6)
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: lemma cont_Ispair1: "cont(Ispair)"
huffman@15576: apply (rule monocontlub2cont)
huffman@15576: apply (rule monofun_Ispair1)
huffman@15576: apply (rule contlub_Ispair1)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma cont_Ispair2: "cont(Ispair(x))"
huffman@15576: apply (rule monocontlub2cont)
huffman@15576: apply (rule monofun_Ispair2)
huffman@15576: apply (rule contlub_Ispair2)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma contlub_Isfst: "contlub(Isfst)"
huffman@15576: apply (rule contlubI)
huffman@15576: apply (intro strip)
huffman@15576: apply (subst lub_sprod [THEN thelubI])
huffman@15576: apply assumption
huffman@15576: apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
huffman@15576: apply assumption
huffman@15576: apply (rule trans)
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: apply (rule sym)
huffman@15576: apply (rule chain_UU_I_inverse)
huffman@15576: apply (rule allI)
huffman@15576: apply (rule strict_Isfst)
huffman@15576: apply (rule contrapos_np)
huffman@15576: apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
huffman@15576: apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
huffman@15576: done
huffman@15576: 
huffman@15576: lemma contlub_Issnd: "contlub(Issnd)"
huffman@15576: apply (rule contlubI)
huffman@15576: apply (intro strip)
huffman@15576: apply (subst lub_sprod [THEN thelubI])
huffman@15576: apply assumption
huffman@15576: apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
huffman@15576: apply assumption
huffman@15576: apply (simp add: Sprod0_ss)
huffman@15576: apply (rule sym)
huffman@15576: apply (rule chain_UU_I_inverse)
huffman@15576: apply (rule allI)
huffman@15576: apply (rule strict_Issnd)
huffman@15576: apply (rule contrapos_np)
huffman@15576: apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
huffman@15576: apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
huffman@15576: done
huffman@15576: 
huffman@15576: lemma cont_Isfst: "cont(Isfst)"
huffman@15576: apply (rule monocontlub2cont)
huffman@15576: apply (rule monofun_Isfst)
huffman@15576: apply (rule contlub_Isfst)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma cont_Issnd: "cont(Issnd)"
huffman@15576: apply (rule monocontlub2cont)
huffman@15576: apply (rule monofun_Issnd)
huffman@15576: apply (rule contlub_Issnd)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
huffman@15576: apply fast
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* convert all lemmas to the continuous versions                            *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemma beta_cfun_sprod [simp]: 
huffman@15576:         "(LAM x y. Ispair x y)$a$b = Ispair a b"
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Ispair2)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma inject_spair: 
huffman@15576:         "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (erule inject_Ispair)
huffman@15576: apply assumption
huffman@15576: apply (erule box_equals)
huffman@15576: apply (rule beta_cfun_sprod)
huffman@15576: apply (rule beta_cfun_sprod)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (rule sym)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule beta_cfun_sprod)
huffman@15576: apply (rule sym)
huffman@15576: apply (rule inst_sprod_pcpo)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_spair: 
huffman@15576:         "(a=UU | b=UU) ==> (:a,b:)=UU"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule beta_cfun_sprod)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule_tac [2] inst_sprod_pcpo [symmetric])
huffman@15576: apply (erule strict_Ispair)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_spair1: "(:UU,b:) = UU"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule_tac [2] inst_sprod_pcpo [symmetric])
huffman@15576: apply (rule strict_Ispair1)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_spair2: "(:a,UU:) = UU"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule_tac [2] inst_sprod_pcpo [symmetric])
huffman@15576: apply (rule strict_Ispair2)
huffman@15576: done
huffman@15576: 
huffman@15576: declare strict_spair1 [simp] strict_spair2 [simp]
huffman@15576: 
huffman@15576: lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (rule strict_Ispair_rev)
huffman@15576: apply auto
huffman@15576: done
huffman@15576: 
huffman@15576: lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (rule defined_Ispair_rev)
huffman@15576: apply auto
huffman@15576: done
huffman@15576: 
huffman@15576: lemma defined_spair: 
huffman@15576:         "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (subst inst_sprod_pcpo)
huffman@15576: apply (erule defined_Ispair)
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: lemma Exh_Sprod2:
huffman@15576:         "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (rule Exh_Sprod [THEN disjE])
huffman@15576: apply (rule disjI1)
huffman@15576: apply (subst inst_sprod_pcpo)
huffman@15576: apply assumption
huffman@15576: apply (rule disjI2)
huffman@15576: apply (erule exE)
huffman@15576: apply (erule exE)
huffman@15576: apply (rule exI)
huffman@15576: apply (rule exI)
huffman@15576: apply (rule conjI)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply fast
huffman@15576: apply fast
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: lemma sprodE:
huffman@15576: assumes prem1: "p=UU ==> Q"
huffman@15576: assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
huffman@15576: shows "Q"
huffman@15576: apply (rule IsprodE)
huffman@15576: apply (rule prem1)
huffman@15576: apply (subst inst_sprod_pcpo)
huffman@15576: apply assumption
huffman@15576: apply (rule prem2)
huffman@15576: prefer 2 apply (assumption)
huffman@15576: prefer 2 apply (assumption)
huffman@15576: apply (unfold spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: lemma strict_sfst: 
huffman@15576:         "p=UU==>sfst$p=UU"
huffman@15576: apply (unfold sfst_def)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Isfst)
huffman@15576: apply (rule strict_Isfst)
huffman@15576: apply (rule inst_sprod_pcpo [THEN subst])
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_sfst1: 
huffman@15576:         "sfst$(:UU,y:) = UU"
huffman@15576: apply (unfold sfst_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Isfst)
huffman@15576: apply (rule strict_Isfst1)
huffman@15576: done
huffman@15576:  
huffman@15576: lemma strict_sfst2: 
huffman@15576:         "sfst$(:x,UU:) = UU"
huffman@15576: apply (unfold sfst_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Isfst)
huffman@15576: apply (rule strict_Isfst2)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_ssnd: 
huffman@15576:         "p=UU==>ssnd$p=UU"
huffman@15576: apply (unfold ssnd_def)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Issnd)
huffman@15576: apply (rule strict_Issnd)
huffman@15576: apply (rule inst_sprod_pcpo [THEN subst])
huffman@15576: apply assumption
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_ssnd1: 
huffman@15576:         "ssnd$(:UU,y:) = UU"
huffman@15576: apply (unfold ssnd_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Issnd)
huffman@15576: apply (rule strict_Issnd1)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma strict_ssnd2: 
huffman@15576:         "ssnd$(:x,UU:) = UU"
huffman@15576: apply (unfold ssnd_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Issnd)
huffman@15576: apply (rule strict_Issnd2)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma sfst2: 
huffman@15576:         "y~=UU ==>sfst$(:x,y:)=x"
huffman@15576: apply (unfold sfst_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Isfst)
huffman@15576: apply (erule Isfst2)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma ssnd2: 
huffman@15576:         "x~=UU ==>ssnd$(:x,y:)=y"
huffman@15576: apply (unfold ssnd_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Issnd)
huffman@15576: apply (erule Issnd2)
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: lemma defined_sfstssnd: 
huffman@15576:         "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
huffman@15576: apply (unfold sfst_def ssnd_def spair_def)
huffman@15576: apply (simplesubst beta_cfun)
huffman@15576: apply (rule cont_Issnd)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Isfst)
huffman@15576: apply (rule defined_IsfstIssnd)
huffman@15576: apply (rule inst_sprod_pcpo [THEN subst])
huffman@15576: apply assumption
huffman@15576: done
huffman@15576:  
huffman@15576: lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
huffman@15576: apply (unfold sfst_def ssnd_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (simplesubst beta_cfun)
huffman@15576: apply (rule cont_Issnd)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (rule cont_Isfst)
huffman@15576: apply (rule surjective_pairing_Sprod [symmetric])
huffman@15576: done
huffman@15576: 
huffman@15576: lemma lub_sprod2: 
huffman@15576: "chain(S) ==> range(S) <<|  
huffman@15576:                (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
huffman@15576: apply (unfold sfst_def ssnd_def spair_def)
huffman@15576: apply (subst beta_cfun_sprod)
huffman@15576: apply (simplesubst beta_cfun [THEN ext])
huffman@15576: apply (rule cont_Issnd)
huffman@15576: apply (subst beta_cfun [THEN ext])
huffman@15576: apply (rule cont_Isfst)
huffman@15576: apply (erule lub_sprod)
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
huffman@15576: (*
huffman@15576:  "chain ?S1 ==>
huffman@15576:  lub (range ?S1) =
huffman@15576:  (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
huffman@15576: *)
huffman@15576: 
huffman@15576: lemma ssplit1: 
huffman@15576:         "ssplit$f$UU=UU"
huffman@15576: apply (unfold ssplit_def)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (simp (no_asm))
huffman@15576: apply (subst strictify1)
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: lemma ssplit2: 
huffman@15576:         "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
huffman@15576: apply (unfold ssplit_def)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (simp (no_asm))
huffman@15576: apply (subst strictify2)
huffman@15576: apply (rule defined_spair)
huffman@15576: apply assumption
huffman@15576: apply assumption
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (simp (no_asm))
huffman@15576: apply (subst sfst2)
huffman@15576: apply assumption
huffman@15576: apply (subst ssnd2)
huffman@15576: apply assumption
huffman@15576: apply (rule refl)
huffman@15576: done
huffman@15576: 
huffman@15576: 
huffman@15576: lemma ssplit3: 
huffman@15576:   "ssplit$spair$z=z"
huffman@15576: apply (unfold ssplit_def)
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (simp (no_asm))
huffman@15576: apply (case_tac "z=UU")
huffman@15576: apply (erule ssubst)
huffman@15576: apply (rule strictify1)
huffman@15576: apply (rule trans)
huffman@15576: apply (rule strictify2)
huffman@15576: apply assumption
huffman@15576: apply (subst beta_cfun)
huffman@15576: apply (simp (no_asm))
huffman@15576: apply (rule surjective_pairing_Sprod2)
huffman@15576: done
huffman@15576: 
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: (* install simplifier for Sprod                                             *)
huffman@15576: (* ------------------------------------------------------------------------ *)
huffman@15576: 
huffman@15576: lemmas Sprod_rews = strict_sfst1 strict_sfst2
huffman@15576:                 strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
huffman@15576:                 ssplit1 ssplit2
huffman@15576: declare Sprod_rews [simp]
huffman@15576: 
huffman@15576: end