src/HOL/Tools/rewrite_hol_proof.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28814 463c9e9111ae
child 30850 5e20f9c20086
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Tools/rewrite_hol_proof.ML
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     4
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     5
Rewrite rules for HOL proofs
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     6
*)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     7
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     8
signature REWRITE_HOL_PROOF =
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
     9
sig
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    10
  val rews: (Proofterm.proof * Proofterm.proof) list
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    11
  val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    12
end;
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    13
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    14
structure RewriteHOLProof : REWRITE_HOL_PROOF =
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    15
struct
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    16
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    17
open Proofterm;
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    18
28801
fc45401bdf6f ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28712
diff changeset
    19
val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
28262
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 27253
diff changeset
    20
    Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    21
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    22
  (** eliminate meta-equality rules **)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    23
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    24
  ["(equal_elim % x1 % x2 %% \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    25
 \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
28712
4f2954d995f0 Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents: 28262
diff changeset
    26
 \      (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    27
 \  (iffD1 % A % B %%  \
28712
4f2954d995f0 Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents: 28262
diff changeset
    28
 \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    29
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    30
   "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    31
 \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
28712
4f2954d995f0 Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents: 28262
diff changeset
    32
 \      (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    33
 \  (iffD2 % A % B %%  \
28712
4f2954d995f0 Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents: 28262
diff changeset
    34
 \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    35
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    36
   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    37
 \    (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) ==  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    38
 \  (cong % TYPE('U) % TYPE('T) % f % g % x % y %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    39
 \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    40
 \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    41
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    42
   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    43
 \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
    44
 \  (HOL.trans % TYPE('T) % x % y % z %%  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    45
 \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    46
 \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    47
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    48
   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) ==  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
    49
 \  (HOL.refl % TYPE('T) % x)",
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    50
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    51
   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    52
 \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    53
 \  (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    54
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    55
   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    56
 \    (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) ==  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    57
 \  (ext % TYPE('U) % TYPE('T) % f % g %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    58
 \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    59
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    60
   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    61
 \    (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    62
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    63
   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    64
 \    (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    65
 \      (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    66
 \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    67
 \  (iffD1 % A = C % B = D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    68
 \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    69
 \      (cong % TYPE('T=>bool) % TYPE('T) %  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    70
 \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
    71
 \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    72
 \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    73
 \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    74
 \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    75
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    76
   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    77
 \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    78
 \      (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    79
 \        (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    80
 \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    81
 \  (iffD2 % A = C % B = D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    82
 \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    83
 \      (cong % TYPE('T=>bool) % TYPE('T) %  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    84
 \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
    85
 \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    86
 \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    87
 \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    88
 \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    89
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    90
   (** rewriting on bool: insert proper congruence rules for logical connectives **)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    91
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    92
   (* All *)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    93
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    94
   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
    95
 \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    96
 \  (allI % TYPE('a) % Q %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    97
 \    (Lam x.  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    98
 \        iffD1 % P x % Q x %% (prf % x) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
    99
 \         (spec % TYPE('a) % P % x %% prf')))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   100
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   101
   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   102
 \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   103
 \  (allI % TYPE('a) % P %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   104
 \    (Lam x.  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   105
 \        iffD2 % P x % Q x %% (prf % x) %%  \
19798
wenzelm
parents: 15570
diff changeset
   106
 \         (spec % TYPE('a) % Q % x %% prf')))",
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   107
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   108
   (* Ex *)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   109
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   110
   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   111
 \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   112
 \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   113
 \    (Lam x H : P x.  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   114
 \        exI % TYPE('a) % Q % x %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   115
 \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   116
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   117
   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   118
 \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   119
 \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   120
 \    (Lam x H : Q x.  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   121
 \        exI % TYPE('a) % P % x %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   122
 \         (iffD2 % P x % Q x %% (prf % x) %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   123
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   124
   (* & *)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   125
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   126
   "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   127
 \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   128
 \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   129
 \  (conjI % B % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   130
 \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   131
 \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   132
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   133
   "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   134
 \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   135
 \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   136
 \  (conjI % A % C %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   137
 \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   138
 \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   139
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   140
   "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   141
 \    (HOL.refl % TYPE(bool=>bool) % op & A)) ==  \
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   142
 \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   143
 \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   144
 \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   145
 \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   146
 \        (HOL.refl % TYPE(bool) % A)))",
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   147
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   148
   (* | *)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   149
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   150
   "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   151
 \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   152
 \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   153
 \  (disjE % A % C % B | D %% prf3 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   154
 \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   155
 \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   156
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   157
   "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   158
 \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   159
 \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   160
 \  (disjE % B % D % A | C %% prf3 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   161
 \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   162
 \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   163
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   164
   "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   165
 \    (HOL.refl % TYPE(bool=>bool) % op | A)) ==  \
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   166
 \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   167
 \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   168
 \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   169
 \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   170
 \        (HOL.refl % TYPE(bool) % A)))",
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   171
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   172
   (* --> *)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   173
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   174
   "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   175
 \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   176
 \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   177
 \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   178
 \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   179
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   180
   "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   181
 \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   182
 \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   183
 \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   184
 \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   185
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   186
   "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   187
 \    (HOL.refl % TYPE(bool=>bool) % op --> A)) ==  \
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   188
 \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   189
 \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   190
 \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   191
 \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   192
 \        (HOL.refl % TYPE(bool) % A)))",
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   193
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   194
   (* ~ *)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   195
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   196
   "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   197
 \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   198
 \  (notI % Q %% (Lam H: Q.  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   199
 \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   200
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   201
   "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   202
 \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   203
 \  (notI % P %% (Lam H: P.  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   204
 \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   205
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   206
   (* = *)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   207
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   208
   "(iffD1 % B % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   209
 \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   210
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   211
 \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   212
 \  (iffD1 % C % D %% prf2 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   213
 \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   214
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   215
   "(iffD2 % B % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   216
 \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   217
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   218
 \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   219
 \  (iffD1 % A % B %% prf1 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   220
 \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   221
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   222
   "(iffD1 % A % C %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   223
 \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   224
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   225
 \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   226
 \  (iffD2 % C % D %% prf2 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   227
 \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   228
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   229
   "(iffD2 % A % C %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   230
 \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   231
 \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   232
 \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   233
 \  (iffD2 % A % B %% prf1 %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   234
 \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   235
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   236
   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   237
 \    (HOL.refl % TYPE(bool=>bool) % op = A)) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   238
 \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   239
 \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   240
 \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   241
 \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   242
 \        (HOL.refl % TYPE(bool) % A)))",
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   243
13916
f078a758e5d8 elim_cong now eta-expands proofs on the fly if required.
berghofe
parents: 13602
diff changeset
   244
   (** transitivity, reflexivity, and symmetry **)
f078a758e5d8 elim_cong now eta-expands proofs on the fly if required.
berghofe
parents: 13602
diff changeset
   245
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   246
   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   247
 \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   248
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   249
   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   250
 \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   251
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   252
   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   253
15530
6f43714517ee Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents: 14981
diff changeset
   254
   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   255
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   256
   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   257
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   258
   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   259
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   260
   (** normalization of HOL proofs **)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   261
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   262
   "(mp % A % B %% (impI % A % B %% prf)) == prf",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   263
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   264
   "(impI % A % B %% (mp % A % B %% prf)) == prf",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   265
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   266
   "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   267
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   268
   "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   269
13602
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   270
   "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   271
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   272
   "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
4cecd1e0f4a9 - additional congruence rules for boolean operators
berghofe
parents: 13404
diff changeset
   273
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   274
   "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   275
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   276
   "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   277
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   278
   "(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   279
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   280
   "(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   281
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   282
   "(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   283
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   284
   "(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   285
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   286
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   287
(** Replace congruence rules by substitution rules **)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   288
28801
fc45401bdf6f ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28712
diff changeset
   289
fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   290
      prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
28801
fc45401bdf6f ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28712
diff changeset
   291
  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15530
diff changeset
   292
  | strip_cong _ _ = NONE;
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   293
28814
463c9e9111ae clarified Thm.proof_body_of vs. Thm.proof_of;
wenzelm
parents: 28801
diff changeset
   294
val subst_prf = fst (strip_combt (Thm.proof_of subst));
463c9e9111ae clarified Thm.proof_body_of vs. Thm.proof_of;
wenzelm
parents: 28801
diff changeset
   295
val sym_prf = fst (strip_combt (Thm.proof_of sym));
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   296
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   297
fun make_subst Ts prf xs (_, []) = prf
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   298
  | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   299
      let val T = fastype_of1 (Ts, x)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   300
      in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15530
diff changeset
   301
        else change_type (SOME [T]) subst_prf %> x %> y %>
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   302
          Abs ("z", T, list_comb (incr_boundvars 1 f,
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   303
            map (incr_boundvars 1) xs @ Bound 0 ::
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   304
            map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   305
          make_subst Ts prf (xs @ [x]) (f, ps)
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   306
      end;
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   307
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   308
fun make_sym Ts ((x, y), prf) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15530
diff changeset
   309
  ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   310
22277
b89dc456dbc6 Fixed bug in mk_AbsP.
berghofe
parents: 21646
diff changeset
   311
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
13916
f078a758e5d8 elim_cong now eta-expands proofs on the fly if required.
berghofe
parents: 13602
diff changeset
   312
28801
fc45401bdf6f ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28712
diff changeset
   313
fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   314
      Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
28801
fc45401bdf6f ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28712
diff changeset
   315
  | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   316
      Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
13916
f078a758e5d8 elim_cong now eta-expands proofs on the fly if required.
berghofe
parents: 13602
diff changeset
   317
        (strip_cong [] (incr_pboundvars 1 0 prf))
28801
fc45401bdf6f ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28712
diff changeset
   318
  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   319
      Option.map (make_subst Ts prf2 [] o
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   320
        apsnd (map (make_sym Ts))) (strip_cong [] prf1)
28801
fc45401bdf6f ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents: 28712
diff changeset
   321
  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   322
      Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
13916
f078a758e5d8 elim_cong now eta-expands proofs on the fly if required.
berghofe
parents: 13602
diff changeset
   323
        apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15530
diff changeset
   324
  | elim_cong _ _ = NONE;
13404
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   325
eeac2bbfe958 Rules for rewriting HOL proofs.
berghofe
parents:
diff changeset
   326
end;