96 fun mk_term t = (if ty then I else map_types (K dummyT)) |
94 fun mk_term t = (if ty then I else map_types (K dummyT)) |
97 (Term.no_dummy_patterns t); |
95 (Term.no_dummy_patterns t); |
98 |
96 |
99 fun prf_of [] (Bound i) = PBound i |
97 fun prf_of [] (Bound i) = PBound i |
100 | prf_of Ts (Const (s, Type ("proof", _))) = |
98 | prf_of Ts (Const (s, Type ("proof", _))) = |
101 change_type (if ty then SOME Ts else NONE) |
99 Proofterm.change_type (if ty then SOME Ts else NONE) |
102 (case Long_Name.explode s of |
100 (case Long_Name.explode s of |
103 "axm" :: xs => |
101 "axm" :: xs => |
104 let |
102 let |
105 val name = Long_Name.implode xs; |
103 val name = Long_Name.implode xs; |
106 val prop = (case AList.lookup (op =) axms name of |
104 val prop = (case AList.lookup (op =) axms name of |
108 | NONE => error ("Unknown axiom " ^ quote name)) |
106 | NONE => error ("Unknown axiom " ^ quote name)) |
109 in PAxm (name, prop, NONE) end |
107 in PAxm (name, prop, NONE) end |
110 | "thm" :: xs => |
108 | "thm" :: xs => |
111 let val name = Long_Name.implode xs; |
109 let val name = Long_Name.implode xs; |
112 in (case AList.lookup (op =) thms name of |
110 in (case AList.lookup (op =) thms name of |
113 SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm)))) |
111 SOME thm => |
|
112 fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm)))) |
114 | NONE => error ("Unknown theorem " ^ quote name)) |
113 | NONE => error ("Unknown theorem " ^ quote name)) |
115 end |
114 end |
116 | _ => error ("Illegal proof constant name: " ^ quote s)) |
115 | _ => error ("Illegal proof constant name: " ^ quote s)) |
117 | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = |
116 | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = |
118 (case try Logic.class_of_const c_class of |
117 (case try Logic.class_of_const c_class of |
119 SOME c => |
118 SOME c => |
120 change_type (if ty then SOME Ts else NONE) |
119 Proofterm.change_type (if ty then SOME Ts else NONE) |
121 (OfClass (TVar ((Name.aT, 0), []), c)) |
120 (OfClass (TVar ((Name.aT, 0), []), c)) |
122 | NONE => error ("Bad class constant: " ^ quote c_class)) |
121 | NONE => error ("Bad class constant: " ^ quote c_class)) |
123 | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop |
122 | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop |
124 | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v |
123 | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v |
125 | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) = |
124 | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) = |
126 if T = proofT then |
125 if T = proofT then |
127 error ("Term variable abstraction may not bind proof variable " ^ quote s) |
126 error ("Term variable abstraction may not bind proof variable " ^ quote s) |
128 else Abst (s, if ty then SOME T else NONE, |
127 else Abst (s, if ty then SOME T else NONE, |
129 incr_pboundvars (~1) 0 (prf_of [] prf)) |
128 Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) |
130 | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = |
129 | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = |
131 AbsP (s, case t of |
130 AbsP (s, case t of |
132 Const ("dummy_pattern", _) => NONE |
131 Const ("dummy_pattern", _) => NONE |
133 | _ $ Const ("dummy_pattern", _) => NONE |
132 | _ $ Const ("dummy_pattern", _) => NONE |
134 | _ => SOME (mk_term t), |
133 | _ => SOME (mk_term t), |
135 incr_pboundvars 0 (~1) (prf_of [] prf)) |
134 Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) |
136 | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = |
135 | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = |
137 prf_of [] prf1 %% prf_of [] prf2 |
136 prf_of [] prf1 %% prf_of [] prf2 |
138 | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = |
137 | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = |
139 prf_of (T::Ts) prf |
138 prf_of (T::Ts) prf |
140 | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % |
139 | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % |
166 mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) |
165 mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) |
167 | term_of _ (PBound i) = Bound i |
166 | term_of _ (PBound i) = Bound i |
168 | term_of Ts (Abst (s, opT, prf)) = |
167 | term_of Ts (Abst (s, opT, prf)) = |
169 let val T = the_default dummyT opT |
168 let val T = the_default dummyT opT |
170 in Const ("Abst", (T --> proofT) --> proofT) $ |
169 in Const ("Abst", (T --> proofT) --> proofT) $ |
171 Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) |
170 Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf)) |
172 end |
171 end |
173 | term_of Ts (AbsP (s, t, prf)) = |
172 | term_of Ts (AbsP (s, t, prf)) = |
174 AbsPt $ the_default (Term.dummy_pattern propT) t $ |
173 AbsPt $ the_default (Term.dummy_pattern propT) t $ |
175 Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) |
174 Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf)) |
176 | term_of Ts (prf1 %% prf2) = |
175 | term_of Ts (prf1 %% prf2) = |
177 AppPt $ term_of Ts prf1 $ term_of Ts prf2 |
176 AppPt $ term_of Ts prf1 $ term_of Ts prf2 |
178 | term_of Ts (prf % opt) = |
177 | term_of Ts (prf % opt) = |
179 let val t = the_default (Term.dummy_pattern dummyT) opt |
178 let val t = the_default (Term.dummy_pattern dummyT) opt |
180 in Const ("Appt", |
179 in Const ("Appt", |
231 let val rd = read_term thy topsort proofT |
230 let val rd = read_term thy topsort proofT |
232 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
231 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
233 |
232 |
234 fun proof_syntax prf = |
233 fun proof_syntax prf = |
235 let |
234 let |
236 val thm_names = Symtab.keys (fold_proof_atoms true |
235 val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
237 (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I |
236 (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I |
238 | _ => I) [prf] Symtab.empty); |
237 | _ => I) [prf] Symtab.empty); |
239 val axm_names = Symtab.keys (fold_proof_atoms true |
238 val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
240 (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
239 (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
241 in |
240 in |
242 add_proof_syntax #> |
241 add_proof_syntax #> |
243 add_proof_atom_consts |
242 add_proof_atom_consts |
244 (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) |
243 (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) |
247 fun proof_of full thm = |
246 fun proof_of full thm = |
248 let |
247 let |
249 val thy = Thm.theory_of_thm thm; |
248 val thy = Thm.theory_of_thm thm; |
250 val prop = Thm.full_prop_of thm; |
249 val prop = Thm.full_prop_of thm; |
251 val prf = Thm.proof_of thm; |
250 val prf = Thm.proof_of thm; |
252 val prf' = (case strip_combt (fst (strip_combP prf)) of |
251 val prf' = |
253 (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else 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 |
254 | _ => prf) |
255 | _ => prf) |
255 in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; |
256 in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; |
256 |
257 |
257 fun pretty_proof ctxt prf = |
258 fun pretty_proof ctxt prf = |
258 ProofContext.pretty_term_abbrev |
259 ProofContext.pretty_term_abbrev |