src/Pure/Proof/proof_rewrite_rules.ML
author berghofe
Sat Feb 02 13:26:51 2002 +0100 (2002-02-02 ago)
changeset 12866 c00df7765656
parent 12237 39aeccee9e1c
child 12906 165f4e1937f4
permissions -rw-r--r--
Rewrite procedure now works for both compact and full proof objects.
berghofe@11522
     1
(*  Title:      Pure/Proof/proof_rewrite_rules.ML
berghofe@11522
     2
    ID:         $Id$
wenzelm@11539
     3
    Author:     Stefan Berghofer, TU Muenchen
wenzelm@11539
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@11522
     5
berghofe@11522
     6
Simplification function for partial proof terms involving
berghofe@11522
     7
meta level rules.
berghofe@11522
     8
*)
berghofe@11522
     9
berghofe@11522
    10
signature PROOF_REWRITE_RULES =
berghofe@11522
    11
sig
berghofe@12866
    12
  val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
berghofe@12866
    13
  val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
berghofe@12237
    14
  val setup : (theory -> theory) list
berghofe@11522
    15
end;
berghofe@11522
    16
berghofe@11522
    17
structure ProofRewriteRules : PROOF_REWRITE_RULES =
berghofe@11522
    18
struct
berghofe@11522
    19
berghofe@11522
    20
open Proofterm;
berghofe@11522
    21
berghofe@12866
    22
fun rew b =
berghofe@12866
    23
  let
berghofe@12866
    24
    fun ? x = if b then Some x else None;
berghofe@12866
    25
    fun ax (prf as PAxm (s, prop, _)) Ts =
berghofe@12866
    26
      if b then PAxm (s, prop, Some Ts) else prf;
berghofe@12866
    27
    fun ty T = if b then
berghofe@12866
    28
        let val Type (_, [Type (_, [U, _]), _]) = T
berghofe@12866
    29
        in Some T end
berghofe@12866
    30
      else None;
berghofe@12866
    31
    val equal_intr_axm = ax equal_intr_axm [];
berghofe@12866
    32
    val equal_elim_axm = ax equal_elim_axm [];
berghofe@12866
    33
    val symmetric_axm = ax symmetric_axm [propT];
berghofe@11522
    34
berghofe@12866
    35
    fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
berghofe@12866
    36
        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
berghofe@12866
    37
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
    38
        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
berghofe@12866
    39
      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    40
        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
berghofe@12866
    41
            Some (equal_intr_axm % B % A %% prf2 %% prf1)
berghofe@12002
    42
berghofe@12866
    43
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
berghofe@12002
    44
        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
berghofe@12866
    45
          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
berghofe@12866
    46
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
berghofe@12866
    47
        Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
berghofe@12002
    48
berghofe@12866
    49
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
berghofe@12866
    50
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    51
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
berghofe@12866
    52
             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
berghofe@12866
    53
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
berghofe@12866
    54
        Some (tg %> B %% (equal_elim_axm %> A %> B %%
berghofe@12866
    55
          (symmetric_axm % ? B % ? A %% prf1) %% prf2))
berghofe@11522
    56
berghofe@12866
    57
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@11612
    58
        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@11612
    59
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
berghofe@12866
    60
             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
berghofe@12866
    61
        let
berghofe@12866
    62
          val _ $ A $ C = Envir.beta_norm X;
berghofe@12866
    63
          val _ $ B $ D = Envir.beta_norm Y
berghofe@12866
    64
        in Some (AbsP ("H1", ? X, AbsP ("H2", ? B,
berghofe@12866
    65
          equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
berghofe@12866
    66
            (PBound 1 %% (equal_elim_axm %> B %> A %%
berghofe@12866
    67
              (symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
berghofe@12866
    68
        end
berghofe@11522
    69
berghofe@12866
    70
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@12866
    71
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    72
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
    73
            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
berghofe@12866
    74
               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
berghofe@12866
    75
        let
berghofe@12866
    76
          val _ $ A $ C = Envir.beta_norm Y;
berghofe@12866
    77
          val _ $ B $ D = Envir.beta_norm X
berghofe@12866
    78
        in Some (AbsP ("H1", ? X, AbsP ("H2", ? A,
berghofe@12866
    79
          equal_elim_axm %> D %> C %%
berghofe@12866
    80
            (symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2)
berghofe@12866
    81
              %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
berghofe@12866
    82
        end
berghofe@11522
    83
berghofe@12866
    84
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@11612
    85
        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
berghofe@11612
    86
          (PAxm ("ProtoPure.reflexive", _, _) % _) %%
berghofe@12866
    87
            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
berghofe@12866
    88
        let
berghofe@12866
    89
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
    90
          val _ $ Q = Envir.beta_norm Y;
berghofe@12866
    91
        in Some (AbsP ("H", ? X, Abst ("x", ty T,
berghofe@12866
    92
            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
berghofe@12866
    93
              (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
berghofe@12866
    94
        end
berghofe@12866
    95
berghofe@12866
    96
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@12866
    97
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
berghofe@12866
    98
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
berghofe@12866
    99
            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
berghofe@12866
   100
              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
berghofe@12866
   101
        let
berghofe@12866
   102
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
   103
          val _ $ Q = Envir.beta_norm Y;
berghofe@12866
   104
          val t = incr_boundvars 1 P $ Bound 0;
berghofe@12866
   105
          val u = incr_boundvars 1 Q $ Bound 0
berghofe@12866
   106
        in Some (AbsP ("H", ? X, Abst ("x", ty T,
berghofe@12866
   107
          equal_elim_axm %> t %> u %%
berghofe@12866
   108
            (symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0))
berghofe@12866
   109
              %% (PBound 0 %> Bound 0))))
berghofe@12866
   110
        end
berghofe@12866
   111
berghofe@12866
   112
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
berghofe@12866
   113
        (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
berghofe@12866
   114
           Some (equal_elim_axm %> B %> C %% prf2 %%
berghofe@12866
   115
             (equal_elim_axm %> A %> B %% prf1 %% prf3))
berghofe@12866
   116
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
berghofe@12866
   117
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   118
          (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
berghofe@12866
   119
           Some (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %%
berghofe@12866
   120
             (equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3))
berghofe@12866
   121
berghofe@12866
   122
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   123
        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
berghofe@12866
   124
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   125
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   126
          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf
berghofe@12866
   127
berghofe@12866
   128
      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   129
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = Some prf
berghofe@11522
   130
berghofe@12866
   131
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   132
        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
berghofe@12866
   133
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   134
            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   135
              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
berghofe@12866
   136
          Some (equal_elim_axm %> C %> D %% prf2 %%
berghofe@12866
   137
            (equal_elim_axm %> A %> C %% prf3 %%
berghofe@12866
   138
              (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4)))
berghofe@12866
   139
berghofe@12866
   140
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   141
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   142
          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
berghofe@12866
   143
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   144
              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   145
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
berghofe@12866
   146
          Some (equal_elim_axm %> A %> B %% prf1 %%
berghofe@12866
   147
            (equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %%
berghofe@12866
   148
              (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4)))
berghofe@11522
   149
berghofe@12866
   150
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   151
        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
berghofe@12866
   152
          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   153
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   154
              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   155
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
berghofe@12866
   156
          Some (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %%
berghofe@12866
   157
            (equal_elim_axm %> B %> D %% prf3 %%
berghofe@12866
   158
              (equal_elim_axm %> A %> B %% prf1 %% prf4)))
berghofe@11522
   159
berghofe@12866
   160
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   161
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   162
          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
berghofe@12866
   163
            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   164
              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   165
                (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   166
                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
berghofe@12866
   167
          Some (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %%
berghofe@12866
   168
            (equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
berghofe@12866
   169
              (equal_elim_axm %> C %> D %% prf2 %% prf4)))
berghofe@11522
   170
berghofe@12866
   171
      | rew' _ _ = None;
berghofe@12866
   172
  in rew' end;
berghofe@12866
   173
berghofe@12866
   174
fun rprocs b = [("Pure/meta_equality", rew b)];
berghofe@12866
   175
val setup = [Proofterm.add_prf_rprocs (rprocs false)];
berghofe@11522
   176
berghofe@11522
   177
end;