9 val proofT: typ |
9 val proofT: typ |
10 val add_proof_syntax: theory -> theory |
10 val add_proof_syntax: theory -> theory |
11 val proof_of_term: theory -> bool -> term -> Proofterm.proof |
11 val proof_of_term: theory -> bool -> term -> Proofterm.proof |
12 val term_of_proof: Proofterm.proof -> term |
12 val term_of_proof: Proofterm.proof -> term |
13 val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) |
13 val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) |
14 val read_term: theory -> typ -> string -> term |
14 val strip_sorts_consttypes: Proof.context -> Proof.context |
15 val read_proof: theory -> bool -> string -> Proofterm.proof |
15 val read_term: theory -> bool -> typ -> string -> term |
|
16 val read_proof: theory -> bool -> bool -> string -> Proofterm.proof |
16 val proof_syntax: Proofterm.proof -> theory -> theory |
17 val proof_syntax: Proofterm.proof -> theory -> theory |
17 val proof_of: bool -> thm -> Proofterm.proof |
18 val proof_of: bool -> thm -> Proofterm.proof |
18 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
19 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
19 val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
20 val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
20 end; |
21 end; |
107 | NONE => error ("Unknown axiom " ^ quote name)) |
108 | NONE => error ("Unknown axiom " ^ quote name)) |
108 in PAxm (name, prop, NONE) end |
109 in PAxm (name, prop, NONE) end |
109 | "thm" :: xs => |
110 | "thm" :: xs => |
110 let val name = Long_Name.implode xs; |
111 let val name = Long_Name.implode xs; |
111 in (case AList.lookup (op =) thms name of |
112 in (case AList.lookup (op =) thms name of |
112 SOME thm => fst (strip_combt (Thm.proof_of thm)) |
113 SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm)))) |
113 | NONE => error ("Unknown theorem " ^ quote name)) |
114 | NONE => error ("Unknown theorem " ^ quote name)) |
114 end |
115 end |
115 | _ => error ("Illegal proof constant name: " ^ quote s)) |
116 | _ => error ("Illegal proof constant name: " ^ quote s)) |
116 | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = |
117 | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = |
117 (case try Logic.class_of_const c_class of |
118 (case try Logic.class_of_const c_class of |
196 (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); |
197 (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); |
197 in |
198 in |
198 (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) |
199 (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) |
199 end; |
200 end; |
200 |
201 |
201 fun read_term thy = |
202 fun strip_sorts_consttypes ctxt = |
|
203 let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt) |
|
204 in Symtab.fold (fn (s, (T, _)) => |
|
205 ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T))) |
|
206 tab ctxt |
|
207 end; |
|
208 |
|
209 fun read_term thy topsort = |
202 let |
210 let |
203 val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy)); |
211 val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy)); |
204 val axm_names = map fst (Theory.all_axioms_of thy); |
212 val axm_names = map fst (Theory.all_axioms_of thy); |
205 val ctxt = thy |
213 val ctxt = thy |
206 |> add_proof_syntax |
214 |> add_proof_syntax |
207 |> add_proof_atom_consts |
215 |> add_proof_atom_consts |
208 (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |
216 (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |
209 |> ProofContext.init_global |
217 |> ProofContext.init_global |
210 |> ProofContext.allow_dummies |
218 |> ProofContext.allow_dummies |
211 |> ProofContext.set_mode ProofContext.mode_schematic; |
219 |> ProofContext.set_mode ProofContext.mode_schematic |
|
220 |> (if topsort then |
|
221 strip_sorts_consttypes #> |
|
222 ProofContext.set_defsort [] |
|
223 else I); |
212 in |
224 in |
213 fn ty => fn s => |
225 fn ty => fn s => |
214 (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |
226 (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |
215 |> TypeInfer.constrain ty |> Syntax.check_term ctxt |
227 |> TypeInfer.constrain ty |> Syntax.check_term ctxt |
216 end; |
228 end; |
217 |
229 |
218 fun read_proof thy = |
230 fun read_proof thy topsort = |
219 let val rd = read_term thy proofT |
231 let val rd = read_term thy topsort proofT |
220 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
232 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
221 |
233 |
222 fun proof_syntax prf = |
234 fun proof_syntax prf = |
223 let |
235 let |
224 val thm_names = Symtab.keys (fold_proof_atoms true |
236 val thm_names = Symtab.keys (fold_proof_atoms true |