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