src/HOL/Tools/rewrite_hol_proof.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 59058 a78612c67ec0
child 67091 1393c2340eec
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Tools/rewrite_hol_proof.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Rewrite rules for HOL proofs
     5 *)
     6 
     7 signature REWRITE_HOL_PROOF =
     8 sig
     9   val rews: (Proofterm.proof * Proofterm.proof) list
    10   val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
    11 end;
    12 
    13 structure RewriteHOLProof : REWRITE_HOL_PROOF =
    14 struct
    15 
    16 val rews = map (apply2 (Proof_Syntax.proof_of_term @{theory} true) o
    17     Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
    18 
    19   (** eliminate meta-equality rules **)
    20 
    21   ["(equal_elim % x1 % x2 %% \
    22  \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
    23  \      (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==  \
    24  \  (iffD1 % A % B %%  \
    25  \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    26 
    27    "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
    28  \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
    29  \      (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==  \
    30  \  (iffD2 % A % B %%  \
    31  \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    32 
    33    "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %%  \
    34  \    (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==  \
    35  \  (cong % TYPE('T) % TYPE('U) % f % g % x % y %%  \
    36  \    (OfClass type_class % TYPE('T)) %% prfU %%  \
    37  \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %%  \
    38  \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))",
    39 
    40    "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %%  \
    41  \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
    42  \  (HOL.trans % TYPE('T) % x % y % z %% prfT %%  \
    43  \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %%  \
    44  \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))",
    45 
    46    "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) ==  \
    47  \  (HOL.refl % TYPE('T) % x %% prfT)",
    48 
    49    "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    50  \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
    51  \  (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))",
    52 
    53    "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %%  \
    54  \    (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==  \
    55  \  (ext % TYPE('T) % TYPE('U) % f % g %%  \
    56  \    (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %%  \
    57  \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %%  \
    58  \       (OfClass type_class % TYPE('U)) %% (prf % x)))",
    59 
    60    "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    61  \    (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf",
    62 
    63    "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
    64  \    (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
    65  \      (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
    66  \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
    67  \  (iffD1 % A = C % B = D %%  \
    68  \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
    69  \      prfT %% arity_type_bool %%  \
    70  \      (cong % TYPE('T) % TYPE('T=>bool) %  \
    71  \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    72  \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
    73  \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
    74  \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
    75  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
    76  \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
    77  \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))",
    78 
    79    "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
    80  \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
    81  \      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
    82  \        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
    83  \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
    84  \  (iffD2 % A = C % B = D %%  \
    85  \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
    86  \      prfT %% arity_type_bool %%  \
    87  \      (cong % TYPE('T) % TYPE('T=>bool) %  \
    88  \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    89  \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
    90  \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
    91  \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
    92  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
    93  \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
    94  \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))",
    95 
    96    (** rewriting on bool: insert proper congruence rules for logical connectives **)
    97 
    98    (* All *)
    99 
   100    "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   101  \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   102  \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   103  \  (allI % TYPE('a) % Q %% prfa %%  \
   104  \    (Lam x.  \
   105  \        iffD1 % P x % Q x %% (prf % x) %%  \
   106  \         (spec % TYPE('a) % P % x %% prfa %% prf')))",
   107 
   108    "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   109  \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   110  \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   111  \  (allI % TYPE('a) % P %% prfa %%  \
   112  \    (Lam x.  \
   113  \        iffD2 % P x % Q x %% (prf % x) %%  \
   114  \         (spec % TYPE('a) % Q % x %% prfa %% prf')))",
   115 
   116    (* Ex *)
   117 
   118    "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   119  \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   120  \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   121  \  (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %%  \
   122  \    (Lam x H : P x.  \
   123  \        exI % TYPE('a) % Q % x %% prfa %%  \
   124  \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
   125 
   126    "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   127  \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   128  \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   129  \  (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %%  \
   130  \    (Lam x H : Q x.  \
   131  \        exI % TYPE('a) % P % x %% prfa %%  \
   132  \         (iffD2 % P x % Q x %% (prf % x) %% H)))",
   133 
   134    (* & *)
   135 
   136    "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   137  \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %%  \
   138  \      (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   139  \  (conjI % B % D %%  \
   140  \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
   141  \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
   142 
   143    "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   144  \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %%  \
   145  \      (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   146  \  (conjI % A % C %%  \
   147  \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
   148  \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
   149 
   150    "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %%  \
   151  \    (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) ==  \
   152  \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %%  \
   153  \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   154  \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
   155  \        prfb %% prfbb %%  \
   156  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %%  \
   157  \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   158  \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   159 
   160    (* | *)
   161 
   162    "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   163  \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %%  \
   164  \      (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   165  \  (disjE % A % C % B | D %% prf3 %%  \
   166  \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
   167  \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
   168 
   169    "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   170  \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %%  \
   171  \      (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   172  \  (disjE % B % D % A | C %% prf3 %%  \
   173  \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
   174  \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
   175 
   176    "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %%  \
   177  \    (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) ==  \
   178  \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %%  \
   179  \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   180  \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
   181  \        prfb %% prfbb %%  \
   182  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %%  \
   183  \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   184  \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   185 
   186    (* --> *)
   187 
   188    "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   189  \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %%  \
   190  \      (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   191  \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
   192  \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
   193 
   194    "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   195  \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %%  \
   196  \      (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   197  \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
   198  \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
   199 
   200    "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %%  \
   201  \    (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) ==  \
   202  \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %%  \
   203  \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   204  \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
   205  \        prfb %% prfbb %%  \
   206  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %%  \
   207  \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   208  \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   209 
   210    (* ~ *)
   211 
   212    "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   213  \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   214  \  (notI % Q %% (Lam H: Q.  \
   215  \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
   216 
   217    "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   218  \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   219  \  (notI % P %% (Lam H: P.  \
   220  \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
   221 
   222    (* = *)
   223 
   224    "(iffD1 % B % D %%  \
   225  \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   226  \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   227  \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   228  \  (iffD1 % C % D %% prf2 %%  \
   229  \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
   230 
   231    "(iffD2 % B % D %%  \
   232  \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   233  \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   234  \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   235  \  (iffD1 % A % B %% prf1 %%  \
   236  \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
   237 
   238    "(iffD1 % A % C %%  \
   239  \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   240  \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   241  \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   242  \  (iffD2 % C % D %% prf2 %%  \
   243  \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
   244 
   245    "(iffD2 % A % C %%  \
   246  \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   247  \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   248  \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   249  \  (iffD2 % A % B %% prf1 %%  \
   250  \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
   251 
   252    "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   253  \    (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) ==  \
   254  \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   255  \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   256  \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
   257  \        prfb %% prfbb %%  \
   258  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %%  \
   259  \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   260  \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   261 
   262    (** transitivity, reflexivity, and symmetry **)
   263 
   264    "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   265  \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
   266 
   267    "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   268  \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
   269 
   270    "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   271 
   272    "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   273 
   274    "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)",
   275 
   276    "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)",
   277 
   278    (** normalization of HOL proofs **)
   279 
   280    "(mp % A % B %% (impI % A % B %% prf)) == prf",
   281 
   282    "(impI % A % B %% (mp % A % B %% prf)) == prf",
   283 
   284    "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x",
   285 
   286    "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf",
   287 
   288    "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)",
   289 
   290    "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf",
   291 
   292    "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
   293 
   294    "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
   295 
   296    "(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
   297 
   298    "(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
   299 
   300    "(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
   301 
   302    "(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
   303 
   304 
   305 (** Replace congruence rules by substitution rules **)
   306 
   307 fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
   308       prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
   309   | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
   310   | strip_cong _ _ = NONE;
   311 
   312 val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst))));
   313 val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym))));
   314 
   315 fun make_subst Ts prf xs (_, []) = prf
   316   | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
   317       let val T = fastype_of1 (Ts, x)
   318       in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
   319         else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %>
   320           Abs ("z", T, list_comb (incr_boundvars 1 f,
   321             map (incr_boundvars 1) xs @ Bound 0 ::
   322             map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
   323           make_subst Ts prf (xs @ [x]) (f, ps)
   324       end;
   325 
   326 fun make_sym Ts ((x, y), (prf, clprf)) =
   327   ((y, x),
   328     (Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
   329 
   330 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
   331 
   332 fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
   333       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
   334   | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
   335       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
   336         (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
   337   | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
   338       Option.map (make_subst Ts prf2 [] o
   339         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
   340   | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
   341       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
   342         apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
   343   | elim_cong_aux _ _ = NONE;
   344 
   345 fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf);
   346 
   347 end;