src/Pure/Proof/proof_rewrite_rules.ML
author berghofe
Wed Feb 20 15:56:26 2002 +0100 (2002-02-20 ago)
changeset 12906 165f4e1937f4
parent 12866 c00df7765656
child 13198 3e40f48a500f
permissions -rw-r--r--
New function for eliminating definitions in proof term.
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@12906
     6
Simplification functions for proof terms involving meta level rules.
berghofe@11522
     7
*)
berghofe@11522
     8
berghofe@11522
     9
signature PROOF_REWRITE_RULES =
berghofe@11522
    10
sig
berghofe@12866
    11
  val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
berghofe@12866
    12
  val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
berghofe@12906
    13
  val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
berghofe@12906
    14
  val elim_defs : Sign.sg -> thm list -> Proofterm.proof -> Proofterm.proof
berghofe@12237
    15
  val setup : (theory -> theory) list
berghofe@11522
    16
end;
berghofe@11522
    17
berghofe@11522
    18
structure ProofRewriteRules : PROOF_REWRITE_RULES =
berghofe@11522
    19
struct
berghofe@11522
    20
berghofe@11522
    21
open Proofterm;
berghofe@11522
    22
berghofe@12866
    23
fun rew b =
berghofe@12866
    24
  let
berghofe@12866
    25
    fun ? x = if b then Some x else None;
berghofe@12866
    26
    fun ax (prf as PAxm (s, prop, _)) Ts =
berghofe@12866
    27
      if b then PAxm (s, prop, Some Ts) else prf;
berghofe@12866
    28
    fun ty T = if b then
berghofe@12866
    29
        let val Type (_, [Type (_, [U, _]), _]) = T
berghofe@12866
    30
        in Some T end
berghofe@12866
    31
      else None;
berghofe@12866
    32
    val equal_intr_axm = ax equal_intr_axm [];
berghofe@12866
    33
    val equal_elim_axm = ax equal_elim_axm [];
berghofe@12866
    34
    val symmetric_axm = ax symmetric_axm [propT];
berghofe@11522
    35
berghofe@12866
    36
    fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
berghofe@12866
    37
        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
berghofe@12866
    38
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
    39
        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
berghofe@12866
    40
      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    41
        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
berghofe@12866
    42
            Some (equal_intr_axm % B % A %% prf2 %% prf1)
berghofe@12002
    43
berghofe@12866
    44
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
berghofe@12002
    45
        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
berghofe@12866
    46
          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
berghofe@12866
    47
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
berghofe@12866
    48
        Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
berghofe@12002
    49
berghofe@12866
    50
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
berghofe@12866
    51
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    52
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
berghofe@12866
    53
             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
berghofe@12866
    54
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
berghofe@12866
    55
        Some (tg %> B %% (equal_elim_axm %> A %> B %%
berghofe@12866
    56
          (symmetric_axm % ? B % ? A %% prf1) %% prf2))
berghofe@11522
    57
berghofe@12866
    58
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@11612
    59
        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@11612
    60
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
berghofe@12866
    61
             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
berghofe@12866
    62
        let
berghofe@12866
    63
          val _ $ A $ C = Envir.beta_norm X;
berghofe@12866
    64
          val _ $ B $ D = Envir.beta_norm Y
berghofe@12866
    65
        in Some (AbsP ("H1", ? X, AbsP ("H2", ? B,
berghofe@12866
    66
          equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
berghofe@12866
    67
            (PBound 1 %% (equal_elim_axm %> B %> A %%
berghofe@12866
    68
              (symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
berghofe@12866
    69
        end
berghofe@11522
    70
berghofe@12866
    71
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@12866
    72
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    73
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
    74
            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
berghofe@12866
    75
               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
berghofe@12866
    76
        let
berghofe@12866
    77
          val _ $ A $ C = Envir.beta_norm Y;
berghofe@12866
    78
          val _ $ B $ D = Envir.beta_norm X
berghofe@12866
    79
        in Some (AbsP ("H1", ? X, AbsP ("H2", ? A,
berghofe@12866
    80
          equal_elim_axm %> D %> C %%
berghofe@12866
    81
            (symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2)
berghofe@12866
    82
              %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
berghofe@12866
    83
        end
berghofe@11522
    84
berghofe@12866
    85
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@11612
    86
        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
berghofe@11612
    87
          (PAxm ("ProtoPure.reflexive", _, _) % _) %%
berghofe@12866
    88
            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
berghofe@12866
    89
        let
berghofe@12866
    90
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
    91
          val _ $ Q = Envir.beta_norm Y;
berghofe@12866
    92
        in Some (AbsP ("H", ? X, Abst ("x", ty T,
berghofe@12866
    93
            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
berghofe@12866
    94
              (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
berghofe@12866
    95
        end
berghofe@12866
    96
berghofe@12866
    97
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
berghofe@12866
    98
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
berghofe@12866
    99
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
berghofe@12866
   100
            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
berghofe@12866
   101
              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
berghofe@12866
   102
        let
berghofe@12866
   103
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
   104
          val _ $ Q = Envir.beta_norm Y;
berghofe@12866
   105
          val t = incr_boundvars 1 P $ Bound 0;
berghofe@12866
   106
          val u = incr_boundvars 1 Q $ Bound 0
berghofe@12866
   107
        in Some (AbsP ("H", ? X, Abst ("x", ty T,
berghofe@12866
   108
          equal_elim_axm %> t %> u %%
berghofe@12866
   109
            (symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0))
berghofe@12866
   110
              %% (PBound 0 %> Bound 0))))
berghofe@12866
   111
        end
berghofe@12866
   112
berghofe@12866
   113
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
berghofe@12866
   114
        (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
berghofe@12866
   115
           Some (equal_elim_axm %> B %> C %% prf2 %%
berghofe@12866
   116
             (equal_elim_axm %> A %> B %% prf1 %% prf3))
berghofe@12866
   117
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
berghofe@12866
   118
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   119
          (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
berghofe@12866
   120
           Some (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %%
berghofe@12866
   121
             (equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3))
berghofe@12866
   122
berghofe@12866
   123
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   124
        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
berghofe@12866
   125
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   126
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   127
          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf
berghofe@12866
   128
berghofe@12866
   129
      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   130
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = Some prf
berghofe@11522
   131
berghofe@12866
   132
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   133
        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
berghofe@12866
   134
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   135
            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   136
              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
berghofe@12866
   137
          Some (equal_elim_axm %> C %> D %% prf2 %%
berghofe@12866
   138
            (equal_elim_axm %> A %> C %% prf3 %%
berghofe@12866
   139
              (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4)))
berghofe@12866
   140
berghofe@12866
   141
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   142
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   143
          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
berghofe@12866
   144
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   145
              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   146
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
berghofe@12866
   147
          Some (equal_elim_axm %> A %> B %% prf1 %%
berghofe@12866
   148
            (equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %%
berghofe@12866
   149
              (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4)))
berghofe@11522
   150
berghofe@12866
   151
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   152
        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
berghofe@12866
   153
          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   154
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   155
              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   156
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
berghofe@12866
   157
          Some (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %%
berghofe@12866
   158
            (equal_elim_axm %> B %> D %% prf3 %%
berghofe@12866
   159
              (equal_elim_axm %> A %> B %% prf1 %% prf4)))
berghofe@11522
   160
berghofe@12866
   161
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   162
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   163
          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
berghofe@12866
   164
            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   165
              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
berghofe@12866
   166
                (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   167
                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
berghofe@12866
   168
          Some (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %%
berghofe@12866
   169
            (equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
berghofe@12866
   170
              (equal_elim_axm %> C %> D %% prf2 %% prf4)))
berghofe@11522
   171
berghofe@12866
   172
      | rew' _ _ = None;
berghofe@12866
   173
  in rew' end;
berghofe@12866
   174
berghofe@12866
   175
fun rprocs b = [("Pure/meta_equality", rew b)];
berghofe@12866
   176
val setup = [Proofterm.add_prf_rprocs (rprocs false)];
berghofe@11522
   177
berghofe@12906
   178
berghofe@12906
   179
(**** apply rewriting function to all terms in proof ****)
berghofe@12906
   180
berghofe@12906
   181
fun rewrite_terms r =
berghofe@12906
   182
  let
berghofe@12906
   183
    fun rew_term Ts t =
berghofe@12906
   184
      let
berghofe@12906
   185
        val frees = map Free (variantlist
berghofe@12906
   186
          (replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
berghofe@12906
   187
        val t' = r (subst_bounds (frees, t));
berghofe@12906
   188
        fun strip [] t = t
berghofe@12906
   189
          | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
berghofe@12906
   190
      in
berghofe@12906
   191
        strip Ts (foldl (uncurry lambda o Library.swap) (t', frees))
berghofe@12906
   192
      end;
berghofe@12906
   193
berghofe@12906
   194
    fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
berghofe@12906
   195
      | rew Ts (prf % Some t) = rew Ts prf % Some (rew_term Ts t)
berghofe@12906
   196
      | rew Ts (Abst (s, Some T, prf)) = Abst (s, Some T, rew (T :: Ts) prf)
berghofe@12906
   197
      | rew Ts (AbsP (s, Some t, prf)) = AbsP (s, Some (rew_term Ts t), rew Ts prf)
berghofe@12906
   198
      | rew _ prf = prf
berghofe@12906
   199
berghofe@12906
   200
  in rew [] end;
berghofe@12906
   201
berghofe@12906
   202
berghofe@12906
   203
(**** eliminate definitions in proof ****)
berghofe@12906
   204
berghofe@12906
   205
fun abs_def thm =
berghofe@12906
   206
  let
berghofe@12906
   207
    val (_, cvs) = Drule.strip_comb (fst (dest_equals (cprop_of thm)));
berghofe@12906
   208
    val thm' = foldr (fn (ct, thm) =>
berghofe@12906
   209
      Thm.abstract_rule (fst (fst (dest_Var (term_of ct)))) ct thm) (cvs, thm);
berghofe@12906
   210
  in
berghofe@12906
   211
    MetaSimplifier.fconv_rule Thm.eta_conversion thm'
berghofe@12906
   212
  end;
berghofe@12906
   213
berghofe@12906
   214
fun vars_of t = rev (foldl_aterms
berghofe@12906
   215
  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
berghofe@12906
   216
berghofe@12906
   217
fun insert_refl defs Ts (prf1 %% prf2) =
berghofe@12906
   218
      insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
berghofe@12906
   219
  | insert_refl defs Ts (Abst (s, Some T, prf)) =
berghofe@12906
   220
      Abst (s, Some T, insert_refl defs (T :: Ts) prf)
berghofe@12906
   221
  | insert_refl defs Ts (AbsP (s, t, prf)) =
berghofe@12906
   222
      AbsP (s, t, insert_refl defs Ts prf)
berghofe@12906
   223
  | insert_refl defs Ts prf = (case strip_combt prf of
berghofe@12906
   224
        (PThm ((s, _), _, prop, Some Ts), ts) =>
berghofe@12906
   225
          if s mem defs then
berghofe@12906
   226
            let
berghofe@12906
   227
              val vs = vars_of prop;
berghofe@12906
   228
              val tvars = term_tvars prop;
berghofe@12906
   229
              val (_, rhs) = Logic.dest_equals prop;
berghofe@12906
   230
              val rhs' = foldl betapply (subst_TVars (map fst tvars ~~ Ts)
berghofe@12906
   231
                (foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
berghofe@12906
   232
                map the ts);
berghofe@12906
   233
            in
berghofe@12906
   234
              change_type (Some [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
berghofe@12906
   235
            end
berghofe@12906
   236
          else prf
berghofe@12906
   237
      | (_, []) => prf
berghofe@12906
   238
      | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
berghofe@12906
   239
berghofe@12906
   240
fun elim_defs sign defs prf =
berghofe@12906
   241
  let
berghofe@12906
   242
    val tsig = Sign.tsig_of sign;
berghofe@12906
   243
    val defs' = map (Logic.dest_equals o prop_of o abs_def) defs;
berghofe@12906
   244
    val defnames = map Thm.name_of_thm defs;
berghofe@12906
   245
    val cnames = map (fst o dest_Const o fst) defs';
berghofe@12906
   246
    val thmnames = map fst (filter_out (fn (s, ps) =>
berghofe@12906
   247
      null (foldr add_term_consts (map fst ps, []) inter cnames))
berghofe@12906
   248
        (Symtab.dest (thms_of_proof Symtab.empty prf))) \\ defnames
berghofe@12906
   249
  in
berghofe@12906
   250
    rewrite_terms (Pattern.rewrite_term tsig defs') (insert_refl defnames []
berghofe@12906
   251
      (Reconstruct.expand_proof sign thmnames prf))
berghofe@12906
   252
  end;
berghofe@12906
   253
berghofe@11522
   254
end;