src/Pure/Proof/proof_rewrite_rules.ML
author wenzelm
Fri Jul 15 15:44:15 2005 +0200 (2005-07-15 ago)
changeset 16861 7446b4be013b
parent 16787 b6b6e2faaa41
child 17018 1e9e0f5877f2
permissions -rw-r--r--
tuned fold on terms;
berghofe@11522
     1
(*  Title:      Pure/Proof/proof_rewrite_rules.ML
berghofe@11522
     2
    ID:         $Id$
wenzelm@11539
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@11522
     4
berghofe@12906
     5
Simplification functions for proof terms involving meta level rules.
berghofe@11522
     6
*)
berghofe@11522
     7
berghofe@11522
     8
signature PROOF_REWRITE_RULES =
berghofe@11522
     9
sig
berghofe@12866
    10
  val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
berghofe@12866
    11
  val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
berghofe@12906
    12
  val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
berghofe@13341
    13
  val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
berghofe@13608
    14
  val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
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
skalberg@15531
    24
    fun ? x = if b then SOME x else NONE;
berghofe@12866
    25
    fun ax (prf as PAxm (s, prop, _)) Ts =
skalberg@15531
    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
skalberg@15531
    29
        in SOME U end
skalberg@15531
    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", _), _, _, _) % _ %%
skalberg@15531
    36
        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = SOME prf
berghofe@12866
    37
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
skalberg@15531
    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)) =
skalberg@15531
    41
            SOME (equal_intr_axm % B % A %% prf2 %% prf1)
berghofe@12002
    42
skalberg@15531
    43
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
skalberg@15531
    44
        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
berghofe@12866
    45
          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
berghofe@12866
    46
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
skalberg@15531
    47
        SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
berghofe@12002
    48
skalberg@15531
    49
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
berghofe@12866
    50
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
    51
          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
berghofe@12866
    52
             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
berghofe@12866
    53
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
skalberg@15531
    54
        SOME (tg %> B %% (equal_elim_axm %> A %> B %%
berghofe@12866
    55
          (symmetric_axm % ? B % ? A %% prf1) %% prf2))
berghofe@11522
    56
skalberg@15531
    57
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
berghofe@11612
    58
        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
    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
skalberg@15531
    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
skalberg@15531
    70
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
berghofe@12866
    71
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    72
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
    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
skalberg@15531
    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
skalberg@15531
    84
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
skalberg@15531
    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;
skalberg@15531
    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
skalberg@15531
    96
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
berghofe@12866
    97
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
skalberg@15531
    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
skalberg@15531
   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
skalberg@15531
   112
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
skalberg@15531
   113
        (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
skalberg@15531
   114
           SOME (equal_elim_axm %> B %> C %% prf2 %%
berghofe@12866
   115
             (equal_elim_axm %> A %> B %% prf1 %% prf3))
skalberg@15531
   116
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
berghofe@12866
   117
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   118
          (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
skalberg@15531
   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", _, _) % _ % _ %%
skalberg@15531
   123
        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf
berghofe@12866
   124
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   125
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   126
          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf
berghofe@12866
   127
berghofe@12866
   128
      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   129
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
berghofe@11522
   130
berghofe@12866
   131
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
skalberg@15531
   132
        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
berghofe@12866
   133
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   134
            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   135
              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
skalberg@15531
   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", _, _) % _ % _ %%
skalberg@15531
   142
          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
berghofe@12866
   143
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   144
              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   145
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
skalberg@15531
   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", _, _) % _ % _ %%
skalberg@15531
   151
        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
berghofe@12866
   152
          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   153
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   154
              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   155
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
skalberg@15531
   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", _, _) % _ % _ %%
skalberg@15531
   162
          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
berghofe@12866
   163
            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   164
              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   165
                (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   166
                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
skalberg@15531
   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@13257
   171
      | rew' _ ((prf as PAxm ("ProtoPure.combination", _, _) %
skalberg@15531
   172
        SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
berghofe@13257
   173
          (PAxm ("ProtoPure.reflexive", _, _) % _)) =
berghofe@13257
   174
        let val (U, V) = (case T of
berghofe@13257
   175
          Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
skalberg@15531
   176
        in SOME (prf %% (ax combination_axm [V, U] %> eq % ? eq % ? t % ? t %%
berghofe@13257
   177
          (ax reflexive_axm [T] % ? eq) %% (ax reflexive_axm [U] % ? t)))
berghofe@13257
   178
        end
berghofe@13257
   179
skalberg@15531
   180
      | rew' _ _ = NONE;
berghofe@12866
   181
  in rew' end;
berghofe@12866
   182
berghofe@12866
   183
fun rprocs b = [("Pure/meta_equality", rew b)];
wenzelm@15801
   184
val _ = Context.add_setup [Proofterm.add_prf_rprocs (rprocs false)];
berghofe@11522
   185
berghofe@12906
   186
berghofe@12906
   187
(**** apply rewriting function to all terms in proof ****)
berghofe@12906
   188
berghofe@12906
   189
fun rewrite_terms r =
berghofe@12906
   190
  let
berghofe@12906
   191
    fun rew_term Ts t =
berghofe@12906
   192
      let
berghofe@12906
   193
        val frees = map Free (variantlist
berghofe@12906
   194
          (replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
berghofe@12906
   195
        val t' = r (subst_bounds (frees, t));
berghofe@12906
   196
        fun strip [] t = t
berghofe@12906
   197
          | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
berghofe@12906
   198
      in
skalberg@15570
   199
        strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees))
berghofe@12906
   200
      end;
berghofe@12906
   201
berghofe@12906
   202
    fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
skalberg@15531
   203
      | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
skalberg@15531
   204
      | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
skalberg@15531
   205
      | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
berghofe@12906
   206
      | rew _ prf = prf
berghofe@12906
   207
berghofe@12906
   208
  in rew [] end;
berghofe@12906
   209
berghofe@12906
   210
berghofe@12906
   211
(**** eliminate definitions in proof ****)
berghofe@12906
   212
wenzelm@16861
   213
fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
berghofe@12906
   214
berghofe@12906
   215
fun insert_refl defs Ts (prf1 %% prf2) =
berghofe@12906
   216
      insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
skalberg@15531
   217
  | insert_refl defs Ts (Abst (s, SOME T, prf)) =
skalberg@15531
   218
      Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
berghofe@12906
   219
  | insert_refl defs Ts (AbsP (s, t, prf)) =
berghofe@12906
   220
      AbsP (s, t, insert_refl defs Ts prf)
berghofe@12906
   221
  | insert_refl defs Ts prf = (case strip_combt prf of
skalberg@15531
   222
        (PThm ((s, _), _, prop, SOME Ts), ts) =>
berghofe@12906
   223
          if s mem defs then
berghofe@12906
   224
            let
berghofe@12906
   225
              val vs = vars_of prop;
berghofe@12906
   226
              val tvars = term_tvars prop;
berghofe@12906
   227
              val (_, rhs) = Logic.dest_equals prop;
skalberg@15570
   228
              val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
skalberg@15574
   229
                (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
skalberg@15570
   230
                map valOf ts);
berghofe@12906
   231
            in
skalberg@15531
   232
              change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
berghofe@12906
   233
            end
berghofe@12906
   234
          else prf
berghofe@12906
   235
      | (_, []) => prf
berghofe@12906
   236
      | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
berghofe@12906
   237
berghofe@13341
   238
fun elim_defs sign r defs prf =
berghofe@12906
   239
  let
berghofe@12906
   240
    val tsig = Sign.tsig_of sign;
berghofe@13341
   241
    val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
berghofe@12906
   242
    val defnames = map Thm.name_of_thm defs;
berghofe@13341
   243
    val f = if not r then I else
berghofe@13341
   244
      let
berghofe@13341
   245
        val cnames = map (fst o dest_Const o fst) defs';
skalberg@15570
   246
        val thms = List.concat (map (fn (s, ps) =>
berghofe@13341
   247
            if s mem defnames then []
skalberg@15531
   248
            else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
nipkow@13646
   249
              null (term_consts p inter cnames)) ps))
berghofe@13341
   250
          (Symtab.dest (thms_of_proof Symtab.empty prf)))
berghofe@13341
   251
      in Reconstruct.expand_proof sign thms end
berghofe@12906
   252
  in
berghofe@13341
   253
    rewrite_terms (Pattern.rewrite_term tsig defs' [])
berghofe@13341
   254
      (insert_refl defnames [] (f prf))
berghofe@12906
   255
  end;
berghofe@12906
   256
berghofe@13608
   257
berghofe@13608
   258
(**** eliminate all variables that don't occur in the proposition ****)
berghofe@13608
   259
berghofe@13608
   260
fun elim_vars mk_default prf =
berghofe@13608
   261
  let
berghofe@13608
   262
    val prop = Reconstruct.prop_of prf;
berghofe@13917
   263
    val tv = term_vars prop;
berghofe@13917
   264
    val tf = term_frees prop;
berghofe@13917
   265
berghofe@13917
   266
    fun mk_default' T = list_abs
berghofe@13917
   267
      (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
berghofe@13917
   268
berghofe@13917
   269
    fun elim_varst (t $ u) = elim_varst t $ elim_varst u
berghofe@13917
   270
      | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
berghofe@13917
   271
      | elim_varst (f as Free (_, T)) = if f mem tf then f else mk_default' T
berghofe@13917
   272
      | elim_varst (v as Var (_, T)) = if v mem tv then v else mk_default' T
berghofe@13917
   273
      | elim_varst t = t
berghofe@13608
   274
  in
berghofe@13917
   275
    map_proof_terms (fn t => if not (null (term_vars t \\ tv)) orelse
berghofe@13917
   276
        not (null (term_frees t \\ tf)) then Envir.beta_norm (elim_varst t)
berghofe@13917
   277
      else t) I prf
berghofe@13608
   278
  end;
berghofe@13608
   279
berghofe@11522
   280
end;