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