# HG changeset patch # User huffman # Date 1116906768 -7200 # Node ID dab0d004732f4607e5e8c23d03842b5408dcdf85 # Parent 3d50b521ab169f52e7f44b566966bbd3879f9e5a Simplified version of strict product theory, using TypedefPcpo diff -r 3d50b521ab16 -r dab0d004732f src/HOLCF/Sprod.ML --- a/src/HOLCF/Sprod.ML Tue May 24 05:51:06 2005 +0200 +++ b/src/HOLCF/Sprod.ML Tue May 24 05:52:48 2005 +0200 @@ -1,75 +1,11 @@ (* legacy ML bindings *) -val Ispair_def = thm "Ispair_def"; -val Isfst_def = thm "Isfst_def"; -val Issnd_def = thm "Issnd_def"; -val SprodI = thm "SprodI"; -val inj_on_Abs_Sprod = thm "inj_on_Abs_Sprod"; -val strict_Spair_Rep = thm "strict_Spair_Rep"; -val defined_Spair_Rep_rev = thm "defined_Spair_Rep_rev"; -val inject_Spair_Rep = thm "inject_Spair_Rep"; -val inject_Ispair = thm "inject_Ispair"; -val strict_Ispair = thm "strict_Ispair"; -val strict_Ispair1 = thm "strict_Ispair1"; -val strict_Ispair2 = thm "strict_Ispair2"; -val strict_Ispair_rev = thm "strict_Ispair_rev"; -val defined_Ispair_rev = thm "defined_Ispair_rev"; -val defined_Ispair = thm "defined_Ispair"; -val Exh_Sprod = thm "Exh_Sprod"; -val IsprodE = thm "IsprodE"; -val strict_Isfst = thm "strict_Isfst"; -val strict_Isfst1 = thm "strict_Isfst1"; -val strict_Isfst2 = thm "strict_Isfst2"; -val strict_Issnd = thm "strict_Issnd"; -val strict_Issnd1 = thm "strict_Issnd1"; -val strict_Issnd2 = thm "strict_Issnd2"; -val Isfst = thm "Isfst"; -val Issnd = thm "Issnd"; -val Isfst2 = thm "Isfst2"; -val Issnd2 = thm "Issnd2"; -val Sprod0_ss = [strict_Isfst1, strict_Isfst2, strict_Issnd1, strict_Issnd2, - Isfst2, Issnd2] -val defined_IsfstIssnd = thm "defined_IsfstIssnd"; -val surjective_pairing_Sprod = thm "surjective_pairing_Sprod"; -val Sel_injective_Sprod = thm "Sel_injective_Sprod"; val less_sprod_def = thm "less_sprod_def"; -val refl_less_sprod = thm "refl_less_sprod"; -val antisym_less_sprod = thm "antisym_less_sprod"; -val trans_less_sprod = thm "trans_less_sprod"; -val inst_sprod_po = thm "inst_sprod_po"; -val minimal_sprod = thm "minimal_sprod"; -val UU_sprod_def = thm "UU_sprod_def"; -val least_sprod = thm "least_sprod"; -val monofun_Ispair1 = thm "monofun_Ispair1"; -val monofun_Ispair2 = thm "monofun_Ispair2"; -val monofun_Ispair = thm "monofun_Ispair"; -val monofun_Isfst = thm "monofun_Isfst"; -val monofun_Issnd = thm "monofun_Issnd"; -val lub_sprod = thm "lub_sprod"; -val thelub_sprod = thm "thelub_sprod"; -val cpo_sprod = thm "cpo_sprod"; val spair_def = thm "spair_def"; val sfst_def = thm "sfst_def"; val ssnd_def = thm "ssnd_def"; val ssplit_def = thm "ssplit_def"; -val inst_sprod_pcpo = thm "inst_sprod_pcpo"; -val sprod3_lemma1 = thm "sprod3_lemma1"; -val sprod3_lemma2 = thm "sprod3_lemma2"; -val sprod3_lemma3 = thm "sprod3_lemma3"; -val contlub_Ispair1 = thm "contlub_Ispair1"; -val sprod3_lemma4 = thm "sprod3_lemma4"; -val sprod3_lemma5 = thm "sprod3_lemma5"; -val sprod3_lemma6 = thm "sprod3_lemma6"; -val contlub_Ispair2 = thm "contlub_Ispair2"; -val cont_Ispair1 = thm "cont_Ispair1"; -val cont_Ispair2 = thm "cont_Ispair2"; -val contlub_Isfst = thm "contlub_Isfst"; -val contlub_Issnd = thm "contlub_Issnd"; -val cont_Isfst = thm "cont_Isfst"; -val cont_Issnd = thm "cont_Issnd"; -val spair_eq = thm "spair_eq"; -val beta_cfun_sprod = thm "beta_cfun_sprod"; val inject_spair = thm "inject_spair"; val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; val strict_spair = thm "strict_spair"; @@ -81,21 +17,12 @@ val Exh_Sprod2 = thm "Exh_Sprod2"; val sprodE = thm "sprodE"; val strict_sfst = thm "strict_sfst"; -val strict_sfst1 = thm "strict_sfst1"; -val strict_sfst2 = thm "strict_sfst2"; val strict_ssnd = thm "strict_ssnd"; -val strict_ssnd1 = thm "strict_ssnd1"; -val strict_ssnd2 = thm "strict_ssnd2"; val sfst2 = thm "sfst2"; val ssnd2 = thm "ssnd2"; val defined_sfstssnd = thm "defined_sfstssnd"; val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; -val lub_sprod2 = thm "lub_sprod2"; -val thelub_sprod2 = thm "thelub_sprod2"; val ssplit1 = thm "ssplit1"; val ssplit2 = thm "ssplit2"; val ssplit3 = thm "ssplit3"; -val Sprod_rews = [strict_sfst1, strict_sfst2, - strict_ssnd1, strict_ssnd2, sfst2, ssnd2, defined_spair, - ssplit1, ssplit2] diff -r 3d50b521ab16 -r dab0d004732f src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Tue May 24 05:51:06 2005 +0200 +++ b/src/HOLCF/Sprod.thy Tue May 24 05:52:48 2005 +0200 @@ -1,6 +1,6 @@ (* Title: HOLCF/Sprod.thy ID: $Id$ - Author: Franz Regensburger + Author: Franz Regensburger and Brian Huffman License: GPL (GNU GENERAL PUBLIC LICENSE) Strict product with typedef. @@ -9,452 +9,76 @@ header {* The type of strict products *} theory Sprod -imports Cfun +imports Cprod TypedefPcpo begin subsection {* Definition of strict product type *} -constdefs - Spair_Rep :: "['a,'b] => ['a,'b] => bool" - "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))" - -typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}" -by auto +typedef (Sprod) ('a, 'b) "**" (infixr 20) = + "{p::'a \ 'b. p = \ \ (cfst\p \ \ \ csnd\p \ \)}" +by (auto simp add: inst_cprod_pcpo) syntax (xsymbols) "**" :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) syntax (HTML output) "**" :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) -consts - Ispair :: "['a,'b] => ('a ** 'b)" - Isfst :: "('a ** 'b) => 'a" - Issnd :: "('a ** 'b) => 'b" - -defs - (*defining the abstract constants*) - - Ispair_def: "Ispair a b == Abs_Sprod(Spair_Rep a b)" - - Isfst_def: "Isfst(p) == THE z. (p=Ispair UU UU --> z=UU) - &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)" - - Issnd_def: "Issnd(p) == THE z. (p=Ispair UU UU --> z=UU) - &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" - -text {* A non-emptiness result for Sprod *} - -lemma SprodI: "(Spair_Rep a b):Sprod" -apply (unfold Sprod_def) -apply (rule CollectI, rule exI, rule exI, rule refl) -done +subsection {* Class instances *} -lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod" -apply (rule inj_on_inverseI) -apply (erule Abs_Sprod_inverse) -done - -text {* Strictness and definedness of @{term Spair_Rep} *} +instance "**" :: (pcpo, pcpo) sq_ord .. +defs (overloaded) + less_sprod_def: "op \ \ \x y. Rep_Sprod x \ Rep_Sprod y" -lemma strict_Spair_Rep: - "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)" -apply (unfold Spair_Rep_def) -apply (rule ext) -apply (rule ext) -apply (rule iffI) -apply fast -apply fast -done - -lemma defined_Spair_Rep_rev: - "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)" -apply (unfold Spair_Rep_def) -apply (case_tac "a=UU|b=UU") -apply assumption -apply (fast dest: fun_cong) -done - -text {* injectivity of @{term Spair_Rep} and @{term Ispair} *} +lemma adm_Sprod: "adm (\x. x \ Sprod)" +by (simp add: Sprod_def) -lemma inject_Spair_Rep: -"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba" - -apply (unfold Spair_Rep_def) -apply (drule fun_cong) -apply (drule fun_cong) -apply (erule iffD1 [THEN mp]) -apply auto -done - -lemma inject_Ispair: - "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba" -apply (unfold Ispair_def) -apply (erule inject_Spair_Rep) -apply assumption -apply (erule inj_on_Abs_Sprod [THEN inj_onD]) -apply (rule SprodI) -apply (rule SprodI) -done - -text {* strictness and definedness of @{term Ispair} *} +lemma UU_Sprod: "\ \ Sprod" +by (simp add: Sprod_def) -lemma strict_Ispair: - "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU" -apply (unfold Ispair_def) -apply (erule strict_Spair_Rep [THEN arg_cong]) -done - -lemma strict_Ispair1: - "Ispair UU b = Ispair UU UU" -apply (unfold Ispair_def) -apply (rule strict_Spair_Rep [THEN arg_cong]) -apply (rule disjI1) -apply (rule refl) -done +instance "**" :: (pcpo, pcpo) po +by (rule typedef_po [OF type_definition_Sprod less_sprod_def]) -lemma strict_Ispair2: - "Ispair a UU = Ispair UU UU" -apply (unfold Ispair_def) -apply (rule strict_Spair_Rep [THEN arg_cong]) -apply (rule disjI2) -apply (rule refl) -done - -lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU" -apply (rule de_Morgan_disj [THEN subst]) -apply (erule contrapos_nn) -apply (erule strict_Ispair) -done +instance "**" :: (pcpo, pcpo) cpo +by (rule typedef_cpo [OF type_definition_Sprod less_sprod_def adm_Sprod]) -lemma defined_Ispair_rev: - "Ispair a b = Ispair UU UU ==> (a = UU | b = UU)" -apply (unfold Ispair_def) -apply (rule defined_Spair_Rep_rev) -apply (rule inj_on_Abs_Sprod [THEN inj_onD]) -apply assumption -apply (rule SprodI) -apply (rule SprodI) -done - -lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)" -apply (rule contrapos_nn) -apply (erule_tac [2] defined_Ispair_rev) -apply (rule de_Morgan_disj [THEN iffD2]) -apply (erule conjI) -apply assumption -done - -text {* Exhaustion of the strict product @{typ "'a ** 'b"} *} +instance "**" :: (pcpo, pcpo) pcpo +by (rule typedef_pcpo_UU [OF type_definition_Sprod less_sprod_def UU_Sprod]) -lemma Exh_Sprod: - "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)" -apply (unfold Ispair_def) -apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE]) -apply (erule exE) -apply (erule exE) -apply (rule excluded_middle [THEN disjE]) -apply (rule disjI2) -apply (rule exI) -apply (rule exI) -apply (rule conjI) -apply (rule Rep_Sprod_inverse [symmetric, THEN trans]) -apply (erule arg_cong) -apply (rule de_Morgan_disj [THEN subst]) -apply assumption -apply (rule disjI1) -apply (rule Rep_Sprod_inverse [symmetric, THEN trans]) -apply (rule_tac f = "Abs_Sprod" in arg_cong) -apply (erule trans) -apply (erule strict_Spair_Rep) -done +lemmas cont_Rep_Sprod = + typedef_cont_Rep [OF type_definition_Sprod less_sprod_def adm_Sprod] -text {* general elimination rule for strict product *} +lemmas cont_Abs_Sprod = + typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod] -lemma IsprodE: -assumes prem1: "p=Ispair UU UU ==> Q" -assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q" -shows "Q" -apply (rule Exh_Sprod [THEN disjE]) -apply (erule prem1) -apply (erule exE) -apply (erule exE) -apply (erule conjE) -apply (erule conjE) -apply (erule prem2) -apply assumption -apply assumption -done +lemmas strict_Rep_Sprod = + typedef_strict_Rep [OF type_definition_Sprod less_sprod_def UU_Sprod] -text {* some results about the selectors @{term Isfst}, @{term Issnd} *} - -lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU" -apply (unfold Isfst_def) -apply (rule the_equality) -apply (rule conjI) -apply fast -apply (intro strip) -apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE) -apply (rule not_sym) -apply (rule defined_Ispair) -apply (fast+) -done +lemmas strict_Abs_Sprod = + typedef_strict_Abs [OF type_definition_Sprod less_sprod_def UU_Sprod] -lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU" -apply (subst strict_Ispair1) -apply (rule strict_Isfst) -apply (rule refl) -done - -lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU" -apply (subst strict_Ispair2) -apply (rule strict_Isfst) -apply (rule refl) -done +lemma UU_Abs_Sprod: "\ = Abs_Sprod <\, \>" +by (simp add: strict_Abs_Sprod inst_cprod_pcpo2 [symmetric]) -lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU" -apply (unfold Issnd_def) -apply (rule the_equality) -apply (rule conjI) -apply fast -apply (intro strip) -apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE) -apply (rule not_sym) -apply (rule defined_Ispair) -apply (fast+) -done - -lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU" -apply (subst strict_Ispair1) -apply (rule strict_Issnd) -apply (rule refl) -done - -lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU" -apply (subst strict_Ispair2) -apply (rule strict_Issnd) -apply (rule refl) +lemma spair_lemma: + "(\ b. a)\b, strictify\(\ a. b)\a> \ Sprod" +apply (simp add: Sprod_def inst_cprod_pcpo2) +apply (case_tac "a = \", case_tac [!] "b = \", simp_all) done -lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x" -apply (unfold Isfst_def) -apply (rule the_equality) -apply (rule conjI) -apply (intro strip) -apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE) -apply (erule defined_Ispair) -apply assumption -apply assumption -apply (intro strip) -apply (rule inject_Ispair [THEN conjunct1]) -prefer 3 apply fast -apply (fast+) -done - -lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y" -apply (unfold Issnd_def) -apply (rule the_equality) -apply (rule conjI) -apply (intro strip) -apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE) -apply (erule defined_Ispair) -apply assumption -apply assumption -apply (intro strip) -apply (rule inject_Ispair [THEN conjunct2]) -prefer 3 apply fast -apply (fast+) -done - -lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x" -apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) -apply (erule Isfst) -apply assumption -apply (erule ssubst) -apply (rule strict_Isfst1) -done - -lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y" -apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE]) -apply (erule Issnd) -apply assumption -apply (erule ssubst) -apply (rule strict_Issnd2) -done - - -text {* instantiate the simplifier *} - -lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2 - Isfst2 Issnd2 - -declare Isfst2 [simp] Issnd2 [simp] - -lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU" -apply (rule_tac p = "p" in IsprodE) -apply simp -apply (erule ssubst) -apply (rule conjI) -apply (simp add: Sprod0_ss) -apply (simp add: Sprod0_ss) -done - - -text {* Surjective pairing: equivalent to @{thm [source] Exh_Sprod} *} - -lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)" -apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE]) -apply (simp add: Sprod0_ss) -apply (erule exE) -apply (erule exE) -apply (simp add: Sprod0_ss) -done - -lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y" -apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ") -apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric]) -apply simp -done - -subsection {* Type @{typ "'a ** 'b"} is a partial order *} - -instance "**" :: (sq_ord, sq_ord) sq_ord .. - -defs (overloaded) - less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2" - -lemma refl_less_sprod: "(p::'a ** 'b) << p" -apply (unfold less_sprod_def) -apply (fast intro: refl_less) -done - -lemma antisym_less_sprod: - "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2" -apply (unfold less_sprod_def) -apply (rule Sel_injective_Sprod) -apply (fast intro: antisym_less) -apply (fast intro: antisym_less) -done - -lemma trans_less_sprod: - "[|(p1::'a ** 'b) << p2;p2 << p3|] ==> p1 << p3" -apply (unfold less_sprod_def) -apply (blast intro: trans_less) -done - -instance "**" :: (pcpo, pcpo) po -by intro_classes - (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+ +subsection {* Definitions of constants *} -text {* for compatibility with old HOLCF-Version *} -lemma inst_sprod_po: "(op <<)=(%x y. Isfst x< Ispair x1 y1 << Ispair x2 y2" -apply (rule trans_less) -apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]]) -prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp]) -apply assumption -apply assumption -done - -text {* @{term Isfst} and @{term Issnd} are monotone *} - -lemma monofun_Isfst: "monofun(Isfst)" -by (simp add: monofun inst_sprod_po) - -lemma monofun_Issnd: "monofun(Issnd)" -by (simp add: monofun inst_sprod_po) - -subsection {* Type @{typ "'a ** 'b"} is a cpo *} +consts + sfst :: "('a ** 'b) \ 'a" + ssnd :: "('a ** 'b) \ 'b" + spair :: "'a \ 'b \ ('a ** 'b)" + ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" -lemma lub_sprod: -"[|chain(S)|] ==> range(S) <<| - Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))" -apply (rule is_lubI) -apply (rule ub_rangeI) -apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst]) -apply (rule monofun_Ispair) -apply (rule is_ub_thelub) -apply (erule monofun_Isfst [THEN ch2ch_monofun]) -apply (rule is_ub_thelub) -apply (erule monofun_Issnd [THEN ch2ch_monofun]) -apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst]) -apply (rule monofun_Ispair) -apply (rule is_lub_thelub) -apply (erule monofun_Isfst [THEN ch2ch_monofun]) -apply (erule monofun_Isfst [THEN ub2ub_monofun]) -apply (rule is_lub_thelub) -apply (erule monofun_Issnd [THEN ch2ch_monofun]) -apply (erule monofun_Issnd [THEN ub2ub_monofun]) -done - -lemmas thelub_sprod = lub_sprod [THEN thelubI, standard] - -lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x" -apply (rule exI) -apply (erule lub_sprod) -done - -instance "**" :: (pcpo, pcpo) cpo -by intro_classes (rule cpo_sprod) - -subsection {* Type @{typ "'a ** 'b"} is pointed *} - -lemma minimal_sprod: "Ispair UU UU << p" -apply (simp add: inst_sprod_po minimal) -done - -lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard] - -lemma least_sprod: "? x::'a**'b.!y. x< 'b -> ('a**'b)" (* continuous strict pairing *) - sfst :: "('a**'b)->'a" - ssnd :: "('a**'b)->'b" - ssplit :: "('a->'b->'c)->('a**'b)->'c" +defs + sfst_def: "sfst \ \ p. cfst\(Rep_Sprod p)" + ssnd_def: "ssnd \ \ p. csnd\(Rep_Sprod p)" + spair_def: "spair \ \ a b. Abs_Sprod + (\ b. a)\b, strictify\(\ a. b)\a>" + ssplit_def: "ssplit \ \ f. strictify\(\ p. f\(sfst\p)\(ssnd\p))" syntax "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") @@ -463,467 +87,107 @@ "(:x, y, z:)" == "(:x, (:y, z:):)" "(:x, y:)" == "spair$x$y" -defs -spair_def: "spair == (LAM x y. Ispair x y)" -sfst_def: "sfst == (LAM p. Isfst p)" -ssnd_def: "ssnd == (LAM p. Issnd p)" -ssplit_def: "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))" - -subsection {* Continuity of @{term Ispair}, @{term Isfst}, @{term Issnd} *} +subsection {* Case analysis *} -lemma sprod3_lemma1: -"[| 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))))" -apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong]) -apply (rule lub_equal) -apply assumption -apply (rule monofun_Isfst [THEN ch2ch_monofun]) -apply (rule ch2ch_fun) -apply (rule monofun_Ispair1 [THEN ch2ch_monofun]) -apply assumption -apply (rule allI) -apply (simp (no_asm_simp)) -apply (rule sym) -apply (drule chain_UU_I_inverse2) -apply (erule exE) -apply (rule lub_chain_maxelem) -apply (erule Issnd2) -apply (rule allI) -apply (rename_tac "j") -apply (case_tac "Y (j) =UU") -apply auto -done - -lemma sprod3_lemma2: -"[| 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))))" -apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) -apply assumption -apply (rule trans) -apply (rule strict_Ispair1) -apply (rule strict_Ispair [symmetric]) -apply (rule disjI1) -apply (rule chain_UU_I_inverse) -apply auto -apply (erule chain_UU_I [THEN spec]) -apply assumption +lemma spair_Abs_Sprod: + "(:a, b:) = Abs_Sprod (\ b. a)\b, strictify\(\ a. b)\a>" +apply (unfold spair_def) +apply (simp add: cont_Abs_Sprod spair_lemma) done - -lemma sprod3_lemma3: -"[| 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))))" -apply (erule ssubst) -apply (rule trans) -apply (rule strict_Ispair2) -apply (rule strict_Ispair [symmetric]) -apply (rule disjI1) -apply (rule chain_UU_I_inverse) -apply (rule allI) -apply (simp add: Sprod0_ss) -done - -lemma contlub_Ispair1: "contlub(Ispair)" -apply (rule contlubI) -apply (intro strip) -apply (rule expand_fun_eq [THEN iffD2]) -apply (intro strip) -apply (subst lub_fun [THEN thelubI]) -apply (erule monofun_Ispair1 [THEN ch2ch_monofun]) -apply (rule trans) -apply (rule_tac [2] thelub_sprod [symmetric]) -apply (rule_tac [2] ch2ch_fun) -apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun]) -apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) -apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE]) -apply (erule sprod3_lemma1) -apply assumption -apply assumption -apply (erule sprod3_lemma2) -apply assumption -apply assumption -apply (erule sprod3_lemma3) -apply assumption -done - -lemma sprod3_lemma4: -"[| 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)))))" -apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong]) -apply (rule sym) -apply (drule chain_UU_I_inverse2) -apply (erule exE) -apply (rule lub_chain_maxelem) -apply (erule Isfst2) -apply (rule allI) -apply (rename_tac "j") -apply (case_tac "Y (j) =UU") -apply auto +lemma Exh_Sprod2: + "z = \ \ (\a b. z = (:a, b:) \ a \ \ \ b \ \)" +apply (rule_tac x=z in Abs_Sprod_cases) +apply (simp add: Sprod_def) +apply (erule disjE) +apply (simp add: strict_Abs_Sprod) +apply (rule disjI2) +apply (rule_tac x="cfst\y" in exI) +apply (rule_tac x="csnd\y" in exI) +apply (simp add: spair_Abs_Sprod Abs_Sprod_inject spair_lemma) +apply (simp add: surjective_pairing_Cprod2) done -lemma sprod3_lemma5: -"[| 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)))))" -apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) -apply assumption -apply (rule trans) -apply (rule strict_Ispair2) -apply (rule strict_Ispair [symmetric]) -apply (rule disjI2) -apply (rule chain_UU_I_inverse) -apply (rule allI) -apply (simp add: Sprod0_ss) -apply (erule chain_UU_I [THEN spec]) -apply assumption +lemma sprodE: + "\p = \ \ Q; \x y. \p = (:x, y:); x \ \; y \ \\ \ Q\ \ Q" +by (cut_tac z=p in Exh_Sprod2, auto) + +subsection {* Properties of @{term spair} *} + +lemma strict_spair1 [simp]: "(:\, b:) = \" +apply (simp add: spair_Abs_Sprod UU_Abs_Sprod) +apply (case_tac "b = \", simp_all) done -lemma sprod3_lemma6: -"[| 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)))))" -apply (rule_tac s = "UU" and t = "x" in ssubst) -apply assumption -apply (rule trans) -apply (rule strict_Ispair1) -apply (rule strict_Ispair [symmetric]) -apply (rule disjI1) -apply (rule chain_UU_I_inverse) -apply (rule allI) -apply (simp add: Sprod0_ss) -done - -lemma contlub_Ispair2: "contlub(Ispair(x))" -apply (rule contlubI) -apply (intro strip) -apply (rule trans) -apply (rule_tac [2] thelub_sprod [symmetric]) -apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun]) -apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) -apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE]) -apply (erule sprod3_lemma4) -apply assumption -apply assumption -apply (erule sprod3_lemma5) -apply assumption -apply assumption -apply (erule sprod3_lemma6) -apply assumption -done - -lemma cont_Ispair1: "cont(Ispair)" -apply (rule monocontlub2cont) -apply (rule monofun_Ispair1) -apply (rule contlub_Ispair1) -done - -lemma cont_Ispair2: "cont(Ispair(x))" -apply (rule monocontlub2cont) -apply (rule monofun_Ispair2) -apply (rule contlub_Ispair2) +lemma strict_spair2 [simp]: "(:a, \:) = \" +apply (simp add: spair_Abs_Sprod UU_Abs_Sprod) +apply (case_tac "a = \", simp_all) done -lemma contlub_Isfst: "contlub(Isfst)" -apply (rule contlubI) -apply (intro strip) -apply (subst lub_sprod [THEN thelubI]) -apply assumption -apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE]) -apply (simp add: Sprod0_ss) -apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst) -apply assumption -apply (rule trans) -apply (simp add: Sprod0_ss) -apply (rule sym) -apply (rule chain_UU_I_inverse) -apply (rule allI) -apply (rule strict_Isfst) -apply (rule contrapos_np) -apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2]) -apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec]) +lemma strict_spair: "a = \ \ b = \ \ (:a, b:) = \" +by auto + +lemma strict_spair_rev: "(:x, y:) \ \ \ x \ \ \ y \ \" +by (erule contrapos_np, auto) + +lemma defined_spair [simp]: + "\a \ \; b \ \\ \ (:a, b:) \ \" +apply (simp add: spair_Abs_Sprod UU_Abs_Sprod) +apply (subst Abs_Sprod_inject) +apply (simp add: Sprod_def) +apply (simp add: Sprod_def inst_cprod_pcpo2) +apply simp done -lemma contlub_Issnd: "contlub(Issnd)" -apply (rule contlubI) -apply (intro strip) -apply (subst lub_sprod [THEN thelubI]) -apply assumption -apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE]) -apply (simp add: Sprod0_ss) -apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst) -apply assumption -apply (simp add: Sprod0_ss) -apply (rule sym) -apply (rule chain_UU_I_inverse) -apply (rule allI) -apply (rule strict_Issnd) -apply (rule contrapos_np) -apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1]) -apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec]) -done - -lemma cont_Isfst: "cont(Isfst)" -apply (rule monocontlub2cont) -apply (rule monofun_Isfst) -apply (rule contlub_Isfst) -done - -lemma cont_Issnd: "cont(Issnd)" -apply (rule monocontlub2cont) -apply (rule monofun_Issnd) -apply (rule contlub_Issnd) -done - -lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)" -apply fast -done - -text {* convert all lemmas to the continuous versions *} - -lemma beta_cfun_sprod [simp]: - "(LAM x y. Ispair x y)$a$b = Ispair a b" -apply (subst beta_cfun) -apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L) -apply (subst beta_cfun) -apply (rule cont_Ispair2) -apply (rule refl) -done +lemma defined_spair_rev: "(:a, b:) = \ \ a = \ \ b = \" +by (erule contrapos_pp, simp) lemma inject_spair: - "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba" -apply (unfold spair_def) -apply (erule inject_Ispair) -apply assumption -apply (erule box_equals) -apply (rule beta_cfun_sprod) -apply (rule beta_cfun_sprod) + "\aa \ \; ba \ \; (:a,b:) = (:aa,ba:)\ \ a = aa \ b = ba" +apply (simp add: spair_Abs_Sprod) +apply (simp add: Abs_Sprod_inject [OF spair_lemma] Sprod_def) +apply (case_tac "a = \", simp_all) +apply (case_tac "b = \", simp_all) done lemma inst_sprod_pcpo2: "UU = (:UU,UU:)" -apply (unfold spair_def) -apply (rule sym) -apply (rule trans) -apply (rule beta_cfun_sprod) -apply (rule sym) -apply (rule inst_sprod_pcpo) -done +by simp -lemma strict_spair: - "(a=UU | b=UU) ==> (:a,b:)=UU" -apply (unfold spair_def) -apply (rule trans) -apply (rule beta_cfun_sprod) -apply (rule trans) -apply (rule_tac [2] inst_sprod_pcpo [symmetric]) -apply (erule strict_Ispair) -done +subsection {* Properties of @{term sfst} and @{term ssnd} *} -lemma strict_spair1: "(:UU,b:) = UU" -apply (unfold spair_def) -apply (subst beta_cfun_sprod) -apply (rule trans) -apply (rule_tac [2] inst_sprod_pcpo [symmetric]) -apply (rule strict_Ispair1) -done - -lemma strict_spair2: "(:a,UU:) = UU" -apply (unfold spair_def) -apply (subst beta_cfun_sprod) -apply (rule trans) -apply (rule_tac [2] inst_sprod_pcpo [symmetric]) -apply (rule strict_Ispair2) -done +lemma strict_sfst [simp]: "sfst\\ = \" +by (simp add: sfst_def cont_Rep_Sprod strict_Rep_Sprod) -declare strict_spair1 [simp] strict_spair2 [simp] - -lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU" -apply (unfold spair_def) -apply (rule strict_Ispair_rev) -apply auto -done +lemma strict_ssnd [simp]: "ssnd\\ = \" +by (simp add: ssnd_def cont_Rep_Sprod strict_Rep_Sprod) -lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)" -apply (unfold spair_def) -apply (rule defined_Ispair_rev) -apply auto -done - -lemma defined_spair [simp]: - "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU" +lemma Rep_Sprod_spair: + "Rep_Sprod (:a, b:) = (\ b. a)\b, strictify\(\ a. b)\a>" apply (unfold spair_def) -apply (subst beta_cfun_sprod) -apply (subst inst_sprod_pcpo) -apply (erule defined_Ispair) -apply assumption -done - -lemma Exh_Sprod2: - "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)" -apply (unfold spair_def) -apply (rule Exh_Sprod [THEN disjE]) -apply (rule disjI1) -apply (subst inst_sprod_pcpo) -apply assumption -apply (rule disjI2) -apply (erule exE) -apply (erule exE) -apply (rule exI) -apply (rule exI) -apply (rule conjI) -apply (subst beta_cfun_sprod) -apply fast -apply fast -done - -lemma sprodE: -assumes prem1: "p=UU ==> Q" -assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q" -shows "Q" -apply (rule IsprodE) -apply (rule prem1) -apply (subst inst_sprod_pcpo) -apply assumption -apply (rule prem2) -prefer 2 apply (assumption) -prefer 2 apply (assumption) -apply (unfold spair_def) -apply (subst beta_cfun_sprod) -apply assumption -done - -lemma strict_sfst: "p=UU==>sfst$p=UU" -apply (unfold sfst_def) -apply (subst beta_cfun) -apply (rule cont_Isfst) -apply (rule strict_Isfst) -apply (rule inst_sprod_pcpo [THEN subst]) -apply assumption -done - -lemma strict_sfst1 [simp]: "sfst$(:UU,y:) = UU" -apply (unfold sfst_def spair_def) -apply (subst beta_cfun_sprod) -apply (subst beta_cfun) -apply (rule cont_Isfst) -apply (rule strict_Isfst1) +apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma) done -lemma strict_sfst2 [simp]: "sfst$(:x,UU:) = UU" -apply (unfold sfst_def spair_def) -apply (subst beta_cfun_sprod) -apply (subst beta_cfun) -apply (rule cont_Isfst) -apply (rule strict_Isfst2) -done - -lemma strict_ssnd: "p=UU==>ssnd$p=UU" -apply (unfold ssnd_def) -apply (subst beta_cfun) -apply (rule cont_Issnd) -apply (rule strict_Issnd) -apply (rule inst_sprod_pcpo [THEN subst]) -apply assumption -done +lemma sfst2 [simp]: "y \ \ \ sfst\(:x, y:) = x" +by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair) -lemma strict_ssnd1 [simp]: "ssnd$(:UU,y:) = UU" -apply (unfold ssnd_def spair_def) -apply (subst beta_cfun_sprod) -apply (subst beta_cfun) -apply (rule cont_Issnd) -apply (rule strict_Issnd1) -done - -lemma strict_ssnd2 [simp]: "ssnd$(:x,UU:) = UU" -apply (unfold ssnd_def spair_def) -apply (subst beta_cfun_sprod) -apply (subst beta_cfun) -apply (rule cont_Issnd) -apply (rule strict_Issnd2) -done - -lemma sfst2 [simp]: "y~=UU ==>sfst$(:x,y:)=x" -apply (unfold sfst_def spair_def) -apply (subst beta_cfun_sprod) -apply (subst beta_cfun) -apply (rule cont_Isfst) -apply (erule Isfst2) -done +lemma ssnd2 [simp]: "x \ \ \ ssnd\(:x, y:) = y" +by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair) -lemma ssnd2 [simp]: "x~=UU ==>ssnd$(:x,y:)=y" -apply (unfold ssnd_def spair_def) -apply (subst beta_cfun_sprod) -apply (subst beta_cfun) -apply (rule cont_Issnd) -apply (erule Issnd2) -done - - -lemma defined_sfstssnd: "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU" -apply (unfold sfst_def ssnd_def spair_def) -apply (simplesubst beta_cfun) -apply (rule cont_Issnd) -apply (subst beta_cfun) -apply (rule cont_Isfst) -apply (rule defined_IsfstIssnd) -apply (rule inst_sprod_pcpo [THEN subst]) -apply assumption -done +lemma defined_sfstssnd: "p \ \ \ sfst\p \ \ \ ssnd\p \ \" +by (rule_tac p=p in sprodE, simp_all) -lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p" -apply (unfold sfst_def ssnd_def spair_def) -apply (subst beta_cfun_sprod) -apply (simplesubst beta_cfun) -apply (rule cont_Issnd) -apply (subst beta_cfun) -apply (rule cont_Isfst) -apply (rule surjective_pairing_Sprod [symmetric]) -done +lemma surjective_pairing_Sprod2: "(:sfst\p, ssnd\p:) = p" +by (rule_tac p=p in sprodE, simp_all) -lemma lub_sprod2: -"chain(S) ==> range(S) <<| - (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)" -apply (unfold sfst_def ssnd_def spair_def) -apply (subst beta_cfun_sprod) -apply (simplesubst beta_cfun [THEN ext]) -apply (rule cont_Issnd) -apply (subst beta_cfun [THEN ext]) -apply (rule cont_Isfst) -apply (erule lub_sprod) -done +subsection {* Properties of @{term ssplit} *} -lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard] -(* - "chain ?S1 ==> - lub (range ?S1) = - (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm -*) - -lemma ssplit1 [simp]: "ssplit$f$UU=UU" +lemma ssplit1 [simp]: "ssplit\f\\ = \" by (simp add: ssplit_def) -lemma ssplit2 [simp]: "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y" +lemma ssplit2 [simp]: "\x \ \; y \ \\ \ ssplit\f\(:x, y:)= f\x\y" by (simp add: ssplit_def) -lemma ssplit3: "ssplit$spair$z=z" -apply (simp add: ssplit_def) -apply (simp add: surjective_pairing_Sprod2) -apply (case_tac "z=UU", simp_all) -done - -text {* install simplifier for Sprod *} - -lemmas Sprod_rews = strict_sfst1 strict_sfst2 - strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair - ssplit1 ssplit2 +lemma ssplit3: "ssplit\spair\z = z" +by (rule_tac p=z in sprodE, simp_all) end