--- a/src/HOLCF/Ssum0.ML Tue Jul 04 14:58:40 2000 +0200
+++ b/src/HOLCF/Ssum0.ML Tue Jul 04 15:58:11 2000 +0200
@@ -10,23 +10,19 @@
(* A non-emptyness result for Sssum *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "SsumIl" Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
- (fn prems =>
- [
- (rtac CollectI 1),
- (rtac disjI1 1),
- (rtac exI 1),
- (rtac refl 1)
- ]);
+val prems = goalw Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum";
+by (rtac CollectI 1);
+by (rtac disjI1 1);
+by (rtac exI 1);
+by (rtac refl 1);
+qed "SsumIl";
-qed_goalw "SsumIr" Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
- (fn prems =>
- [
- (rtac CollectI 1),
- (rtac disjI2 1),
- (rtac exI 1),
- (rtac refl 1)
- ]);
+val prems = goalw Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum";
+by (rtac CollectI 1);
+by (rtac disjI2 1);
+by (rtac exI 1);
+by (rtac refl 1);
+qed "SsumIr";
Goal "inj_on Abs_Ssum Ssum";
by (rtac inj_on_inverseI 1);
@@ -37,58 +33,48 @@
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "strict_SinlSinr_Rep" Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
- "Sinl_Rep(UU) = Sinr_Rep(UU)"
- (fn prems =>
- [
- (rtac ext 1),
- (rtac ext 1),
- (rtac ext 1),
- (fast_tac HOL_cs 1)
- ]);
+val prems = goalw Ssum0.thy [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";
-qed_goalw "strict_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
- "Isinl(UU) = Isinr(UU)"
- (fn prems =>
- [
- (rtac (strict_SinlSinr_Rep RS arg_cong) 1)
- ]);
+val prems = goalw Ssum0.thy [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 *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "noteq_SinlSinr_Rep" Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
- "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
- (fn prems =>
- [
- (rtac conjI 1),
- (case_tac "a=UU" 1),
- (atac 1),
- (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2
- RS mp RS conjunct1 RS sym) 1),
- (fast_tac HOL_cs 1),
- (atac 1),
- (case_tac "b=UU" 1),
- (atac 1),
- (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1
- RS mp RS conjunct1 RS sym) 1),
- (fast_tac HOL_cs 1),
- (atac 1)
- ]);
+val prems = goalw Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
+ "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU";
+by (rtac conjI 1);
+by (case_tac "a=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+by (case_tac "b=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+qed "noteq_SinlSinr_Rep";
-qed_goalw "noteq_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
- "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac noteq_SinlSinr_Rep 1),
- (etac (inj_on_Abs_Ssum RS inj_onD) 1),
- (rtac SsumIl 1),
- (rtac SsumIr 1)
- ]);
+val prems = goalw Ssum0.thy [Isinl_def,Isinr_def]
+ "Isinl(a)=Isinr(b) ==> a=UU & b=UU";
+by (cut_facts_tac prems 1);
+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";
@@ -96,49 +82,37 @@
(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "inject_Sinl_Rep1" Ssum0.thy [Sinl_Rep_def]
- "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
- (fn prems =>
- [
- (case_tac "a=UU" 1),
- (atac 1),
- (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong
- RS iffD2 RS mp RS conjunct1 RS sym) 1),
- (fast_tac HOL_cs 1),
- (atac 1)
- ]);
+val prems = goalw Ssum0.thy [Sinl_Rep_def]
+ "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
+by (case_tac "a=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+qed "inject_Sinl_Rep1";
-qed_goalw "inject_Sinr_Rep1" Ssum0.thy [Sinr_Rep_def]
- "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
- (fn prems =>
- [
- (case_tac "b=UU" 1),
- (atac 1),
- (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong
- RS iffD2 RS mp RS conjunct1 RS sym) 1),
- (fast_tac HOL_cs 1),
- (atac 1)
- ]);
+val prems = goalw Ssum0.thy [Sinr_Rep_def]
+ "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
+by (case_tac "b=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+qed "inject_Sinr_Rep1";
-qed_goalw "inject_Sinl_Rep2" Ssum0.thy [Sinl_Rep_def]
-"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
- (fn prems =>
- [
- (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong
- RS iffD1 RS mp RS conjunct1) 1),
- (fast_tac HOL_cs 1),
- (resolve_tac prems 1)
- ]);
+val prems = goalw Ssum0.thy [Sinl_Rep_def]
+"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2";
+by (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1) 1);
+by (fast_tac HOL_cs 1);
+by (resolve_tac prems 1);
+qed "inject_Sinl_Rep2";
-qed_goalw "inject_Sinr_Rep2" Ssum0.thy [Sinr_Rep_def]
-"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
- (fn prems =>
- [
- (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong
- RS iffD1 RS mp RS conjunct1) 1),
- (fast_tac HOL_cs 1),
- (resolve_tac prems 1)
- ]);
+val prems = goalw Ssum0.thy [Sinr_Rep_def]
+"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2";
+by (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1) 1);
+by (fast_tac HOL_cs 1);
+by (resolve_tac prems 1);
+qed "inject_Sinr_Rep2";
Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
by (case_tac "a1=UU" 1);
@@ -166,27 +140,23 @@
by (atac 1);
qed "inject_Sinr_Rep";
-qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def]
-"Isinl(a1)=Isinl(a2)==> a1=a2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac inject_Sinl_Rep 1),
- (etac (inj_on_Abs_Ssum RS inj_onD) 1),
- (rtac SsumIl 1),
- (rtac SsumIl 1)
- ]);
+val prems = goalw Ssum0.thy [Isinl_def]
+"Isinl(a1)=Isinl(a2)==> a1=a2";
+by (cut_facts_tac prems 1);
+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";
-qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def]
-"Isinr(b1)=Isinr(b2) ==> b1=b2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac inject_Sinr_Rep 1),
- (etac (inj_on_Abs_Ssum RS inj_onD) 1),
- (rtac SsumIr 1),
- (rtac SsumIr 1)
- ]);
+val prems = goalw Ssum0.thy [Isinr_def]
+"Isinr(b1)=Isinr(b2) ==> b1=b2";
+by (cut_facts_tac prems 1);
+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";
Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
by (rtac contrapos 1);
@@ -205,46 +175,44 @@
(* choice of the bottom representation is arbitrary *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "Exh_Ssum" Ssum0.thy [Isinl_def,Isinr_def]
- "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"
- (fn prems =>
- [
- (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1),
- (etac disjE 1),
- (etac exE 1),
- (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
- (etac disjI1 1),
- (rtac disjI2 1),
- (rtac disjI1 1),
- (rtac exI 1),
- (rtac conjI 1),
- (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
- (etac arg_cong 1),
- (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1),
- (etac arg_cong 2),
- (etac contrapos 1),
- (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
- (rtac trans 1),
- (etac arg_cong 1),
- (etac arg_cong 1),
- (etac exE 1),
- (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
- (etac disjI1 1),
- (rtac disjI2 1),
- (rtac disjI2 1),
- (rtac exI 1),
- (rtac conjI 1),
- (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
- (etac arg_cong 1),
- (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1),
- (hyp_subst_tac 2),
- (rtac (strict_SinlSinr_Rep RS sym) 2),
- (etac contrapos 1),
- (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
- (rtac trans 1),
- (etac arg_cong 1),
- (etac arg_cong 1)
- ]);
+val prems = goalw Ssum0.thy [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 1);
+by (etac arg_cong 2);
+by (etac contrapos 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 1);
+by (hyp_subst_tac 2);
+by (rtac (strict_SinlSinr_Rep RS sym) 2);
+by (etac contrapos 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 ++ *)
@@ -282,83 +250,77 @@
(* rewrites for Iwhen *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "Iwhen1" Ssum0.thy [Iwhen_def]
- "Iwhen f g (Isinl UU) = UU"
- (fn prems =>
- [
- (rtac select_equality 1),
- (rtac conjI 1),
- (fast_tac HOL_cs 1),
- (rtac conjI 1),
- (strip_tac 1),
- (res_inst_tac [("P","a=UU")] notE 1),
- (fast_tac HOL_cs 1),
- (rtac inject_Isinl 1),
- (rtac sym 1),
- (fast_tac HOL_cs 1),
- (strip_tac 1),
- (res_inst_tac [("P","b=UU")] notE 1),
- (fast_tac HOL_cs 1),
- (rtac inject_Isinr 1),
- (rtac sym 1),
- (rtac (strict_IsinlIsinr RS subst) 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
+val prems = goalw Ssum0.thy [Iwhen_def]
+ "Iwhen f g (Isinl UU) = UU";
+by (rtac select_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";
-qed_goalw "Iwhen2" Ssum0.thy [Iwhen_def]
- "x~=UU ==> Iwhen f g (Isinl x) = f`x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac select_equality 1),
- (fast_tac HOL_cs 2),
- (rtac conjI 1),
- (strip_tac 1),
- (res_inst_tac [("P","x=UU")] notE 1),
- (atac 1),
- (rtac inject_Isinl 1),
- (atac 1),
- (rtac conjI 1),
- (strip_tac 1),
- (rtac cfun_arg_cong 1),
- (rtac inject_Isinl 1),
- (fast_tac HOL_cs 1),
- (strip_tac 1),
- (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1),
- (fast_tac HOL_cs 2),
- (rtac contrapos 1),
- (etac noteq_IsinlIsinr 2),
- (fast_tac HOL_cs 1)
- ]);
+val prems = goalw Ssum0.thy [Iwhen_def]
+ "x~=UU ==> Iwhen f g (Isinl x) = f`x";
+by (cut_facts_tac prems 1);
+by (rtac select_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 1);
+by (etac noteq_IsinlIsinr 2);
+by (fast_tac HOL_cs 1);
+qed "Iwhen2";
-qed_goalw "Iwhen3" Ssum0.thy [Iwhen_def]
- "y~=UU ==> Iwhen f g (Isinr y) = g`y"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac select_equality 1),
- (fast_tac HOL_cs 2),
- (rtac conjI 1),
- (strip_tac 1),
- (res_inst_tac [("P","y=UU")] notE 1),
- (atac 1),
- (rtac inject_Isinr 1),
- (rtac (strict_IsinlIsinr RS subst) 1),
- (atac 1),
- (rtac conjI 1),
- (strip_tac 1),
- (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1),
- (fast_tac HOL_cs 2),
- (rtac contrapos 1),
- (etac (sym RS noteq_IsinlIsinr) 2),
- (fast_tac HOL_cs 1),
- (strip_tac 1),
- (rtac cfun_arg_cong 1),
- (rtac inject_Isinr 1),
- (fast_tac HOL_cs 1)
- ]);
+val prems = goalw Ssum0.thy [Iwhen_def]
+ "y~=UU ==> Iwhen f g (Isinr y) = g`y";
+by (cut_facts_tac prems 1);
+by (rtac select_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 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 *)