src/HOLCF/Ssum1.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4535 f24cebc299e4
child 9169 85a47aa21f74
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Ssum1.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory Ssum1.thy
     7 *)
     8 
     9 open Ssum1;
    10 
    11 local 
    12 
    13 fun eq_left s1 s2 = 
    14         (
    15         (res_inst_tac [("s",s1),("t",s2)] (inject_Isinl RS subst) 1)
    16         THEN    (rtac trans 1)
    17         THEN    (atac 2)
    18         THEN    (etac sym 1));
    19 
    20 fun eq_right s1 s2 = 
    21         (
    22         (res_inst_tac [("s",s1),("t",s2)] (inject_Isinr RS subst) 1)
    23         THEN    (rtac trans 1)
    24         THEN    (atac 2)
    25         THEN    (etac sym 1));
    26 
    27 fun UU_left s1 = 
    28         (
    29         (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct1 RS ssubst)1)
    30         THEN (rtac trans 1)
    31         THEN (atac 2)
    32         THEN (etac sym 1));
    33 
    34 fun UU_right s1 = 
    35         (
    36         (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1)
    37         THEN (rtac trans 1)
    38         THEN (atac 2)
    39         THEN (etac sym 1))
    40 
    41 in
    42 
    43 val less_ssum1a = prove_goalw thy [less_ssum_def]
    44 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
    45  (fn prems =>
    46         [
    47         (cut_facts_tac prems 1),
    48         (rtac select_equality 1),
    49         (dtac conjunct1 2),
    50         (dtac spec 2),
    51         (dtac spec 2),
    52         (etac mp 2),
    53         (fast_tac HOL_cs 2),
    54         (rtac conjI 1),
    55         (strip_tac 1),
    56         (etac conjE 1),
    57         (eq_left "x" "u"),
    58         (eq_left "y" "xa"),
    59         (rtac refl 1),
    60         (rtac conjI 1),
    61         (strip_tac 1),
    62         (etac conjE 1),
    63         (UU_left "x"),
    64         (UU_right "v"),
    65         (Simp_tac 1),
    66         (rtac conjI 1),
    67         (strip_tac 1),
    68         (etac conjE 1),
    69         (eq_left "x" "u"),
    70         (UU_left "y"),
    71         (rtac iffI 1),
    72         (etac UU_I 1),
    73         (res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
    74         (atac 1),
    75         (rtac refl_less 1),
    76         (strip_tac 1),
    77         (etac conjE 1),
    78         (UU_left "x"),
    79         (UU_right "v"),
    80         (Simp_tac 1)
    81         ]);
    82 
    83 
    84 val less_ssum1b = prove_goalw thy [less_ssum_def]
    85 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
    86  (fn prems =>
    87         [
    88         (cut_facts_tac prems 1),
    89         (rtac select_equality 1),
    90         (dtac conjunct2 2),
    91         (dtac conjunct1 2),
    92         (dtac spec 2),
    93         (dtac spec 2),
    94         (etac mp 2),
    95         (fast_tac HOL_cs 2),
    96         (rtac conjI 1),
    97         (strip_tac 1),
    98         (etac conjE 1),
    99         (UU_right "x"),
   100         (UU_left "u"),
   101         (Simp_tac 1),
   102         (rtac conjI 1),
   103         (strip_tac 1),
   104         (etac conjE 1),
   105         (eq_right "x" "v"),
   106         (eq_right "y" "ya"),
   107         (rtac refl 1),
   108         (rtac conjI 1),
   109         (strip_tac 1),
   110         (etac conjE 1),
   111         (UU_right "x"),
   112         (UU_left "u"),
   113         (Simp_tac 1),
   114         (strip_tac 1),
   115         (etac conjE 1),
   116         (eq_right "x" "v"),
   117         (UU_right "y"),
   118         (rtac iffI 1),
   119         (etac UU_I 1),
   120         (res_inst_tac [("s","UU::'b"),("t","x")] subst 1),
   121         (etac sym 1),
   122         (rtac refl_less 1)
   123         ]);
   124 
   125 
   126 val less_ssum1c = prove_goalw thy [less_ssum_def]
   127 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
   128  (fn prems =>
   129         [
   130         (cut_facts_tac prems 1),
   131         (rtac select_equality 1),
   132         (rtac conjI 1),
   133         (strip_tac 1),
   134         (etac conjE 1),
   135         (eq_left  "x" "u"),
   136         (UU_left "xa"),
   137         (rtac iffI 1),
   138         (res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
   139         (atac 1),
   140         (rtac refl_less 1),
   141         (etac UU_I 1),
   142         (rtac conjI 1),
   143         (strip_tac 1),
   144         (etac conjE 1),
   145         (UU_left "x"),
   146         (UU_right "v"),
   147         (Simp_tac 1),
   148         (rtac conjI 1),
   149         (strip_tac 1),
   150         (etac conjE 1),
   151         (eq_left  "x" "u"),
   152         (rtac refl 1),
   153         (strip_tac 1),
   154         (etac conjE 1),
   155         (UU_left "x"),
   156         (UU_right "v"),
   157         (Simp_tac 1),
   158         (dtac conjunct2 1),
   159         (dtac conjunct2 1),
   160         (dtac conjunct1 1),
   161         (dtac spec 1),
   162         (dtac spec 1),
   163         (etac mp 1),
   164         (fast_tac HOL_cs 1)
   165         ]);
   166 
   167 
   168 val less_ssum1d = prove_goalw thy [less_ssum_def]
   169 "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
   170  (fn prems =>
   171         [
   172         (cut_facts_tac prems 1),
   173         (rtac select_equality 1),
   174         (dtac conjunct2 2),
   175         (dtac conjunct2 2),
   176         (dtac conjunct2 2),
   177         (dtac spec 2),
   178         (dtac spec 2),
   179         (etac mp 2),
   180         (fast_tac HOL_cs 2),
   181         (rtac conjI 1),
   182         (strip_tac 1),
   183         (etac conjE 1),
   184         (UU_right "x"),
   185         (UU_left "u"),
   186         (Simp_tac 1),
   187         (rtac conjI 1),
   188         (strip_tac 1),
   189         (etac conjE 1),
   190         (UU_right "ya"),
   191         (eq_right "x" "v"),
   192         (rtac iffI 1),
   193         (etac UU_I 2),
   194         (res_inst_tac [("s","UU"),("t","x")] subst 1),
   195         (etac sym 1),
   196         (rtac refl_less 1),
   197         (rtac conjI 1),
   198         (strip_tac 1),
   199         (etac conjE 1),
   200         (UU_right "x"),
   201         (UU_left "u"),
   202         (Simp_tac 1),
   203         (strip_tac 1),
   204         (etac conjE 1),
   205         (eq_right "x" "v"),
   206         (rtac refl 1)
   207         ])
   208 end;
   209 
   210 
   211 (* ------------------------------------------------------------------------ *)
   212 (* optimize lemmas about less_ssum                                          *)
   213 (* ------------------------------------------------------------------------ *)
   214 
   215 qed_goal "less_ssum2a" thy 
   216         "(Isinl x) << (Isinl y) = (x << y)"
   217  (fn prems =>
   218         [
   219         (rtac less_ssum1a 1),
   220         (rtac refl 1),
   221         (rtac refl 1)
   222         ]);
   223 
   224 qed_goal "less_ssum2b" thy 
   225         "(Isinr x) << (Isinr y) = (x << y)"
   226  (fn prems =>
   227         [
   228         (rtac less_ssum1b 1),
   229         (rtac refl 1),
   230         (rtac refl 1)
   231         ]);
   232 
   233 qed_goal "less_ssum2c" thy 
   234         "(Isinl x) << (Isinr y) = (x = UU)"
   235  (fn prems =>
   236         [
   237         (rtac less_ssum1c 1),
   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 
   251 
   252 (* ------------------------------------------------------------------------ *)
   253 (* less_ssum is a partial order on ++                                     *)
   254 (* ------------------------------------------------------------------------ *)
   255 
   256 qed_goal "refl_less_ssum" thy "(p::'a++'b) << p"
   257  (fn prems =>
   258         [
   259         (res_inst_tac [("p","p")] IssumE2 1),
   260         (hyp_subst_tac 1),
   261         (rtac (less_ssum2a RS iffD2) 1),
   262         (rtac refl_less 1),
   263         (hyp_subst_tac 1),
   264         (rtac (less_ssum2b RS iffD2) 1),
   265         (rtac refl_less 1)
   266         ]);
   267 
   268 qed_goal "antisym_less_ssum" thy 
   269  "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
   270  (fn prems =>
   271         [
   272         (cut_facts_tac prems 1),
   273         (res_inst_tac [("p","p1")] IssumE2 1),
   274         (hyp_subst_tac 1),
   275         (res_inst_tac [("p","p2")] IssumE2 1),
   276         (hyp_subst_tac 1),
   277         (res_inst_tac [("f","Isinl")] arg_cong 1),
   278         (rtac antisym_less 1),
   279         (etac (less_ssum2a RS iffD1) 1),
   280         (etac (less_ssum2a RS iffD1) 1),
   281         (hyp_subst_tac 1),
   282         (etac (less_ssum2d RS iffD1 RS ssubst) 1),
   283         (etac (less_ssum2c RS iffD1 RS ssubst) 1),
   284         (rtac strict_IsinlIsinr 1),
   285         (hyp_subst_tac 1),
   286         (res_inst_tac [("p","p2")] IssumE2 1),
   287         (hyp_subst_tac 1),
   288         (etac (less_ssum2c RS iffD1 RS ssubst) 1),
   289         (etac (less_ssum2d RS iffD1 RS ssubst) 1),
   290         (rtac (strict_IsinlIsinr RS sym) 1),
   291         (hyp_subst_tac 1),
   292         (res_inst_tac [("f","Isinr")] arg_cong 1),
   293         (rtac antisym_less 1),
   294         (etac (less_ssum2b RS iffD1) 1),
   295         (etac (less_ssum2b RS iffD1) 1)
   296         ]);
   297 
   298 qed_goal "trans_less_ssum" thy 
   299  "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
   300  (fn prems =>
   301         [
   302         (cut_facts_tac prems 1),
   303         (res_inst_tac [("p","p1")] IssumE2 1),
   304         (hyp_subst_tac 1),
   305         (res_inst_tac [("p","p3")] IssumE2 1),
   306         (hyp_subst_tac 1),
   307         (rtac (less_ssum2a RS iffD2) 1),
   308         (res_inst_tac [("p","p2")] IssumE2 1),
   309         (hyp_subst_tac 1),
   310         (rtac trans_less 1),
   311         (etac (less_ssum2a RS iffD1) 1),
   312         (etac (less_ssum2a RS iffD1) 1),
   313         (hyp_subst_tac 1),
   314         (etac (less_ssum2c RS iffD1 RS ssubst) 1),
   315         (rtac minimal 1),
   316         (hyp_subst_tac 1),
   317         (rtac (less_ssum2c RS iffD2) 1),
   318         (res_inst_tac [("p","p2")] IssumE2 1),
   319         (hyp_subst_tac 1),
   320         (rtac UU_I 1),
   321         (rtac trans_less 1),
   322         (etac (less_ssum2a RS iffD1) 1),
   323         (rtac (antisym_less_inverse RS conjunct1) 1),
   324         (etac (less_ssum2c RS iffD1) 1),
   325         (hyp_subst_tac 1),
   326         (etac (less_ssum2c RS iffD1) 1),
   327         (hyp_subst_tac 1),
   328         (res_inst_tac [("p","p3")] IssumE2 1),
   329         (hyp_subst_tac 1),
   330         (rtac (less_ssum2d RS iffD2) 1),
   331         (res_inst_tac [("p","p2")] IssumE2 1),
   332         (hyp_subst_tac 1),
   333         (etac (less_ssum2d RS iffD1) 1),
   334         (hyp_subst_tac 1),
   335         (rtac UU_I 1),
   336         (rtac trans_less 1),
   337         (etac (less_ssum2b RS iffD1) 1),
   338         (rtac (antisym_less_inverse RS conjunct1) 1),
   339         (etac (less_ssum2d RS iffD1) 1),
   340         (hyp_subst_tac 1),
   341         (rtac (less_ssum2b RS iffD2) 1),
   342         (res_inst_tac [("p","p2")] IssumE2 1),
   343         (hyp_subst_tac 1),
   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