author | wenzelm |
Sat, 09 Apr 2016 13:28:32 +0200 | |
changeset 62922 | 96691631c1eb |
parent 62761 | 5c672b22dcc2 |
child 62958 | b41c1cb5e251 |
permissions | -rw-r--r-- |
11522 | 1 |
(* Title: Pure/Proof/proof_syntax.ML |
11539 | 2 |
Author: Stefan Berghofer, TU Muenchen |
11522 | 3 |
|
4 |
Function for parsing and printing proof terms. |
|
5 |
*) |
|
6 |
||
7 |
signature PROOF_SYNTAX = |
|
8 |
sig |
|
17078 | 9 |
val proofT: typ |
10 |
val add_proof_syntax: theory -> theory |
|
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
11 |
val proof_of_term: theory -> bool -> term -> Proofterm.proof |
17078 | 12 |
val term_of_proof: Proofterm.proof -> term |
13 |
val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) |
|
37227
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
14 |
val read_term: theory -> bool -> typ -> string -> term |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
15 |
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof |
17078 | 16 |
val proof_syntax: Proofterm.proof -> theory -> theory |
62922 | 17 |
val proof_of: Proof.context -> bool -> thm -> Proofterm.proof |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
18 |
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
19 |
val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
11522 | 20 |
end; |
21 |
||
33388 | 22 |
structure Proof_Syntax : PROOF_SYNTAX = |
11522 | 23 |
struct |
24 |
||
25 |
(**** add special syntax for embedding proof terms ****) |
|
26 |
||
27 |
val proofT = Type ("proof", []); |
|
11614 | 28 |
val paramT = Type ("param", []); |
29 |
val paramsT = Type ("params", []); |
|
11522 | 30 |
val idtT = Type ("idt", []); |
24848 | 31 |
val aT = TFree (Name.aT, []); |
11522 | 32 |
|
62752 | 33 |
|
11522 | 34 |
(** constants for theorems and axioms **) |
35 |
||
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
36 |
fun add_proof_atom_consts names thy = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
37 |
thy |
30435
e62d6ecab6ad
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset
|
38 |
|> Sign.root_path |
56239 | 39 |
|> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); |
11522 | 40 |
|
62752 | 41 |
|
11522 | 42 |
(** constants for application and abstraction **) |
11614 | 43 |
|
62752 | 44 |
fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); |
45 |
||
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
46 |
fun add_proof_syntax thy = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
47 |
thy |
22796 | 48 |
|> Sign.root_path |
36449 | 49 |
|> Sign.set_defsort [] |
56436 | 50 |
|> Sign.add_types_global |
51 |
[(Binding.make ("proof", @{here}), 0, NoSyn)] |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset
|
52 |
|> fold (snd oo Sign.declare_const_global) |
62752 | 53 |
[((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)), |
54 |
((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)), |
|
56436 | 55 |
((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn), |
56 |
((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn), |
|
57 |
((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn), |
|
58 |
((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn), |
|
59 |
((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn), |
|
62761 | 60 |
((Binding.make ("MinProof", @{here}), proofT), Mixfix.mixfix "?")] |
56436 | 61 |
|> Sign.add_nonterminals_global |
62 |
[Binding.make ("param", @{here}), |
|
63 |
Binding.make ("params", @{here})] |
|
56240 | 64 |
|> Sign.add_syntax Syntax.mode_default |
62752 | 65 |
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)), |
66 |
("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), |
|
67 |
("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), |
|
68 |
("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)), |
|
62761 | 69 |
("", paramT --> paramT, Mixfix.mixfix "'(_')"), |
70 |
("", idtT --> paramsT, Mixfix.mixfix "_"), |
|
71 |
("", paramT --> paramsT, Mixfix.mixfix "_")] |
|
61957
301833d9013a
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
60826
diff
changeset
|
72 |
|> Sign.add_syntax (Print_Mode.ASCII, true) |
62752 | 73 |
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)), |
74 |
(Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)), |
|
75 |
(Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))] |
|
42204 | 76 |
|> Sign.add_trrules (map Syntax.Parse_Print_Rule |
56436 | 77 |
[(Ast.mk_appl (Ast.Constant "_Lam") |
78 |
[Ast.mk_appl (Ast.Constant "_Lam0") |
|
79 |
[Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"], |
|
80 |
Ast.mk_appl (Ast.Constant "_Lam") |
|
81 |
[Ast.Variable "l", |
|
82 |
Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]), |
|
83 |
(Ast.mk_appl (Ast.Constant "_Lam") |
|
84 |
[Ast.mk_appl (Ast.Constant "_Lam1") |
|
85 |
[Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"], |
|
86 |
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A", |
|
87 |
(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), |
|
88 |
(Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"], |
|
89 |
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst")) |
|
90 |
[(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); |
|
11522 | 91 |
|
92 |
||
93 |
(**** translation between proof terms and pure terms ****) |
|
94 |
||
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
95 |
fun proof_of_term thy ty = |
11522 | 96 |
let |
56161 | 97 |
val thms = Global_Theory.all_thms_of thy true; |
16350 | 98 |
val axms = Theory.all_axioms_of thy; |
11522 | 99 |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
19618
diff
changeset
|
100 |
fun mk_term t = (if ty then I else map_types (K dummyT)) |
11614 | 101 |
(Term.no_dummy_patterns t); |
102 |
||
11522 | 103 |
fun prf_of [] (Bound i) = PBound i |
104 |
| prf_of Ts (Const (s, Type ("proof", _))) = |
|
37310 | 105 |
Proofterm.change_type (if ty then SOME Ts else NONE) |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
106 |
(case Long_Name.explode s of |
11614 | 107 |
"axm" :: xs => |
11522 | 108 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
109 |
val name = Long_Name.implode xs; |
17223 | 110 |
val prop = (case AList.lookup (op =) axms name of |
15531 | 111 |
SOME prop => prop |
112 |
| NONE => error ("Unknown axiom " ^ quote name)) |
|
113 |
in PAxm (name, prop, NONE) end |
|
11614 | 114 |
| "thm" :: xs => |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
115 |
let val name = Long_Name.implode xs; |
17223 | 116 |
in (case AList.lookup (op =) thms name of |
37310 | 117 |
SOME thm => |
118 |
fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm)))) |
|
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
119 |
| NONE => error ("Unknown theorem " ^ quote name)) |
11522 | 120 |
end |
121 |
| _ => error ("Illegal proof constant name: " ^ quote s)) |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset
|
122 |
| prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = |
31903 | 123 |
(case try Logic.class_of_const c_class of |
124 |
SOME c => |
|
37310 | 125 |
Proofterm.change_type (if ty then SOME Ts else NONE) |
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset
|
126 |
(OfClass (TVar ((Name.aT, 0), []), c)) |
31903 | 127 |
| NONE => error ("Bad class constant: " ^ quote c_class)) |
13199 | 128 |
| prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop |
11522 | 129 |
| prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v |
130 |
| prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) = |
|
25245
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
131 |
if T = proofT then |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
132 |
error ("Term variable abstraction may not bind proof variable " ^ quote s) |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
133 |
else Abst (s, if ty then SOME T else NONE, |
37310 | 134 |
Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) |
11522 | 135 |
| prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = |
11614 | 136 |
AbsP (s, case t of |
56241 | 137 |
Const ("Pure.dummy_pattern", _) => NONE |
138 |
| _ $ Const ("Pure.dummy_pattern", _) => NONE |
|
15531 | 139 |
| _ => SOME (mk_term t), |
37310 | 140 |
Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) |
11522 | 141 |
| prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = |
11614 | 142 |
prf_of [] prf1 %% prf_of [] prf2 |
56243 | 143 |
| prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) = |
11522 | 144 |
prf_of (T::Ts) prf |
11614 | 145 |
| prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % |
56241 | 146 |
(case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) |
11522 | 147 |
| prf_of _ t = error ("Not a proof term:\n" ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26626
diff
changeset
|
148 |
Syntax.string_of_term_global thy t) |
11522 | 149 |
|
150 |
in prf_of [] end; |
|
151 |
||
152 |
||
153 |
val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT); |
|
154 |
val AppPt = Const ("AppP", [proofT, proofT] ---> proofT); |
|
13199 | 155 |
val Hypt = Const ("Hyp", propT --> proofT); |
156 |
val Oraclet = Const ("Oracle", propT --> proofT); |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset
|
157 |
val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT); |
13199 | 158 |
val MinProoft = Const ("MinProof", proofT); |
11522 | 159 |
|
19473 | 160 |
val mk_tyapp = fold (fn T => fn prf => Const ("Appt", |
19391 | 161 |
[proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); |
11522 | 162 |
|
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
163 |
fun term_of _ (PThm (_, ((name, _, NONE), _))) = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
164 |
Const (Long_Name.append "thm" name, proofT) |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
165 |
| term_of _ (PThm (_, ((name, _, SOME Ts), _))) = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
166 |
mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT)) |
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
167 |
| term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) |
15531 | 168 |
| term_of _ (PAxm (name, _, SOME Ts)) = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
169 |
mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) |
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset
|
170 |
| term_of _ (OfClass (T, c)) = |
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset
|
171 |
mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) |
11522 | 172 |
| term_of _ (PBound i) = Bound i |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
173 |
| term_of Ts (Abst (s, opT, prf)) = |
18939 | 174 |
let val T = the_default dummyT opT |
11522 | 175 |
in Const ("Abst", (T --> proofT) --> proofT) $ |
37310 | 176 |
Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf)) |
11522 | 177 |
end |
178 |
| term_of Ts (AbsP (s, t, prf)) = |
|
45156 | 179 |
AbsPt $ the_default Term.dummy_prop t $ |
37310 | 180 |
Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf)) |
11614 | 181 |
| term_of Ts (prf1 %% prf2) = |
11522 | 182 |
AppPt $ term_of Ts prf1 $ term_of Ts prf2 |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
183 |
| term_of Ts (prf % opt) = |
45156 | 184 |
let val t = the_default Term.dummy opt |
11522 | 185 |
in Const ("Appt", |
186 |
[proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $ |
|
187 |
term_of Ts prf $ t |
|
188 |
end |
|
189 |
| term_of Ts (Hyp t) = Hypt $ t |
|
190 |
| term_of Ts (Oracle (_, t, _)) = Oraclet $ t |
|
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
191 |
| term_of Ts MinProof = MinProoft; |
11522 | 192 |
|
193 |
val term_of_proof = term_of []; |
|
194 |
||
195 |
fun cterm_of_proof thy prf = |
|
196 |
let |
|
56161 | 197 |
val thm_names = map fst (Global_Theory.all_thms_of thy true); |
16350 | 198 |
val axm_names = map fst (Theory.all_axioms_of thy); |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
199 |
val thy' = thy |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
200 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
201 |
|> add_proof_atom_consts |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
202 |
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); |
11522 | 203 |
in |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset
|
204 |
(Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) |
11522 | 205 |
end; |
206 |
||
37227
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
207 |
fun read_term thy topsort = |
11522 | 208 |
let |
56161 | 209 |
val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true)); |
16350 | 210 |
val axm_names = map fst (Theory.all_axioms_of thy); |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
211 |
val ctxt = thy |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
212 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
213 |
|> add_proof_atom_consts |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
214 |
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |
42360 | 215 |
|> Proof_Context.init_global |
216 |
|> Proof_Context.allow_dummies |
|
217 |
|> Proof_Context.set_mode Proof_Context.mode_schematic |
|
42406
05f2468d6b36
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
wenzelm
parents:
42375
diff
changeset
|
218 |
|> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []); |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
219 |
in |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
220 |
fn ty => fn s => |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
221 |
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |
39288 | 222 |
|> Type.constraint ty |> Syntax.check_term ctxt |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
223 |
end; |
11522 | 224 |
|
37227
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
225 |
fun read_proof thy topsort = |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
226 |
let val rd = read_term thy topsort proofT |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35262
diff
changeset
|
227 |
in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
11522 | 228 |
|
17078 | 229 |
fun proof_syntax prf = |
11522 | 230 |
let |
37310 | 231 |
val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
232 |
(fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I |
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
233 |
| _ => I) [prf] Symtab.empty); |
37310 | 234 |
val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
235 |
(fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
11522 | 236 |
in |
17078 | 237 |
add_proof_syntax #> |
238 |
add_proof_atom_consts |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
239 |
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) |
11522 | 240 |
end; |
241 |
||
62922 | 242 |
fun proof_of ctxt full raw_thm = |
17078 | 243 |
let |
62922 | 244 |
val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm; |
17078 | 245 |
val prop = Thm.full_prop_of thm; |
28814 | 246 |
val prf = Thm.proof_of thm; |
37310 | 247 |
val prf' = |
248 |
(case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of |
|
249 |
(PThm (_, ((_, prop', _), body)), _) => |
|
250 |
if prop = prop' then Proofterm.join_proof body else prf |
|
17078 | 251 |
| _ => prf) |
62922 | 252 |
in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end; |
17078 | 253 |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
254 |
fun pretty_proof ctxt prf = |
42360 | 255 |
Proof_Context.pretty_term_abbrev |
55725
9d605a21d7ec
prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
wenzelm
parents:
52788
diff
changeset
|
256 |
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
257 |
(term_of_proof prf); |
17078 | 258 |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
259 |
fun pretty_proof_of ctxt full th = |
62922 | 260 |
pretty_proof ctxt (proof_of ctxt full th); |
11522 | 261 |
|
262 |
end; |