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