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