# HG changeset patch # User huffman # Date 1109810252 -3600 # Node ID 41bfe19eabe2bb19453b5f7e731c8015c97e063e # Parent 60743edae74a183a5c2c5bdabedd320a0d8be8b6 converted to new-style theory diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum0.ML --- a/src/HOLCF/Ssum0.ML Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum0.ML Thu Mar 03 01:37:32 2005 +0100 @@ -1,292 +1,29 @@ -(* Title: HOLCF/Ssum0.ML - ID: $Id$ - Author: Franz Regensburger -Strict sum with typedef -*) - -(* ------------------------------------------------------------------------ *) -(* A non-emptyness result for Sssum *) -(* ------------------------------------------------------------------------ *) - -Goalw [Ssum_def] "Sinl_Rep(a):Ssum"; -by (Blast_tac 1); -qed "SsumIl"; - -Goalw [Ssum_def] "Sinr_Rep(a):Ssum"; -by (Blast_tac 1); -qed "SsumIr"; - -Goal "inj_on Abs_Ssum Ssum"; -by (rtac inj_on_inverseI 1); -by (etac Abs_Ssum_inverse 1); -qed "inj_on_Abs_Ssum"; - -(* ------------------------------------------------------------------------ *) -(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *) -(* ------------------------------------------------------------------------ *) - -Goalw [Sinr_Rep_def,Sinl_Rep_def] - "Sinl_Rep(UU) = Sinr_Rep(UU)"; -by (rtac ext 1); -by (rtac ext 1); -by (rtac ext 1); -by (fast_tac HOL_cs 1); -qed "strict_SinlSinr_Rep"; - -Goalw [Isinl_def,Isinr_def] - "Isinl(UU) = Isinr(UU)"; -by (rtac (strict_SinlSinr_Rep RS arg_cong) 1); -qed "strict_IsinlIsinr"; - - -(* ------------------------------------------------------------------------ *) -(* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) -(* ------------------------------------------------------------------------ *) - -Goalw [Sinl_Rep_def,Sinr_Rep_def] - "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"; -by (blast_tac (claset() addSDs [fun_cong]) 1); -qed "noteq_SinlSinr_Rep"; - - -Goalw [Isinl_def,Isinr_def] - "Isinl(a)=Isinr(b) ==> a=UU & b=UU"; -by (rtac noteq_SinlSinr_Rep 1); -by (etac (inj_on_Abs_Ssum RS inj_onD) 1); -by (rtac SsumIl 1); -by (rtac SsumIr 1); -qed "noteq_IsinlIsinr"; - - - -(* ------------------------------------------------------------------------ *) -(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) -(* ------------------------------------------------------------------------ *) - -Goalw [Sinl_Rep_def] "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"; -by (blast_tac (claset() addSDs [fun_cong]) 1); -qed "inject_Sinl_Rep1"; - -Goalw [Sinr_Rep_def] "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"; -by (blast_tac (claset() addSDs [fun_cong]) 1); -qed "inject_Sinr_Rep1"; - -Goalw [Sinl_Rep_def] -"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"; -by (blast_tac (claset() addSDs [fun_cong]) 1); -qed "inject_Sinl_Rep2"; - -Goalw [Sinr_Rep_def] -"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"; -by (blast_tac (claset() addSDs [fun_cong]) 1); -qed "inject_Sinr_Rep2"; - -Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"; -by (case_tac "a1=UU" 1); -by (hyp_subst_tac 1); -by (rtac (inject_Sinl_Rep1 RS sym) 1); -by (etac sym 1); -by (case_tac "a2=UU" 1); -by (hyp_subst_tac 1); -by (etac inject_Sinl_Rep1 1); -by (etac inject_Sinl_Rep2 1); -by (atac 1); -by (atac 1); -qed "inject_Sinl_Rep"; - -Goal "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"; -by (case_tac "b1=UU" 1); -by (hyp_subst_tac 1); -by (rtac (inject_Sinr_Rep1 RS sym) 1); -by (etac sym 1); -by (case_tac "b2=UU" 1); -by (hyp_subst_tac 1); -by (etac inject_Sinr_Rep1 1); -by (etac inject_Sinr_Rep2 1); -by (atac 1); -by (atac 1); -qed "inject_Sinr_Rep"; - -Goalw [Isinl_def] "Isinl(a1)=Isinl(a2)==> a1=a2"; -by (rtac inject_Sinl_Rep 1); -by (etac (inj_on_Abs_Ssum RS inj_onD) 1); -by (rtac SsumIl 1); -by (rtac SsumIl 1); -qed "inject_Isinl"; - -Goalw [Isinr_def] "Isinr(b1)=Isinr(b2) ==> b1=b2"; -by (rtac inject_Sinr_Rep 1); -by (etac (inj_on_Abs_Ssum RS inj_onD) 1); -by (rtac SsumIr 1); -by (rtac SsumIr 1); -qed "inject_Isinr"; - -AddSDs [inject_Isinl, inject_Isinr]; - -Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"; -by (Blast_tac 1); -qed "inject_Isinl_rev"; - -Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"; -by (Blast_tac 1); -qed "inject_Isinr_rev"; - -(* ------------------------------------------------------------------------ *) -(* Exhaustion of the strict sum ++ *) -(* choice of the bottom representation is arbitrary *) -(* ------------------------------------------------------------------------ *) +(* legacy ML bindings *) -Goalw [Isinl_def,Isinr_def] - "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"; -by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1); -by (etac disjE 1); -by (etac exE 1); -by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1); -by (etac disjI1 1); -by (rtac disjI2 1); -by (rtac disjI1 1); -by (rtac exI 1); -by (rtac conjI 1); -by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); -by (etac arg_cong 1); -by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos_nn 1); -by (etac arg_cong 2); -by (etac contrapos_nn 1); -by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); -by (rtac trans 1); -by (etac arg_cong 1); -by (etac arg_cong 1); -by (etac exE 1); -by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1); -by (etac disjI1 1); -by (rtac disjI2 1); -by (rtac disjI2 1); -by (rtac exI 1); -by (rtac conjI 1); -by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); -by (etac arg_cong 1); -by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos_nn 1); -by (hyp_subst_tac 2); -by (rtac (strict_SinlSinr_Rep RS sym) 2); -by (etac contrapos_nn 1); -by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); -by (rtac trans 1); -by (etac arg_cong 1); -by (etac arg_cong 1); -qed "Exh_Ssum"; - -(* ------------------------------------------------------------------------ *) -(* elimination rules for the strict sum ++ *) -(* ------------------------------------------------------------------------ *) - -val prems = Goal - "[|p=Isinl(UU) ==> Q ;\ -\ !!x.[|p=Isinl(x); x~=UU |] ==> Q;\ -\ !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"; -by (rtac (Exh_Ssum RS disjE) 1); -by (etac disjE 2); -by (eresolve_tac prems 1); -by (etac exE 1); -by (etac conjE 1); -by (eresolve_tac prems 1); -by (atac 1); -by (etac exE 1); -by (etac conjE 1); -by (eresolve_tac prems 1); -by (atac 1); -qed "IssumE"; - -val prems = Goal -"[| !!x. [| p = Isinl(x) |] ==> Q; !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"; -by (rtac IssumE 1); -by (eresolve_tac prems 1); -by (eresolve_tac prems 1); -by (eresolve_tac prems 1); -qed "IssumE2"; - - - - -(* ------------------------------------------------------------------------ *) -(* rewrites for Iwhen *) -(* ------------------------------------------------------------------------ *) - -Goalw [Iwhen_def] - "Iwhen f g (Isinl UU) = UU"; -by (rtac some_equality 1); -by (rtac conjI 1); -by (fast_tac HOL_cs 1); -by (rtac conjI 1); -by (strip_tac 1); -by (res_inst_tac [("P","a=UU")] notE 1); -by (fast_tac HOL_cs 1); -by (rtac inject_Isinl 1); -by (rtac sym 1); -by (fast_tac HOL_cs 1); -by (strip_tac 1); -by (res_inst_tac [("P","b=UU")] notE 1); -by (fast_tac HOL_cs 1); -by (rtac inject_Isinr 1); -by (rtac sym 1); -by (rtac (strict_IsinlIsinr RS subst) 1); -by (fast_tac HOL_cs 1); -by (fast_tac HOL_cs 1); -qed "Iwhen1"; - - -Goalw [Iwhen_def] - "x~=UU ==> Iwhen f g (Isinl x) = f$x"; -by (rtac some_equality 1); -by (fast_tac HOL_cs 2); -by (rtac conjI 1); -by (strip_tac 1); -by (res_inst_tac [("P","x=UU")] notE 1); -by (atac 1); -by (rtac inject_Isinl 1); -by (atac 1); -by (rtac conjI 1); -by (strip_tac 1); -by (rtac cfun_arg_cong 1); -by (rtac inject_Isinl 1); -by (fast_tac HOL_cs 1); -by (strip_tac 1); -by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1); -by (fast_tac HOL_cs 2); -by (rtac contrapos_nn 1); -by (etac noteq_IsinlIsinr 2); -by (fast_tac HOL_cs 1); -qed "Iwhen2"; - -Goalw [Iwhen_def] - "y~=UU ==> Iwhen f g (Isinr y) = g$y"; -by (rtac some_equality 1); -by (fast_tac HOL_cs 2); -by (rtac conjI 1); -by (strip_tac 1); -by (res_inst_tac [("P","y=UU")] notE 1); -by (atac 1); -by (rtac inject_Isinr 1); -by (rtac (strict_IsinlIsinr RS subst) 1); -by (atac 1); -by (rtac conjI 1); -by (strip_tac 1); -by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1); -by (fast_tac HOL_cs 2); -by (rtac contrapos_nn 1); -by (etac (sym RS noteq_IsinlIsinr) 2); -by (fast_tac HOL_cs 1); -by (strip_tac 1); -by (rtac cfun_arg_cong 1); -by (rtac inject_Isinr 1); -by (fast_tac HOL_cs 1); -qed "Iwhen3"; - -(* ------------------------------------------------------------------------ *) -(* instantiate the simplifier *) -(* ------------------------------------------------------------------------ *) - -val Ssum0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] addsimps - [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3]; - -Addsimps [strict_IsinlIsinr RS sym, Iwhen1, Iwhen2, Iwhen3]; +val Isinl_def = thm "Isinl_def"; +val Isinr_def = thm "Isinr_def"; +val Iwhen_def = thm "Iwhen_def"; +val SsumIl = thm "SsumIl"; +val SsumIr = thm "SsumIr"; +val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum"; +val strict_SinlSinr_Rep = thm "strict_SinlSinr_Rep"; +val strict_IsinlIsinr = thm "strict_IsinlIsinr"; +val noteq_SinlSinr_Rep = thm "noteq_SinlSinr_Rep"; +val noteq_IsinlIsinr = thm "noteq_IsinlIsinr"; +val inject_Sinl_Rep1 = thm "inject_Sinl_Rep1"; +val inject_Sinr_Rep1 = thm "inject_Sinr_Rep1"; +val inject_Sinl_Rep2 = thm "inject_Sinl_Rep2"; +val inject_Sinr_Rep2 = thm "inject_Sinr_Rep2"; +val inject_Sinl_Rep = thm "inject_Sinl_Rep"; +val inject_Sinr_Rep = thm "inject_Sinr_Rep"; +val inject_Isinl = thm "inject_Isinl"; +val inject_Isinr = thm "inject_Isinr"; +val inject_Isinl_rev = thm "inject_Isinl_rev"; +val inject_Isinr_rev = thm "inject_Isinr_rev"; +val Exh_Ssum = thm "Exh_Ssum"; +val IssumE = thm "IssumE"; +val IssumE2 = thm "IssumE2"; +val Iwhen1 = thm "Iwhen1"; +val Iwhen2 = thm "Iwhen2"; +val Iwhen3 = thm "Iwhen3"; diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum0.thy --- a/src/HOLCF/Ssum0.thy Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum0.thy Thu Mar 03 01:37:32 2005 +0100 @@ -1,25 +1,27 @@ (* Title: HOLCF/Ssum0.thy ID: $Id$ Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) Strict sum with typedef *) -Ssum0 = Cfun3 + +theory Ssum0 = Cfun3: constdefs - Sinl_Rep :: ['a,'a,'b,bool]=>bool + Sinl_Rep :: "['a,'a,'b,bool]=>bool" "Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))" - Sinr_Rep :: ['b,'a,'b,bool]=>bool + Sinr_Rep :: "['b,'a,'b,bool]=>bool" "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))" typedef (Ssum) ('a, 'b) "++" (infixr 10) = "{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}" +by auto syntax (xsymbols) - "++" :: [type, type] => type ("(_ \\/ _)" [21, 20] 20) + "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) syntax (HTML output) - "++" :: [type, type] => type ("(_ \\/ _)" [21, 20] 20) + "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) consts Isinl :: "'a => ('a ++ 'b)" @@ -27,12 +29,316 @@ Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c" defs (*defining the abstract constants*) - Isinl_def "Isinl(a) == Abs_Ssum(Sinl_Rep(a))" - Isinr_def "Isinr(b) == Abs_Ssum(Sinr_Rep(b))" + Isinl_def: "Isinl(a) == Abs_Ssum(Sinl_Rep(a))" + Isinr_def: "Isinr(b) == Abs_Ssum(Sinr_Rep(b))" - Iwhen_def "Iwhen(f)(g)(s) == @z. + Iwhen_def: "Iwhen(f)(g)(s) == @z. (s=Isinl(UU) --> z=UU) &(!a. a~=UU & s=Isinl(a) --> z=f$a) &(!b. b~=UU & s=Isinr(b) --> z=g$b)" +(* Title: HOLCF/Ssum0.ML + ID: $Id$ + Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Strict sum with typedef +*) + +(* ------------------------------------------------------------------------ *) +(* A non-emptyness result for Sssum *) +(* ------------------------------------------------------------------------ *) + +lemma SsumIl: "Sinl_Rep(a):Ssum" +apply (unfold Ssum_def) +apply blast +done + +lemma SsumIr: "Sinr_Rep(a):Ssum" +apply (unfold Ssum_def) +apply blast +done + +lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum" +apply (rule inj_on_inverseI) +apply (erule Abs_Ssum_inverse) +done + +(* ------------------------------------------------------------------------ *) +(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *) +(* ------------------------------------------------------------------------ *) + +lemma strict_SinlSinr_Rep: + "Sinl_Rep(UU) = Sinr_Rep(UU)" + +apply (unfold Sinr_Rep_def Sinl_Rep_def) +apply (rule ext) +apply (rule ext) +apply (rule ext) +apply fast +done + +lemma strict_IsinlIsinr: + "Isinl(UU) = Isinr(UU)" +apply (unfold Isinl_def Isinr_def) +apply (rule strict_SinlSinr_Rep [THEN arg_cong]) +done + + +(* ------------------------------------------------------------------------ *) +(* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) +(* ------------------------------------------------------------------------ *) + +lemma noteq_SinlSinr_Rep: + "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU" + +apply (unfold Sinl_Rep_def Sinr_Rep_def) +apply (blast dest!: fun_cong) +done + + +lemma noteq_IsinlIsinr: + "Isinl(a)=Isinr(b) ==> a=UU & b=UU" + +apply (unfold Isinl_def Isinr_def) +apply (rule noteq_SinlSinr_Rep) +apply (erule inj_on_Abs_Ssum [THEN inj_onD]) +apply (rule SsumIl) +apply (rule SsumIr) +done + + + +(* ------------------------------------------------------------------------ *) +(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) +(* ------------------------------------------------------------------------ *) + +lemma inject_Sinl_Rep1: "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU" +apply (unfold Sinl_Rep_def) +apply (blast dest!: fun_cong) +done + +lemma inject_Sinr_Rep1: "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU" +apply (unfold Sinr_Rep_def) +apply (blast dest!: fun_cong) +done + +lemma inject_Sinl_Rep2: +"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2" +apply (unfold Sinl_Rep_def) +apply (blast dest!: fun_cong) +done + +lemma inject_Sinr_Rep2: +"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2" +apply (unfold Sinr_Rep_def) +apply (blast dest!: fun_cong) +done + +lemma inject_Sinl_Rep: "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2" +apply (case_tac "a1=UU") +apply simp +apply (rule inject_Sinl_Rep1 [symmetric]) +apply (erule sym) +apply (case_tac "a2=UU") +apply simp +apply (drule inject_Sinl_Rep1) +apply simp +apply (erule inject_Sinl_Rep2) +apply assumption +apply assumption +done + +lemma inject_Sinr_Rep: "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2" +apply (case_tac "b1=UU") +apply simp +apply (rule inject_Sinr_Rep1 [symmetric]) +apply (erule sym) +apply (case_tac "b2=UU") +apply simp +apply (drule inject_Sinr_Rep1) +apply simp +apply (erule inject_Sinr_Rep2) +apply assumption +apply assumption +done + +lemma inject_Isinl: "Isinl(a1)=Isinl(a2)==> a1=a2" +apply (unfold Isinl_def) +apply (rule inject_Sinl_Rep) +apply (erule inj_on_Abs_Ssum [THEN inj_onD]) +apply (rule SsumIl) +apply (rule SsumIl) +done + +lemma inject_Isinr: "Isinr(b1)=Isinr(b2) ==> b1=b2" +apply (unfold Isinr_def) +apply (rule inject_Sinr_Rep) +apply (erule inj_on_Abs_Ssum [THEN inj_onD]) +apply (rule SsumIr) +apply (rule SsumIr) +done + +declare inject_Isinl [dest!] inject_Isinr [dest!] + +lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)" +apply blast +done + +lemma inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)" +apply blast +done + +(* ------------------------------------------------------------------------ *) +(* Exhaustion of the strict sum ++ *) +(* choice of the bottom representation is arbitrary *) +(* ------------------------------------------------------------------------ *) + +lemma Exh_Ssum: + "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)" +apply (unfold Isinl_def Isinr_def) +apply (rule Rep_Ssum[unfolded Ssum_def, THEN CollectE]) +apply (erule disjE) +apply (erule exE) +apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))") +apply (erule disjI1) +apply (rule disjI2) +apply (rule disjI1) +apply (rule exI) +apply (rule conjI) +apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) +apply (erule arg_cong) +apply (rule_tac Q = "Sinl_Rep (a) =Sinl_Rep (UU) " in contrapos_nn) +apply (erule_tac [2] arg_cong) +apply (erule contrapos_nn) +apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) +apply (rule trans) +apply (erule arg_cong) +apply (erule arg_cong) +apply (erule exE) +apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))") +apply (erule disjI1) +apply (rule disjI2) +apply (rule disjI2) +apply (rule exI) +apply (rule conjI) +apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) +apply (erule arg_cong) +apply (rule_tac Q = "Sinr_Rep (b) =Sinl_Rep (UU) " in contrapos_nn) +prefer 2 apply simp +apply (rule strict_SinlSinr_Rep [symmetric]) +apply (erule contrapos_nn) +apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) +apply (rule trans) +apply (erule arg_cong) +apply (erule arg_cong) +done + +(* ------------------------------------------------------------------------ *) +(* elimination rules for the strict sum ++ *) +(* ------------------------------------------------------------------------ *) + +lemma IssumE: + "[|p=Isinl(UU) ==> Q ; + !!x.[|p=Isinl(x); x~=UU |] ==> Q; + !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q" +apply (rule Exh_Ssum [THEN disjE]) +apply auto +done + +lemma IssumE2: +"[| !!x. [| p = Isinl(x) |] ==> Q; !!y. [| p = Isinr(y) |] ==> Q |] ==>Q" +apply (rule IssumE) +apply auto +done + + + + +(* ------------------------------------------------------------------------ *) +(* rewrites for Iwhen *) +(* ------------------------------------------------------------------------ *) + +lemma Iwhen1: + "Iwhen f g (Isinl UU) = UU" +apply (unfold Iwhen_def) +apply (rule some_equality) +apply (rule conjI) +apply fast +apply (rule conjI) +apply (intro strip) +apply (rule_tac P = "a=UU" in notE) +apply fast +apply (rule inject_Isinl) +apply (rule sym) +apply fast +apply (intro strip) +apply (rule_tac P = "b=UU" in notE) +apply fast +apply (rule inject_Isinr) +apply (rule sym) +apply (rule strict_IsinlIsinr [THEN subst]) +apply fast +apply fast +done + + +lemma Iwhen2: + "x~=UU ==> Iwhen f g (Isinl x) = f$x" + +apply (unfold Iwhen_def) +apply (rule some_equality) +prefer 2 apply fast +apply (rule conjI) +apply (intro strip) +apply (rule_tac P = "x=UU" in notE) +apply assumption +apply (rule inject_Isinl) +apply assumption +apply (rule conjI) +apply (intro strip) +apply (rule cfun_arg_cong) +apply (rule inject_Isinl) +apply fast +apply (intro strip) +apply (rule_tac P = "Isinl (x) = Isinr (b) " in notE) +prefer 2 apply fast +apply (rule contrapos_nn) +apply (erule_tac [2] noteq_IsinlIsinr) +apply fast +done + +lemma Iwhen3: + "y~=UU ==> Iwhen f g (Isinr y) = g$y" +apply (unfold Iwhen_def) +apply (rule some_equality) +prefer 2 apply fast +apply (rule conjI) +apply (intro strip) +apply (rule_tac P = "y=UU" in notE) +apply assumption +apply (rule inject_Isinr) +apply (rule strict_IsinlIsinr [THEN subst]) +apply assumption +apply (rule conjI) +apply (intro strip) +apply (rule_tac P = "Isinr (y) = Isinl (a) " in notE) +prefer 2 apply fast +apply (rule contrapos_nn) +apply (erule_tac [2] sym [THEN noteq_IsinlIsinr]) +apply fast +apply (intro strip) +apply (rule cfun_arg_cong) +apply (rule inject_Isinr) +apply fast +done + +(* ------------------------------------------------------------------------ *) +(* instantiate the simplifier *) +(* ------------------------------------------------------------------------ *) + +lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3 + +declare Ssum0_ss [simp] + end diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum1.ML --- a/src/HOLCF/Ssum1.ML Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum1.ML Thu Mar 03 01:37:32 2005 +0100 @@ -1,311 +1,15 @@ -(* Title: HOLCF/Ssum1.ML - ID: $Id$ - Author: Franz Regensburger -Partial ordering for the strict sum ++ -*) - -fun eq_left s1 s2 = - ( - (res_inst_tac [("s",s1),("t",s2)] (inject_Isinl RS subst) 1) - THEN (rtac trans 1) - THEN (atac 2) - THEN (etac sym 1)); - -fun eq_right s1 s2 = - ( - (res_inst_tac [("s",s1),("t",s2)] (inject_Isinr RS subst) 1) - THEN (rtac trans 1) - THEN (atac 2) - THEN (etac sym 1)); - -fun UU_left s1 = - ( - (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct1 RS ssubst)1) - THEN (rtac trans 1) - THEN (atac 2) - THEN (etac sym 1)); - -fun UU_right s1 = - ( - (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1) - THEN (rtac trans 1) - THEN (atac 2) - THEN (etac sym 1)); - -Goalw [less_ssum_def] -"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"; -by (rtac some_equality 1); -by (dtac conjunct1 2); -by (dtac spec 2); -by (dtac spec 2); -by (etac mp 2); -by (fast_tac HOL_cs 2); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (eq_left "x" "u"); -by (eq_left "y" "xa"); -by (rtac refl 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_left "x"); -by (UU_right "v"); -by (Simp_tac 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (eq_left "x" "u"); -by (UU_left "y"); -by (rtac iffI 1); -by (etac UU_I 1); -by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1); -by (atac 1); -by (rtac refl_less 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_left "x"); -by (UU_right "v"); -by (Simp_tac 1); -qed "less_ssum1a"; - - -Goalw [less_ssum_def] -"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"; -by (rtac some_equality 1); -by (dtac conjunct2 2); -by (dtac conjunct1 2); -by (dtac spec 2); -by (dtac spec 2); -by (etac mp 2); -by (fast_tac HOL_cs 2); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_right "x"); -by (UU_left "u"); -by (Simp_tac 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (eq_right "x" "v"); -by (eq_right "y" "ya"); -by (rtac refl 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_right "x"); -by (UU_left "u"); -by (Simp_tac 1); -by (strip_tac 1); -by (etac conjE 1); -by (eq_right "x" "v"); -by (UU_right "y"); -by (rtac iffI 1); -by (etac UU_I 1); -by (res_inst_tac [("s","UU::'b"),("t","x")] subst 1); -by (etac sym 1); -by (rtac refl_less 1); -qed "less_ssum1b"; - - -Goalw [less_ssum_def] -"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"; -by (rtac some_equality 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (eq_left "x" "u"); -by (UU_left "xa"); -by (rtac iffI 1); -by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1); -by (atac 1); -by (rtac refl_less 1); -by (etac UU_I 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_left "x"); -by (UU_right "v"); -by (Simp_tac 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (eq_left "x" "u"); -by (rtac refl 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_left "x"); -by (UU_right "v"); -by (Simp_tac 1); -by (dtac conjunct2 1); -by (dtac conjunct2 1); -by (dtac conjunct1 1); -by (dtac spec 1); -by (dtac spec 1); -by (etac mp 1); -by (fast_tac HOL_cs 1); -qed "less_ssum1c"; - +(* legacy ML bindings *) -Goalw [less_ssum_def] -"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"; -by (rtac some_equality 1); -by (dtac conjunct2 2); -by (dtac conjunct2 2); -by (dtac conjunct2 2); -by (dtac spec 2); -by (dtac spec 2); -by (etac mp 2); -by (fast_tac HOL_cs 2); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_right "x"); -by (UU_left "u"); -by (Simp_tac 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_right "ya"); -by (eq_right "x" "v"); -by (rtac iffI 1); -by (etac UU_I 2); -by (res_inst_tac [("s","UU"),("t","x")] subst 1); -by (etac sym 1); -by (rtac refl_less 1); -by (rtac conjI 1); -by (strip_tac 1); -by (etac conjE 1); -by (UU_right "x"); -by (UU_left "u"); -by (Simp_tac 1); -by (strip_tac 1); -by (etac conjE 1); -by (eq_right "x" "v"); -by (rtac refl 1); -qed "less_ssum1d"; - - -(* ------------------------------------------------------------------------ *) -(* optimize lemmas about less_ssum *) -(* ------------------------------------------------------------------------ *) - -Goal "(Isinl x) << (Isinl y) = (x << y)"; -by (rtac less_ssum1a 1); -by (rtac refl 1); -by (rtac refl 1); -qed "less_ssum2a"; - -Goal "(Isinr x) << (Isinr y) = (x << y)"; -by (rtac less_ssum1b 1); -by (rtac refl 1); -by (rtac refl 1); -qed "less_ssum2b"; - -Goal "(Isinl x) << (Isinr y) = (x = UU)"; -by (rtac less_ssum1c 1); -by (rtac refl 1); -by (rtac refl 1); -qed "less_ssum2c"; - -Goal "(Isinr x) << (Isinl y) = (x = UU)"; -by (rtac less_ssum1d 1); -by (rtac refl 1); -by (rtac refl 1); -qed "less_ssum2d"; - - -(* ------------------------------------------------------------------------ *) -(* less_ssum is a partial order on ++ *) -(* ------------------------------------------------------------------------ *) - -Goal "(p::'a++'b) << p"; -by (res_inst_tac [("p","p")] IssumE2 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum2a RS iffD2) 1); -by (rtac refl_less 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum2b RS iffD2) 1); -by (rtac refl_less 1); -qed "refl_less_ssum"; - -Goal "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"; -by (res_inst_tac [("p","p1")] IssumE2 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("p","p2")] IssumE2 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("f","Isinl")] arg_cong 1); -by (rtac antisym_less 1); -by (etac (less_ssum2a RS iffD1) 1); -by (etac (less_ssum2a RS iffD1) 1); -by (hyp_subst_tac 1); -by (etac (less_ssum2d RS iffD1 RS ssubst) 1); -by (etac (less_ssum2c RS iffD1 RS ssubst) 1); -by (rtac strict_IsinlIsinr 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("p","p2")] IssumE2 1); -by (hyp_subst_tac 1); -by (etac (less_ssum2c RS iffD1 RS ssubst) 1); -by (etac (less_ssum2d RS iffD1 RS ssubst) 1); -by (rtac (strict_IsinlIsinr RS sym) 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("f","Isinr")] arg_cong 1); -by (rtac antisym_less 1); -by (etac (less_ssum2b RS iffD1) 1); -by (etac (less_ssum2b RS iffD1) 1); -qed "antisym_less_ssum"; - -Goal "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"; -by (res_inst_tac [("p","p1")] IssumE2 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("p","p3")] IssumE2 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum2a RS iffD2) 1); -by (res_inst_tac [("p","p2")] IssumE2 1); -by (hyp_subst_tac 1); -by (rtac trans_less 1); -by (etac (less_ssum2a RS iffD1) 1); -by (etac (less_ssum2a RS iffD1) 1); -by (hyp_subst_tac 1); -by (etac (less_ssum2c RS iffD1 RS ssubst) 1); -by (rtac minimal 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum2c RS iffD2) 1); -by (res_inst_tac [("p","p2")] IssumE2 1); -by (hyp_subst_tac 1); -by (rtac UU_I 1); -by (rtac trans_less 1); -by (etac (less_ssum2a RS iffD1) 1); -by (rtac (antisym_less_inverse RS conjunct1) 1); -by (etac (less_ssum2c RS iffD1) 1); -by (hyp_subst_tac 1); -by (etac (less_ssum2c RS iffD1) 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("p","p3")] IssumE2 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum2d RS iffD2) 1); -by (res_inst_tac [("p","p2")] IssumE2 1); -by (hyp_subst_tac 1); -by (etac (less_ssum2d RS iffD1) 1); -by (hyp_subst_tac 1); -by (rtac UU_I 1); -by (rtac trans_less 1); -by (etac (less_ssum2b RS iffD1) 1); -by (rtac (antisym_less_inverse RS conjunct1) 1); -by (etac (less_ssum2d RS iffD1) 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum2b RS iffD2) 1); -by (res_inst_tac [("p","p2")] IssumE2 1); -by (hyp_subst_tac 1); -by (etac (less_ssum2d RS iffD1 RS ssubst) 1); -by (rtac minimal 1); -by (hyp_subst_tac 1); -by (rtac trans_less 1); -by (etac (less_ssum2b RS iffD1) 1); -by (etac (less_ssum2b RS iffD1) 1); -qed "trans_less_ssum"; - - - +val less_ssum_def = thm "less_ssum_def"; +val less_ssum1a = thm "less_ssum1a"; +val less_ssum1b = thm "less_ssum1b"; +val less_ssum1c = thm "less_ssum1c"; +val less_ssum1d = thm "less_ssum1d"; +val less_ssum2a = thm "less_ssum2a"; +val less_ssum2b = thm "less_ssum2b"; +val less_ssum2c = thm "less_ssum2c"; +val less_ssum2d = thm "less_ssum2d"; +val refl_less_ssum = thm "refl_less_ssum"; +val antisym_less_ssum = thm "antisym_less_ssum"; +val trans_less_ssum = thm "trans_less_ssum"; diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum1.thy --- a/src/HOLCF/Ssum1.thy Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum1.thy Thu Mar 03 01:37:32 2005 +0100 @@ -1,21 +1,314 @@ (* Title: HOLCF/Ssum1.thy ID: $Id$ Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) Partial ordering for the strict sum ++ *) -Ssum1 = Ssum0 + +theory Ssum1 = Ssum0: -instance "++"::(pcpo,pcpo)sq_ord +instance "++"::(pcpo,pcpo)sq_ord .. -defs - less_ssum_def "(op <<) == (%s1 s2.@z. +defs (overloaded) + less_ssum_def: "(op <<) == (%s1 s2.@z. (! u x. s1=Isinl u & s2=Isinl x --> z = u << x) &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y) &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU)) &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))" +(* Title: HOLCF/Ssum1.ML + ID: $Id$ + Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Partial ordering for the strict sum ++ +*) + +lemma less_ssum1a: +"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)" +apply (unfold less_ssum_def) +apply (rule some_equality) +apply (drule_tac [2] conjunct1) +apply (drule_tac [2] spec) +apply (drule_tac [2] spec) +apply (erule_tac [2] mp) +prefer 2 apply fast +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule inject_Isinl) +apply (drule inject_Isinl) +apply simp +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr[OF sym]) +apply simp +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule inject_Isinl) +apply (drule noteq_IsinlIsinr[OF sym]) +apply simp +apply (rule eq_UU_iff[symmetric]) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr[OF sym]) +apply simp +done + + +lemma less_ssum1b: +"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)" + +apply (unfold less_ssum_def) +apply (rule some_equality) +apply (drule_tac [2] conjunct2) +apply (drule_tac [2] conjunct1) +apply (drule_tac [2] spec) +apply (drule_tac [2] spec) +apply (erule_tac [2] mp) +prefer 2 apply fast +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr) +apply (drule noteq_IsinlIsinr) +apply simp +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule inject_Isinr) +apply (drule inject_Isinr) +apply simp +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr) +apply (drule inject_Isinr) +apply simp +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule inject_Isinr) +apply (drule noteq_IsinlIsinr) +apply simp +apply (rule eq_UU_iff[symmetric]) +done + + +lemma less_ssum1c: +"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)" + +apply (unfold less_ssum_def) +apply (rule some_equality) +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule inject_Isinl) +apply (drule noteq_IsinlIsinr) +apply simp +apply (rule eq_UU_iff) +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr[OF sym]) +apply (drule inject_Isinr) +apply simp +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule inject_Isinl) +apply (drule inject_Isinr) +apply simp +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr[OF sym]) +apply (drule noteq_IsinlIsinr) +apply simp +apply (drule conjunct2) +apply (drule conjunct2) +apply (drule conjunct1) +apply (drule spec) +apply (drule spec) +apply (erule mp) +apply fast +done + + +lemma less_ssum1d: +"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)" + +apply (unfold less_ssum_def) +apply (rule some_equality) +apply (drule_tac [2] conjunct2) +apply (drule_tac [2] conjunct2) +apply (drule_tac [2] conjunct2) +apply (drule_tac [2] spec) +apply (drule_tac [2] spec) +apply (erule_tac [2] mp) +prefer 2 apply fast +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr) +apply (drule inject_Isinl) +apply simp +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr[OF sym]) +apply (drule inject_Isinr) +apply simp +apply (rule eq_UU_iff) +apply (rule conjI) +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule noteq_IsinlIsinr) +apply (drule noteq_IsinlIsinr[OF sym]) +apply simp +apply (intro strip) +apply (erule conjE) +apply simp +apply (drule inject_Isinr) +apply simp +done + + +(* ------------------------------------------------------------------------ *) +(* optimize lemmas about less_ssum *) +(* ------------------------------------------------------------------------ *) + +lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)" +apply (rule less_ssum1a) +apply (rule refl) +apply (rule refl) +done + +lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)" +apply (rule less_ssum1b) +apply (rule refl) +apply (rule refl) +done + +lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)" +apply (rule less_ssum1c) +apply (rule refl) +apply (rule refl) +done + +lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)" +apply (rule less_ssum1d) +apply (rule refl) +apply (rule refl) +done + + +(* ------------------------------------------------------------------------ *) +(* less_ssum is a partial order on ++ *) +(* ------------------------------------------------------------------------ *) + +lemma refl_less_ssum: "(p::'a++'b) << p" +apply (rule_tac p = "p" in IssumE2) +apply (erule ssubst) +apply (rule less_ssum2a [THEN iffD2]) +apply (rule refl_less) +apply (erule ssubst) +apply (rule less_ssum2b [THEN iffD2]) +apply (rule refl_less) +done + +lemma antisym_less_ssum: "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2" +apply (rule_tac p = "p1" in IssumE2) +apply simp +apply (rule_tac p = "p2" in IssumE2) +apply simp +apply (rule_tac f = "Isinl" in arg_cong) +apply (rule antisym_less) +apply (erule less_ssum2a [THEN iffD1]) +apply (erule less_ssum2a [THEN iffD1]) +apply simp +apply (erule less_ssum2d [THEN iffD1, THEN ssubst]) +apply (erule less_ssum2c [THEN iffD1, THEN ssubst]) +apply (rule strict_IsinlIsinr) +apply simp +apply (rule_tac p = "p2" in IssumE2) +apply simp +apply (erule less_ssum2c [THEN iffD1, THEN ssubst]) +apply (erule less_ssum2d [THEN iffD1, THEN ssubst]) +apply (rule strict_IsinlIsinr [symmetric]) +apply simp +apply (rule_tac f = "Isinr" in arg_cong) +apply (rule antisym_less) +apply (erule less_ssum2b [THEN iffD1]) +apply (erule less_ssum2b [THEN iffD1]) +done + +lemma trans_less_ssum: "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3" +apply (rule_tac p = "p1" in IssumE2) +apply simp +apply (rule_tac p = "p3" in IssumE2) +apply simp +apply (rule less_ssum2a [THEN iffD2]) +apply (rule_tac p = "p2" in IssumE2) +apply simp +apply (rule trans_less) +apply (erule less_ssum2a [THEN iffD1]) +apply (erule less_ssum2a [THEN iffD1]) +apply simp +apply (erule less_ssum2c [THEN iffD1, THEN ssubst]) +apply (rule minimal) +apply simp +apply (rule less_ssum2c [THEN iffD2]) +apply (rule_tac p = "p2" in IssumE2) +apply simp +apply (rule UU_I) +apply (rule trans_less) +apply (erule less_ssum2a [THEN iffD1]) +apply (rule antisym_less_inverse [THEN conjunct1]) +apply (erule less_ssum2c [THEN iffD1]) +apply simp +apply (erule less_ssum2c [THEN iffD1]) +apply simp +apply (rule_tac p = "p3" in IssumE2) +apply simp +apply (rule less_ssum2d [THEN iffD2]) +apply (rule_tac p = "p2" in IssumE2) +apply simp +apply (erule less_ssum2d [THEN iffD1]) +apply simp +apply (rule UU_I) +apply (rule trans_less) +apply (erule less_ssum2b [THEN iffD1]) +apply (rule antisym_less_inverse [THEN conjunct1]) +apply (erule less_ssum2d [THEN iffD1]) +apply simp +apply (rule less_ssum2b [THEN iffD2]) +apply (rule_tac p = "p2" in IssumE2) +apply simp +apply (erule less_ssum2d [THEN iffD1, THEN ssubst]) +apply (rule minimal) +apply simp +apply (rule trans_less) +apply (erule less_ssum2b [THEN iffD1]) +apply (erule less_ssum2b [THEN iffD1]) +done + end diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum2.ML --- a/src/HOLCF/Ssum2.ML Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum2.ML Thu Mar 03 01:37:32 2005 +0100 @@ -1,352 +1,29 @@ -(* Title: HOLCF/Ssum2.ML - ID: $Id$ - Author: Franz Regensburger -Class Instance ++::(pcpo,pcpo)po -*) - -(* for compatibility with old HOLCF-Version *) -Goal "(op <<)=(%s1 s2.@z.\ -\ (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)\ -\ &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)\ -\ &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))\ -\ &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"; -by (fold_goals_tac [less_ssum_def]); -by (rtac refl 1); -qed "inst_ssum_po"; - -(* ------------------------------------------------------------------------ *) -(* access to less_ssum in class po *) -(* ------------------------------------------------------------------------ *) - -Goal "Isinl x << Isinl y = x << y"; -by (simp_tac (simpset() addsimps [less_ssum2a]) 1); -qed "less_ssum3a"; - -Goal "Isinr x << Isinr y = x << y"; -by (simp_tac (simpset() addsimps [less_ssum2b]) 1); -qed "less_ssum3b"; - -Goal "Isinl x << Isinr y = (x = UU)"; -by (simp_tac (simpset() addsimps [less_ssum2c]) 1); -qed "less_ssum3c"; - -Goal "Isinr x << Isinl y = (x = UU)"; -by (simp_tac (simpset() addsimps [less_ssum2d]) 1); -qed "less_ssum3d"; - -(* ------------------------------------------------------------------------ *) -(* type ssum ++ is pointed *) -(* ------------------------------------------------------------------------ *) - -Goal "Isinl UU << s"; -by (res_inst_tac [("p","s")] IssumE2 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum3a RS iffD2) 1); -by (rtac minimal 1); -by (hyp_subst_tac 1); -by (stac strict_IsinlIsinr 1); -by (rtac (less_ssum3b RS iffD2) 1); -by (rtac minimal 1); -qed "minimal_ssum"; - -bind_thm ("UU_ssum_def",minimal_ssum RS minimal2UU RS sym); - -Goal "? x::'a++'b.!y. x< (? i.! x. Y(i)~=Isinl(x))"; -by (fast_tac HOL_cs 1); -qed "ssum_lemma1"; - -Goal "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] \ -\ ==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)"; -by (etac exE 1); -by (res_inst_tac [("p","Y(i)")] IssumE 1); -by (dtac spec 1); -by (contr_tac 1); -by (dtac spec 1); -by (contr_tac 1); -by (fast_tac HOL_cs 1); -qed "ssum_lemma2"; - +(* legacy ML bindings *) -Goal "[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] \ -\ ==> (!i.? y. Y(i)=Isinr(y))"; -by (etac exE 1); -by (etac exE 1); -by (rtac allI 1); -by (res_inst_tac [("p","Y(ia)")] IssumE 1); -by (rtac exI 1); -by (rtac trans 1); -by (rtac strict_IsinlIsinr 2); -by (atac 1); -by (etac exI 2); -by (etac conjE 1); -by (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1); -by (hyp_subst_tac 2); -by (etac exI 2); -by (eres_inst_tac [("P","x=UU")] notE 1); -by (rtac (less_ssum3d RS iffD1) 1); -by (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1); -by (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1); -by (etac (chain_mono) 1); -by (atac 1); -by (eres_inst_tac [("P","xa=UU")] notE 1); -by (rtac (less_ssum3c RS iffD1) 1); -by (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1); -by (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1); -by (etac (chain_mono) 1); -by (atac 1); -qed "ssum_lemma3"; - -Goal "chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"; -by (rtac case_split_thm 1); -by (etac disjI1 1); -by (rtac disjI2 1); -by (etac ssum_lemma3 1); -by (rtac ssum_lemma2 1); -by (etac ssum_lemma1 1); -qed "ssum_lemma4"; - - -(* ------------------------------------------------------------------------ *) -(* restricted surjectivity of Isinl *) -(* ------------------------------------------------------------------------ *) - -Goal "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"; -by (hyp_subst_tac 1); -by (case_tac "x=UU" 1); -by (asm_simp_tac Ssum0_ss 1); -by (asm_simp_tac Ssum0_ss 1); -qed "ssum_lemma5"; - -(* ------------------------------------------------------------------------ *) -(* restricted surjectivity of Isinr *) -(* ------------------------------------------------------------------------ *) - -Goal "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"; -by (hyp_subst_tac 1); -by (case_tac "x=UU" 1); -by (asm_simp_tac Ssum0_ss 1); -by (asm_simp_tac Ssum0_ss 1); -qed "ssum_lemma6"; - -(* ------------------------------------------------------------------------ *) -(* technical lemmas *) -(* ------------------------------------------------------------------------ *) - -Goal "[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU"; -by (res_inst_tac [("p","z")] IssumE 1); -by (hyp_subst_tac 1); -by (etac notE 1); -by (rtac antisym_less 1); -by (etac (less_ssum3a RS iffD1) 1); -by (rtac minimal 1); -by (fast_tac HOL_cs 1); -by (hyp_subst_tac 1); -by (rtac notE 1); -by (etac (less_ssum3c RS iffD1) 2); -by (atac 1); -qed "ssum_lemma7"; - -Goal "[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU"; -by (res_inst_tac [("p","z")] IssumE 1); -by (hyp_subst_tac 1); -by (etac notE 1); -by (etac (less_ssum3d RS iffD1) 1); -by (hyp_subst_tac 1); -by (rtac notE 1); -by (etac (less_ssum3d RS iffD1) 2); -by (atac 1); -by (fast_tac HOL_cs 1); -qed "ssum_lemma8"; - -(* ------------------------------------------------------------------------ *) -(* the type 'a ++ 'b is a cpo in three steps *) -(* ------------------------------------------------------------------------ *) - -Goal "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\ -\ range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"; -by (rtac is_lubI 1); -by (rtac ub_rangeI 1); -by (etac allE 1); -by (etac exE 1); -by (res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1); -by (atac 1); -by (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1); -by (rtac is_ub_thelub 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (strip_tac 1); -by (res_inst_tac [("p","u")] IssumE2 1); -by (res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1); -by (atac 1); -by (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1); -by (rtac is_lub_thelub 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (etac (monofun_Iwhen3 RS ub2ub_monofun) 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum3c RS iffD2) 1); -by (rtac chain_UU_I_inverse 1); -by (rtac allI 1); -by (res_inst_tac [("p","Y(i)")] IssumE 1); -by (asm_simp_tac Ssum0_ss 1); -by (asm_simp_tac Ssum0_ss 2); -by (etac notE 1); -by (rtac (less_ssum3c RS iffD1) 1); -by (res_inst_tac [("t","Isinl(x)")] subst 1); -by (atac 1); -by (etac (ub_rangeD) 1); -qed "lub_ssum1a"; - - -Goal "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\ -\ range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"; -by (rtac is_lubI 1); -by (rtac ub_rangeI 1); -by (etac allE 1); -by (etac exE 1); -by (res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1); -by (atac 1); -by (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1); -by (rtac is_ub_thelub 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (strip_tac 1); -by (res_inst_tac [("p","u")] IssumE2 1); -by (hyp_subst_tac 1); -by (rtac (less_ssum3d RS iffD2) 1); -by (rtac chain_UU_I_inverse 1); -by (rtac allI 1); -by (res_inst_tac [("p","Y(i)")] IssumE 1); -by (asm_simp_tac Ssum0_ss 1); -by (asm_simp_tac Ssum0_ss 1); -by (etac notE 1); -by (rtac (less_ssum3d RS iffD1) 1); -by (res_inst_tac [("t","Isinr(y)")] subst 1); -by (atac 1); -by (etac (ub_rangeD) 1); -by (res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1); -by (atac 1); -by (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1); -by (rtac is_lub_thelub 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (etac (monofun_Iwhen3 RS ub2ub_monofun) 1); -qed "lub_ssum1b"; - - -bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI); -(* -[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==> - lub (range ?Y1) = Isinl - (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i)))) -*) - -bind_thm ("thelub_ssum1b", lub_ssum1b RS thelubI); -(* -[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==> - lub (range ?Y1) = Isinr - (lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i)))) -*) - -Goal "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"; -by (rtac (ssum_lemma4 RS disjE) 1); -by (atac 1); -by (rtac exI 1); -by (etac lub_ssum1a 1); -by (atac 1); -by (rtac exI 1); -by (etac lub_ssum1b 1); -by (atac 1); -qed "cpo_ssum"; - +val inst_ssum_po = thm "inst_ssum_po"; +val less_ssum3a = thm "less_ssum3a"; +val less_ssum3b = thm "less_ssum3b"; +val less_ssum3c = thm "less_ssum3c"; +val less_ssum3d = thm "less_ssum3d"; +val minimal_ssum = thm "minimal_ssum"; +val UU_ssum_def = thm "UU_ssum_def"; +val least_ssum = thm "least_ssum"; +val monofun_Isinl = thm "monofun_Isinl"; +val monofun_Isinr = thm "monofun_Isinr"; +val monofun_Iwhen1 = thm "monofun_Iwhen1"; +val monofun_Iwhen2 = thm "monofun_Iwhen2"; +val monofun_Iwhen3 = thm "monofun_Iwhen3"; +val ssum_lemma1 = thm "ssum_lemma1"; +val ssum_lemma2 = thm "ssum_lemma2"; +val ssum_lemma3 = thm "ssum_lemma3"; +val ssum_lemma4 = thm "ssum_lemma4"; +val ssum_lemma5 = thm "ssum_lemma5"; +val ssum_lemma6 = thm "ssum_lemma6"; +val ssum_lemma7 = thm "ssum_lemma7"; +val ssum_lemma8 = thm "ssum_lemma8"; +val lub_ssum1a = thm "lub_ssum1a"; +val lub_ssum1b = thm "lub_ssum1b"; +val thelub_ssum1a = thm "thelub_ssum1a"; +val thelub_ssum1b = thm "thelub_ssum1b"; +val cpo_ssum = thm "cpo_ssum"; diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum2.thy --- a/src/HOLCF/Ssum2.thy Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum2.thy Thu Mar 03 01:37:32 2005 +0100 @@ -1,13 +1,366 @@ (* Title: HOLCF/ssum2.thy ID: $Id$ Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Class Instance ++::(pcpo,pcpo)po +*) + +theory Ssum2 = Ssum1: + +instance "++"::(pcpo,pcpo)po +apply (intro_classes) +apply (rule refl_less_ssum) +apply (rule antisym_less_ssum, assumption+) +apply (rule trans_less_ssum, assumption+) +done + +(* Title: HOLCF/Ssum2.ML + ID: $Id$ + Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) Class Instance ++::(pcpo,pcpo)po *) -Ssum2 = Ssum1 + +(* for compatibility with old HOLCF-Version *) +lemma inst_ssum_po: "(op <<)=(%s1 s2.@z. + (! u x. s1=Isinl u & s2=Isinl x --> z = u << x) + &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y) + &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU)) + &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))" +apply (fold less_ssum_def) +apply (rule refl) +done + +(* ------------------------------------------------------------------------ *) +(* access to less_ssum in class po *) +(* ------------------------------------------------------------------------ *) + +lemma less_ssum3a: "Isinl x << Isinl y = x << y" +apply (simp (no_asm) add: less_ssum2a) +done + +lemma less_ssum3b: "Isinr x << Isinr y = x << y" +apply (simp (no_asm) add: less_ssum2b) +done + +lemma less_ssum3c: "Isinl x << Isinr y = (x = UU)" +apply (simp (no_asm) add: less_ssum2c) +done + +lemma less_ssum3d: "Isinr x << Isinl y = (x = UU)" +apply (simp (no_asm) add: less_ssum2d) +done + +(* ------------------------------------------------------------------------ *) +(* type ssum ++ is pointed *) +(* ------------------------------------------------------------------------ *) + +lemma minimal_ssum: "Isinl UU << s" +apply (rule_tac p = "s" in IssumE2) +apply simp +apply (rule less_ssum3a [THEN iffD2]) +apply (rule minimal) +apply simp +apply (subst strict_IsinlIsinr) +apply (rule less_ssum3b [THEN iffD2]) +apply (rule minimal) +done + +lemmas UU_ssum_def = minimal_ssum [THEN minimal2UU, symmetric, standard] + +lemma least_ssum: "? x::'a++'b.!y. x< (? i.! x. Y(i)~=Isinl(x))" +apply fast +done + +lemma ssum_lemma2: "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] + ==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)" +apply (erule exE) +apply (rule_tac p = "Y (i) " in IssumE) +apply (drule spec) +apply (erule notE, assumption) +apply (drule spec) +apply (erule notE, assumption) +apply fast +done + -instance "++"::(pcpo,pcpo)po (refl_less_ssum,antisym_less_ssum,trans_less_ssum) +lemma ssum_lemma3: "[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] + ==> (!i.? y. Y(i)=Isinr(y))" +apply (erule exE) +apply (erule exE) +apply (rule allI) +apply (rule_tac p = "Y (ia) " in IssumE) +apply (rule exI) +apply (rule trans) +apply (rule_tac [2] strict_IsinlIsinr) +apply assumption +apply (erule_tac [2] exI) +apply (erule conjE) +apply (rule_tac m = "i" and n = "ia" in nat_less_cases) +prefer 2 apply simp +apply (rule exI, rule refl) +apply (erule_tac P = "x=UU" in notE) +apply (rule less_ssum3d [THEN iffD1]) +apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst) +apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst) +apply (erule chain_mono) +apply assumption +apply (erule_tac P = "xa=UU" in notE) +apply (rule less_ssum3c [THEN iffD1]) +apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst) +apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst) +apply (erule chain_mono) +apply assumption +done + +lemma ssum_lemma4: "chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))" +apply (rule case_split_thm) +apply (erule disjI1) +apply (rule disjI2) +apply (erule ssum_lemma3) +apply (rule ssum_lemma2) +apply (erule ssum_lemma1) +done + + +(* ------------------------------------------------------------------------ *) +(* restricted surjectivity of Isinl *) +(* ------------------------------------------------------------------------ *) + +lemma ssum_lemma5: "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z" +apply simp +apply (case_tac "x=UU") +apply simp +apply simp +done + +(* ------------------------------------------------------------------------ *) +(* restricted surjectivity of Isinr *) +(* ------------------------------------------------------------------------ *) + +lemma ssum_lemma6: "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z" +apply simp +apply (case_tac "x=UU") +apply simp +apply simp +done + +(* ------------------------------------------------------------------------ *) +(* technical lemmas *) +(* ------------------------------------------------------------------------ *) + +lemma ssum_lemma7: "[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU" +apply (rule_tac p = "z" in IssumE) +apply simp +apply (erule notE) +apply (rule antisym_less) +apply (erule less_ssum3a [THEN iffD1]) +apply (rule minimal) +apply fast +apply simp +apply (rule notE) +apply (erule_tac [2] less_ssum3c [THEN iffD1]) +apply assumption +done + +lemma ssum_lemma8: "[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU" +apply (rule_tac p = "z" in IssumE) +apply simp +apply (erule notE) +apply (erule less_ssum3d [THEN iffD1]) +apply simp +apply (rule notE) +apply (erule_tac [2] less_ssum3d [THEN iffD1]) +apply assumption +apply fast +done + +(* ------------------------------------------------------------------------ *) +(* the type 'a ++ 'b is a cpo in three steps *) +(* ------------------------------------------------------------------------ *) + +lemma lub_ssum1a: "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==> + range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))" +apply (rule is_lubI) +apply (rule ub_rangeI) +apply (erule allE) +apply (erule exE) +apply (rule_tac t = "Y (i) " in ssum_lemma5 [THEN subst]) +apply assumption +apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp]) +apply (rule is_ub_thelub) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (rule_tac p = "u" in IssumE2) +apply (rule_tac t = "u" in ssum_lemma5 [THEN subst]) +apply assumption +apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp]) +apply (rule is_lub_thelub) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (erule monofun_Iwhen3 [THEN ub2ub_monofun]) +apply simp +apply (rule less_ssum3c [THEN iffD2]) +apply (rule chain_UU_I_inverse) +apply (rule allI) +apply (rule_tac p = "Y (i) " in IssumE) +apply simp +apply simp +apply (erule notE) +apply (rule less_ssum3c [THEN iffD1]) +apply (rule_tac t = "Isinl (x) " in subst) +apply assumption +apply (erule ub_rangeD) +apply simp +done + + +lemma lub_ssum1b: "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==> + range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))" +apply (rule is_lubI) +apply (rule ub_rangeI) +apply (erule allE) +apply (erule exE) +apply (rule_tac t = "Y (i) " in ssum_lemma6 [THEN subst]) +apply assumption +apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp]) +apply (rule is_ub_thelub) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (rule_tac p = "u" in IssumE2) +apply simp +apply (rule less_ssum3d [THEN iffD2]) +apply (rule chain_UU_I_inverse) +apply (rule allI) +apply (rule_tac p = "Y (i) " in IssumE) +apply simp +apply simp +apply (erule notE) +apply (rule less_ssum3d [THEN iffD1]) +apply (rule_tac t = "Isinr (y) " in subst) +apply assumption +apply (erule ub_rangeD) +apply (rule_tac t = "u" in ssum_lemma6 [THEN subst]) +apply assumption +apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp]) +apply (rule is_lub_thelub) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (erule monofun_Iwhen3 [THEN ub2ub_monofun]) +done + + +lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard] +(* +[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==> + lub (range ?Y1) = Isinl + (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i)))) +*) + +lemmas thelub_ssum1b = lub_ssum1b [THEN thelubI, standard] +(* +[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==> + lub (range ?Y1) = Isinr + (lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i)))) +*) + +lemma cpo_ssum: "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x" +apply (rule ssum_lemma4 [THEN disjE]) +apply assumption +apply (rule exI) +apply (erule lub_ssum1a) +apply assumption +apply (rule exI) +apply (erule lub_ssum1b) +apply assumption +done end diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum3.ML --- a/src/HOLCF/Ssum3.ML Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum3.ML Thu Mar 03 01:37:32 2005 +0100 @@ -1,571 +1,48 @@ -(* Title: HOLCF/Ssum3.ML - ID: $Id$ - Author: Franz Regensburger -Class instance of ++ for class pcpo -*) - -(* for compatibility with old HOLCF-Version *) -Goal "UU = Isinl UU"; -by (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1); -qed "inst_ssum_pcpo"; - -Addsimps [inst_ssum_pcpo RS sym]; - -(* ------------------------------------------------------------------------ *) -(* continuity for Isinl and Isinr *) -(* ------------------------------------------------------------------------ *) - -Goal "contlub(Isinl)"; -by (rtac contlubI 1); -by (strip_tac 1); -by (rtac trans 1); -by (rtac (thelub_ssum1a RS sym) 2); -by (rtac allI 3); -by (rtac exI 3); -by (rtac refl 3); -by (etac (monofun_Isinl RS ch2ch_monofun) 2); -by (case_tac "lub(range(Y))=UU" 1); -by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1); -by (atac 1); -by (res_inst_tac [("f","Isinl")] arg_cong 1); -by (rtac (chain_UU_I_inverse RS sym) 1); -by (rtac allI 1); -by (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1); -by (etac (chain_UU_I RS spec ) 1); -by (atac 1); -by (rtac Iwhen1 1); -by (res_inst_tac [("f","Isinl")] arg_cong 1); -by (rtac lub_equal 1); -by (atac 1); -by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (etac (monofun_Isinl RS ch2ch_monofun) 1); -by (rtac allI 1); -by (case_tac "Y(k)=UU" 1); -by (asm_simp_tac Ssum0_ss 1); -by (asm_simp_tac Ssum0_ss 1); -qed "contlub_Isinl"; - -Goal "contlub(Isinr)"; -by (rtac contlubI 1); -by (strip_tac 1); -by (rtac trans 1); -by (rtac (thelub_ssum1b RS sym) 2); -by (rtac allI 3); -by (rtac exI 3); -by (rtac refl 3); -by (etac (monofun_Isinr RS ch2ch_monofun) 2); -by (case_tac "lub(range(Y))=UU" 1); -by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1); -by (atac 1); -by ((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)); -by (rtac allI 1); -by (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1); -by (etac (chain_UU_I RS spec ) 1); -by (atac 1); -by (rtac (strict_IsinlIsinr RS subst) 1); -by (rtac Iwhen1 1); -by ((rtac arg_cong 1) THEN (rtac lub_equal 1)); -by (atac 1); -by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (etac (monofun_Isinr RS ch2ch_monofun) 1); -by (rtac allI 1); -by (case_tac "Y(k)=UU" 1); -by (asm_simp_tac Ssum0_ss 1); -by (asm_simp_tac Ssum0_ss 1); -qed "contlub_Isinr"; - -Goal "cont(Isinl)"; -by (rtac monocontlub2cont 1); -by (rtac monofun_Isinl 1); -by (rtac contlub_Isinl 1); -qed "cont_Isinl"; - -Goal "cont(Isinr)"; -by (rtac monocontlub2cont 1); -by (rtac monofun_Isinr 1); -by (rtac contlub_Isinr 1); -qed "cont_Isinr"; - -AddIffs [cont_Isinl, cont_Isinr]; - - -(* ------------------------------------------------------------------------ *) -(* continuity for Iwhen in the firts two arguments *) -(* ------------------------------------------------------------------------ *) - -Goal "contlub(Iwhen)"; -by (rtac contlubI 1); -by (strip_tac 1); -by (rtac trans 1); -by (rtac (thelub_fun RS sym) 2); -by (etac (monofun_Iwhen1 RS ch2ch_monofun) 2); -by (rtac (expand_fun_eq RS iffD2) 1); -by (strip_tac 1); -by (rtac trans 1); -by (rtac (thelub_fun RS sym) 2); -by (rtac ch2ch_fun 2); -by (etac (monofun_Iwhen1 RS ch2ch_monofun) 2); -by (rtac (expand_fun_eq RS iffD2) 1); -by (strip_tac 1); -by (res_inst_tac [("p","xa")] IssumE 1); -by (asm_simp_tac Ssum0_ss 1); -by (rtac (lub_const RS thelubI RS sym) 1); -by (asm_simp_tac Ssum0_ss 1); -by (etac contlub_cfun_fun 1); -by (asm_simp_tac Ssum0_ss 1); -by (rtac (lub_const RS thelubI RS sym) 1); -qed "contlub_Iwhen1"; - -Goal "contlub(Iwhen(f))"; -by (rtac contlubI 1); -by (strip_tac 1); -by (rtac trans 1); -by (rtac (thelub_fun RS sym) 2); -by (etac (monofun_Iwhen2 RS ch2ch_monofun) 2); -by (rtac (expand_fun_eq RS iffD2) 1); -by (strip_tac 1); -by (res_inst_tac [("p","x")] IssumE 1); -by (asm_simp_tac Ssum0_ss 1); -by (rtac (lub_const RS thelubI RS sym) 1); -by (asm_simp_tac Ssum0_ss 1); -by (rtac (lub_const RS thelubI RS sym) 1); -by (asm_simp_tac Ssum0_ss 1); -by (etac contlub_cfun_fun 1); -qed "contlub_Iwhen2"; - -(* ------------------------------------------------------------------------ *) -(* continuity for Iwhen in its third argument *) -(* ------------------------------------------------------------------------ *) - -(* ------------------------------------------------------------------------ *) -(* first 5 ugly lemmas *) -(* ------------------------------------------------------------------------ *) - -Goal "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"; -by (strip_tac 1); -by (res_inst_tac [("p","Y(i)")] IssumE 1); -by (etac exI 1); -by (etac exI 1); -by (res_inst_tac [("P","y=UU")] notE 1); -by (atac 1); -by (rtac (less_ssum3d RS iffD1) 1); -by (etac subst 1); -by (etac subst 1); -by (etac is_ub_thelub 1); -qed "ssum_lemma9"; - - -Goal "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"; -by (strip_tac 1); -by (res_inst_tac [("p","Y(i)")] IssumE 1); -by (rtac exI 1); -by (etac trans 1); -by (rtac strict_IsinlIsinr 1); -by (etac exI 2); -by (res_inst_tac [("P","xa=UU")] notE 1); -by (atac 1); -by (rtac (less_ssum3c RS iffD1) 1); -by (etac subst 1); -by (etac subst 1); -by (etac is_ub_thelub 1); -qed "ssum_lemma10"; - -Goal "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\ -\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"; -by (asm_simp_tac Ssum0_ss 1); -by (rtac (chain_UU_I_inverse RS sym) 1); -by (rtac allI 1); -by (res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1); -by (rtac (inst_ssum_pcpo RS subst) 1); -by (rtac (chain_UU_I RS spec RS sym) 1); -by (atac 1); -by (etac (inst_ssum_pcpo RS ssubst) 1); -by (asm_simp_tac Ssum0_ss 1); -qed "ssum_lemma11"; - -Goal "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\ -\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"; -by (asm_simp_tac Ssum0_ss 1); -by (res_inst_tac [("t","x")] subst 1); -by (rtac inject_Isinl 1); -by (rtac trans 1); -by (atac 2); -by (rtac (thelub_ssum1a RS sym) 1); -by (atac 1); -by (etac ssum_lemma9 1); -by (atac 1); -by (rtac trans 1); -by (rtac contlub_cfun_arg 1); -by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (atac 1); -by (rtac lub_equal2 1); -by (rtac (chain_mono2 RS exE) 1); -by (atac 2); -by (rtac chain_UU_I_inverse2 1); -by (stac inst_ssum_pcpo 1); -by (etac contrapos_np 1); -by (rtac inject_Isinl 1); -by (rtac trans 1); -by (etac sym 1); -by (etac notnotD 1); -by (rtac exI 1); -by (strip_tac 1); -by (rtac (ssum_lemma9 RS spec RS exE) 1); -by (atac 1); -by (atac 1); -by (res_inst_tac [("t","Y(i)")] ssubst 1); -by (atac 1); -by (rtac trans 1); -by (rtac cfun_arg_cong 1); -by (rtac Iwhen2 1); -by (Force_tac 1); -by (res_inst_tac [("t","Y(i)")] ssubst 1); -by (atac 1); -by Auto_tac; -by (stac Iwhen2 1); -by (Force_tac 1); -by (simp_tac (simpset_of Cfun3.thy) 1); -by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -qed "ssum_lemma12"; - - -Goal "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\ -\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"; -by (asm_simp_tac Ssum0_ss 1); -by (res_inst_tac [("t","x")] subst 1); -by (rtac inject_Isinr 1); -by (rtac trans 1); -by (atac 2); -by (rtac (thelub_ssum1b RS sym) 1); -by (atac 1); -by (etac ssum_lemma10 1); -by (atac 1); -by (rtac trans 1); -by (rtac contlub_cfun_arg 1); -by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (atac 1); -by (rtac lub_equal2 1); -by (rtac (chain_mono2 RS exE) 1); -by (atac 2); -by (rtac chain_UU_I_inverse2 1); -by (stac inst_ssum_pcpo 1); -by (etac contrapos_np 1); -by (rtac inject_Isinr 1); -by (rtac trans 1); -by (etac sym 1); -by (rtac (strict_IsinlIsinr RS subst) 1); -by (etac notnotD 1); -by (rtac exI 1); -by (strip_tac 1); -by (rtac (ssum_lemma10 RS spec RS exE) 1); -by (atac 1); -by (atac 1); -by (res_inst_tac [("t","Y(i)")] ssubst 1); -by (atac 1); -by (rtac trans 1); -by (rtac cfun_arg_cong 1); -by (rtac Iwhen3 1); -by (Force_tac 1); -by (res_inst_tac [("t","Y(i)")] ssubst 1); -by (atac 1); -by (stac Iwhen3 1); -by (Force_tac 1); -by (res_inst_tac [("t","Y(i)")] ssubst 1); -by (atac 1); -by (simp_tac (simpset_of Cfun3.thy) 1); -by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1); -qed "ssum_lemma13"; - +(* legacy ML bindings *) -Goal "contlub(Iwhen(f)(g))"; -by (rtac contlubI 1); -by (strip_tac 1); -by (res_inst_tac [("p","lub(range(Y))")] IssumE 1); -by (etac ssum_lemma11 1); -by (atac 1); -by (etac ssum_lemma12 1); -by (atac 1); -by (atac 1); -by (etac ssum_lemma13 1); -by (atac 1); -by (atac 1); -qed "contlub_Iwhen3"; - -Goal "cont(Iwhen)"; -by (rtac monocontlub2cont 1); -by (rtac monofun_Iwhen1 1); -by (rtac contlub_Iwhen1 1); -qed "cont_Iwhen1"; - -Goal "cont(Iwhen(f))"; -by (rtac monocontlub2cont 1); -by (rtac monofun_Iwhen2 1); -by (rtac contlub_Iwhen2 1); -qed "cont_Iwhen2"; - -Goal "cont(Iwhen(f)(g))"; -by (rtac monocontlub2cont 1); -by (rtac monofun_Iwhen3 1); -by (rtac contlub_Iwhen3 1); -qed "cont_Iwhen3"; - -(* ------------------------------------------------------------------------ *) -(* continuous versions of lemmas for 'a ++ 'b *) -(* ------------------------------------------------------------------------ *) - -Goalw [sinl_def] "sinl$UU =UU"; -by (simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1); -by (rtac (inst_ssum_pcpo RS sym) 1); -qed "strict_sinl"; -Addsimps [strict_sinl]; - -Goalw [sinr_def] "sinr$UU=UU"; -by (simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1); -by (rtac (inst_ssum_pcpo RS sym) 1); -qed "strict_sinr"; -Addsimps [strict_sinr]; - -Goalw [sinl_def,sinr_def] - "sinl$a=sinr$b ==> a=UU & b=UU"; -by (auto_tac (claset() addSDs [noteq_IsinlIsinr], simpset())); -qed "noteq_sinlsinr"; - -Goalw [sinl_def,sinr_def] - "sinl$a1=sinl$a2==> a1=a2"; -by Auto_tac; -qed "inject_sinl"; - -Goalw [sinl_def,sinr_def] - "sinr$a1=sinr$a2==> a1=a2"; -by Auto_tac; -qed "inject_sinr"; - -AddSDs [inject_sinl, inject_sinr]; - -Goal "x~=UU ==> sinl$x ~= UU"; -by (etac contrapos_nn 1); -by (rtac inject_sinl 1); -by Auto_tac; -qed "defined_sinl"; -Addsimps [defined_sinl]; - -Goal "x~=UU ==> sinr$x ~= UU"; -by (etac contrapos_nn 1); -by (rtac inject_sinr 1); -by Auto_tac; -qed "defined_sinr"; -Addsimps [defined_sinr]; - -Goalw [sinl_def,sinr_def] - "z=UU | (? a. z=sinl$a & a~=UU) | (? b. z=sinr$b & b~=UU)"; -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1); -by (stac inst_ssum_pcpo 1); -by (rtac Exh_Ssum 1); -qed "Exh_Ssum1"; - - -val [major,prem2,prem3] = Goalw [sinl_def,sinr_def] - "[|p=UU ==> Q ;\ -\ !!x.[|p=sinl$x; x~=UU |] ==> Q;\ -\ !!y.[|p=sinr$y; y~=UU |] ==> Q|] ==> Q"; -by (rtac (major RS IssumE) 1); -by (stac inst_ssum_pcpo 1); -by (atac 1); -by (rtac prem2 1); -by (atac 2); -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1); -by (rtac prem3 1); -by (atac 2); -by (Asm_simp_tac 1); -qed "ssumE"; - - -val [preml,premr] = Goalw [sinl_def,sinr_def] - "[|!!x.[|p=sinl$x|] ==> Q;\ -\ !!y.[|p=sinr$y|] ==> Q|] ==> Q"; -by (rtac IssumE2 1); -by (rtac preml 1); -by (rtac premr 2); -by Auto_tac; -qed "ssumE2"; - -val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont2cont_CF1L]) 1)); - -Goalw [sscase_def,sinl_def,sinr_def] - "sscase$f$g$UU = UU"; -by (stac inst_ssum_pcpo 1); -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (simp_tac Ssum0_ss 1); -qed "sscase1"; -Addsimps [sscase1]; - - -val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)); - -Goalw [sscase_def,sinl_def,sinr_def] - "x~=UU==> sscase$f$g$(sinl$x) = f$x"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (asm_simp_tac Ssum0_ss 1); -qed "sscase2"; -Addsimps [sscase2]; - -Goalw [sscase_def,sinl_def,sinr_def] - "x~=UU==> sscase$f$g$(sinr$x) = g$x"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (asm_simp_tac Ssum0_ss 1); -qed "sscase3"; -Addsimps [sscase3]; - - -Goalw [sinl_def,sinr_def] - "(sinl$x << sinl$y) = (x << y)"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (rtac less_ssum3a 1); -qed "less_ssum4a"; - -Goalw [sinl_def,sinr_def] - "(sinr$x << sinr$y) = (x << y)"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (rtac less_ssum3b 1); -qed "less_ssum4b"; - -Goalw [sinl_def,sinr_def] - "(sinl$x << sinr$y) = (x = UU)"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (rtac less_ssum3c 1); -qed "less_ssum4c"; - -Goalw [sinl_def,sinr_def] - "(sinr$x << sinl$y) = (x = UU)"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (rtac less_ssum3d 1); -qed "less_ssum4d"; - -Goalw [sinl_def,sinr_def] - "chain(Y) ==> (!i.? x.(Y i)=sinl$x)|(!i.? y.(Y i)=sinr$y)"; -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1); -by (etac ssum_lemma4 1); -qed "ssum_chainE"; - - -Goalw [sinl_def,sinr_def,sscase_def] -"[| chain(Y); !i.? x. Y(i) = sinl$x |] ==>\ -\ lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac (beta_cfun RS ext) 1); -by tac; -by (rtac thelub_ssum1a 1); -by (atac 1); -by (rtac allI 1); -by (etac allE 1); -by (etac exE 1); -by (rtac exI 1); -by (etac box_equals 1); -by (rtac refl 1); -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1); -qed "thelub_ssum2a"; - -Goalw [sinl_def,sinr_def,sscase_def] -"[| chain(Y); !i.? x. Y(i) = sinr$x |] ==>\ -\ lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac beta_cfun 1); -by tac; -by (stac (beta_cfun RS ext) 1); -by tac; -by (rtac thelub_ssum1b 1); -by (atac 1); -by (rtac allI 1); -by (etac allE 1); -by (etac exE 1); -by (rtac exI 1); -by (etac box_equals 1); -by (rtac refl 1); -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); -qed "thelub_ssum2b"; - -Goalw [sinl_def,sinr_def] - "[| chain(Y); lub(range(Y)) = sinl$x|] ==> !i.? x. Y(i)=sinl$x"; -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); -by (etac ssum_lemma9 1); -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); -qed "thelub_ssum2a_rev"; - -Goalw [sinl_def,sinr_def] - "[| chain(Y); lub(range(Y)) = sinr$x|] ==> !i.? x. Y(i)=sinr$x"; -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); -by (etac ssum_lemma10 1); -by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); -qed "thelub_ssum2b_rev"; - -Goal "chain(Y) ==>\ -\ lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))\ -\ | lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"; -by (rtac (ssum_chainE RS disjE) 1); -by (atac 1); -by (rtac disjI1 1); -by (etac thelub_ssum2a 1); -by (atac 1); -by (rtac disjI2 1); -by (etac thelub_ssum2b 1); -by (atac 1); -qed "thelub_ssum3"; - -Goal "sscase$sinl$sinr$z=z"; -by (res_inst_tac [("p","z")] ssumE 1); -by Auto_tac; -qed "sscase4"; - - -(* ------------------------------------------------------------------------ *) -(* install simplifier for Ssum *) -(* ------------------------------------------------------------------------ *) - -val Ssum_rews = [strict_sinl,strict_sinr,defined_sinl,defined_sinr, - sscase1,sscase2,sscase3]; +val sinl_def = thm "sinl_def"; +val sinr_def = thm "sinr_def"; +val sscase_def = thm "sscase_def"; +val inst_ssum_pcpo = thm "inst_ssum_pcpo"; +val contlub_Isinl = thm "contlub_Isinl"; +val contlub_Isinr = thm "contlub_Isinr"; +val cont_Isinl = thm "cont_Isinl"; +val cont_Isinr = thm "cont_Isinr"; +val contlub_Iwhen1 = thm "contlub_Iwhen1"; +val contlub_Iwhen2 = thm "contlub_Iwhen2"; +val ssum_lemma9 = thm "ssum_lemma9"; +val ssum_lemma10 = thm "ssum_lemma10"; +val ssum_lemma11 = thm "ssum_lemma11"; +val ssum_lemma12 = thm "ssum_lemma12"; +val ssum_lemma13 = thm "ssum_lemma13"; +val contlub_Iwhen3 = thm "contlub_Iwhen3"; +val cont_Iwhen1 = thm "cont_Iwhen1"; +val cont_Iwhen2 = thm "cont_Iwhen2"; +val cont_Iwhen3 = thm "cont_Iwhen3"; +val strict_sinl = thm "strict_sinl"; +val strict_sinr = thm "strict_sinr"; +val noteq_sinlsinr = thm "noteq_sinlsinr"; +val inject_sinl = thm "inject_sinl"; +val inject_sinr = thm "inject_sinr"; +val defined_sinl = thm "defined_sinl"; +val defined_sinr = thm "defined_sinr"; +val Exh_Ssum1 = thm "Exh_Ssum1"; +val ssumE = thm "ssumE"; +val ssumE2 = thm "ssumE2"; +val sscase1 = thm "sscase1"; +val sscase2 = thm "sscase2"; +val sscase3 = thm "sscase3"; +val less_ssum4a = thm "less_ssum4a"; +val less_ssum4b = thm "less_ssum4b"; +val less_ssum4c = thm "less_ssum4c"; +val less_ssum4d = thm "less_ssum4d"; +val ssum_chainE = thm "ssum_chainE"; +val thelub_ssum2a = thm "thelub_ssum2a"; +val thelub_ssum2b = thm "thelub_ssum2b"; +val thelub_ssum2a_rev = thm "thelub_ssum2a_rev"; +val thelub_ssum2b_rev = thm "thelub_ssum2b_rev"; +val thelub_ssum3 = thm "thelub_ssum3"; +val sscase4 = thm "sscase4"; +val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr, + sscase1, sscase2, sscase3] diff -r 60743edae74a -r 41bfe19eabe2 src/HOLCF/Ssum3.thy --- a/src/HOLCF/Ssum3.thy Thu Mar 03 00:42:04 2005 +0100 +++ b/src/HOLCF/Ssum3.thy Thu Mar 03 01:37:32 2005 +0100 @@ -1,13 +1,18 @@ (* Title: HOLCF/ssum3.thy ID: $Id$ Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) Class instance of ++ for class pcpo *) -Ssum3 = Ssum2 + +theory Ssum3 = Ssum2: -instance "++" :: (pcpo,pcpo)pcpo (least_ssum,cpo_ssum) +instance "++" :: (pcpo,pcpo)pcpo +apply (intro_classes) +apply (erule cpo_ssum) +apply (rule least_ssum) +done consts sinl :: "'a -> ('a++'b)" @@ -16,11 +21,604 @@ defs -sinl_def "sinl == (LAM x. Isinl(x))" -sinr_def "sinr == (LAM x. Isinr(x))" -sscase_def "sscase == (LAM f g s. Iwhen(f)(g)(s))" +sinl_def: "sinl == (LAM x. Isinl(x))" +sinr_def: "sinr == (LAM x. Isinr(x))" +sscase_def: "sscase == (LAM f g s. Iwhen(f)(g)(s))" translations "case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s" +(* Title: HOLCF/Ssum3.ML + ID: $Id$ + Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Class instance of ++ for class pcpo +*) + +(* for compatibility with old HOLCF-Version *) +lemma inst_ssum_pcpo: "UU = Isinl UU" +apply (simp add: UU_def UU_ssum_def) +done + +declare inst_ssum_pcpo [symmetric, simp] + +(* ------------------------------------------------------------------------ *) +(* continuity for Isinl and Isinr *) +(* ------------------------------------------------------------------------ *) + +lemma contlub_Isinl: "contlub(Isinl)" +apply (rule contlubI) +apply (intro strip) +apply (rule trans) +apply (rule_tac [2] thelub_ssum1a [symmetric]) +apply (rule_tac [3] allI) +apply (rule_tac [3] exI) +apply (rule_tac [3] refl) +apply (erule_tac [2] monofun_Isinl [THEN ch2ch_monofun]) +apply (case_tac "lub (range (Y))=UU") +apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) +apply assumption +apply (rule_tac f = "Isinl" in arg_cong) +apply (rule chain_UU_I_inverse [symmetric]) +apply (rule allI) +apply (rule_tac s = "UU" and t = "Y (i) " in ssubst) +apply (erule chain_UU_I [THEN spec]) +apply assumption +apply (rule Iwhen1) +apply (rule_tac f = "Isinl" in arg_cong) +apply (rule lub_equal) +apply assumption +apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (erule monofun_Isinl [THEN ch2ch_monofun]) +apply (rule allI) +apply (case_tac "Y (k) =UU") +apply (erule ssubst) +apply (rule Iwhen1[symmetric]) +apply simp +done + +lemma contlub_Isinr: "contlub(Isinr)" +apply (rule contlubI) +apply (intro strip) +apply (rule trans) +apply (rule_tac [2] thelub_ssum1b [symmetric]) +apply (rule_tac [3] allI) +apply (rule_tac [3] exI) +apply (rule_tac [3] refl) +apply (erule_tac [2] monofun_Isinr [THEN ch2ch_monofun]) +apply (case_tac "lub (range (Y))=UU") +apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) +apply assumption +apply (rule arg_cong, rule chain_UU_I_inverse [symmetric]) +apply (rule allI) +apply (rule_tac s = "UU" and t = "Y (i) " in ssubst) +apply (erule chain_UU_I [THEN spec]) +apply assumption +apply (rule strict_IsinlIsinr [THEN subst]) +apply (rule Iwhen1) +apply (rule arg_cong, rule lub_equal) +apply assumption +apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (erule monofun_Isinr [THEN ch2ch_monofun]) +apply (rule allI) +apply (case_tac "Y (k) =UU") +apply (simp only: Ssum0_ss) +apply simp +done + +lemma cont_Isinl: "cont(Isinl)" +apply (rule monocontlub2cont) +apply (rule monofun_Isinl) +apply (rule contlub_Isinl) +done + +lemma cont_Isinr: "cont(Isinr)" +apply (rule monocontlub2cont) +apply (rule monofun_Isinr) +apply (rule contlub_Isinr) +done + +declare cont_Isinl [iff] cont_Isinr [iff] + + +(* ------------------------------------------------------------------------ *) +(* continuity for Iwhen in the firts two arguments *) +(* ------------------------------------------------------------------------ *) + +lemma contlub_Iwhen1: "contlub(Iwhen)" +apply (rule contlubI) +apply (intro strip) +apply (rule trans) +apply (rule_tac [2] thelub_fun [symmetric]) +apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun]) +apply (rule expand_fun_eq [THEN iffD2]) +apply (intro strip) +apply (rule trans) +apply (rule_tac [2] thelub_fun [symmetric]) +apply (rule_tac [2] ch2ch_fun) +apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun]) +apply (rule expand_fun_eq [THEN iffD2]) +apply (intro strip) +apply (rule_tac p = "xa" in IssumE) +apply (simp only: Ssum0_ss) +apply (rule lub_const [THEN thelubI, symmetric]) +apply simp +apply (erule contlub_cfun_fun) +apply simp +apply (rule lub_const [THEN thelubI, symmetric]) +done + +lemma contlub_Iwhen2: "contlub(Iwhen(f))" +apply (rule contlubI) +apply (intro strip) +apply (rule trans) +apply (rule_tac [2] thelub_fun [symmetric]) +apply (erule_tac [2] monofun_Iwhen2 [THEN ch2ch_monofun]) +apply (rule expand_fun_eq [THEN iffD2]) +apply (intro strip) +apply (rule_tac p = "x" in IssumE) +apply (simp only: Ssum0_ss) +apply (rule lub_const [THEN thelubI, symmetric]) +apply simp +apply (rule lub_const [THEN thelubI, symmetric]) +apply simp +apply (erule contlub_cfun_fun) +done + +(* ------------------------------------------------------------------------ *) +(* continuity for Iwhen in its third argument *) +(* ------------------------------------------------------------------------ *) + +(* ------------------------------------------------------------------------ *) +(* first 5 ugly lemmas *) +(* ------------------------------------------------------------------------ *) + +lemma ssum_lemma9: "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)" +apply (intro strip) +apply (rule_tac p = "Y (i) " in IssumE) +apply (erule exI) +apply (erule exI) +apply (rule_tac P = "y=UU" in notE) +apply assumption +apply (rule less_ssum3d [THEN iffD1]) +apply (erule subst) +apply (erule subst) +apply (erule is_ub_thelub) +done + + +lemma ssum_lemma10: "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)" +apply (intro strip) +apply (rule_tac p = "Y (i) " in IssumE) +apply (rule exI) +apply (erule trans) +apply (rule strict_IsinlIsinr) +apply (erule_tac [2] exI) +apply (rule_tac P = "xa=UU" in notE) +apply assumption +apply (rule less_ssum3c [THEN iffD1]) +apply (erule subst) +apply (erule subst) +apply (erule is_ub_thelub) +done + +lemma ssum_lemma11: "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==> + Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" +apply (simp only: Ssum0_ss) +apply (rule chain_UU_I_inverse [symmetric]) +apply (rule allI) +apply (rule_tac s = "Isinl (UU) " and t = "Y (i) " in subst) +apply (rule inst_ssum_pcpo [THEN subst]) +apply (rule chain_UU_I [THEN spec, symmetric]) +apply assumption +apply (erule inst_ssum_pcpo [THEN ssubst]) +apply (simp only: Ssum0_ss) +done + +lemma ssum_lemma12: "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==> + Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" +apply simp +apply (rule_tac t = "x" in subst) +apply (rule inject_Isinl) +apply (rule trans) +prefer 2 apply (assumption) +apply (rule thelub_ssum1a [symmetric]) +apply assumption +apply (erule ssum_lemma9) +apply assumption +apply (rule trans) +apply (rule contlub_cfun_arg) +apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply assumption +apply (rule lub_equal2) +apply (rule chain_mono2 [THEN exE]) +prefer 2 apply (assumption) +apply (rule chain_UU_I_inverse2) +apply (subst inst_ssum_pcpo) +apply (erule contrapos_np) +apply (rule inject_Isinl) +apply (rule trans) +apply (erule sym) +apply (erule notnotD) +apply (rule exI) +apply (intro strip) +apply (rule ssum_lemma9 [THEN spec, THEN exE]) +apply assumption +apply assumption +apply (rule_tac t = "Y (i) " in ssubst) +apply assumption +apply (rule trans) +apply (rule cfun_arg_cong) +apply (rule Iwhen2) +apply force +apply (rule_tac t = "Y (i) " in ssubst) +apply assumption +apply auto +apply (subst Iwhen2) +apply force +apply (rule refl) +apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun]) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +done + + +lemma ssum_lemma13: "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==> + Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" +apply simp +apply (rule_tac t = "x" in subst) +apply (rule inject_Isinr) +apply (rule trans) +prefer 2 apply (assumption) +apply (rule thelub_ssum1b [symmetric]) +apply assumption +apply (erule ssum_lemma10) +apply assumption +apply (rule trans) +apply (rule contlub_cfun_arg) +apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply assumption +apply (rule lub_equal2) +apply (rule chain_mono2 [THEN exE]) +prefer 2 apply (assumption) +apply (rule chain_UU_I_inverse2) +apply (subst inst_ssum_pcpo) +apply (erule contrapos_np) +apply (rule inject_Isinr) +apply (rule trans) +apply (erule sym) +apply (rule strict_IsinlIsinr [THEN subst]) +apply (erule notnotD) +apply (rule exI) +apply (intro strip) +apply (rule ssum_lemma10 [THEN spec, THEN exE]) +apply assumption +apply assumption +apply (rule_tac t = "Y (i) " in ssubst) +apply assumption +apply (rule trans) +apply (rule cfun_arg_cong) +apply (rule Iwhen3) +apply force +apply (rule_tac t = "Y (i) " in ssubst) +apply assumption +apply (subst Iwhen3) +apply force +apply (rule_tac t = "Y (i) " in ssubst) +apply assumption +apply simp +apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun]) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) +done + + +lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))" +apply (rule contlubI) +apply (intro strip) +apply (rule_tac p = "lub (range (Y))" in IssumE) +apply (erule ssum_lemma11) +apply assumption +apply (erule ssum_lemma12) +apply assumption +apply assumption +apply (erule ssum_lemma13) +apply assumption +apply assumption +done + +lemma cont_Iwhen1: "cont(Iwhen)" +apply (rule monocontlub2cont) +apply (rule monofun_Iwhen1) +apply (rule contlub_Iwhen1) +done + +lemma cont_Iwhen2: "cont(Iwhen(f))" +apply (rule monocontlub2cont) +apply (rule monofun_Iwhen2) +apply (rule contlub_Iwhen2) +done + +lemma cont_Iwhen3: "cont(Iwhen(f)(g))" +apply (rule monocontlub2cont) +apply (rule monofun_Iwhen3) +apply (rule contlub_Iwhen3) +done + +(* ------------------------------------------------------------------------ *) +(* continuous versions of lemmas for 'a ++ 'b *) +(* ------------------------------------------------------------------------ *) + +lemma strict_sinl: "sinl$UU =UU" + +apply (unfold sinl_def) +apply (simp add: cont_Isinl) +done +declare strict_sinl [simp] + +lemma strict_sinr: "sinr$UU=UU" +apply (unfold sinr_def) +apply (simp add: cont_Isinr) +done +declare strict_sinr [simp] + +lemma noteq_sinlsinr: + "sinl$a=sinr$b ==> a=UU & b=UU" +apply (unfold sinl_def sinr_def) +apply (auto dest!: noteq_IsinlIsinr) +done + +lemma inject_sinl: + "sinl$a1=sinl$a2==> a1=a2" +apply (unfold sinl_def sinr_def) +apply auto +done + +lemma inject_sinr: + "sinr$a1=sinr$a2==> a1=a2" +apply (unfold sinl_def sinr_def) +apply auto +done + +declare inject_sinl [dest!] inject_sinr [dest!] + +lemma defined_sinl: "x~=UU ==> sinl$x ~= UU" +apply (erule contrapos_nn) +apply (rule inject_sinl) +apply auto +done +declare defined_sinl [simp] + +lemma defined_sinr: "x~=UU ==> sinr$x ~= UU" +apply (erule contrapos_nn) +apply (rule inject_sinr) +apply auto +done +declare defined_sinr [simp] + +lemma Exh_Ssum1: + "z=UU | (? a. z=sinl$a & a~=UU) | (? b. z=sinr$b & b~=UU)" +apply (unfold sinl_def sinr_def) +apply simp +apply (subst inst_ssum_pcpo) +apply (rule Exh_Ssum) +done + + +lemma ssumE: +assumes major: "p=UU ==> Q" +assumes prem2: "!!x.[|p=sinl$x; x~=UU |] ==> Q" +assumes prem3: "!!y.[|p=sinr$y; y~=UU |] ==> Q" +shows "Q" +apply (rule major [THEN IssumE]) +apply (subst inst_ssum_pcpo) +apply assumption +apply (rule prem2) +prefer 2 apply (assumption) +apply (simp add: sinl_def) +apply (rule prem3) +prefer 2 apply (assumption) +apply (simp add: sinr_def) +done + + +lemma ssumE2: +assumes preml: "!!x.[|p=sinl$x|] ==> Q" +assumes premr: "!!y.[|p=sinr$y|] ==> Q" +shows "Q" +apply (rule IssumE2) +apply (rule preml) +apply (rule_tac [2] premr) +apply (unfold sinl_def sinr_def) +apply auto +done + +lemmas ssum_conts = cont_lemmas1 cont_Iwhen1 cont_Iwhen2 + cont_Iwhen3 cont2cont_CF1L + +lemma sscase1: + "sscase$f$g$UU = UU" +apply (unfold sscase_def sinl_def sinr_def) +apply (subst inst_ssum_pcpo) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (simp only: Ssum0_ss) +done +declare sscase1 [simp] + + +lemma sscase2: + "x~=UU==> sscase$f$g$(sinl$x) = f$x" +apply (unfold sscase_def sinl_def sinr_def) +apply (simplesubst beta_cfun) +apply (rule cont_Isinl) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply simp +done +declare sscase2 [simp] + +lemma sscase3: + "x~=UU==> sscase$f$g$(sinr$x) = g$x" +apply (unfold sscase_def sinl_def sinr_def) +apply (simplesubst beta_cfun) +apply (rule cont_Isinr) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply simp +done +declare sscase3 [simp] + + +lemma less_ssum4a: + "(sinl$x << sinl$y) = (x << y)" + +apply (unfold sinl_def sinr_def) +apply (subst beta_cfun) +apply (rule cont_Isinl) +apply (subst beta_cfun) +apply (rule cont_Isinl) +apply (rule less_ssum3a) +done + +lemma less_ssum4b: + "(sinr$x << sinr$y) = (x << y)" +apply (unfold sinl_def sinr_def) +apply (subst beta_cfun) +apply (rule cont_Isinr) +apply (subst beta_cfun) +apply (rule cont_Isinr) +apply (rule less_ssum3b) +done + +lemma less_ssum4c: + "(sinl$x << sinr$y) = (x = UU)" +apply (unfold sinl_def sinr_def) +apply (simplesubst beta_cfun) +apply (rule cont_Isinr) +apply (subst beta_cfun) +apply (rule cont_Isinl) +apply (rule less_ssum3c) +done + +lemma less_ssum4d: + "(sinr$x << sinl$y) = (x = UU)" +apply (unfold sinl_def sinr_def) +apply (simplesubst beta_cfun) +apply (rule cont_Isinl) +apply (subst beta_cfun) +apply (rule cont_Isinr) +apply (rule less_ssum3d) +done + +lemma ssum_chainE: + "chain(Y) ==> (!i.? x.(Y i)=sinl$x)|(!i.? y.(Y i)=sinr$y)" +apply (unfold sinl_def sinr_def) +apply simp +apply (erule ssum_lemma4) +done + + +lemma thelub_ssum2a: +"[| chain(Y); !i.? x. Y(i) = sinl$x |] ==> + lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))" + +apply (unfold sinl_def sinr_def sscase_def) +apply (subst beta_cfun) +apply (rule cont_Isinl) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun [THEN ext]) +apply (intro ssum_conts) +apply (rule thelub_ssum1a) +apply assumption +apply (rule allI) +apply (erule allE) +apply (erule exE) +apply (rule exI) +apply (erule box_equals) +apply (rule refl) +apply simp +done + +lemma thelub_ssum2b: +"[| chain(Y); !i.? x. Y(i) = sinr$x |] ==> + lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))" +apply (unfold sinl_def sinr_def sscase_def) +apply (subst beta_cfun) +apply (rule cont_Isinr) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun) +apply (intro ssum_conts) +apply (subst beta_cfun [THEN ext]) +apply (intro ssum_conts) +apply (rule thelub_ssum1b) +apply assumption +apply (rule allI) +apply (erule allE) +apply (erule exE) +apply (rule exI) +apply (erule box_equals) +apply (rule refl) +apply simp +done + +lemma thelub_ssum2a_rev: + "[| chain(Y); lub(range(Y)) = sinl$x|] ==> !i.? x. Y(i)=sinl$x" +apply (unfold sinl_def sinr_def) +apply simp +apply (erule ssum_lemma9) +apply simp +done + +lemma thelub_ssum2b_rev: + "[| chain(Y); lub(range(Y)) = sinr$x|] ==> !i.? x. Y(i)=sinr$x" +apply (unfold sinl_def sinr_def) +apply simp +apply (erule ssum_lemma10) +apply simp +done + +lemma thelub_ssum3: "chain(Y) ==> + lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i)))) + | lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))" +apply (rule ssum_chainE [THEN disjE]) +apply assumption +apply (rule disjI1) +apply (erule thelub_ssum2a) +apply assumption +apply (rule disjI2) +apply (erule thelub_ssum2b) +apply assumption +done + +lemma sscase4: "sscase$sinl$sinr$z=z" +apply (rule_tac p = "z" in ssumE) +apply auto +done + + +(* ------------------------------------------------------------------------ *) +(* install simplifier for Ssum *) +(* ------------------------------------------------------------------------ *) + +lemmas Ssum_rews = strict_sinl strict_sinr defined_sinl defined_sinr + sscase1 sscase2 sscase3 + end