src/HOLCF/Ssum0.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15568 41bfe19eabe2
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/Ssum0.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Strict sum with typedef
     6 *)
     7 
     8 (* ------------------------------------------------------------------------ *)
     9 (* A non-emptyness result for Sssum                                         *)
    10 (* ------------------------------------------------------------------------ *)
    11 
    12 Goalw [Ssum_def] "Sinl_Rep(a):Ssum";
    13 by (Blast_tac 1);
    14 qed "SsumIl";
    15 
    16 Goalw [Ssum_def] "Sinr_Rep(a):Ssum";
    17 by (Blast_tac 1);
    18 qed "SsumIr";
    19 
    20 Goal "inj_on Abs_Ssum Ssum";
    21 by (rtac inj_on_inverseI 1);
    22 by (etac Abs_Ssum_inverse 1);
    23 qed "inj_on_Abs_Ssum";
    24 
    25 (* ------------------------------------------------------------------------ *)
    26 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
    27 (* ------------------------------------------------------------------------ *)
    28 
    29 Goalw [Sinr_Rep_def,Sinl_Rep_def]
    30  "Sinl_Rep(UU) = Sinr_Rep(UU)";
    31 by (rtac ext 1);
    32 by (rtac ext 1);
    33 by (rtac ext 1);
    34 by (fast_tac HOL_cs 1);
    35 qed "strict_SinlSinr_Rep";
    36 
    37 Goalw [Isinl_def,Isinr_def]
    38  "Isinl(UU) = Isinr(UU)";
    39 by (rtac (strict_SinlSinr_Rep RS arg_cong) 1);
    40 qed "strict_IsinlIsinr";
    41 
    42 
    43 (* ------------------------------------------------------------------------ *)
    44 (* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
    45 (* ------------------------------------------------------------------------ *)
    46 
    47 Goalw [Sinl_Rep_def,Sinr_Rep_def]
    48         "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU";
    49 by (blast_tac (claset() addSDs [fun_cong]) 1);
    50 qed "noteq_SinlSinr_Rep";
    51 
    52 
    53 Goalw [Isinl_def,Isinr_def]
    54         "Isinl(a)=Isinr(b) ==> a=UU & b=UU";
    55 by (rtac noteq_SinlSinr_Rep 1);
    56 by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
    57 by (rtac SsumIl 1);
    58 by (rtac SsumIr 1);
    59 qed "noteq_IsinlIsinr";
    60 
    61 
    62 
    63 (* ------------------------------------------------------------------------ *)
    64 (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
    65 (* ------------------------------------------------------------------------ *)
    66 
    67 Goalw [Sinl_Rep_def] "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
    68 by (blast_tac (claset() addSDs [fun_cong]) 1);
    69 qed "inject_Sinl_Rep1";
    70 
    71 Goalw [Sinr_Rep_def] "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
    72 by (blast_tac (claset() addSDs [fun_cong]) 1);
    73 qed "inject_Sinr_Rep1";
    74 
    75 Goalw [Sinl_Rep_def]
    76 "[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2";
    77 by (blast_tac (claset() addSDs [fun_cong]) 1);
    78 qed "inject_Sinl_Rep2";
    79 
    80 Goalw [Sinr_Rep_def]
    81 "[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2";
    82 by (blast_tac (claset() addSDs [fun_cong]) 1);
    83 qed "inject_Sinr_Rep2";
    84 
    85 Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
    86 by (case_tac "a1=UU" 1);
    87 by (hyp_subst_tac 1);
    88 by (rtac (inject_Sinl_Rep1 RS sym) 1);
    89 by (etac sym 1);
    90 by (case_tac "a2=UU" 1);
    91 by (hyp_subst_tac 1);
    92 by (etac inject_Sinl_Rep1 1);
    93 by (etac inject_Sinl_Rep2 1);
    94 by (atac 1);
    95 by (atac 1);
    96 qed "inject_Sinl_Rep";
    97 
    98 Goal "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2";
    99 by (case_tac "b1=UU" 1);
   100 by (hyp_subst_tac 1);
   101 by (rtac (inject_Sinr_Rep1 RS sym) 1);
   102 by (etac sym 1);
   103 by (case_tac "b2=UU" 1);
   104 by (hyp_subst_tac 1);
   105 by (etac inject_Sinr_Rep1 1);
   106 by (etac inject_Sinr_Rep2 1);
   107 by (atac 1);
   108 by (atac 1);
   109 qed "inject_Sinr_Rep";
   110 
   111 Goalw [Isinl_def] "Isinl(a1)=Isinl(a2)==> a1=a2";
   112 by (rtac inject_Sinl_Rep 1);
   113 by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
   114 by (rtac SsumIl 1);
   115 by (rtac SsumIl 1);
   116 qed "inject_Isinl";
   117 
   118 Goalw [Isinr_def] "Isinr(b1)=Isinr(b2) ==> b1=b2";
   119 by (rtac inject_Sinr_Rep 1);
   120 by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
   121 by (rtac SsumIr 1);
   122 by (rtac SsumIr 1);
   123 qed "inject_Isinr";
   124 
   125 AddSDs [inject_Isinl, inject_Isinr];
   126 
   127 Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
   128 by (Blast_tac 1);
   129 qed "inject_Isinl_rev";
   130 
   131 Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)";
   132 by (Blast_tac 1);
   133 qed "inject_Isinr_rev";
   134 
   135 (* ------------------------------------------------------------------------ *)
   136 (* Exhaustion of the strict sum ++                                          *)
   137 (* choice of the bottom representation is arbitrary                         *)
   138 (* ------------------------------------------------------------------------ *)
   139 
   140 Goalw [Isinl_def,Isinr_def]
   141         "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)";
   142 by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1);
   143 by (etac disjE 1);
   144 by (etac exE 1);
   145 by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
   146 by (etac disjI1 1);
   147 by (rtac disjI2 1);
   148 by (rtac disjI1 1);
   149 by (rtac exI 1);
   150 by (rtac conjI 1);
   151 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
   152 by (etac arg_cong 1);
   153 by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos_nn 1);
   154 by (etac arg_cong 2);
   155 by (etac contrapos_nn 1);
   156 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
   157 by (rtac trans 1);
   158 by (etac arg_cong 1);
   159 by (etac arg_cong 1);
   160 by (etac exE 1);
   161 by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
   162 by (etac disjI1 1);
   163 by (rtac disjI2 1);
   164 by (rtac disjI2 1);
   165 by (rtac exI 1);
   166 by (rtac conjI 1);
   167 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
   168 by (etac arg_cong 1);
   169 by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos_nn 1);
   170 by (hyp_subst_tac 2);
   171 by (rtac (strict_SinlSinr_Rep RS sym) 2);
   172 by (etac contrapos_nn 1);
   173 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
   174 by (rtac trans 1);
   175 by (etac arg_cong 1);
   176 by (etac arg_cong 1);
   177 qed "Exh_Ssum";
   178 
   179 (* ------------------------------------------------------------------------ *)
   180 (* elimination rules for the strict sum ++                                  *)
   181 (* ------------------------------------------------------------------------ *)
   182 
   183 val prems = Goal
   184         "[|p=Isinl(UU) ==> Q ;\
   185 \       !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
   186 \       !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q";
   187 by (rtac (Exh_Ssum RS disjE) 1);
   188 by (etac disjE 2);
   189 by (eresolve_tac prems 1);
   190 by (etac exE 1);
   191 by (etac conjE 1);
   192 by (eresolve_tac prems 1);
   193 by (atac 1);
   194 by (etac exE 1);
   195 by (etac conjE 1);
   196 by (eresolve_tac prems 1);
   197 by (atac 1);
   198 qed "IssumE";
   199 
   200 val prems = Goal
   201 "[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q";
   202 by (rtac IssumE 1);
   203 by (eresolve_tac prems 1);
   204 by (eresolve_tac prems 1);
   205 by (eresolve_tac prems 1);
   206 qed "IssumE2";
   207 
   208 
   209 
   210 
   211 (* ------------------------------------------------------------------------ *)
   212 (* rewrites for Iwhen                                                       *)
   213 (* ------------------------------------------------------------------------ *)
   214 
   215 Goalw [Iwhen_def]
   216         "Iwhen f g (Isinl UU) = UU";
   217 by (rtac some_equality 1);
   218 by (rtac conjI 1);
   219 by (fast_tac HOL_cs  1);
   220 by (rtac conjI 1);
   221 by (strip_tac 1);
   222 by (res_inst_tac [("P","a=UU")] notE 1);
   223 by (fast_tac HOL_cs  1);
   224 by (rtac inject_Isinl 1);
   225 by (rtac sym 1);
   226 by (fast_tac HOL_cs  1);
   227 by (strip_tac 1);
   228 by (res_inst_tac [("P","b=UU")] notE 1);
   229 by (fast_tac HOL_cs  1);
   230 by (rtac inject_Isinr 1);
   231 by (rtac sym 1);
   232 by (rtac (strict_IsinlIsinr RS subst) 1);
   233 by (fast_tac HOL_cs  1);
   234 by (fast_tac HOL_cs  1);
   235 qed "Iwhen1";
   236 
   237 
   238 Goalw [Iwhen_def]
   239         "x~=UU ==> Iwhen f g (Isinl x) = f$x";
   240 by (rtac some_equality 1);
   241 by (fast_tac HOL_cs  2);
   242 by (rtac conjI 1);
   243 by (strip_tac 1);
   244 by (res_inst_tac [("P","x=UU")] notE 1);
   245 by (atac 1);
   246 by (rtac inject_Isinl 1);
   247 by (atac 1);
   248 by (rtac conjI 1);
   249 by (strip_tac 1);
   250 by (rtac cfun_arg_cong 1);
   251 by (rtac inject_Isinl 1);
   252 by (fast_tac HOL_cs  1);
   253 by (strip_tac 1);
   254 by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1);
   255 by (fast_tac HOL_cs  2);
   256 by (rtac contrapos_nn 1);
   257 by (etac noteq_IsinlIsinr 2);
   258 by (fast_tac HOL_cs  1);
   259 qed "Iwhen2";
   260 
   261 Goalw [Iwhen_def]
   262         "y~=UU ==> Iwhen f g (Isinr y) = g$y";
   263 by (rtac some_equality 1);
   264 by (fast_tac HOL_cs  2);
   265 by (rtac conjI 1);
   266 by (strip_tac 1);
   267 by (res_inst_tac [("P","y=UU")] notE 1);
   268 by (atac 1);
   269 by (rtac inject_Isinr 1);
   270 by (rtac (strict_IsinlIsinr RS subst) 1);
   271 by (atac 1);
   272 by (rtac conjI 1);
   273 by (strip_tac 1);
   274 by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1);
   275 by (fast_tac HOL_cs  2);
   276 by (rtac contrapos_nn 1);
   277 by (etac (sym RS noteq_IsinlIsinr) 2);
   278 by (fast_tac HOL_cs  1);
   279 by (strip_tac 1);
   280 by (rtac cfun_arg_cong 1);
   281 by (rtac inject_Isinr 1);
   282 by (fast_tac HOL_cs  1);
   283 qed "Iwhen3";
   284 
   285 (* ------------------------------------------------------------------------ *)
   286 (* instantiate the simplifier                                               *)
   287 (* ------------------------------------------------------------------------ *)
   288 
   289 val Ssum0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] addsimps 
   290                 [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
   291 
   292 Addsimps [strict_IsinlIsinr RS sym, Iwhen1, Iwhen2, Iwhen3];