src/Pure/Proof/proof_rewrite_rules.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 62922 96691631c1eb
child 70412 64ead6de6212
permissions -rw-r--r--
tuned;
berghofe@11522
     1
(*  Title:      Pure/Proof/proof_rewrite_rules.ML
wenzelm@11539
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@11522
     3
berghofe@12906
     4
Simplification functions for proof terms involving meta level rules.
berghofe@11522
     5
*)
berghofe@11522
     6
berghofe@11522
     7
signature PROOF_REWRITE_RULES =
berghofe@11522
     8
sig
berghofe@37233
     9
  val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
wenzelm@33722
    10
  val rprocs : bool ->
berghofe@37233
    11
    (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
berghofe@12906
    12
  val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
wenzelm@62922
    13
  val elim_defs : Proof.context -> 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
wenzelm@62922
    17
  val mk_of_sort_proof : Proof.context -> term option list -> typ * sort -> Proofterm.proof list
wenzelm@62922
    18
  val expand_of_class : Proof.context -> typ list -> term option list -> Proofterm.proof ->
berghofe@37233
    19
    (Proofterm.proof * Proofterm.proof) option
berghofe@11522
    20
end;
berghofe@11522
    21
berghofe@11522
    22
structure ProofRewriteRules : PROOF_REWRITE_RULES =
berghofe@11522
    23
struct
berghofe@11522
    24
berghofe@37233
    25
fun rew b _ _ =
berghofe@12866
    26
  let
haftmann@17137
    27
    fun ?? x = if b then SOME x else NONE;
berghofe@12866
    28
    fun ax (prf as PAxm (s, prop, _)) Ts =
skalberg@15531
    29
      if b then PAxm (s, prop, SOME Ts) else prf;
berghofe@12866
    30
    fun ty T = if b then
berghofe@12866
    31
        let val Type (_, [Type (_, [U, _]), _]) = T
skalberg@15531
    32
        in SOME U end
skalberg@15531
    33
      else NONE;
wenzelm@37310
    34
    val equal_intr_axm = ax Proofterm.equal_intr_axm [];
wenzelm@37310
    35
    val equal_elim_axm = ax Proofterm.equal_elim_axm [];
wenzelm@37310
    36
    val symmetric_axm = ax Proofterm.symmetric_axm [propT];
berghofe@11522
    37
wenzelm@28806
    38
    fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
wenzelm@28806
    39
        (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
wenzelm@28806
    40
      | rew' (PThm (_, (("Pure.conjunctionD1", _, _), _)) % _ % _ %%
wenzelm@28806
    41
        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% prf %% _)) = SOME prf
wenzelm@28806
    42
      | rew' (PThm (_, (("Pure.conjunctionD2", _, _), _)) % _ % _ %%
wenzelm@28806
    43
        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
wenzelm@26424
    44
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
wenzelm@26424
    45
        (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
wenzelm@26424
    46
      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
    47
        (PAxm ("Pure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
skalberg@15531
    48
            SOME (equal_intr_axm % B % A %% prf2 %% prf1)
berghofe@12002
    49
wenzelm@26424
    50
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
wenzelm@56244
    51
        (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
wenzelm@26424
    52
          _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
wenzelm@28806
    53
        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
skalberg@15531
    54
        SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
berghofe@12002
    55
wenzelm@26424
    56
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
wenzelm@26424
    57
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@56244
    58
          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
wenzelm@26424
    59
             _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
wenzelm@28806
    60
        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
skalberg@15531
    61
        SOME (tg %> B %% (equal_elim_axm %> A %> B %%
haftmann@17137
    62
          (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
berghofe@11522
    63
wenzelm@26424
    64
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
wenzelm@26424
    65
        (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
wenzelm@56245
    66
          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
wenzelm@26424
    67
             (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
berghofe@12866
    68
        let
berghofe@12866
    69
          val _ $ A $ C = Envir.beta_norm X;
berghofe@12866
    70
          val _ $ B $ D = Envir.beta_norm Y
haftmann@17137
    71
        in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
wenzelm@37310
    72
          Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %%
berghofe@12866
    73
            (PBound 1 %% (equal_elim_axm %> B %> A %%
wenzelm@37310
    74
              (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %%
wenzelm@37310
    75
                PBound 0)))))
berghofe@12866
    76
        end
berghofe@11522
    77
wenzelm@26424
    78
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
wenzelm@26424
    79
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
    80
          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
wenzelm@56245
    81
            (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
wenzelm@26424
    82
               (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
berghofe@12866
    83
        let
berghofe@12866
    84
          val _ $ A $ C = Envir.beta_norm Y;
berghofe@12866
    85
          val _ $ B $ D = Envir.beta_norm X
haftmann@17137
    86
        in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
berghofe@12866
    87
          equal_elim_axm %> D %> C %%
wenzelm@37310
    88
            (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %%
wenzelm@37310
    89
              (PBound 1 %%
wenzelm@37310
    90
                (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0)))))
berghofe@12866
    91
        end
berghofe@11522
    92
wenzelm@26424
    93
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
wenzelm@56245
    94
        (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
wenzelm@26424
    95
          (PAxm ("Pure.reflexive", _, _) % _) %%
wenzelm@26424
    96
            (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
berghofe@12866
    97
        let
berghofe@12866
    98
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
    99
          val _ $ Q = Envir.beta_norm Y;
haftmann@17137
   100
        in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
berghofe@12866
   101
            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
wenzelm@37310
   102
              (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
berghofe@12866
   103
        end
berghofe@12866
   104
wenzelm@26424
   105
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
wenzelm@26424
   106
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
wenzelm@56245
   107
          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
wenzelm@26424
   108
            (PAxm ("Pure.reflexive", _, _) % _) %%
wenzelm@26424
   109
              (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
berghofe@12866
   110
        let
berghofe@12866
   111
          val Const (_, T) $ P = Envir.beta_norm X;
berghofe@12866
   112
          val _ $ Q = Envir.beta_norm Y;
berghofe@12866
   113
          val t = incr_boundvars 1 P $ Bound 0;
berghofe@12866
   114
          val u = incr_boundvars 1 Q $ Bound 0
haftmann@17137
   115
        in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
berghofe@12866
   116
          equal_elim_axm %> t %> u %%
wenzelm@37310
   117
            (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0))
berghofe@12866
   118
              %% (PBound 0 %> Bound 0))))
berghofe@12866
   119
        end
berghofe@12866
   120
wenzelm@26424
   121
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
wenzelm@26424
   122
        (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
skalberg@15531
   123
           SOME (equal_elim_axm %> B %> C %% prf2 %%
berghofe@12866
   124
             (equal_elim_axm %> A %> B %% prf1 %% prf3))
wenzelm@26424
   125
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
wenzelm@26424
   126
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
   127
          (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
haftmann@17137
   128
           SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %%
haftmann@17137
   129
             (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf2) %% prf3))
berghofe@12866
   130
wenzelm@26424
   131
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
wenzelm@26424
   132
        (PAxm ("Pure.reflexive", _, _) % _) %% prf) = SOME prf
wenzelm@26424
   133
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
wenzelm@26424
   134
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
   135
          (PAxm ("Pure.reflexive", _, _) % _)) %% prf) = SOME prf
berghofe@12866
   136
wenzelm@26424
   137
      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
   138
        (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
berghofe@11522
   139
wenzelm@26424
   140
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
wenzelm@26424
   141
        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
wenzelm@26424
   142
          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
wenzelm@56245
   143
            (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
wenzelm@26424
   144
              (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
skalberg@15531
   145
          SOME (equal_elim_axm %> C %> D %% prf2 %%
berghofe@12866
   146
            (equal_elim_axm %> A %> C %% prf3 %%
haftmann@17137
   147
              (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% prf4)))
berghofe@12866
   148
wenzelm@26424
   149
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
wenzelm@26424
   150
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
   151
          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
wenzelm@26424
   152
            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
wenzelm@56245
   153
              (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
wenzelm@26424
   154
                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
skalberg@15531
   155
          SOME (equal_elim_axm %> A %> B %% prf1 %%
haftmann@17137
   156
            (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
haftmann@17137
   157
              (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4)))
berghofe@11522
   158
wenzelm@26424
   159
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
wenzelm@26424
   160
        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
wenzelm@26424
   161
          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
   162
            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
wenzelm@56245
   163
              (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
wenzelm@26424
   164
                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
haftmann@17137
   165
          SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
berghofe@12866
   166
            (equal_elim_axm %> B %> D %% prf3 %%
berghofe@12866
   167
              (equal_elim_axm %> A %> B %% prf1 %% prf4)))
berghofe@11522
   168
wenzelm@26424
   169
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
wenzelm@26424
   170
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
   171
          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
wenzelm@26424
   172
            (PAxm ("Pure.symmetric", _, _) % _ % _ %%
wenzelm@26424
   173
              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
wenzelm@56245
   174
                (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
wenzelm@26424
   175
                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
haftmann@17137
   176
          SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
haftmann@17137
   177
            (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
berghofe@12866
   178
              (equal_elim_axm %> C %> D %% prf2 %% prf4)))
berghofe@11522
   179
wenzelm@26424
   180
      | rew' ((prf as PAxm ("Pure.combination", _, _) %
wenzelm@56245
   181
        SOME ((eq as Const ("Pure.eq", T)) $ t) % _ % _ % _) %%
wenzelm@26424
   182
          (PAxm ("Pure.reflexive", _, _) % _)) =
berghofe@13257
   183
        let val (U, V) = (case T of
berghofe@13257
   184
          Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
wenzelm@37310
   185
        in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
wenzelm@37310
   186
          (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t)))
berghofe@13257
   187
        end
berghofe@13257
   188
wenzelm@19309
   189
      | rew' _ = NONE;
wenzelm@37310
   190
  in rew' #> Option.map (rpair Proofterm.no_skel) end;
berghofe@12866
   191
wenzelm@28806
   192
fun rprocs b = [rew b];
wenzelm@53171
   193
val _ = Theory.setup (fold Proofterm.add_prf_rproc (rprocs false));
berghofe@11522
   194
berghofe@12906
   195
berghofe@12906
   196
(**** apply rewriting function to all terms in proof ****)
berghofe@12906
   197
berghofe@12906
   198
fun rewrite_terms r =
berghofe@12906
   199
  let
berghofe@12906
   200
    fun rew_term Ts t =
berghofe@12906
   201
      let
wenzelm@29271
   202
        val frees =
wenzelm@43329
   203
          map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
berghofe@12906
   204
        val t' = r (subst_bounds (frees, t));
berghofe@12906
   205
        fun strip [] t = t
berghofe@12906
   206
          | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
berghofe@12906
   207
      in
wenzelm@19473
   208
        strip Ts (fold lambda frees t')
berghofe@12906
   209
      end;
berghofe@12906
   210
berghofe@12906
   211
    fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
skalberg@15531
   212
      | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
skalberg@15531
   213
      | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
skalberg@15531
   214
      | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
berghofe@12906
   215
      | rew _ prf = prf
berghofe@12906
   216
berghofe@12906
   217
  in rew [] end;
berghofe@12906
   218
berghofe@12906
   219
berghofe@12906
   220
(**** eliminate definitions in proof ****)
berghofe@12906
   221
wenzelm@16861
   222
fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
berghofe@12906
   223
berghofe@12906
   224
fun insert_refl defs Ts (prf1 %% prf2) =
berghofe@37233
   225
      let val (prf1', b) = insert_refl defs Ts prf1
berghofe@37233
   226
      in
berghofe@37233
   227
        if b then (prf1', true)
berghofe@37233
   228
        else (prf1' %% fst (insert_refl defs Ts prf2), false)
berghofe@37233
   229
      end
skalberg@15531
   230
  | insert_refl defs Ts (Abst (s, SOME T, prf)) =
berghofe@37233
   231
      (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
berghofe@12906
   232
  | insert_refl defs Ts (AbsP (s, t, prf)) =
berghofe@37233
   233
      (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
wenzelm@37310
   234
  | insert_refl defs Ts prf =
wenzelm@37310
   235
      (case Proofterm.strip_combt prf of
wenzelm@28806
   236
        (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
wenzelm@20664
   237
          if member (op =) defs s then
berghofe@12906
   238
            let
berghofe@12906
   239
              val vs = vars_of prop;
krauss@36042
   240
              val tvars = Term.add_tvars prop [] |> rev;
berghofe@37233
   241
              val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
wenzelm@18185
   242
              val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
wenzelm@23178
   243
                (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
wenzelm@19466
   244
                map the ts);
berghofe@12906
   245
            in
wenzelm@37310
   246
              (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')])
wenzelm@37310
   247
                Proofterm.reflexive_axm %> rhs', true)
berghofe@12906
   248
            end
berghofe@37233
   249
          else (prf, false)
berghofe@37233
   250
      | (_, []) => (prf, false)
wenzelm@37310
   251
      | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
berghofe@12906
   252
wenzelm@62922
   253
fun elim_defs ctxt r defs prf =
berghofe@12906
   254
  let
berghofe@37233
   255
    val defs' = map (Logic.dest_equals o
wenzelm@59582
   256
      map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
wenzelm@36744
   257
    val defnames = map Thm.derivation_name defs;
berghofe@13341
   258
    val f = if not r then I else
berghofe@13341
   259
      let
berghofe@13341
   260
        val cnames = map (fst o dest_Const o fst) defs';
wenzelm@37310
   261
        val thms = Proofterm.fold_proof_atoms true
wenzelm@28806
   262
          (fn PThm (_, ((name, prop, _), _)) =>
wenzelm@29271
   263
              if member (op =) defnames name orelse
wenzelm@29271
   264
                not (exists_Const (member (op =) cnames o #1) prop)
wenzelm@29271
   265
              then I
wenzelm@28806
   266
              else cons (name, SOME prop)
wenzelm@28806
   267
            | _ => I) [prf] [];
wenzelm@62922
   268
      in Reconstruct.expand_proof ctxt thms end;
berghofe@12906
   269
  in
wenzelm@62922
   270
    rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' [])
berghofe@37233
   271
      (fst (insert_refl defnames [] (f prf)))
berghofe@12906
   272
  end;
berghofe@12906
   273
berghofe@13608
   274
berghofe@13608
   275
(**** eliminate all variables that don't occur in the proposition ****)
berghofe@13608
   276
berghofe@13608
   277
fun elim_vars mk_default prf =
berghofe@13608
   278
  let
berghofe@13608
   279
    val prop = Reconstruct.prop_of prf;
wenzelm@19309
   280
    val tv = Term.add_vars prop [];
wenzelm@19309
   281
    val tf = Term.add_frees prop [];
wenzelm@19309
   282
wenzelm@19309
   283
    fun hidden_variable (Var v) = not (member (op =) tv v)
wenzelm@19309
   284
      | hidden_variable (Free f) = not (member (op =) tf f)
wenzelm@19309
   285
      | hidden_variable _ = false;
berghofe@13917
   286
wenzelm@46219
   287
    fun mk_default' T =
wenzelm@46219
   288
      fold_rev (Term.abs o pair "x") (binder_types T) (mk_default (body_type T));
berghofe@13917
   289
berghofe@13917
   290
    fun elim_varst (t $ u) = elim_varst t $ elim_varst u
berghofe@13917
   291
      | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
wenzelm@19309
   292
      | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
wenzelm@19309
   293
      | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
wenzelm@19309
   294
      | elim_varst t = t;
berghofe@13608
   295
  in
wenzelm@37310
   296
    Proofterm.map_proof_terms (fn t =>
wenzelm@19309
   297
      if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
berghofe@13608
   298
  end;
berghofe@13608
   299
berghofe@22280
   300
berghofe@22280
   301
(**** convert between hhf and non-hhf form ****)
berghofe@22280
   302
berghofe@22280
   303
fun hhf_proof P Q prf =
berghofe@22280
   304
  let
berghofe@22280
   305
    val params = Logic.strip_params Q;
berghofe@22280
   306
    val Hs = Logic.strip_assums_hyp P;
berghofe@22280
   307
    val Hs' = Logic.strip_assums_hyp Q;
berghofe@22280
   308
    val k = length Hs;
berghofe@22280
   309
    val l = length params;
wenzelm@56245
   310
    fun mk_prf i j Hs Hs' (Const ("Pure.all", _) $ Abs (_, _, P)) prf =
berghofe@22280
   311
          mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
wenzelm@56245
   312
      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("Pure.imp", _) $ _ $ P) prf =
berghofe@22280
   313
          mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
berghofe@22280
   314
      | mk_prf _ _ _ _ _ prf = prf
berghofe@22280
   315
  in
berghofe@22280
   316
    prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
berghofe@22280
   317
    fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>
berghofe@22280
   318
    fold_rev (fn (s, T) => fn prf => Abst (s, SOME T, prf)) params
berghofe@22280
   319
  end
berghofe@22280
   320
and un_hhf_proof P Q prf =
berghofe@22280
   321
  let
berghofe@22280
   322
    val params = Logic.strip_params Q;
berghofe@22280
   323
    val Hs = Logic.strip_assums_hyp P;
berghofe@22280
   324
    val Hs' = Logic.strip_assums_hyp Q;
berghofe@22280
   325
    val k = length Hs;
berghofe@22280
   326
    val l = length params;
wenzelm@56245
   327
    fun mk_prf (Const ("Pure.all", _) $ Abs (s, T, P)) prf =
berghofe@22280
   328
          Abst (s, SOME T, mk_prf P prf)
wenzelm@56245
   329
      | mk_prf (Const ("Pure.imp", _) $ P $ Q) prf =
berghofe@22280
   330
          AbsP ("H", SOME P, mk_prf Q prf)
berghofe@22280
   331
      | mk_prf _ prf = prf
berghofe@22280
   332
  in
berghofe@22280
   333
    prf |> Proofterm.incr_pboundvars k l |>
berghofe@22280
   334
    fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>
berghofe@22280
   335
    fold (fn ((H, H'), i) => fn prf => prf %% hhf_proof H' H (PBound i))
berghofe@22280
   336
      (Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
berghofe@22280
   337
    mk_prf Q
berghofe@22280
   338
  end;
berghofe@22280
   339
berghofe@37233
   340
berghofe@37233
   341
(**** expand OfClass proofs ****)
berghofe@37233
   342
wenzelm@62922
   343
fun mk_of_sort_proof ctxt hs (T, S) =
berghofe@37233
   344
  let
berghofe@37233
   345
    val hs' = map
berghofe@37233
   346
      (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
berghofe@37233
   347
        | NONE => NONE) hs;
berghofe@37233
   348
    val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
berghofe@37233
   349
    fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
berghofe@37233
   350
    val subst = map_atyps
berghofe@37233
   351
      (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
berghofe@37233
   352
        | T as TFree (s, _) => TFree (s, get_sort T));
berghofe@37233
   353
    fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
berghofe@37233
   354
        ~1 => error "expand_of_class: missing class hypothesis"
berghofe@37233
   355
      | i => PBound i;
berghofe@37233
   356
    fun reconstruct prf prop = prf |>
wenzelm@62922
   357
      Reconstruct.reconstruct_proof ctxt prop |>
wenzelm@62922
   358
      Reconstruct.expand_proof ctxt [("", NONE)] |>
wenzelm@37310
   359
      Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
berghofe@37233
   360
  in
berghofe@37233
   361
    map2 reconstruct
wenzelm@62922
   362
      (Proofterm.of_sort_proof (Proof_Context.theory_of ctxt)
wenzelm@62922
   363
        (OfClass o apfst Type.strip_sorts) (subst T, S))
berghofe@37233
   364
      (Logic.mk_of_sort (T, S))
berghofe@37233
   365
  end;
berghofe@37233
   366
wenzelm@62922
   367
fun expand_of_class ctxt Ts hs (OfClass (T, c)) =
wenzelm@62922
   368
      mk_of_sort_proof ctxt hs (T, [c]) |>
wenzelm@37310
   369
      hd |> rpair Proofterm.no_skel |> SOME
wenzelm@62922
   370
  | expand_of_class ctxt Ts hs _ = NONE;
berghofe@37233
   371
berghofe@11522
   372
end;