src/HOLCF/Ssum1.ML
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 1461
diff changeset
     1
(*  Title:      HOLCF/Ssum1.ML
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
     3
    Author:     Franz Regensburger
12030
wenzelm
parents: 9969
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
     6
Partial ordering for the strict sum ++
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
fun eq_left s1 s2 = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    10
        (
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    11
        (res_inst_tac [("s",s1),("t",s2)] (inject_Isinl RS subst) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    12
        THEN    (rtac trans 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    13
        THEN    (atac 2)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    14
        THEN    (etac sym 1));
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
fun eq_right s1 s2 = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    17
        (
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    18
        (res_inst_tac [("s",s1),("t",s2)] (inject_Isinr RS subst) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    19
        THEN    (rtac trans 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    20
        THEN    (atac 2)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    21
        THEN    (etac sym 1));
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    22
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    23
fun UU_left s1 = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    24
        (
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    25
        (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct1 RS ssubst)1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    26
        THEN (rtac trans 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    27
        THEN (atac 2)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    28
        THEN (etac sym 1));
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    29
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    30
fun UU_right s1 = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    31
        (
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    32
        (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    33
        THEN (rtac trans 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    34
        THEN (atac 2)
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    35
        THEN (etac sym 1));
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    36
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    37
Goalw [less_ssum_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    38
"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)";
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9248
diff changeset
    39
by (rtac some_equality 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    40
by (dtac conjunct1 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    41
by (dtac spec 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    42
by (dtac spec 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    43
by (etac mp 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    44
by (fast_tac HOL_cs 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    45
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    46
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    47
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    48
by (eq_left "x" "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    49
by (eq_left "y" "xa");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    50
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    51
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    52
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    53
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    54
by (UU_left "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    55
by (UU_right "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    56
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    57
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    58
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    59
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    60
by (eq_left "x" "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    61
by (UU_left "y");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    62
by (rtac iffI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    63
by (etac UU_I 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    64
by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    65
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    66
by (rtac refl_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    67
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    68
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    69
by (UU_left "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    70
by (UU_right "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    71
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    72
qed "less_ssum1a";
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    73
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    74
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    75
Goalw [less_ssum_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    76
"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)";
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9248
diff changeset
    77
by (rtac some_equality 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    78
by (dtac conjunct2 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    79
by (dtac conjunct1 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    80
by (dtac spec 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    81
by (dtac spec 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    82
by (etac mp 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    83
by (fast_tac HOL_cs 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    84
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    85
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    86
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    87
by (UU_right "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    88
by (UU_left "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    89
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    90
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    91
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    92
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    93
by (eq_right "x" "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    94
by (eq_right "y" "ya");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    95
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    96
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    97
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    98
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
    99
by (UU_right "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   100
by (UU_left "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   101
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   102
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   103
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   104
by (eq_right "x" "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   105
by (UU_right "y");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   106
by (rtac iffI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   107
by (etac UU_I 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   108
by (res_inst_tac [("s","UU::'b"),("t","x")] subst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   109
by (etac sym 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   110
by (rtac refl_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   111
qed "less_ssum1b";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   112
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   113
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   114
Goalw [less_ssum_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   115
"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)";
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9248
diff changeset
   116
by (rtac some_equality 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   117
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   118
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   119
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   120
by (eq_left  "x" "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   121
by (UU_left "xa");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   122
by (rtac iffI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   123
by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   124
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   125
by (rtac refl_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   126
by (etac UU_I 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   127
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   128
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   129
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   130
by (UU_left "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   131
by (UU_right "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   132
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   133
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   134
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   135
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   136
by (eq_left  "x" "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   137
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   138
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   139
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   140
by (UU_left "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   141
by (UU_right "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   142
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   143
by (dtac conjunct2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   144
by (dtac conjunct2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   145
by (dtac conjunct1 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   146
by (dtac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   147
by (dtac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   148
by (etac mp 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   149
by (fast_tac HOL_cs 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   150
qed "less_ssum1c";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   151
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   152
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   153
Goalw [less_ssum_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   154
"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)";
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9248
diff changeset
   155
by (rtac some_equality 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   156
by (dtac conjunct2 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   157
by (dtac conjunct2 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   158
by (dtac conjunct2 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   159
by (dtac spec 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   160
by (dtac spec 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   161
by (etac mp 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   162
by (fast_tac HOL_cs 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   163
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   164
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   165
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   166
by (UU_right "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   167
by (UU_left "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   168
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   169
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   170
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   171
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   172
by (UU_right "ya");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   173
by (eq_right "x" "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   174
by (rtac iffI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   175
by (etac UU_I 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   176
by (res_inst_tac [("s","UU"),("t","x")] subst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   177
by (etac sym 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   178
by (rtac refl_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   179
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   180
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   181
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   182
by (UU_right "x");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   183
by (UU_left "u");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   184
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   185
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   186
by (etac conjE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   187
by (eq_right "x" "v");
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   188
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   189
qed "less_ssum1d";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   190
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   191
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   192
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   193
(* optimize lemmas about less_ssum                                          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   194
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   195
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   196
Goal "(Isinl x) << (Isinl y) = (x << y)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   197
by (rtac less_ssum1a 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   198
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   199
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   200
qed "less_ssum2a";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   201
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   202
Goal "(Isinr x) << (Isinr y) = (x << y)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   203
by (rtac less_ssum1b 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   204
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   205
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   206
qed "less_ssum2b";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   207
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   208
Goal "(Isinl x) << (Isinr y) = (x = UU)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   209
by (rtac less_ssum1c 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   210
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   211
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   212
qed "less_ssum2c";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   213
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   214
Goal "(Isinr x) << (Isinl y) = (x = UU)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   215
by (rtac less_ssum1d 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   216
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   217
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   218
qed "less_ssum2d";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   219
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   220
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   221
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   222
(* less_ssum is a partial order on ++                                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   223
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   224
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   225
Goal "(p::'a++'b) << p";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   226
by (res_inst_tac [("p","p")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   227
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   228
by (rtac (less_ssum2a RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   229
by (rtac refl_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   230
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   231
by (rtac (less_ssum2b RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   232
by (rtac refl_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   233
qed "refl_less_ssum";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   234
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   235
Goal "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   236
by (res_inst_tac [("p","p1")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   237
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   238
by (res_inst_tac [("p","p2")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   239
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   240
by (res_inst_tac [("f","Isinl")] arg_cong 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   241
by (rtac antisym_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   242
by (etac (less_ssum2a RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   243
by (etac (less_ssum2a RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   244
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   245
by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   246
by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   247
by (rtac strict_IsinlIsinr 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   248
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   249
by (res_inst_tac [("p","p2")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   250
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   251
by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   252
by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   253
by (rtac (strict_IsinlIsinr RS sym) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   254
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   255
by (res_inst_tac [("f","Isinr")] arg_cong 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   256
by (rtac antisym_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   257
by (etac (less_ssum2b RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   258
by (etac (less_ssum2b RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   259
qed "antisym_less_ssum";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   260
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   261
Goal "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   262
by (res_inst_tac [("p","p1")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   263
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   264
by (res_inst_tac [("p","p3")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   265
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   266
by (rtac (less_ssum2a RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   267
by (res_inst_tac [("p","p2")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   268
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   269
by (rtac trans_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   270
by (etac (less_ssum2a RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   271
by (etac (less_ssum2a RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   272
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   273
by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   274
by (rtac minimal 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   275
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   276
by (rtac (less_ssum2c RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   277
by (res_inst_tac [("p","p2")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   278
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   279
by (rtac UU_I 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   280
by (rtac trans_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   281
by (etac (less_ssum2a RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   282
by (rtac (antisym_less_inverse RS conjunct1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   283
by (etac (less_ssum2c RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   284
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   285
by (etac (less_ssum2c RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   286
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   287
by (res_inst_tac [("p","p3")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   288
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   289
by (rtac (less_ssum2d RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   290
by (res_inst_tac [("p","p2")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   291
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   292
by (etac (less_ssum2d RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   293
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   294
by (rtac UU_I 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   295
by (rtac trans_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   296
by (etac (less_ssum2b RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   297
by (rtac (antisym_less_inverse RS conjunct1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   298
by (etac (less_ssum2d RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   299
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   300
by (rtac (less_ssum2b RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   301
by (res_inst_tac [("p","p2")] IssumE2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   302
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   303
by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   304
by (rtac minimal 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   305
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   306
by (rtac trans_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   307
by (etac (less_ssum2b RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   308
by (etac (less_ssum2b RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 4535
diff changeset
   309
qed "trans_less_ssum";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   310
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   311
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   312