author | wenzelm |
Sun, 20 Oct 2019 20:38:22 +0200 | |
changeset 70915 | bd4d37edfee4 |
parent 70914 | 05c4c6a99b3f |
child 70979 | 7abe5abb4c05 |
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 add_proof_syntax: theory -> theory |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
10 |
val proof_of_term: theory -> bool -> term -> 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
|
11 |
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
|
12 |
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof |
17078 | 13 |
val proof_syntax: Proofterm.proof -> theory -> theory |
70449 | 14 |
val proof_of: bool -> thm -> Proofterm.proof |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
15 |
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
70839
2136e4670ad2
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
wenzelm
parents:
70813
diff
changeset
|
16 |
val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T |
11522 | 17 |
end; |
18 |
||
33388 | 19 |
structure Proof_Syntax : PROOF_SYNTAX = |
11522 | 20 |
struct |
21 |
||
22 |
(**** add special syntax for embedding proof terms ****) |
|
23 |
||
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
24 |
val proofT = Proofterm.proofT; |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
25 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
26 |
local |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
27 |
|
11614 | 28 |
val paramT = Type ("param", []); |
29 |
val paramsT = Type ("params", []); |
|
11522 | 30 |
val idtT = Type ("idt", []); |
70387 | 31 |
val aT = Term.aT []; |
11522 | 32 |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
33 |
fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); |
11522 | 34 |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
35 |
in |
62752 | 36 |
|
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
37 |
fun add_proof_syntax thy = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
38 |
thy |
22796 | 39 |
|> Sign.root_path |
36449 | 40 |
|> Sign.set_defsort [] |
56436 | 41 |
|> Sign.add_nonterminals_global |
64556 | 42 |
[Binding.make ("param", \<^here>), |
43 |
Binding.make ("params", \<^here>)] |
|
56240 | 44 |
|> Sign.add_syntax Syntax.mode_default |
62752 | 45 |
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)), |
46 |
("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), |
|
47 |
("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), |
|
48 |
("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)), |
|
62761 | 49 |
("", paramT --> paramT, Mixfix.mixfix "'(_')"), |
50 |
("", idtT --> paramsT, Mixfix.mixfix "_"), |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
51 |
("", paramT --> paramsT, Mixfix.mixfix "_"), |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
52 |
(Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)), |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
53 |
(Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)), |
70407 | 54 |
(Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "\<^bold>?")] |
42204 | 55 |
|> Sign.add_trrules (map Syntax.Parse_Print_Rule |
56436 | 56 |
[(Ast.mk_appl (Ast.Constant "_Lam") |
57 |
[Ast.mk_appl (Ast.Constant "_Lam0") |
|
58 |
[Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"], |
|
59 |
Ast.mk_appl (Ast.Constant "_Lam") |
|
60 |
[Ast.Variable "l", |
|
61 |
Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]), |
|
62 |
(Ast.mk_appl (Ast.Constant "_Lam") |
|
63 |
[Ast.mk_appl (Ast.Constant "_Lam1") |
|
64 |
[Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"], |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
65 |
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A", |
56436 | 66 |
(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), |
67 |
(Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"], |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
68 |
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst")) |
56436 | 69 |
[(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); |
11522 | 70 |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
71 |
end; |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
72 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
73 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
74 |
(** constants for theorems and axioms **) |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
75 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
76 |
fun add_proof_atom_consts names thy = |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
77 |
thy |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
78 |
|> Sign.root_path |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
79 |
|> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
80 |
|
11522 | 81 |
|
82 |
(**** translation between proof terms and pure terms ****) |
|
83 |
||
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
84 |
fun proof_of_term thy ty = |
11522 | 85 |
let |
56161 | 86 |
val thms = Global_Theory.all_thms_of thy true; |
16350 | 87 |
val axms = Theory.all_axioms_of thy; |
11522 | 88 |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
19618
diff
changeset
|
89 |
fun mk_term t = (if ty then I else map_types (K dummyT)) |
11614 | 90 |
(Term.no_dummy_patterns t); |
91 |
||
11522 | 92 |
fun prf_of [] (Bound i) = PBound i |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
93 |
| prf_of Ts (Const (s, Type ("Pure.proof", _))) = |
70417 | 94 |
Proofterm.change_types (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
|
95 |
(case Long_Name.explode s of |
11614 | 96 |
"axm" :: xs => |
11522 | 97 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
98 |
val name = Long_Name.implode xs; |
17223 | 99 |
val prop = (case AList.lookup (op =) axms name of |
15531 | 100 |
SOME prop => prop |
101 |
| NONE => error ("Unknown axiom " ^ quote name)) |
|
102 |
in PAxm (name, prop, NONE) end |
|
11614 | 103 |
| "thm" :: xs => |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
104 |
let val name = Long_Name.implode xs; |
17223 | 105 |
in (case AList.lookup (op =) thms name of |
37310 | 106 |
SOME thm => |
107 |
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
|
108 |
| NONE => error ("Unknown theorem " ^ quote name)) |
11522 | 109 |
end |
110 |
| _ => error ("Illegal proof constant name: " ^ quote s)) |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
111 |
| prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) = |
31903 | 112 |
(case try Logic.class_of_const c_class of |
113 |
SOME c => |
|
70417 | 114 |
Proofterm.change_types (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
|
115 |
(OfClass (TVar ((Name.aT, 0), []), c)) |
31903 | 116 |
| NONE => error ("Bad class constant: " ^ quote c_class)) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
117 |
| prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
118 |
| prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
119 |
| prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) = |
25245
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
120 |
if T = proofT then |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
121 |
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
|
122 |
else Abst (s, if ty then SOME T else NONE, |
37310 | 123 |
Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
124 |
| prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) = |
11614 | 125 |
AbsP (s, case t of |
56241 | 126 |
Const ("Pure.dummy_pattern", _) => NONE |
127 |
| _ $ Const ("Pure.dummy_pattern", _) => NONE |
|
15531 | 128 |
| _ => SOME (mk_term t), |
37310 | 129 |
Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
130 |
| prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) = |
11614 | 131 |
prf_of [] prf1 %% prf_of [] prf2 |
70418 | 132 |
| prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type ("itself", [T]))) = |
11522 | 133 |
prf_of (T::Ts) prf |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
134 |
| prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf % |
56241 | 135 |
(case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) |
11522 | 136 |
| 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
|
137 |
Syntax.string_of_term_global thy t) |
11522 | 138 |
|
139 |
in prf_of [] end; |
|
140 |
||
141 |
||
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
|
142 |
fun read_term thy topsort = |
11522 | 143 |
let |
56161 | 144 |
val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true)); |
16350 | 145 |
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
|
146 |
val ctxt = thy |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
147 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
148 |
|> add_proof_atom_consts |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
149 |
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |
42360 | 150 |
|> Proof_Context.init_global |
151 |
|> Proof_Context.allow_dummies |
|
152 |
|> Proof_Context.set_mode Proof_Context.mode_schematic |
|
62958
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
153 |
|> topsort ? |
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
154 |
(Proof_Context.set_defsort [] #> |
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
155 |
Config.put Type_Infer.object_logic false #> |
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
156 |
Config.put Type_Infer_Context.const_sorts false); |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
157 |
in |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
158 |
fn ty => fn s => |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
159 |
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |
39288 | 160 |
|> Type.constraint ty |> Syntax.check_term ctxt |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
161 |
end; |
11522 | 162 |
|
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
|
163 |
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
|
164 |
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
|
165 |
in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
11522 | 166 |
|
17078 | 167 |
fun proof_syntax prf = |
11522 | 168 |
let |
37310 | 169 |
val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
70493 | 170 |
(fn PThm ({name, ...}, _) => if name <> "" then Symtab.update (name, ()) else I |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
171 |
| _ => I) [prf] Symtab.empty); |
37310 | 172 |
val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
173 |
(fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
11522 | 174 |
in |
17078 | 175 |
add_proof_syntax #> |
176 |
add_proof_atom_consts |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
177 |
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) |
11522 | 178 |
end; |
179 |
||
70449 | 180 |
fun proof_of full thm = |
17078 | 181 |
let |
70449 | 182 |
val thy = Thm.theory_of_thm thm; |
17078 | 183 |
val prop = Thm.full_prop_of thm; |
28814 | 184 |
val prf = Thm.proof_of thm; |
70813 | 185 |
in |
186 |
(case fst (Proofterm.strip_combt (fst (Proofterm.strip_combP prf))) of |
|
187 |
PThm ({prop = prop', ...}, thm_body) => |
|
188 |
if prop = prop' then Proofterm.thm_body_proof_raw thm_body else prf |
|
189 |
| _ => prf) |
|
190 |
|> full ? Proofterm.reconstruct_proof thy prop |
|
191 |
end; |
|
17078 | 192 |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
193 |
fun pretty_proof ctxt prf = |
42360 | 194 |
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
|
195 |
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
196 |
(Proofterm.term_of_proof prf); |
17078 | 197 |
|
70839
2136e4670ad2
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
wenzelm
parents:
70813
diff
changeset
|
198 |
fun pretty_standard_proof_of ctxt full thm = |
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset
|
199 |
pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); |
11522 | 200 |
|
201 |
end; |