src/Pure/Proof/proof_rewrite_rules.ML
author hoelzl
Tue, 21 Dec 2010 15:00:59 +0100
changeset 41368 8afa26855137
parent 37310 96e2b9a6f074
child 43322 1f6f6454f115
permissions -rw-r--r--
use DERIV_intros
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     1
(*  Title:      Pure/Proof/proof_rewrite_rules.ML
11539
0f17da240450 tuned headers;
wenzelm
parents: 11522
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     3
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
     4
Simplification functions for proof terms involving meta level rules.
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     5
*)
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     6
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     7
signature PROOF_REWRITE_RULES =
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     8
sig
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
     9
  val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
33722
e588744f14da generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents: 29271
diff changeset
    10
  val rprocs : bool ->
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
    11
    (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
    12
  val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17137
diff changeset
    13
  val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
13608
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
    14
  val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
22280
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
    15
  val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
    16
  val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
    17
  val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
    18
  val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
    19
    (Proofterm.proof * Proofterm.proof) option
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    20
end;
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    21
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    22
structure ProofRewriteRules : PROOF_REWRITE_RULES =
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    23
struct
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    24
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
    25
fun rew b _ _ =
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    26
  let
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
    27
    fun ?? x = if b then SOME x else NONE;
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    28
    fun ax (prf as PAxm (s, prop, _)) Ts =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    29
      if b then PAxm (s, prop, SOME Ts) else prf;
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    30
    fun ty T = if b then
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    31
        let val Type (_, [Type (_, [U, _]), _]) = T
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    32
        in SOME U end
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    33
      else NONE;
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    34
    val equal_intr_axm = ax Proofterm.equal_intr_axm [];
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    35
    val equal_elim_axm = ax Proofterm.equal_elim_axm [];
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    36
    val symmetric_axm = ax Proofterm.symmetric_axm [propT];
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    37
28806
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    38
    fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    39
        (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    40
      | rew' (PThm (_, (("Pure.conjunctionD1", _, _), _)) % _ % _ %%
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    41
        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% prf %% _)) = SOME prf
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    42
      | rew' (PThm (_, (("Pure.conjunctionD2", _, _), _)) % _ % _ %%
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    43
        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    44
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    45
        (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    46
      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    47
        (PAxm ("Pure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    48
            SOME (equal_intr_axm % B % A %% prf2 %% prf1)
12002
bc9b5bad0e7b Additional rules for simplifying inside "Goal"
berghofe
parents: 11612
diff changeset
    49
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    50
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    51
        (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    52
          _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
28806
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    53
        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    54
        SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
12002
bc9b5bad0e7b Additional rules for simplifying inside "Goal"
berghofe
parents: 11612
diff changeset
    55
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    56
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    57
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    58
          (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    59
             _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
28806
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
    60
        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    61
        SOME (tg %> B %% (equal_elim_axm %> A %> B %%
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
    62
          (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    63
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    64
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    65
        (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    66
          (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    67
             (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    68
        let
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    69
          val _ $ A $ C = Envir.beta_norm X;
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    70
          val _ $ B $ D = Envir.beta_norm Y
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
    71
        in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    72
          Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %%
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    73
            (PBound 1 %% (equal_elim_axm %> B %> A %%
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    74
              (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %%
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    75
                PBound 0)))))
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    76
        end
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    77
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    78
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    79
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    80
          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    81
            (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    82
               (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    83
        let
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    84
          val _ $ A $ C = Envir.beta_norm Y;
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    85
          val _ $ B $ D = Envir.beta_norm X
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
    86
        in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    87
          equal_elim_axm %> D %> C %%
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    88
            (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %%
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    89
              (PBound 1 %%
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
    90
                (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0)))))
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    91
        end
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    92
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    93
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    94
        (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    95
          (PAxm ("Pure.reflexive", _, _) % _) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
    96
            (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    97
        let
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    98
          val Const (_, T) $ P = Envir.beta_norm X;
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
    99
          val _ $ Q = Envir.beta_norm Y;
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   100
        in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   101
            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   102
              (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   103
        end
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   104
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   105
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   106
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   107
          (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   108
            (PAxm ("Pure.reflexive", _, _) % _) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   109
              (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   110
        let
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   111
          val Const (_, T) $ P = Envir.beta_norm X;
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   112
          val _ $ Q = Envir.beta_norm Y;
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   113
          val t = incr_boundvars 1 P $ Bound 0;
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   114
          val u = incr_boundvars 1 Q $ Bound 0
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   115
        in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   116
          equal_elim_axm %> t %> u %%
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   117
            (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0))
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   118
              %% (PBound 0 %> Bound 0))))
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   119
        end
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   120
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   121
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   122
        (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   123
           SOME (equal_elim_axm %> B %> C %% prf2 %%
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   124
             (equal_elim_axm %> A %> B %% prf1 %% prf3))
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   125
      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   126
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   127
          (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   128
           SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %%
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   129
             (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf2) %% prf3))
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   130
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   131
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   132
        (PAxm ("Pure.reflexive", _, _) % _) %% prf) = SOME prf
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   133
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   134
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   135
          (PAxm ("Pure.reflexive", _, _) % _)) %% prf) = SOME prf
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   136
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   137
      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   138
        (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   139
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   140
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   141
        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   142
          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   143
            (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   144
              (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   145
          SOME (equal_elim_axm %> C %> D %% prf2 %%
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   146
            (equal_elim_axm %> A %> C %% prf3 %%
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   147
              (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% prf4)))
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   148
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   149
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   150
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   151
          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   152
            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   153
              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   154
                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   155
          SOME (equal_elim_axm %> A %> B %% prf1 %%
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   156
            (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   157
              (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4)))
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   158
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   159
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   160
        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   161
          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   162
            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   163
              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   164
                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   165
          SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   166
            (equal_elim_axm %> B %> D %% prf3 %%
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   167
              (equal_elim_axm %> A %> B %% prf1 %% prf4)))
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   168
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   169
      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   170
        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   171
          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   172
            (PAxm ("Pure.symmetric", _, _) % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   173
              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   174
                (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   175
                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
17137
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   176
          SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
0f48fbb60a61 replaced ? by ??
haftmann
parents: 17018
diff changeset
   177
            (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   178
              (equal_elim_axm %> C %> D %% prf2 %% prf4)))
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   179
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   180
      | rew' ((prf as PAxm ("Pure.combination", _, _) %
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   181
        SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 23178
diff changeset
   182
          (PAxm ("Pure.reflexive", _, _) % _)) =
13257
1b7104a1c0bd Additional rule for rewriting on ==.
berghofe
parents: 13198
diff changeset
   183
        let val (U, V) = (case T of
1b7104a1c0bd Additional rule for rewriting on ==.
berghofe
parents: 13198
diff changeset
   184
          Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   185
        in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   186
          (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t)))
13257
1b7104a1c0bd Additional rule for rewriting on ==.
berghofe
parents: 13198
diff changeset
   187
        end
1b7104a1c0bd Additional rule for rewriting on ==.
berghofe
parents: 13198
diff changeset
   188
19309
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   189
      | rew' _ = NONE;
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   190
  in rew' #> Option.map (rpair Proofterm.no_skel) end;
12866
c00df7765656 Rewrite procedure now works for both compact and full proof objects.
berghofe
parents: 12237
diff changeset
   191
28806
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
   192
fun rprocs b = [rew b];
26463
9283b4185fdf Context.>> : operate on Context.generic;
wenzelm
parents: 26435
diff changeset
   193
val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   194
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   195
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   196
(**** apply rewriting function to all terms in proof ****)
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   197
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   198
fun rewrite_terms r =
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   199
  let
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   200
    fun rew_term Ts t =
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   201
      let
29271
1d685baea08e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 28806
diff changeset
   202
        val frees =
1d685baea08e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 28806
diff changeset
   203
          map Free (Name.invent_list (OldTerm.add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   204
        val t' = r (subst_bounds (frees, t));
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   205
        fun strip [] t = t
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   206
          | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   207
      in
19473
wenzelm
parents: 19466
diff changeset
   208
        strip Ts (fold lambda frees t')
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   209
      end;
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   210
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   211
    fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   212
      | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   213
      | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   214
      | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   215
      | rew _ prf = prf
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   216
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   217
  in rew [] end;
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   218
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   219
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   220
(**** eliminate definitions in proof ****)
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   221
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16787
diff changeset
   222
fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   223
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   224
fun insert_refl defs Ts (prf1 %% prf2) =
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   225
      let val (prf1', b) = insert_refl defs Ts prf1
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   226
      in
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   227
        if b then (prf1', true)
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   228
        else (prf1' %% fst (insert_refl defs Ts prf2), false)
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   229
      end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   230
  | insert_refl defs Ts (Abst (s, SOME T, prf)) =
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   231
      (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   232
  | insert_refl defs Ts (AbsP (s, t, prf)) =
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   233
      (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   234
  | insert_refl defs Ts prf =
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   235
      (case Proofterm.strip_combt prf of
28806
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
   236
        (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
20664
ffbc5a57191a member (op =);
wenzelm
parents: 20076
diff changeset
   237
          if member (op =) defs s then
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   238
            let
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   239
              val vs = vars_of prop;
36042
85efdadee8ae switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents: 33722
diff changeset
   240
              val tvars = Term.add_tvars prop [] |> rev;
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   241
              val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
18185
9d51fad6bb1f Term.betapplys;
wenzelm
parents: 18024
diff changeset
   242
              val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
23178
07ba6b58b3d2 simplified/unified list fold;
wenzelm
parents: 22662
diff changeset
   243
                (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
19466
wenzelm
parents: 19309
diff changeset
   244
                map the ts);
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   245
            in
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   246
              (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')])
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   247
                Proofterm.reflexive_axm %> rhs', true)
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   248
            end
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   249
          else (prf, false)
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   250
      | (_, []) => (prf, false)
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   251
      | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   252
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17137
diff changeset
   253
fun elim_defs thy r defs prf =
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   254
  let
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   255
    val defs' = map (Logic.dest_equals o
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   256
      map_types Type.strip_sorts o prop_of o Drule.abs_def) defs;
36744
6e1f3d609a68 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
wenzelm
parents: 36042
diff changeset
   257
    val defnames = map Thm.derivation_name defs;
13341
f15ed50d16cf - Moved abs_def to drule.ML
berghofe
parents: 13257
diff changeset
   258
    val f = if not r then I else
f15ed50d16cf - Moved abs_def to drule.ML
berghofe
parents: 13257
diff changeset
   259
      let
f15ed50d16cf - Moved abs_def to drule.ML
berghofe
parents: 13257
diff changeset
   260
        val cnames = map (fst o dest_Const o fst) defs';
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   261
        val thms = Proofterm.fold_proof_atoms true
28806
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
   262
          (fn PThm (_, ((name, prop, _), _)) =>
29271
1d685baea08e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 28806
diff changeset
   263
              if member (op =) defnames name orelse
1d685baea08e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 28806
diff changeset
   264
                not (exists_Const (member (op =) cnames o #1) prop)
1d685baea08e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 28806
diff changeset
   265
              then I
28806
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
   266
              else cons (name, SOME prop)
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
   267
            | _ => I) [prf] [];
ba0ffe4cfc2b rewrite_proof: simplified simprocs (no name required);
wenzelm
parents: 26463
diff changeset
   268
      in Reconstruct.expand_proof thy thms end;
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   269
  in
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17137
diff changeset
   270
    rewrite_terms (Pattern.rewrite_term thy defs' [])
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   271
      (fst (insert_refl defnames [] (f prf)))
12906
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   272
  end;
165f4e1937f4 New function for eliminating definitions in proof term.
berghofe
parents: 12866
diff changeset
   273
13608
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   274
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   275
(**** eliminate all variables that don't occur in the proposition ****)
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   276
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   277
fun elim_vars mk_default prf =
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   278
  let
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   279
    val prop = Reconstruct.prop_of prf;
19309
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   280
    val tv = Term.add_vars prop [];
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   281
    val tf = Term.add_frees prop [];
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   282
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   283
    fun hidden_variable (Var v) = not (member (op =) tv v)
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   284
      | hidden_variable (Free f) = not (member (op =) tf f)
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   285
      | hidden_variable _ = false;
13917
a67c9e6570ac elim_vars now handles both Vars and Frees.
berghofe
parents: 13646
diff changeset
   286
a67c9e6570ac elim_vars now handles both Vars and Frees.
berghofe
parents: 13646
diff changeset
   287
    fun mk_default' T = list_abs
a67c9e6570ac elim_vars now handles both Vars and Frees.
berghofe
parents: 13646
diff changeset
   288
      (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
a67c9e6570ac elim_vars now handles both Vars and Frees.
berghofe
parents: 13646
diff changeset
   289
a67c9e6570ac elim_vars now handles both Vars and Frees.
berghofe
parents: 13646
diff changeset
   290
    fun elim_varst (t $ u) = elim_varst t $ elim_varst u
a67c9e6570ac elim_vars now handles both Vars and Frees.
berghofe
parents: 13646
diff changeset
   291
      | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
19309
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   292
      | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   293
      | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   294
      | elim_varst t = t;
13608
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   295
  in
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   296
    Proofterm.map_proof_terms (fn t =>
19309
8ea43e9ad83a avoid polymorphic equality;
wenzelm
parents: 19126
diff changeset
   297
      if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
13608
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   298
  end;
9a6f43b8eae1 Added function elim_vars.
berghofe
parents: 13341
diff changeset
   299
22280
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   300
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   301
(**** convert between hhf and non-hhf form ****)
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   302
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   303
fun hhf_proof P Q prf =
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   304
  let
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   305
    val params = Logic.strip_params Q;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   306
    val Hs = Logic.strip_assums_hyp P;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   307
    val Hs' = Logic.strip_assums_hyp Q;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   308
    val k = length Hs;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   309
    val l = length params;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   310
    fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   311
          mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   312
      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   313
          mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   314
      | mk_prf _ _ _ _ _ prf = prf
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   315
  in
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   316
    prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   317
    fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   318
    fold_rev (fn (s, T) => fn prf => Abst (s, SOME T, prf)) params
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   319
  end
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   320
and un_hhf_proof P Q prf =
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   321
  let
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   322
    val params = Logic.strip_params Q;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   323
    val Hs = Logic.strip_assums_hyp P;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   324
    val Hs' = Logic.strip_assums_hyp Q;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   325
    val k = length Hs;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   326
    val l = length params;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   327
    fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   328
          Abst (s, SOME T, mk_prf P prf)
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   329
      | mk_prf (Const ("==>", _) $ P $ Q) prf =
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   330
          AbsP ("H", SOME P, mk_prf Q prf)
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   331
      | mk_prf _ prf = prf
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   332
  in
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   333
    prf |> Proofterm.incr_pboundvars k l |>
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   334
    fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   335
    fold (fn ((H, H'), i) => fn prf => prf %% hhf_proof H' H (PBound i))
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   336
      (Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   337
    mk_prf Q
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   338
  end;
a20a203c8f41 Added functions hhf_proof and un_hhf_proof.
berghofe
parents: 21646
diff changeset
   339
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   340
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   341
(**** expand OfClass proofs ****)
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   342
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   343
fun mk_of_sort_proof thy hs (T, S) =
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   344
  let
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   345
    val hs' = map
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   346
      (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   347
        | NONE => NONE) hs;
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   348
    val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   349
    fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   350
    val subst = map_atyps
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   351
      (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   352
        | T as TFree (s, _) => TFree (s, get_sort T));
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   353
    fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   354
        ~1 => error "expand_of_class: missing class hypothesis"
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   355
      | i => PBound i;
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   356
    fun reconstruct prf prop = prf |>
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   357
      Reconstruct.reconstruct_proof thy prop |>
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   358
      Reconstruct.expand_proof thy [("", NONE)] |>
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   359
      Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   360
  in
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   361
    map2 reconstruct
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   362
      (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   363
      (Logic.mk_of_sort (T, S))
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   364
  end;
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   365
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   366
fun expand_of_class thy Ts hs (OfClass (T, c)) =
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   367
      mk_of_sort_proof thy hs (T, [c]) |>
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37233
diff changeset
   368
      hd |> rpair Proofterm.no_skel |> SOME
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   369
  | expand_of_class thy Ts hs _ = NONE;
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36744
diff changeset
   370
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   371
end;