Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Ssum1.ML
changeset 9169 85a47aa21f74
parent 4535 f24cebc299e4
child 9245 428385c4bc50
equal deleted inserted replaced
9168:77658111e122 9169:85a47aa21f74 
     1 (*  Title:      HOLCF/Ssum1.ML
 
     1 (*  Title:      HOLCF/Ssum1.ML
 
     2     ID:         $Id$
 
     2     ID:         $Id$
 
     3     Author:     Franz Regensburger
 
     3     Author:     Franz Regensburger
 
     4     Copyright   1993  Technische Universitaet Muenchen
 
     4     Copyright   1993  Technische Universitaet Muenchen
 
     5 
     5 
     6 Lemmas for theory Ssum1.thy
 
     6 Partial ordering for the strict sum ++
 
     7 *)
 
     7 *)
 
     8 
       
     9 open Ssum1;
 
       
    10 
     8 
    11 local 
     9 local 
    12 
    10 
    13 fun eq_left s1 s2 = 
    11 fun eq_left s1 s2 = 
    14         (
 
    12         (
 
   210 
   208 
   211 (* ------------------------------------------------------------------------ *)
 
   209 (* ------------------------------------------------------------------------ *)
 
   212 (* optimize lemmas about less_ssum                                          *)
 
   210 (* optimize lemmas about less_ssum                                          *)
 
   213 (* ------------------------------------------------------------------------ *)
 
   211 (* ------------------------------------------------------------------------ *)
 
   214 
   212 
   215 qed_goal "less_ssum2a" thy 
   213 Goal "(Isinl x) << (Isinl y) = (x << y)";
 
   216         "(Isinl x) << (Isinl y) = (x << y)"
 
   214 by (rtac less_ssum1a 1);
 
   217  (fn prems =>
 
   215 by (rtac refl 1);
 
   218         [
 
   216 by (rtac refl 1);
 
   219         (rtac less_ssum1a 1),
 
   217 qed "less_ssum2a";
 
   220         (rtac refl 1),
 
   218 
   221         (rtac refl 1)
 
   219 Goal "(Isinr x) << (Isinr y) = (x << y)";
 
   222         ]);
 
   220 by (rtac less_ssum1b 1);
 
   223 
   221 by (rtac refl 1);
 
   224 qed_goal "less_ssum2b" thy 
   222 by (rtac refl 1);
 
   225         "(Isinr x) << (Isinr y) = (x << y)"
 
   223 qed "less_ssum2b";
 
   226  (fn prems =>
 
   224 
   227         [
 
   225 Goal "(Isinl x) << (Isinr y) = (x = UU)";
 
   228         (rtac less_ssum1b 1),
 
   226 by (rtac less_ssum1c 1);
 
   229         (rtac refl 1),
 
   227 by (rtac refl 1);
 
   230         (rtac refl 1)
 
   228 by (rtac refl 1);
 
   231         ]);
 
   229 qed "less_ssum2c";
 
   232 
   230 
   233 qed_goal "less_ssum2c" thy 
   231 Goal "(Isinr x) << (Isinl y) = (x = UU)";
 
   234         "(Isinl x) << (Isinr y) = (x = UU)"
 
   232 by (rtac less_ssum1d 1);
 
   235  (fn prems =>
 
   233 by (rtac refl 1);
 
   236         [
 
   234 by (rtac refl 1);
 
   237         (rtac less_ssum1c 1),
 
   235 qed "less_ssum2d";
 
   238         (rtac refl 1),
 
       
   239         (rtac refl 1)
 
       
   240         ]);
 
       
   241 
       
   242 qed_goal "less_ssum2d" thy 
       
   243         "(Isinr x) << (Isinl y) = (x = UU)"
 
       
   244  (fn prems =>
 
       
   245         [
 
       
   246         (rtac less_ssum1d 1),
 
       
   247         (rtac refl 1),
 
       
   248         (rtac refl 1)
 
       
   249         ]);
 
       
   250 
   236 
   251 
   237 
   252 (* ------------------------------------------------------------------------ *)
 
   238 (* ------------------------------------------------------------------------ *)
 
   253 (* less_ssum is a partial order on ++                                     *)
 
   239 (* less_ssum is a partial order on ++                                     *)
 
   254 (* ------------------------------------------------------------------------ *)
 
   240 (* ------------------------------------------------------------------------ *)
 
   255 
   241 
   256 qed_goal "refl_less_ssum" thy "(p::'a++'b) << p"
 
   242 Goal "(p::'a++'b) << p";
 
   257  (fn prems =>
 
   243 by (res_inst_tac [("p","p")] IssumE2 1);
 
   258         [
 
   244 by (hyp_subst_tac 1);
 
   259         (res_inst_tac [("p","p")] IssumE2 1),
 
   245 by (rtac (less_ssum2a RS iffD2) 1);
 
   260         (hyp_subst_tac 1),
 
   246 by (rtac refl_less 1);
 
   261         (rtac (less_ssum2a RS iffD2) 1),
 
   247 by (hyp_subst_tac 1);
 
   262         (rtac refl_less 1),
 
   248 by (rtac (less_ssum2b RS iffD2) 1);
 
   263         (hyp_subst_tac 1),
 
   249 by (rtac refl_less 1);
 
   264         (rtac (less_ssum2b RS iffD2) 1),
 
   250 qed "refl_less_ssum";
 
   265         (rtac refl_less 1)
 
   251 
   266         ]);
 
   252 Goal "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2";
 
   267 
   253 by (res_inst_tac [("p","p1")] IssumE2 1);
 
   268 qed_goal "antisym_less_ssum" thy 
   254 by (hyp_subst_tac 1);
 
   269  "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
 
   255 by (res_inst_tac [("p","p2")] IssumE2 1);
 
   270  (fn prems =>
 
   256 by (hyp_subst_tac 1);
 
   271         [
 
   257 by (res_inst_tac [("f","Isinl")] arg_cong 1);
 
   272         (cut_facts_tac prems 1),
 
   258 by (rtac antisym_less 1);
 
   273         (res_inst_tac [("p","p1")] IssumE2 1),
 
   259 by (etac (less_ssum2a RS iffD1) 1);
 
   274         (hyp_subst_tac 1),
 
   260 by (etac (less_ssum2a RS iffD1) 1);
 
   275         (res_inst_tac [("p","p2")] IssumE2 1),
 
   261 by (hyp_subst_tac 1);
 
   276         (hyp_subst_tac 1),
 
   262 by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
 
   277         (res_inst_tac [("f","Isinl")] arg_cong 1),
 
   263 by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
 
   278         (rtac antisym_less 1),
 
   264 by (rtac strict_IsinlIsinr 1);
 
   279         (etac (less_ssum2a RS iffD1) 1),
 
   265 by (hyp_subst_tac 1);
 
   280         (etac (less_ssum2a RS iffD1) 1),
 
   266 by (res_inst_tac [("p","p2")] IssumE2 1);
 
   281         (hyp_subst_tac 1),
 
   267 by (hyp_subst_tac 1);
 
   282         (etac (less_ssum2d RS iffD1 RS ssubst) 1),
 
   268 by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
 
   283         (etac (less_ssum2c RS iffD1 RS ssubst) 1),
 
   269 by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
 
   284         (rtac strict_IsinlIsinr 1),
 
   270 by (rtac (strict_IsinlIsinr RS sym) 1);
 
   285         (hyp_subst_tac 1),
 
   271 by (hyp_subst_tac 1);
 
   286         (res_inst_tac [("p","p2")] IssumE2 1),
 
   272 by (res_inst_tac [("f","Isinr")] arg_cong 1);
 
   287         (hyp_subst_tac 1),
 
   273 by (rtac antisym_less 1);
 
   288         (etac (less_ssum2c RS iffD1 RS ssubst) 1),
 
   274 by (etac (less_ssum2b RS iffD1) 1);
 
   289         (etac (less_ssum2d RS iffD1 RS ssubst) 1),
 
   275 by (etac (less_ssum2b RS iffD1) 1);
 
   290         (rtac (strict_IsinlIsinr RS sym) 1),
 
   276 qed "antisym_less_ssum";
 
   291         (hyp_subst_tac 1),
 
   277 
   292         (res_inst_tac [("f","Isinr")] arg_cong 1),
 
   278 Goal "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3";
 
   293         (rtac antisym_less 1),
 
   279 by (res_inst_tac [("p","p1")] IssumE2 1);
 
   294         (etac (less_ssum2b RS iffD1) 1),
 
   280 by (hyp_subst_tac 1);
 
   295         (etac (less_ssum2b RS iffD1) 1)
 
   281 by (res_inst_tac [("p","p3")] IssumE2 1);
 
   296         ]);
 
   282 by (hyp_subst_tac 1);
 
   297 
   283 by (rtac (less_ssum2a RS iffD2) 1);
 
   298 qed_goal "trans_less_ssum" thy 
   284 by (res_inst_tac [("p","p2")] IssumE2 1);
 
   299  "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
 
   285 by (hyp_subst_tac 1);
 
   300  (fn prems =>
 
   286 by (rtac trans_less 1);
 
   301         [
 
   287 by (etac (less_ssum2a RS iffD1) 1);
 
   302         (cut_facts_tac prems 1),
 
   288 by (etac (less_ssum2a RS iffD1) 1);
 
   303         (res_inst_tac [("p","p1")] IssumE2 1),
 
   289 by (hyp_subst_tac 1);
 
   304         (hyp_subst_tac 1),
 
   290 by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
 
   305         (res_inst_tac [("p","p3")] IssumE2 1),
 
   291 by (rtac minimal 1);
 
   306         (hyp_subst_tac 1),
 
   292 by (hyp_subst_tac 1);
 
   307         (rtac (less_ssum2a RS iffD2) 1),
 
   293 by (rtac (less_ssum2c RS iffD2) 1);
 
   308         (res_inst_tac [("p","p2")] IssumE2 1),
 
   294 by (res_inst_tac [("p","p2")] IssumE2 1);
 
   309         (hyp_subst_tac 1),
 
   295 by (hyp_subst_tac 1);
 
   310         (rtac trans_less 1),
 
   296 by (rtac UU_I 1);
 
   311         (etac (less_ssum2a RS iffD1) 1),
 
   297 by (rtac trans_less 1);
 
   312         (etac (less_ssum2a RS iffD1) 1),
 
   298 by (etac (less_ssum2a RS iffD1) 1);
 
   313         (hyp_subst_tac 1),
 
   299 by (rtac (antisym_less_inverse RS conjunct1) 1);
 
   314         (etac (less_ssum2c RS iffD1 RS ssubst) 1),
 
   300 by (etac (less_ssum2c RS iffD1) 1);
 
   315         (rtac minimal 1),
 
   301 by (hyp_subst_tac 1);
 
   316         (hyp_subst_tac 1),
 
   302 by (etac (less_ssum2c RS iffD1) 1);
 
   317         (rtac (less_ssum2c RS iffD2) 1),
 
   303 by (hyp_subst_tac 1);
 
   318         (res_inst_tac [("p","p2")] IssumE2 1),
 
   304 by (res_inst_tac [("p","p3")] IssumE2 1);
 
   319         (hyp_subst_tac 1),
 
   305 by (hyp_subst_tac 1);
 
   320         (rtac UU_I 1),
 
   306 by (rtac (less_ssum2d RS iffD2) 1);
 
   321         (rtac trans_less 1),
 
   307 by (res_inst_tac [("p","p2")] IssumE2 1);
 
   322         (etac (less_ssum2a RS iffD1) 1),
 
   308 by (hyp_subst_tac 1);
 
   323         (rtac (antisym_less_inverse RS conjunct1) 1),
 
   309 by (etac (less_ssum2d RS iffD1) 1);
 
   324         (etac (less_ssum2c RS iffD1) 1),
 
   310 by (hyp_subst_tac 1);
 
   325         (hyp_subst_tac 1),
 
   311 by (rtac UU_I 1);
 
   326         (etac (less_ssum2c RS iffD1) 1),
 
   312 by (rtac trans_less 1);
 
   327         (hyp_subst_tac 1),
 
   313 by (etac (less_ssum2b RS iffD1) 1);
 
   328         (res_inst_tac [("p","p3")] IssumE2 1),
 
   314 by (rtac (antisym_less_inverse RS conjunct1) 1);
 
   329         (hyp_subst_tac 1),
 
   315 by (etac (less_ssum2d RS iffD1) 1);
 
   330         (rtac (less_ssum2d RS iffD2) 1),
 
   316 by (hyp_subst_tac 1);
 
   331         (res_inst_tac [("p","p2")] IssumE2 1),
 
   317 by (rtac (less_ssum2b RS iffD2) 1);
 
   332         (hyp_subst_tac 1),
 
   318 by (res_inst_tac [("p","p2")] IssumE2 1);
 
   333         (etac (less_ssum2d RS iffD1) 1),
 
   319 by (hyp_subst_tac 1);
 
   334         (hyp_subst_tac 1),
 
   320 by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
 
   335         (rtac UU_I 1),
 
   321 by (rtac minimal 1);
 
   336         (rtac trans_less 1),
 
   322 by (hyp_subst_tac 1);
 
   337         (etac (less_ssum2b RS iffD1) 1),
 
   323 by (rtac trans_less 1);
 
   338         (rtac (antisym_less_inverse RS conjunct1) 1),
 
   324 by (etac (less_ssum2b RS iffD1) 1);
 
   339         (etac (less_ssum2d RS iffD1) 1),
 
   325 by (etac (less_ssum2b RS iffD1) 1);
 
   340         (hyp_subst_tac 1),
 
   326 qed "trans_less_ssum";
 
   341         (rtac (less_ssum2b RS iffD2) 1),
 
   327 
   342         (res_inst_tac [("p","p2")] IssumE2 1),
 
   328 
   343         (hyp_subst_tac 1),
 
   329 
   344         (etac (less_ssum2d RS iffD1 RS ssubst) 1),
 
       
   345         (rtac minimal 1),
 
       
   346         (hyp_subst_tac 1),
 
       
   347         (rtac trans_less 1),
 
       
   348         (etac (less_ssum2b RS iffD1) 1),
 
       
   349         (etac (less_ssum2b RS iffD1) 1)
 
       
   350         ]);
 
       
   351 
       
   352 
       
   353
isabelle