src/HOL/Tools/rewrite_hol_proof.ML
author berghofe
Sun Jul 21 15:43:14 2002 +0200 (2002-07-21)
changeset 13404 eeac2bbfe958
child 13602 4cecd1e0f4a9
permissions -rw-r--r--
Rules for rewriting HOL proofs.
berghofe@13404
     1
(*  Title:      HOL/Tools/rewrite_hol_proof.ML
berghofe@13404
     2
    ID:         $Id$
berghofe@13404
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@13404
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@13404
     5
berghofe@13404
     6
Rewrite rules for HOL proofs
berghofe@13404
     7
*)
berghofe@13404
     8
berghofe@13404
     9
signature REWRITE_HOL_PROOF =
berghofe@13404
    10
sig
berghofe@13404
    11
  val rews: (Proofterm.proof * Proofterm.proof) list
berghofe@13404
    12
  val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
berghofe@13404
    13
end;
berghofe@13404
    14
berghofe@13404
    15
structure RewriteHOLProof : REWRITE_HOL_PROOF =
berghofe@13404
    16
struct
berghofe@13404
    17
berghofe@13404
    18
open Proofterm;
berghofe@13404
    19
berghofe@13404
    20
val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
berghofe@13404
    21
    Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
berghofe@13404
    22
berghofe@13404
    23
  (** eliminate meta-equality rules **)
berghofe@13404
    24
berghofe@13404
    25
  ["(equal_elim % x1 % x2 %% \
berghofe@13404
    26
 \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
berghofe@13404
    27
 \      (axm.reflexive % TYPE('T3) % x4) %% prf1) %% prf2) ==  \
berghofe@13404
    28
 \  (iffD1 % A % B %%  \
berghofe@13404
    29
 \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
berghofe@13404
    30
berghofe@13404
    31
   "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
berghofe@13404
    32
 \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
berghofe@13404
    33
 \      (axm.reflexive % TYPE('T4) % x6) %% prf1)) %% prf2) ==  \
berghofe@13404
    34
 \  (iffD2 % A % B %%  \
berghofe@13404
    35
 \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
berghofe@13404
    36
berghofe@13404
    37
   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
berghofe@13404
    38
 \    (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) ==  \
berghofe@13404
    39
 \  (cong % TYPE('U) % TYPE('T) % f % g % x % y %%  \
berghofe@13404
    40
 \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %%  \
berghofe@13404
    41
 \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
berghofe@13404
    42
berghofe@13404
    43
   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %%  \
berghofe@13404
    44
 \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
berghofe@13404
    45
 \  (trans % TYPE('T) % x % y % z %%  \
berghofe@13404
    46
 \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %%  \
berghofe@13404
    47
 \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
berghofe@13404
    48
berghofe@13404
    49
   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) ==  \
berghofe@13404
    50
 \  (refl % TYPE('T) % x)",
berghofe@13404
    51
berghofe@13404
    52
   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
berghofe@13404
    53
 \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
berghofe@13404
    54
 \  (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
berghofe@13404
    55
berghofe@13404
    56
   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %%  \
berghofe@13404
    57
 \    (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) ==  \
berghofe@13404
    58
 \  (ext % TYPE('U) % TYPE('T) % f % g %%  \
berghofe@13404
    59
 \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
berghofe@13404
    60
berghofe@13404
    61
   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
berghofe@13404
    62
 \    (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
berghofe@13404
    63
berghofe@13404
    64
   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
berghofe@13404
    65
 \    (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
berghofe@13404
    66
 \      (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
berghofe@13404
    67
 \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
berghofe@13404
    68
 \  (iffD1 % A = C % B = D %%  \
berghofe@13404
    69
 \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
berghofe@13404
    70
 \      (cong % TYPE('T=>bool) % TYPE('T) %  \
berghofe@13404
    71
 \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
berghofe@13404
    72
 \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
berghofe@13404
    73
 \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
berghofe@13404
    74
 \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
berghofe@13404
    75
 \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
berghofe@13404
    76
berghofe@13404
    77
   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
berghofe@13404
    78
 \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
berghofe@13404
    79
 \      (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
berghofe@13404
    80
 \        (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
berghofe@13404
    81
 \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
berghofe@13404
    82
 \  (iffD2 % A = C % B = D %%  \
berghofe@13404
    83
 \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
berghofe@13404
    84
 \      (cong % TYPE('T=>bool) % TYPE('T) %  \
berghofe@13404
    85
 \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
berghofe@13404
    86
 \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
berghofe@13404
    87
 \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
berghofe@13404
    88
 \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
berghofe@13404
    89
 \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
berghofe@13404
    90
berghofe@13404
    91
   (** rewriting on bool: insert proper congruence rules for logical connectives **)
berghofe@13404
    92
berghofe@13404
    93
   (* All *)
berghofe@13404
    94
berghofe@13404
    95
   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
berghofe@13404
    96
 \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
berghofe@13404
    97
 \  (allI % TYPE('a) % Q %%  \
berghofe@13404
    98
 \    (Lam x.  \
berghofe@13404
    99
 \        iffD1 % P x % Q x %% (prf % x) %%  \
berghofe@13404
   100
 \         (spec % TYPE('a) % P % x %% prf')))",
berghofe@13404
   101
berghofe@13404
   102
   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
berghofe@13404
   103
 \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
berghofe@13404
   104
 \  (allI % TYPE('a) % P %%  \
berghofe@13404
   105
 \    (Lam x.  \
berghofe@13404
   106
 \        iffD2 % P x % Q x %% (prf % x) %%  \
berghofe@13404
   107
 \         (spec % TYPE('a) % ?Q % x %% prf')))",
berghofe@13404
   108
berghofe@13404
   109
   (* Ex *)
berghofe@13404
   110
berghofe@13404
   111
   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
berghofe@13404
   112
 \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
berghofe@13404
   113
 \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
berghofe@13404
   114
 \    (Lam x H : P x.  \
berghofe@13404
   115
 \        exI % TYPE('a) % Q % x %%  \
berghofe@13404
   116
 \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
berghofe@13404
   117
berghofe@13404
   118
   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
berghofe@13404
   119
 \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
berghofe@13404
   120
 \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
berghofe@13404
   121
 \    (Lam x H : Q x.  \
berghofe@13404
   122
 \        exI % TYPE('a) % P % x %%  \
berghofe@13404
   123
 \         (iffD2 % P x % Q x %% (prf % x) %% H)))",
berghofe@13404
   124
berghofe@13404
   125
   (* & *)
berghofe@13404
   126
berghofe@13404
   127
   "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
berghofe@13404
   128
 \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
berghofe@13404
   129
 \      (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
berghofe@13404
   130
 \  (conjI % B % D %%  \
berghofe@13404
   131
 \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
berghofe@13404
   132
 \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
berghofe@13404
   133
berghofe@13404
   134
   "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
berghofe@13404
   135
 \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
berghofe@13404
   136
 \      (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
berghofe@13404
   137
 \  (conjI % A % C %%  \
berghofe@13404
   138
 \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
berghofe@13404
   139
 \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
berghofe@13404
   140
berghofe@13404
   141
   (* | *)
berghofe@13404
   142
berghofe@13404
   143
   "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
berghofe@13404
   144
 \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
berghofe@13404
   145
 \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
berghofe@13404
   146
 \  (disjE % A % C % B | D %% prf3 %%  \
berghofe@13404
   147
 \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
berghofe@13404
   148
 \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
berghofe@13404
   149
berghofe@13404
   150
   "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
berghofe@13404
   151
 \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
berghofe@13404
   152
 \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
berghofe@13404
   153
 \  (disjE % B % D % A | C %% prf3 %%  \
berghofe@13404
   154
 \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
berghofe@13404
   155
 \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
berghofe@13404
   156
berghofe@13404
   157
   (* --> *)
berghofe@13404
   158
berghofe@13404
   159
   "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
berghofe@13404
   160
 \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
berghofe@13404
   161
 \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
berghofe@13404
   162
 \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
berghofe@13404
   163
 \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
berghofe@13404
   164
berghofe@13404
   165
   "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
berghofe@13404
   166
 \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
berghofe@13404
   167
 \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
berghofe@13404
   168
 \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
berghofe@13404
   169
 \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
berghofe@13404
   170
berghofe@13404
   171
   (* ~ *)
berghofe@13404
   172
berghofe@13404
   173
   "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
berghofe@13404
   174
 \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
berghofe@13404
   175
 \  (notI % Q %% (Lam H: Q.  \
berghofe@13404
   176
 \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
berghofe@13404
   177
berghofe@13404
   178
   "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
berghofe@13404
   179
 \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
berghofe@13404
   180
 \  (notI % P %% (Lam H: P.  \
berghofe@13404
   181
 \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
berghofe@13404
   182
berghofe@13404
   183
   (* = *)
berghofe@13404
   184
berghofe@13404
   185
   "(iffD1 % B % D %%  \
berghofe@13404
   186
 \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
berghofe@13404
   187
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
berghofe@13404
   188
 \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
berghofe@13404
   189
 \  (iffD1 % C % D %% prf2 %%  \
berghofe@13404
   190
 \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
berghofe@13404
   191
berghofe@13404
   192
   "(iffD2 % B % D %%  \
berghofe@13404
   193
 \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
berghofe@13404
   194
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
berghofe@13404
   195
 \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
berghofe@13404
   196
 \  (iffD1 % A % B %% prf1 %%  \
berghofe@13404
   197
 \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
berghofe@13404
   198
berghofe@13404
   199
   "(iffD1 % A % C %%  \
berghofe@13404
   200
 \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
berghofe@13404
   201
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
berghofe@13404
   202
 \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
berghofe@13404
   203
 \  (iffD2 % C % D %% prf2 %%  \
berghofe@13404
   204
 \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
berghofe@13404
   205
berghofe@13404
   206
   "(iffD2 % A % C %%  \
berghofe@13404
   207
 \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
berghofe@13404
   208
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
berghofe@13404
   209
 \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
berghofe@13404
   210
 \  (iffD2 % A % B %% prf1 %%  \
berghofe@13404
   211
 \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
berghofe@13404
   212
berghofe@13404
   213
   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
berghofe@13404
   214
 \    (refl % TYPE(bool) % op = A)) ==  \
berghofe@13404
   215
 \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
berghofe@13404
   216
 \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
berghofe@13404
   217
 \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
berghofe@13404
   218
 \        (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
berghofe@13404
   219
 \        (refl % TYPE(bool) % A % A)))",
berghofe@13404
   220
berghofe@13404
   221
   "(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
berghofe@13404
   222
 \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
berghofe@13404
   223
berghofe@13404
   224
   "(iffD2 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
berghofe@13404
   225
 \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
berghofe@13404
   226
berghofe@13404
   227
   "(iffD1 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
berghofe@13404
   228
berghofe@13404
   229
   "(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
berghofe@13404
   230
berghofe@13404
   231
   (** normalization of HOL proofs **)
berghofe@13404
   232
berghofe@13404
   233
   "(mp % A % B %% (impI % A % B %% prf)) == prf",
berghofe@13404
   234
berghofe@13404
   235
   "(impI % A % B %% (mp % A % B %% prf)) == prf",
berghofe@13404
   236
berghofe@13404
   237
   "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
berghofe@13404
   238
berghofe@13404
   239
   "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
berghofe@13404
   240
berghofe@13404
   241
   "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
berghofe@13404
   242
berghofe@13404
   243
   "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
berghofe@13404
   244
berghofe@13404
   245
   "(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
berghofe@13404
   246
berghofe@13404
   247
   "(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
berghofe@13404
   248
berghofe@13404
   249
   "(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
berghofe@13404
   250
berghofe@13404
   251
   "(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
berghofe@13404
   252
berghofe@13404
   253
berghofe@13404
   254
(** Replace congruence rules by substitution rules **)
berghofe@13404
   255
berghofe@13404
   256
fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % Some x % Some y %%
berghofe@13404
   257
      prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
berghofe@13404
   258
  | strip_cong ps (PThm (("HOL.refl", _), _, _, _) % Some f) = Some (f, ps)
berghofe@13404
   259
  | strip_cong _ _ = None;
berghofe@13404
   260
berghofe@13404
   261
val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
berghofe@13404
   262
val sym_prf = fst (strip_combt (#2 (#der (rep_thm sym))));
berghofe@13404
   263
berghofe@13404
   264
fun make_subst Ts prf xs (_, []) = prf
berghofe@13404
   265
  | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
berghofe@13404
   266
      let val T = fastype_of1 (Ts, x)
berghofe@13404
   267
      in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
berghofe@13404
   268
        else change_type (Some [T]) subst_prf %> x %> y %>
berghofe@13404
   269
          Abs ("z", T, list_comb (incr_boundvars 1 f,
berghofe@13404
   270
            map (incr_boundvars 1) xs @ Bound 0 ::
berghofe@13404
   271
            map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
berghofe@13404
   272
          make_subst Ts prf (xs @ [x]) (f, ps)
berghofe@13404
   273
      end;
berghofe@13404
   274
berghofe@13404
   275
fun make_sym Ts ((x, y), prf) =
berghofe@13404
   276
  ((y, x), change_type (Some [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
berghofe@13404
   277
berghofe@13404
   278
fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) =
berghofe@13404
   279
      apsome (make_subst Ts prf2 []) (strip_cong [] prf1)
berghofe@13404
   280
  | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) =
berghofe@13404
   281
      apsome (make_subst Ts prf2 [] o
berghofe@13404
   282
        apsnd (map (make_sym Ts))) (strip_cong [] prf1)
berghofe@13404
   283
  | elim_cong _ _ = None;
berghofe@13404
   284
berghofe@13404
   285
end;