src/Pure/Proof/proof_rewrite_rules.ML
author wenzelm
Thu May 31 23:47:36 2007 +0200 (2007-05-31 ago)
changeset 23178 07ba6b58b3d2
parent 22662 3e492ba59355
child 26424 a6cad32a27b0
permissions -rw-r--r--
simplified/unified list fold;
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
wenzelm@17203
    13
  val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
berghofe@13608
    14
  val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
berghofe@22280
    15
  val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
berghofe@22280
    16
  val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
berghofe@11522
    17
end;
berghofe@11522
    18
berghofe@11522
    19
structure ProofRewriteRules : PROOF_REWRITE_RULES =
berghofe@11522
    20
struct
berghofe@11522
    21
berghofe@11522
    22
open Proofterm;
berghofe@11522
    23
wenzelm@19309
    24
fun rew b _ =
berghofe@12866
    25
  let
haftmann@17137
    26
    fun ?? x = if b then SOME x else NONE;
berghofe@12866
    27
    fun ax (prf as PAxm (s, prop, _)) Ts =
skalberg@15531
    28
      if b then PAxm (s, prop, SOME Ts) else prf;
berghofe@12866
    29
    fun ty T = if b then
berghofe@12866
    30
        let val Type (_, [Type (_, [U, _]), _]) = T
skalberg@15531
    31
        in SOME U end
skalberg@15531
    32
      else NONE;
berghofe@12866
    33
    val equal_intr_axm = ax equal_intr_axm [];
berghofe@12866
    34
    val equal_elim_axm = ax equal_elim_axm [];
berghofe@12866
    35
    val symmetric_axm = ax symmetric_axm [propT];
berghofe@11522
    36
wenzelm@21646
    37
    fun rew' (PThm ("ProtoPure.protectD", _, _, _) % _ %%
wenzelm@21646
    38
        (PThm ("ProtoPure.protectI", _, _, _) % _ %% prf)) = SOME prf
wenzelm@21646
    39
      | rew' (PThm ("ProtoPure.conjunctionD1", _, _, _) % _ % _ %%
wenzelm@21646
    40
        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
wenzelm@21646
    41
      | rew' (PThm ("ProtoPure.conjunctionD2", _, _, _) % _ % _ %%
wenzelm@21646
    42
        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
wenzelm@19309
    43
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
skalberg@15531
    44
        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
wenzelm@19309
    45
      | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    46
        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
skalberg@15531
    47
            SOME (equal_intr_axm % B % A %% prf2 %% prf1)
berghofe@12002
    48
wenzelm@19309
    49
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
wenzelm@18024
    50
        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
berghofe@12866
    51
          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
wenzelm@21646
    52
        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
skalberg@15531
    53
        SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
berghofe@12002
    54
wenzelm@19309
    55
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
berghofe@12866
    56
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
wenzelm@18024
    57
          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
berghofe@12866
    58
             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
wenzelm@21646
    59
        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
skalberg@15531
    60
        SOME (tg %> B %% (equal_elim_axm %> A %> B %%
haftmann@17137
    61
          (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
berghofe@11522
    62
wenzelm@19309
    63
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
berghofe@11612
    64
        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
    65
          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
berghofe@12866
    66
             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
berghofe@12866
    67
        let
berghofe@12866
    68
          val _ $ A $ C = Envir.beta_norm X;
berghofe@12866
    69
          val _ $ B $ D = Envir.beta_norm Y
haftmann@17137
    70
        in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
berghofe@12866
    71
          equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
berghofe@12866
    72
            (PBound 1 %% (equal_elim_axm %> B %> A %%
haftmann@17137
    73
              (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
berghofe@12866
    74
        end
berghofe@11522
    75
wenzelm@19309
    76
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
berghofe@12866
    77
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
    78
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
    79
            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
berghofe@12866
    80
               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
berghofe@12866
    81
        let
berghofe@12866
    82
          val _ $ A $ C = Envir.beta_norm Y;
berghofe@12866
    83
          val _ $ B $ D = Envir.beta_norm X
haftmann@17137
    84
        in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
berghofe@12866
    85
          equal_elim_axm %> D %> C %%
haftmann@17137
    86
            (symmetric_axm % ?? C % ?? D %% incr_pboundvars 2 0 prf2)
berghofe@12866
    87
              %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
berghofe@12866
    88
        end
berghofe@11522
    89
wenzelm@19309
    90
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
skalberg@15531
    91
        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
berghofe@11612
    92
          (PAxm ("ProtoPure.reflexive", _, _) % _) %%
berghofe@12866
    93
            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
berghofe@12866
    94
        let
berghofe@12866
    95
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
    96
          val _ $ Q = Envir.beta_norm Y;
haftmann@17137
    97
        in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
berghofe@12866
    98
            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
berghofe@12866
    99
              (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
berghofe@12866
   100
        end
berghofe@12866
   101
wenzelm@19309
   102
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
berghofe@12866
   103
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
skalberg@15531
   104
          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
berghofe@12866
   105
            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
berghofe@12866
   106
              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
berghofe@12866
   107
        let
berghofe@12866
   108
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
   109
          val _ $ Q = Envir.beta_norm Y;
berghofe@12866
   110
          val t = incr_boundvars 1 P $ Bound 0;
berghofe@12866
   111
          val u = incr_boundvars 1 Q $ Bound 0
haftmann@17137
   112
        in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
berghofe@12866
   113
          equal_elim_axm %> t %> u %%
haftmann@17137
   114
            (symmetric_axm % ?? u % ?? t %% (incr_pboundvars 1 1 prf %> Bound 0))
berghofe@12866
   115
              %% (PBound 0 %> Bound 0))))
berghofe@12866
   116
        end
berghofe@12866
   117
wenzelm@19309
   118
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
skalberg@15531
   119
        (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
skalberg@15531
   120
           SOME (equal_elim_axm %> B %> C %% prf2 %%
berghofe@12866
   121
             (equal_elim_axm %> A %> B %% prf1 %% prf3))
wenzelm@19309
   122
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
berghofe@12866
   123
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   124
          (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
haftmann@17137
   125
           SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %%
haftmann@17137
   126
             (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf2) %% prf3))
berghofe@12866
   127
wenzelm@19309
   128
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
skalberg@15531
   129
        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf
wenzelm@19309
   130
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   131
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   132
          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf
berghofe@12866
   133
wenzelm@19309
   134
      | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   135
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
berghofe@11522
   136
wenzelm@19309
   137
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
skalberg@15531
   138
        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
berghofe@12866
   139
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   140
            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   141
              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
skalberg@15531
   142
          SOME (equal_elim_axm %> C %> D %% prf2 %%
berghofe@12866
   143
            (equal_elim_axm %> A %> C %% prf3 %%
haftmann@17137
   144
              (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% prf4)))
berghofe@12866
   145
wenzelm@19309
   146
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   147
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   148
          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
berghofe@12866
   149
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   150
              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   151
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
skalberg@15531
   152
          SOME (equal_elim_axm %> A %> B %% prf1 %%
haftmann@17137
   153
            (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
haftmann@17137
   154
              (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4)))
berghofe@11522
   155
wenzelm@19309
   156
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
skalberg@15531
   157
        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
berghofe@12866
   158
          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   159
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   160
              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   161
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
haftmann@17137
   162
          SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
berghofe@12866
   163
            (equal_elim_axm %> B %> D %% prf3 %%
berghofe@12866
   164
              (equal_elim_axm %> A %> B %% prf1 %% prf4)))
berghofe@11522
   165
wenzelm@19309
   166
      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
berghofe@12866
   167
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
skalberg@15531
   168
          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
berghofe@12866
   169
            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
berghofe@12866
   170
              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
skalberg@15531
   171
                (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
berghofe@12866
   172
                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
haftmann@17137
   173
          SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
haftmann@17137
   174
            (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
berghofe@12866
   175
              (equal_elim_axm %> C %> D %% prf2 %% prf4)))
berghofe@11522
   176
wenzelm@19309
   177
      | rew' ((prf as PAxm ("ProtoPure.combination", _, _) %
skalberg@15531
   178
        SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
berghofe@13257
   179
          (PAxm ("ProtoPure.reflexive", _, _) % _)) =
berghofe@13257
   180
        let val (U, V) = (case T of
berghofe@13257
   181
          Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
haftmann@17137
   182
        in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%
haftmann@17137
   183
          (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
berghofe@13257
   184
        end
berghofe@13257
   185
wenzelm@19309
   186
      | rew' _ = NONE;
berghofe@12866
   187
  in rew' end;
berghofe@12866
   188
berghofe@12866
   189
fun rprocs b = [("Pure/meta_equality", rew b)];
haftmann@22662
   190
val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false));
berghofe@11522
   191
berghofe@12906
   192
berghofe@12906
   193
(**** apply rewriting function to all terms in proof ****)
berghofe@12906
   194
berghofe@12906
   195
fun rewrite_terms r =
berghofe@12906
   196
  let
berghofe@12906
   197
    fun rew_term Ts t =
berghofe@12906
   198
      let
wenzelm@20076
   199
        val frees = map Free (Name.invent_list (add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
berghofe@12906
   200
        val t' = r (subst_bounds (frees, t));
berghofe@12906
   201
        fun strip [] t = t
berghofe@12906
   202
          | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
berghofe@12906
   203
      in
wenzelm@19473
   204
        strip Ts (fold lambda frees t')
berghofe@12906
   205
      end;
berghofe@12906
   206
berghofe@12906
   207
    fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
skalberg@15531
   208
      | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
skalberg@15531
   209
      | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
skalberg@15531
   210
      | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
berghofe@12906
   211
      | rew _ prf = prf
berghofe@12906
   212
berghofe@12906
   213
  in rew [] end;
berghofe@12906
   214
berghofe@12906
   215
berghofe@12906
   216
(**** eliminate definitions in proof ****)
berghofe@12906
   217
wenzelm@16861
   218
fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
berghofe@12906
   219
berghofe@12906
   220
fun insert_refl defs Ts (prf1 %% prf2) =
berghofe@12906
   221
      insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
skalberg@15531
   222
  | insert_refl defs Ts (Abst (s, SOME T, prf)) =
skalberg@15531
   223
      Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
berghofe@12906
   224
  | insert_refl defs Ts (AbsP (s, t, prf)) =
berghofe@12906
   225
      AbsP (s, t, insert_refl defs Ts prf)
berghofe@12906
   226
  | insert_refl defs Ts prf = (case strip_combt prf of
wenzelm@21646
   227
        (PThm (s, _, prop, SOME Ts), ts) =>
wenzelm@20664
   228
          if member (op =) defs s then
berghofe@12906
   229
            let
berghofe@12906
   230
              val vs = vars_of prop;
berghofe@12906
   231
              val tvars = term_tvars prop;
berghofe@12906
   232
              val (_, rhs) = Logic.dest_equals prop;
wenzelm@18185
   233
              val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
wenzelm@23178
   234
                (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
wenzelm@19466
   235
                map the ts);
berghofe@12906
   236
            in
skalberg@15531
   237
              change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
berghofe@12906
   238
            end
berghofe@12906
   239
          else prf
berghofe@12906
   240
      | (_, []) => prf
berghofe@12906
   241
      | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
berghofe@12906
   242
wenzelm@17203
   243
fun elim_defs thy r defs prf =
berghofe@12906
   244
  let
berghofe@13341
   245
    val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
wenzelm@21646
   246
    val defnames = map Thm.get_name defs;
berghofe@13341
   247
    val f = if not r then I else
berghofe@13341
   248
      let
berghofe@13341
   249
        val cnames = map (fst o dest_Const o fst) defs';
wenzelm@19482
   250
        val thms = maps (fn (s, ps) =>
wenzelm@20664
   251
            if member (op =) defnames s then []
skalberg@15531
   252
            else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
nipkow@13646
   253
              null (term_consts p inter cnames)) ps))
wenzelm@19482
   254
          (Symtab.dest (thms_of_proof prf Symtab.empty))
wenzelm@17203
   255
      in Reconstruct.expand_proof thy thms end
berghofe@12906
   256
  in
wenzelm@17203
   257
    rewrite_terms (Pattern.rewrite_term thy defs' [])
berghofe@13341
   258
      (insert_refl defnames [] (f prf))
berghofe@12906
   259
  end;
berghofe@12906
   260
berghofe@13608
   261
berghofe@13608
   262
(**** eliminate all variables that don't occur in the proposition ****)
berghofe@13608
   263
berghofe@13608
   264
fun elim_vars mk_default prf =
berghofe@13608
   265
  let
berghofe@13608
   266
    val prop = Reconstruct.prop_of prf;
wenzelm@19309
   267
    val tv = Term.add_vars prop [];
wenzelm@19309
   268
    val tf = Term.add_frees prop [];
wenzelm@19309
   269
wenzelm@19309
   270
    fun hidden_variable (Var v) = not (member (op =) tv v)
wenzelm@19309
   271
      | hidden_variable (Free f) = not (member (op =) tf f)
wenzelm@19309
   272
      | hidden_variable _ = false;
berghofe@13917
   273
berghofe@13917
   274
    fun mk_default' T = list_abs
berghofe@13917
   275
      (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
berghofe@13917
   276
berghofe@13917
   277
    fun elim_varst (t $ u) = elim_varst t $ elim_varst u
berghofe@13917
   278
      | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
wenzelm@19309
   279
      | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
wenzelm@19309
   280
      | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
wenzelm@19309
   281
      | elim_varst t = t;
berghofe@13608
   282
  in
wenzelm@19309
   283
    map_proof_terms (fn t =>
wenzelm@19309
   284
      if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
berghofe@13608
   285
  end;
berghofe@13608
   286
berghofe@22280
   287
berghofe@22280
   288
(**** convert between hhf and non-hhf form ****)
berghofe@22280
   289
berghofe@22280
   290
fun hhf_proof P Q prf =
berghofe@22280
   291
  let
berghofe@22280
   292
    val params = Logic.strip_params Q;
berghofe@22280
   293
    val Hs = Logic.strip_assums_hyp P;
berghofe@22280
   294
    val Hs' = Logic.strip_assums_hyp Q;
berghofe@22280
   295
    val k = length Hs;
berghofe@22280
   296
    val l = length params;
berghofe@22280
   297
    fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
berghofe@22280
   298
          mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
berghofe@22280
   299
      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
berghofe@22280
   300
          mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
berghofe@22280
   301
      | mk_prf _ _ _ _ _ prf = prf
berghofe@22280
   302
  in
berghofe@22280
   303
    prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
berghofe@22280
   304
    fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>
berghofe@22280
   305
    fold_rev (fn (s, T) => fn prf => Abst (s, SOME T, prf)) params
berghofe@22280
   306
  end
berghofe@22280
   307
and un_hhf_proof P Q prf =
berghofe@22280
   308
  let
berghofe@22280
   309
    val params = Logic.strip_params Q;
berghofe@22280
   310
    val Hs = Logic.strip_assums_hyp P;
berghofe@22280
   311
    val Hs' = Logic.strip_assums_hyp Q;
berghofe@22280
   312
    val k = length Hs;
berghofe@22280
   313
    val l = length params;
berghofe@22280
   314
    fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
berghofe@22280
   315
          Abst (s, SOME T, mk_prf P prf)
berghofe@22280
   316
      | mk_prf (Const ("==>", _) $ P $ Q) prf =
berghofe@22280
   317
          AbsP ("H", SOME P, mk_prf Q prf)
berghofe@22280
   318
      | mk_prf _ prf = prf
berghofe@22280
   319
  in
berghofe@22280
   320
    prf |> Proofterm.incr_pboundvars k l |>
berghofe@22280
   321
    fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>
berghofe@22280
   322
    fold (fn ((H, H'), i) => fn prf => prf %% hhf_proof H' H (PBound i))
berghofe@22280
   323
      (Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
berghofe@22280
   324
    mk_prf Q
berghofe@22280
   325
  end;
berghofe@22280
   326
berghofe@11522
   327
end;