--- 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";
--- 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 ("(_ \\<oplus>/ _)" [21, 20] 20)
+ "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
syntax (HTML output)
- "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
+ "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [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
--- 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";
--- 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
--- 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<<y";
-by (res_inst_tac [("x","Isinl UU")] exI 1);
-by (rtac (minimal_ssum RS allI) 1);
-qed "least_ssum";
-
-(* ------------------------------------------------------------------------ *)
-(* Isinl, Isinr are monotone *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [monofun] "monofun(Isinl)";
-by (strip_tac 1);
-by (etac (less_ssum3a RS iffD2) 1);
-qed "monofun_Isinl";
-
-Goalw [monofun] "monofun(Isinr)";
-by (strip_tac 1);
-by (etac (less_ssum3b RS iffD2) 1);
-qed "monofun_Isinr";
-
-
-(* ------------------------------------------------------------------------ *)
-(* Iwhen is monotone in all arguments *)
-(* ------------------------------------------------------------------------ *)
-
-
-Goalw [monofun] "monofun(Iwhen)";
-by (strip_tac 1);
-by (rtac (less_fun RS iffD2) 1);
-by (strip_tac 1);
-by (rtac (less_fun RS iffD2) 1);
-by (strip_tac 1);
-by (res_inst_tac [("p","xb")] IssumE 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (etac monofun_cfun_fun 1);
-by (asm_simp_tac Ssum0_ss 1);
-qed "monofun_Iwhen1";
-
-Goalw [monofun] "monofun(Iwhen(f))";
-by (strip_tac 1);
-by (rtac (less_fun RS iffD2) 1);
-by (strip_tac 1);
-by (res_inst_tac [("p","xa")] IssumE 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (etac monofun_cfun_fun 1);
-qed "monofun_Iwhen2";
-
-Goalw [monofun] "monofun(Iwhen(f)(g))";
-by (strip_tac 1);
-by (res_inst_tac [("p","x")] IssumE 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("p","y")] IssumE 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (res_inst_tac [("P","xa=UU")] notE 1);
-by (atac 1);
-by (rtac UU_I 1);
-by (rtac (less_ssum3a RS iffD1) 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (rtac monofun_cfun_arg 1);
-by (etac (less_ssum3a RS iffD1) 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("s","UU"),("t","xa")] subst 1);
-by (etac (less_ssum3c RS iffD1 RS sym) 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("p","y")] IssumE 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("s","UU"),("t","ya")] subst 1);
-by (etac (less_ssum3d RS iffD1 RS sym) 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("s","UU"),("t","ya")] subst 1);
-by (etac (less_ssum3d RS iffD1 RS sym) 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac Ssum0_ss 1);
-by (rtac monofun_cfun_arg 1);
-by (etac (less_ssum3b RS iffD1) 1);
-qed "monofun_Iwhen3";
-
-
-(* ------------------------------------------------------------------------ *)
-(* some kind of exhaustion rules for chains in 'a ++ 'b *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "[|~(!i.? x. Y(i::nat)=Isinl(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";
--- 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<<y"
+apply (rule_tac x = "Isinl UU" in exI)
+apply (rule minimal_ssum [THEN allI])
+done
+
+(* ------------------------------------------------------------------------ *)
+(* Isinl, Isinr are monotone *)
+(* ------------------------------------------------------------------------ *)
+
+lemma monofun_Isinl: "monofun(Isinl)"
+
+apply (unfold monofun)
+apply (intro strip)
+apply (erule less_ssum3a [THEN iffD2])
+done
+
+lemma monofun_Isinr: "monofun(Isinr)"
+apply (unfold monofun)
+apply (intro strip)
+apply (erule less_ssum3b [THEN iffD2])
+done
+
+
+(* ------------------------------------------------------------------------ *)
+(* Iwhen is monotone in all arguments *)
+(* ------------------------------------------------------------------------ *)
+
+
+lemma monofun_Iwhen1: "monofun(Iwhen)"
+
+
+apply (unfold monofun)
+apply (intro strip)
+apply (rule less_fun [THEN iffD2])
+apply (intro strip)
+apply (rule less_fun [THEN iffD2])
+apply (intro strip)
+apply (rule_tac p = "xb" in IssumE)
+apply simp
+apply simp
+apply (erule monofun_cfun_fun)
+apply simp
+done
+
+lemma monofun_Iwhen2: "monofun(Iwhen(f))"
+apply (unfold monofun)
+apply (intro strip)
+apply (rule less_fun [THEN iffD2])
+apply (intro strip)
+apply (rule_tac p = "xa" in IssumE)
+apply simp
+apply simp
+apply simp
+apply (erule monofun_cfun_fun)
+done
+
+lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))"
+apply (unfold monofun)
+apply (intro strip)
+apply (rule_tac p = "x" in IssumE)
+apply simp
+apply (rule_tac p = "y" in IssumE)
+apply simp
+apply (rule_tac P = "xa=UU" in notE)
+apply assumption
+apply (rule UU_I)
+apply (rule less_ssum3a [THEN iffD1])
+apply assumption
+apply simp
+apply (rule monofun_cfun_arg)
+apply (erule less_ssum3a [THEN iffD1])
+apply (simp del: Iwhen2)
+apply (rule_tac s = "UU" and t = "xa" in subst)
+apply (erule less_ssum3c [THEN iffD1, symmetric])
+apply simp
+apply (rule_tac p = "y" in IssumE)
+apply simp
+apply (simp only: less_ssum3d)
+apply (simp only: less_ssum3d)
+apply simp
+apply (rule monofun_cfun_arg)
+apply (erule less_ssum3b [THEN iffD1])
+done
+
+
+(* ------------------------------------------------------------------------ *)
+(* some kind of exhaustion rules for chains in 'a ++ 'b *)
+(* ------------------------------------------------------------------------ *)
+
+lemma ssum_lemma1: "[|~(!i.? x. Y(i::nat)=Isinl(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
--- 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]
--- 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