author | hoelzl |
Tue, 21 Dec 2010 15:00:59 +0100 | |
changeset 41368 | 8afa26855137 |
parent 39557 | fe5722fce758 |
child 42204 | b3277168c1e7 |
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 strip_sorts_consttypes: Proof.context -> Proof.context |
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_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
|
16 |
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof |
17078 | 17 |
val proof_syntax: Proofterm.proof -> theory -> theory |
18 |
val proof_of: bool -> thm -> Proofterm.proof |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
19 |
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
20 |
val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
11522 | 21 |
end; |
22 |
||
33388 | 23 |
structure Proof_Syntax : PROOF_SYNTAX = |
11522 | 24 |
struct |
25 |
||
26 |
(**** add special syntax for embedding proof terms ****) |
|
27 |
||
28 |
val proofT = Type ("proof", []); |
|
11614 | 29 |
val paramT = Type ("param", []); |
30 |
val paramsT = Type ("params", []); |
|
11522 | 31 |
val idtT = Type ("idt", []); |
24848 | 32 |
val aT = TFree (Name.aT, []); |
11522 | 33 |
|
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 |
e62d6ecab6ad
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset
|
39 |
|> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); |
11522 | 40 |
|
41 |
(** constants for application and abstraction **) |
|
11614 | 42 |
|
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
43 |
fun add_proof_syntax thy = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
44 |
thy |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
45 |
|> Theory.copy |
22796 | 46 |
|> Sign.root_path |
36449 | 47 |
|> Sign.set_defsort [] |
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
29635
diff
changeset
|
48 |
|> Sign.add_types [(Binding.name "proof", 0, NoSyn)] |
35122 | 49 |
|> fold (snd oo Sign.declare_const) |
50 |
[((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)), |
|
51 |
((Binding.name "AppP", [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)), |
|
52 |
((Binding.name "Abst", (aT --> proofT) --> proofT), NoSyn), |
|
53 |
((Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT), NoSyn), |
|
54 |
((Binding.name "Hyp", propT --> proofT), NoSyn), |
|
55 |
((Binding.name "Oracle", propT --> proofT), NoSyn), |
|
56 |
((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn), |
|
57 |
((Binding.name "MinProof", proofT), Delimfix "?")] |
|
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
29635
diff
changeset
|
58 |
|> Sign.add_nonterminals [Binding.name "param", Binding.name "params"] |
22796 | 59 |
|> Sign.add_syntax_i |
11640 | 60 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), |
11614 | 61 |
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
62 |
("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
|
63 |
("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)), |
|
64 |
("", paramT --> paramT, Delimfix "'(_')"), |
|
65 |
("", idtT --> paramsT, Delimfix "_"), |
|
66 |
("", paramT --> paramsT, Delimfix "_")] |
|
35122 | 67 |
|> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) |
11640 | 68 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)), |
35262
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
35122
diff
changeset
|
69 |
(Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)), |
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
35122
diff
changeset
|
70 |
(Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))] |
22796 | 71 |
|> Sign.add_modesyntax_i ("latex", false) |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
72 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))] |
22796 | 73 |
|> Sign.add_trrules_i (map Syntax.ParsePrintRule |
11522 | 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"], |
35262
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
35122
diff
changeset
|
80 |
Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A", |
11522 | 81 |
(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]), |
11614 | 82 |
(Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"], |
35262
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
35122
diff
changeset
|
83 |
Syntax.mk_appl (Constant (Syntax.mark_const "Abst")) |
11614 | 84 |
[(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]); |
11522 | 85 |
|
86 |
||
87 |
(**** translation between proof terms and pure terms ****) |
|
88 |
||
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
89 |
fun proof_of_term thy ty = |
11522 | 90 |
let |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39288
diff
changeset
|
91 |
val thms = Global_Theory.all_thms_of thy; |
16350 | 92 |
val axms = Theory.all_axioms_of thy; |
11522 | 93 |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
19618
diff
changeset
|
94 |
fun mk_term t = (if ty then I else map_types (K dummyT)) |
11614 | 95 |
(Term.no_dummy_patterns t); |
96 |
||
11522 | 97 |
fun prf_of [] (Bound i) = PBound i |
98 |
| prf_of Ts (Const (s, Type ("proof", _))) = |
|
37310 | 99 |
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
|
100 |
(case Long_Name.explode s of |
11614 | 101 |
"axm" :: xs => |
11522 | 102 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
103 |
val name = Long_Name.implode xs; |
17223 | 104 |
val prop = (case AList.lookup (op =) axms name of |
15531 | 105 |
SOME prop => prop |
106 |
| NONE => error ("Unknown axiom " ^ quote name)) |
|
107 |
in PAxm (name, prop, NONE) end |
|
11614 | 108 |
| "thm" :: xs => |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
109 |
let val name = Long_Name.implode xs; |
17223 | 110 |
in (case AList.lookup (op =) thms name of |
37310 | 111 |
SOME thm => |
112 |
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
|
113 |
| NONE => error ("Unknown theorem " ^ quote name)) |
11522 | 114 |
end |
115 |
| _ => 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
|
116 |
| prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = |
31903 | 117 |
(case try Logic.class_of_const c_class of |
118 |
SOME c => |
|
37310 | 119 |
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
|
120 |
(OfClass (TVar ((Name.aT, 0), []), c)) |
31903 | 121 |
| NONE => error ("Bad class constant: " ^ quote c_class)) |
13199 | 122 |
| prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop |
11522 | 123 |
| prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v |
124 |
| 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
|
125 |
if T = proofT then |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
126 |
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
|
127 |
else Abst (s, if ty then SOME T else NONE, |
37310 | 128 |
Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) |
11522 | 129 |
| prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = |
11614 | 130 |
AbsP (s, case t of |
15531 | 131 |
Const ("dummy_pattern", _) => NONE |
132 |
| _ $ Const ("dummy_pattern", _) => NONE |
|
133 |
| _ => SOME (mk_term t), |
|
37310 | 134 |
Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) |
11522 | 135 |
| prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = |
11614 | 136 |
prf_of [] prf1 %% prf_of [] prf2 |
11522 | 137 |
| prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = |
138 |
prf_of (T::Ts) prf |
|
11614 | 139 |
| prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % |
15531 | 140 |
(case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t)) |
11522 | 141 |
| 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
|
142 |
Syntax.string_of_term_global thy t) |
11522 | 143 |
|
144 |
in prf_of [] end; |
|
145 |
||
146 |
||
147 |
val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT); |
|
148 |
val AppPt = Const ("AppP", [proofT, proofT] ---> proofT); |
|
13199 | 149 |
val Hypt = Const ("Hyp", propT --> proofT); |
150 |
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
|
151 |
val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT); |
13199 | 152 |
val MinProoft = Const ("MinProof", proofT); |
11522 | 153 |
|
19473 | 154 |
val mk_tyapp = fold (fn T => fn prf => Const ("Appt", |
19391 | 155 |
[proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); |
11522 | 156 |
|
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
157 |
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
|
158 |
Const (Long_Name.append "thm" name, proofT) |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
159 |
| 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
|
160 |
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
|
161 |
| term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) |
15531 | 162 |
| 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
|
163 |
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
|
164 |
| term_of _ (OfClass (T, c)) = |
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset
|
165 |
mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) |
11522 | 166 |
| term_of _ (PBound i) = Bound i |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
167 |
| term_of Ts (Abst (s, opT, prf)) = |
18939 | 168 |
let val T = the_default dummyT opT |
11522 | 169 |
in Const ("Abst", (T --> proofT) --> proofT) $ |
37310 | 170 |
Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf)) |
11522 | 171 |
end |
172 |
| term_of Ts (AbsP (s, t, prf)) = |
|
18939 | 173 |
AbsPt $ the_default (Term.dummy_pattern propT) t $ |
37310 | 174 |
Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf)) |
11614 | 175 |
| term_of Ts (prf1 %% prf2) = |
11522 | 176 |
AppPt $ term_of Ts prf1 $ term_of Ts prf2 |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
177 |
| term_of Ts (prf % opt) = |
18939 | 178 |
let val t = the_default (Term.dummy_pattern dummyT) opt |
11522 | 179 |
in Const ("Appt", |
180 |
[proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $ |
|
181 |
term_of Ts prf $ t |
|
182 |
end |
|
183 |
| term_of Ts (Hyp t) = Hypt $ t |
|
184 |
| term_of Ts (Oracle (_, t, _)) = Oraclet $ t |
|
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
185 |
| term_of Ts MinProof = MinProoft; |
11522 | 186 |
|
187 |
val term_of_proof = term_of []; |
|
188 |
||
189 |
fun cterm_of_proof thy prf = |
|
190 |
let |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39288
diff
changeset
|
191 |
val thm_names = map fst (Global_Theory.all_thms_of thy); |
16350 | 192 |
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
|
193 |
val thy' = thy |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
194 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
195 |
|> add_proof_atom_consts |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
196 |
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); |
11522 | 197 |
in |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
198 |
(cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) |
11522 | 199 |
end; |
200 |
||
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
|
201 |
fun strip_sorts_consttypes ctxt = |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
202 |
let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt) |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
203 |
in Symtab.fold (fn (s, (T, _)) => |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
204 |
ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T))) |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
205 |
tab ctxt |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
206 |
end; |
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 |
|
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
208 |
fun read_term thy topsort = |
11522 | 209 |
let |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39288
diff
changeset
|
210 |
val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy)); |
16350 | 211 |
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
|
212 |
val ctxt = thy |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
213 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
214 |
|> add_proof_atom_consts |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
215 |
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36449
diff
changeset
|
216 |
|> ProofContext.init_global |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
217 |
|> ProofContext.allow_dummies |
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
|
218 |
|> ProofContext.set_mode ProofContext.mode_schematic |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
219 |
|> (if topsort then |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
220 |
strip_sorts_consttypes #> |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
221 |
ProofContext.set_defsort [] |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
222 |
else I); |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
223 |
in |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
224 |
fn ty => fn s => |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
225 |
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |
39288 | 226 |
|> Type.constraint ty |> Syntax.check_term ctxt |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
227 |
end; |
11522 | 228 |
|
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
|
229 |
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
|
230 |
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
|
231 |
in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
11522 | 232 |
|
17078 | 233 |
fun proof_syntax prf = |
11522 | 234 |
let |
37310 | 235 |
val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
236 |
(fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I |
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
237 |
| _ => I) [prf] Symtab.empty); |
37310 | 238 |
val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
239 |
(fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
11522 | 240 |
in |
17078 | 241 |
add_proof_syntax #> |
242 |
add_proof_atom_consts |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
243 |
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) |
11522 | 244 |
end; |
245 |
||
17078 | 246 |
fun proof_of full thm = |
247 |
let |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25245
diff
changeset
|
248 |
val thy = Thm.theory_of_thm thm; |
17078 | 249 |
val prop = Thm.full_prop_of thm; |
28814 | 250 |
val prf = Thm.proof_of thm; |
37310 | 251 |
val prf' = |
252 |
(case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of |
|
253 |
(PThm (_, ((_, prop', _), body)), _) => |
|
254 |
if prop = prop' then Proofterm.join_proof body else prf |
|
17078 | 255 |
| _ => prf) |
256 |
in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; |
|
257 |
||
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
258 |
fun pretty_proof ctxt prf = |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
259 |
ProofContext.pretty_term_abbrev |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
260 |
(ProofContext.transfer_syntax (proof_syntax prf (ProofContext.theory_of ctxt)) ctxt) |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
261 |
(term_of_proof prf); |
17078 | 262 |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
263 |
fun pretty_proof_of ctxt full th = |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
264 |
pretty_proof ctxt (proof_of full th); |
11522 | 265 |
|
266 |
end; |