author | wenzelm |
Wed, 31 Aug 2005 15:46:40 +0200 | |
changeset 17203 | 29b2563f5c11 |
parent 17137 | 0f48fbb60a61 |
child 17979 | 09485bdd4b6f |
permissions | -rw-r--r-- |
11522 | 1 |
(* Title: Pure/Proof/proof_rewrite_rules.ML |
2 |
ID: $Id$ |
|
11539 | 3 |
Author: Stefan Berghofer, TU Muenchen |
11522 | 4 |
|
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
5 |
Simplification functions for proof terms involving meta level rules. |
11522 | 6 |
*) |
7 |
||
8 |
signature PROOF_REWRITE_RULES = |
|
9 |
sig |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
10 |
val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
11 |
val rprocs : bool -> (string * (typ list -> 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 | 13 |
val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof |
13608 | 14 |
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof |
11522 | 15 |
end; |
16 |
||
17 |
structure ProofRewriteRules : PROOF_REWRITE_RULES = |
|
18 |
struct |
|
19 |
||
20 |
open Proofterm; |
|
21 |
||
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
22 |
fun rew b = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
23 |
let |
17137 | 24 |
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
|
25 |
fun ax (prf as PAxm (s, prop, _)) Ts = |
15531 | 26 |
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
|
27 |
fun ty T = if b then |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
28 |
let val Type (_, [Type (_, [U, _]), _]) = T |
15531 | 29 |
in SOME U end |
30 |
else NONE; |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
31 |
val equal_intr_axm = ax equal_intr_axm []; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
32 |
val equal_elim_axm = ax equal_elim_axm []; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
33 |
val symmetric_axm = ax symmetric_axm [propT]; |
11522 | 34 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
35 |
fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %% |
15531 | 36 |
(PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = SOME prf |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
37 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
15531 | 38 |
(PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
39 |
| rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
40 |
(PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) = |
15531 | 41 |
SOME (equal_intr_axm % B % A %% prf2 %% prf1) |
12002 | 42 |
|
15531 | 43 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% |
44 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) % |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
45 |
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
46 |
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) = |
15531 | 47 |
SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2)) |
12002 | 48 |
|
15531 | 49 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
50 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
15531 | 51 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) % |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
52 |
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
53 |
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) = |
15531 | 54 |
SOME (tg %> B %% (equal_elim_axm %> A %> B %% |
17137 | 55 |
(symmetric_axm % ?? B % ?? A %% prf1) %% prf2)) |
11522 | 56 |
|
15531 | 57 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %% |
11612 | 58 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
15531 | 59 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
60 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
61 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
62 |
val _ $ A $ C = Envir.beta_norm X; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
63 |
val _ $ B $ D = Envir.beta_norm Y |
17137 | 64 |
in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B, |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
65 |
equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
66 |
(PBound 1 %% (equal_elim_axm %> B %> A %% |
17137 | 67 |
(symmetric_axm % ?? A % ?? B %% 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
|
68 |
end |
11522 | 69 |
|
15531 | 70 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
71 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
72 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
15531 | 73 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
74 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
75 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
76 |
val _ $ A $ C = Envir.beta_norm Y; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
77 |
val _ $ B $ D = Envir.beta_norm X |
17137 | 78 |
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
|
79 |
equal_elim_axm %> D %> C %% |
17137 | 80 |
(symmetric_axm % ?? C % ?? D %% incr_pboundvars 2 0 prf2) |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
81 |
%% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0))))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
82 |
end |
11522 | 83 |
|
15531 | 84 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %% |
85 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %% |
|
11612 | 86 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
87 |
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
88 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
89 |
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
|
90 |
val _ $ Q = Envir.beta_norm Y; |
17137 | 91 |
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
|
92 |
equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
93 |
(incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0)))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
94 |
end |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
95 |
|
15531 | 96 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
97 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
15531 | 98 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
99 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
100 |
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
101 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
102 |
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
|
103 |
val _ $ Q = Envir.beta_norm Y; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
104 |
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
|
105 |
val u = incr_boundvars 1 Q $ Bound 0 |
17137 | 106 |
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
|
107 |
equal_elim_axm %> t %> u %% |
17137 | 108 |
(symmetric_axm % ?? u % ?? t %% (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
|
109 |
%% (PBound 0 %> Bound 0)))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
110 |
end |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
111 |
|
15531 | 112 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %% |
113 |
(PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) = |
|
114 |
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
|
115 |
(equal_elim_axm %> A %> B %% prf1 %% prf3)) |
15531 | 116 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
117 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
15531 | 118 |
(PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) = |
17137 | 119 |
SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %% |
120 |
(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
|
121 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
122 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
15531 | 123 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
124 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
125 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
15531 | 126 |
(PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
127 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
128 |
| rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
15531 | 129 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf |
11522 | 130 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
131 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
15531 | 132 |
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
133 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
15531 | 134 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
135 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) = |
15531 | 136 |
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
|
137 |
(equal_elim_axm %> A %> C %% prf3 %% |
17137 | 138 |
(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
|
139 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
140 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
141 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
15531 | 142 |
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
143 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
15531 | 144 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
145 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) = |
15531 | 146 |
SOME (equal_elim_axm %> A %> B %% prf1 %% |
17137 | 147 |
(equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %% |
148 |
(equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4))) |
|
11522 | 149 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
150 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
15531 | 151 |
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
152 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
153 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
15531 | 154 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
155 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) = |
17137 | 156 |
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
|
157 |
(equal_elim_axm %> B %> D %% prf3 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
158 |
(equal_elim_axm %> A %> B %% prf1 %% prf4))) |
11522 | 159 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
160 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
161 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
15531 | 162 |
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
163 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
164 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
15531 | 165 |
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
166 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) = |
17137 | 167 |
SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% |
168 |
(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
|
169 |
(equal_elim_axm %> C %> D %% prf2 %% prf4))) |
11522 | 170 |
|
13257 | 171 |
| rew' _ ((prf as PAxm ("ProtoPure.combination", _, _) % |
15531 | 172 |
SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %% |
13257 | 173 |
(PAxm ("ProtoPure.reflexive", _, _) % _)) = |
174 |
let val (U, V) = (case T of |
|
175 |
Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT)) |
|
17137 | 176 |
in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %% |
177 |
(ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t))) |
|
13257 | 178 |
end |
179 |
||
15531 | 180 |
| rew' _ _ = NONE; |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
181 |
in rew' end; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
182 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
183 |
fun rprocs b = [("Pure/meta_equality", rew b)]; |
15801 | 184 |
val _ = Context.add_setup [Proofterm.add_prf_rprocs (rprocs false)]; |
11522 | 185 |
|
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
186 |
|
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
187 |
(**** apply rewriting function to all terms in proof ****) |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
188 |
|
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
189 |
fun rewrite_terms r = |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
190 |
let |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
191 |
fun rew_term Ts t = |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
192 |
let |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
193 |
val frees = map Free (variantlist |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
194 |
(replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts); |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
195 |
val t' = r (subst_bounds (frees, t)); |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
196 |
fun strip [] t = t |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
197 |
| strip (_ :: xs) (Abs (_, _, t)) = strip xs t; |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
198 |
in |
15570 | 199 |
strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees)) |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
200 |
end; |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
201 |
|
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
202 |
fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2 |
15531 | 203 |
| rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t) |
204 |
| rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf) |
|
205 |
| 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
|
206 |
| rew _ prf = prf |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
207 |
|
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
208 |
in rew [] end; |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
209 |
|
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 |
(**** eliminate definitions in proof ****) |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
212 |
|
16861 | 213 |
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
|
214 |
|
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
215 |
fun insert_refl defs Ts (prf1 %% prf2) = |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
216 |
insert_refl defs Ts prf1 %% insert_refl defs Ts prf2 |
15531 | 217 |
| insert_refl defs Ts (Abst (s, SOME T, prf)) = |
218 |
Abst (s, SOME T, insert_refl defs (T :: Ts) prf) |
|
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
219 |
| insert_refl defs Ts (AbsP (s, t, prf)) = |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
220 |
AbsP (s, t, insert_refl defs Ts prf) |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
221 |
| insert_refl defs Ts prf = (case strip_combt prf of |
15531 | 222 |
(PThm ((s, _), _, prop, SOME Ts), ts) => |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
223 |
if s mem defs then |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
224 |
let |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
225 |
val vs = vars_of prop; |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
226 |
val tvars = term_tvars prop; |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
227 |
val (_, rhs) = Logic.dest_equals prop; |
15570 | 228 |
val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
229 |
(foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs), |
15570 | 230 |
map valOf ts); |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
231 |
in |
15531 | 232 |
change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs' |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
233 |
end |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
234 |
else prf |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
235 |
| (_, []) => prf |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
236 |
| (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts)); |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
237 |
|
17203 | 238 |
fun elim_defs thy r defs prf = |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
239 |
let |
13341 | 240 |
val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
241 |
val defnames = map Thm.name_of_thm defs; |
13341 | 242 |
val f = if not r then I else |
243 |
let |
|
244 |
val cnames = map (fst o dest_Const o fst) defs'; |
|
15570 | 245 |
val thms = List.concat (map (fn (s, ps) => |
13341 | 246 |
if s mem defnames then [] |
15531 | 247 |
else map (pair s o SOME o fst) (filter_out (fn (p, _) => |
13646 | 248 |
null (term_consts p inter cnames)) ps)) |
17018 | 249 |
(Symtab.dest (thms_of_proof prf Symtab.empty))) |
17203 | 250 |
in Reconstruct.expand_proof thy thms end |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
251 |
in |
17203 | 252 |
rewrite_terms (Pattern.rewrite_term thy defs' []) |
13341 | 253 |
(insert_refl defnames [] (f prf)) |
12906
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
254 |
end; |
165f4e1937f4
New function for eliminating definitions in proof term.
berghofe
parents:
12866
diff
changeset
|
255 |
|
13608 | 256 |
|
257 |
(**** eliminate all variables that don't occur in the proposition ****) |
|
258 |
||
259 |
fun elim_vars mk_default prf = |
|
260 |
let |
|
261 |
val prop = Reconstruct.prop_of prf; |
|
13917 | 262 |
val tv = term_vars prop; |
263 |
val tf = term_frees prop; |
|
264 |
||
265 |
fun mk_default' T = list_abs |
|
266 |
(apfst (map (pair "x")) (apsnd mk_default (strip_type T))); |
|
267 |
||
268 |
fun elim_varst (t $ u) = elim_varst t $ elim_varst u |
|
269 |
| elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t) |
|
270 |
| elim_varst (f as Free (_, T)) = if f mem tf then f else mk_default' T |
|
271 |
| elim_varst (v as Var (_, T)) = if v mem tv then v else mk_default' T |
|
272 |
| elim_varst t = t |
|
13608 | 273 |
in |
13917 | 274 |
map_proof_terms (fn t => if not (null (term_vars t \\ tv)) orelse |
275 |
not (null (term_frees t \\ tf)) then Envir.beta_norm (elim_varst t) |
|
276 |
else t) I prf |
|
13608 | 277 |
end; |
278 |
||
11522 | 279 |
end; |