11522
|
1 |
(* Title: Pure/Proof/proof_syntax.ML
|
|
2 |
ID: $Id$
|
11539
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
11522
|
5 |
|
|
6 |
Function for parsing and printing proof terms.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature PROOF_SYNTAX =
|
|
10 |
sig
|
|
11 |
val proofT : typ
|
|
12 |
val add_proof_syntax : Sign.sg -> Sign.sg
|
|
13 |
val disambiguate_names : theory -> Proofterm.proof ->
|
|
14 |
Proofterm.proof * Proofterm.proof Symtab.table
|
|
15 |
val proof_of_term : theory -> Proofterm.proof Symtab.table ->
|
|
16 |
bool -> term -> Proofterm.proof
|
|
17 |
val term_of_proof : Proofterm.proof -> term
|
|
18 |
val cterm_of_proof : theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
|
|
19 |
val read_term : theory -> typ -> string -> term
|
|
20 |
val read_proof : theory -> bool -> string -> Proofterm.proof
|
|
21 |
val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
|
|
22 |
val pretty_proof_of : bool -> thm -> Pretty.T
|
|
23 |
val print_proof_of : bool -> thm -> unit
|
|
24 |
end;
|
|
25 |
|
|
26 |
structure ProofSyntax : PROOF_SYNTAX =
|
|
27 |
struct
|
|
28 |
|
|
29 |
open Proofterm;
|
|
30 |
|
|
31 |
(**** add special syntax for embedding proof terms ****)
|
|
32 |
|
|
33 |
val proofT = Type ("proof", []);
|
11614
|
34 |
val paramT = Type ("param", []);
|
|
35 |
val paramsT = Type ("params", []);
|
11522
|
36 |
val idtT = Type ("idt", []);
|
|
37 |
val aT = TFree ("'a", ["logic"]);
|
|
38 |
|
|
39 |
(** constants for theorems and axioms **)
|
|
40 |
|
|
41 |
fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
|
|
42 |
|
|
43 |
fun add_proof_atom_consts names sg = Sign.add_consts_i
|
|
44 |
(map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);
|
|
45 |
|
|
46 |
(** constants for application and abstraction **)
|
11614
|
47 |
|
11522
|
48 |
fun add_proof_syntax sg =
|
|
49 |
sg
|
|
50 |
|> Sign.copy
|
|
51 |
|> Sign.add_path "/"
|
|
52 |
|> Sign.add_defsort_i ["logic"]
|
|
53 |
|> Sign.add_types [("proof", 0, NoSyn)]
|
|
54 |
|> Sign.add_arities [("proof", [], "logic")]
|
|
55 |
|> Sign.add_consts_i
|
11614
|
56 |
[("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
|
|
57 |
("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
|
11522
|
58 |
("Abst", (aT --> proofT) --> proofT, NoSyn),
|
|
59 |
("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn)]
|
11614
|
60 |
|> Sign.add_nonterminals ["param", "params"]
|
11522
|
61 |
|> Sign.add_syntax_i
|
11614
|
62 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(3Lam _./ _)", [0, 3], 3)),
|
|
63 |
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
|
|
64 |
("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
|
|
65 |
("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
|
|
66 |
("", paramT --> paramT, Delimfix "'(_')"),
|
|
67 |
("", idtT --> paramsT, Delimfix "_"),
|
|
68 |
("", paramT --> paramsT, Delimfix "_")]
|
11522
|
69 |
|> Sign.add_modesyntax_i (("xsymbols", true),
|
11614
|
70 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(3\\<Lambda>_./ _)", [0, 3], 3)),
|
11522
|
71 |
("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
|
|
72 |
("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
|
|
73 |
|> Sign.add_trrules_i (map Syntax.ParsePrintRule
|
|
74 |
[(Syntax.mk_appl (Constant "_Lam")
|
11614
|
75 |
[Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
|
|
76 |
Syntax.mk_appl (Constant "_Lam")
|
|
77 |
[Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
|
|
78 |
(Syntax.mk_appl (Constant "_Lam")
|
11522
|
79 |
[Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
|
|
80 |
Syntax.mk_appl (Constant "AbsP") [Variable "A",
|
|
81 |
(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
|
11614
|
82 |
(Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
|
11522
|
83 |
Syntax.mk_appl (Constant "Abst")
|
11614
|
84 |
[(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
|
11522
|
85 |
|
|
86 |
|
|
87 |
(**** create unambiguous theorem names ****)
|
|
88 |
|
|
89 |
fun disambiguate_names thy prf =
|
|
90 |
let
|
|
91 |
val thms = thms_of_proof Symtab.empty prf;
|
|
92 |
val thms' = map (apsnd (#prop o rep_thm)) (flat
|
|
93 |
(map PureThy.thms_of (thy :: Theory.ancestors_of thy)));
|
|
94 |
|
|
95 |
val tab = Symtab.foldl (fn (tab, (key, ps)) =>
|
|
96 |
let val prop = if_none (assoc (thms', key)) (Bound 0)
|
|
97 |
in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
|
|
98 |
if prop <> prop' then
|
|
99 |
(Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
|
|
100 |
else x) (ps, (tab, 1)))
|
|
101 |
end) (Symtab.empty, thms);
|
|
102 |
|
|
103 |
fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
|
|
104 |
| rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
|
11614
|
105 |
| rename (prf1 %% prf2) = rename prf1 %% rename prf2
|
|
106 |
| rename (prf % t) = rename prf % t
|
11522
|
107 |
| rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
|
|
108 |
let
|
|
109 |
val prop' = if_none (assoc (thms', s)) (Bound 0);
|
|
110 |
val ps = map fst (the (Symtab.lookup (thms, s))) \ prop'
|
|
111 |
in if prop = prop' then prf' else
|
|
112 |
PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
|
|
113 |
prf, prop, Ts)
|
|
114 |
end
|
|
115 |
| rename prf = prf
|
|
116 |
|
|
117 |
in (rename prf, tab) end;
|
|
118 |
|
|
119 |
|
|
120 |
(**** translation between proof terms and pure terms ****)
|
|
121 |
|
|
122 |
fun change_type T (PThm (name, prf, prop, _)) = PThm (name, prf, prop, T)
|
|
123 |
| change_type T (PAxm (name, prop, _)) = PAxm (name, prop, T)
|
|
124 |
| change_type _ _ = error "Not a proper theorem";
|
|
125 |
|
|
126 |
fun proof_of_term thy tab ty =
|
|
127 |
let
|
|
128 |
val thys = thy :: Theory.ancestors_of thy;
|
|
129 |
val thms = flat (map thms_of thys);
|
|
130 |
val axms = flat (map (Symtab.dest o #axioms o rep_theory) thys);
|
|
131 |
|
11614
|
132 |
fun mk_term t = (if ty then I else map_term_types (K dummyT))
|
|
133 |
(Term.no_dummy_patterns t);
|
|
134 |
|
11522
|
135 |
fun prf_of [] (Bound i) = PBound i
|
|
136 |
| prf_of Ts (Const (s, Type ("proof", _))) =
|
|
137 |
change_type (if ty then Some Ts else None)
|
|
138 |
(case NameSpace.unpack s of
|
11614
|
139 |
"axm" :: xs =>
|
11522
|
140 |
let
|
|
141 |
val name = NameSpace.pack xs;
|
|
142 |
val prop = (case assoc (axms, name) of
|
|
143 |
Some prop => prop
|
|
144 |
| None => error ("Unknown axiom " ^ quote name))
|
|
145 |
in PAxm (name, prop, None) end
|
11614
|
146 |
| "thm" :: xs =>
|
11522
|
147 |
let val name = NameSpace.pack xs;
|
|
148 |
in (case assoc (thms, name) of
|
|
149 |
Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
|
|
150 |
| None => (case Symtab.lookup (tab, name) of
|
|
151 |
Some prf => prf
|
|
152 |
| None => error ("Unknown theorem " ^ quote name)))
|
|
153 |
end
|
|
154 |
| _ => error ("Illegal proof constant name: " ^ quote s))
|
|
155 |
| prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
|
|
156 |
| prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
|
|
157 |
Abst (s, if ty then Some T else None,
|
|
158 |
incr_pboundvars (~1) 0 (prf_of [] prf))
|
|
159 |
| prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
|
11614
|
160 |
AbsP (s, case t of
|
|
161 |
Const ("dummy_pattern", _) => None
|
|
162 |
| _ $ Const ("dummy_pattern", _) => None
|
|
163 |
| _ => Some (mk_term t),
|
11522
|
164 |
incr_pboundvars 0 (~1) (prf_of [] prf))
|
|
165 |
| prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
|
11614
|
166 |
prf_of [] prf1 %% prf_of [] prf2
|
11522
|
167 |
| prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
|
|
168 |
prf_of (T::Ts) prf
|
11614
|
169 |
| prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
|
|
170 |
(case t of Const ("dummy_pattern", _) => None | _ => Some (mk_term t))
|
11522
|
171 |
| prf_of _ t = error ("Not a proof term:\n" ^
|
|
172 |
Sign.string_of_term (sign_of thy) t)
|
|
173 |
|
|
174 |
in prf_of [] end;
|
|
175 |
|
|
176 |
|
|
177 |
val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
|
|
178 |
val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
|
|
179 |
val Hypt = Free ("Hyp", propT --> proofT);
|
|
180 |
val Oraclet = Free ("Oracle", propT --> proofT);
|
|
181 |
val MinProoft = Free ("?", proofT);
|
|
182 |
|
|
183 |
val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
|
|
184 |
[proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
|
|
185 |
|
|
186 |
fun term_of _ (PThm ((name, _), _, _, None)) =
|
11614
|
187 |
Const (add_prefix "thm" name, proofT)
|
11522
|
188 |
| term_of _ (PThm ((name, _), _, _, Some Ts)) =
|
11614
|
189 |
mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
|
|
190 |
| term_of _ (PAxm (name, _, None)) = Const (add_prefix "axm" name, proofT)
|
11522
|
191 |
| term_of _ (PAxm (name, _, Some Ts)) =
|
11614
|
192 |
mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
|
11522
|
193 |
| term_of _ (PBound i) = Bound i
|
|
194 |
| term_of Ts (Abst (s, opT, prf)) =
|
|
195 |
let val T = if_none opT dummyT
|
|
196 |
in Const ("Abst", (T --> proofT) --> proofT) $
|
|
197 |
Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
|
|
198 |
end
|
|
199 |
| term_of Ts (AbsP (s, t, prf)) =
|
|
200 |
AbsPt $ if_none t (Const ("dummy_pattern", propT)) $
|
|
201 |
Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
|
11614
|
202 |
| term_of Ts (prf1 %% prf2) =
|
11522
|
203 |
AppPt $ term_of Ts prf1 $ term_of Ts prf2
|
11614
|
204 |
| term_of Ts (prf % opt) =
|
11522
|
205 |
let val t = if_none opt (Const ("dummy_pattern", dummyT))
|
|
206 |
in Const ("Appt",
|
|
207 |
[proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
|
|
208 |
term_of Ts prf $ t
|
|
209 |
end
|
|
210 |
| term_of Ts (Hyp t) = Hypt $ t
|
|
211 |
| term_of Ts (Oracle (_, t, _)) = Oraclet $ t
|
|
212 |
| term_of Ts (MinProof _) = MinProoft;
|
|
213 |
|
|
214 |
val term_of_proof = term_of [];
|
|
215 |
|
|
216 |
fun cterm_of_proof thy prf =
|
|
217 |
let
|
|
218 |
val (prf', tab) = disambiguate_names thy prf;
|
|
219 |
val thys = thy :: Theory.ancestors_of thy;
|
|
220 |
val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys))) @
|
|
221 |
map fst (Symtab.dest tab);
|
|
222 |
val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
|
|
223 |
val sg = sign_of thy |>
|
|
224 |
add_proof_syntax |>
|
|
225 |
add_proof_atom_consts
|
11614
|
226 |
(map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
|
11522
|
227 |
in
|
|
228 |
(cterm_of sg (term_of_proof prf'),
|
|
229 |
proof_of_term thy tab true o Thm.term_of)
|
|
230 |
end;
|
|
231 |
|
|
232 |
fun read_term thy =
|
|
233 |
let
|
|
234 |
val thys = thy :: Theory.ancestors_of thy;
|
|
235 |
val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys)));
|
|
236 |
val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
|
|
237 |
val sg = sign_of thy |>
|
|
238 |
add_proof_syntax |>
|
|
239 |
add_proof_atom_consts
|
11614
|
240 |
(map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
|
11522
|
241 |
in
|
|
242 |
(fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
|
|
243 |
end;
|
|
244 |
|
|
245 |
fun read_proof thy =
|
|
246 |
let val rd = read_term thy proofT
|
|
247 |
in
|
|
248 |
(fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)))
|
|
249 |
end;
|
|
250 |
|
|
251 |
fun pretty_proof sg prf =
|
|
252 |
let
|
|
253 |
val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ "";
|
|
254 |
val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf));
|
|
255 |
val sg' = sg |>
|
|
256 |
add_proof_syntax |>
|
|
257 |
add_proof_atom_consts
|
11614
|
258 |
(map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
|
11522
|
259 |
in
|
|
260 |
Sign.pretty_term sg' (term_of_proof prf)
|
|
261 |
end;
|
|
262 |
|
|
263 |
fun pretty_proof_of full thm =
|
|
264 |
let
|
|
265 |
val {sign, der = (_, prf), prop, ...} = rep_thm thm;
|
|
266 |
val prf' = (case strip_combt (fst (strip_combP prf)) of
|
|
267 |
(PThm (_, prf', prop', _), _) => if prop=prop' then prf' else prf
|
|
268 |
| _ => prf)
|
|
269 |
in
|
|
270 |
pretty_proof sign
|
11614
|
271 |
(if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
|
11522
|
272 |
end;
|
|
273 |
|
|
274 |
val print_proof_of = Pretty.writeln oo pretty_proof_of;
|
|
275 |
|
|
276 |
end;
|