57 val certify_inst: theory -> |
57 val certify_inst: theory -> |
58 ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> |
58 ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> |
59 (ctyp * ctyp) list * (cterm * cterm) list |
59 (ctyp * ctyp) list * (cterm * cterm) list |
60 val certify_instantiate: |
60 val certify_instantiate: |
61 ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm |
61 ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm |
62 val unvarify: thm -> thm |
62 val unvarify_global: thm -> thm |
63 val close_derivation: thm -> thm |
63 val close_derivation: thm -> thm |
64 val add_axiom: binding * term -> theory -> thm * theory |
64 val add_axiom: binding * term -> theory -> thm * theory |
65 val add_def: bool -> bool -> binding * term -> theory -> thm * theory |
65 val add_def: bool -> bool -> binding * term -> theory -> thm * theory |
66 type binding = binding * attribute list |
66 type binding = binding * attribute list |
67 val empty_binding: binding |
67 val empty_binding: binding |
293 |
293 |
294 fun certify_instantiate insts th = |
294 fun certify_instantiate insts th = |
295 Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th; |
295 Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th; |
296 |
296 |
297 |
297 |
298 (* unvarify: global schematic variables *) |
298 (* unvarify_global: global schematic variables *) |
299 |
299 |
300 fun unvarify th = |
300 fun unvarify_global th = |
301 let |
301 let |
302 val prop = Thm.full_prop_of th; |
302 val prop = Thm.full_prop_of th; |
303 val _ = map Logic.unvarify (prop :: Thm.hyps_of th) |
303 val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) |
304 handle TERM (msg, _) => raise THM (msg, 0, [th]); |
304 handle TERM (msg, _) => raise THM (msg, 0, [th]); |
305 |
305 |
306 val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); |
306 val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); |
307 val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => |
307 val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => |
308 let val T' = Term_Subst.instantiateT instT T |
308 let val T' = Term_Subst.instantiateT instT T |
324 |
324 |
325 fun add_axiom (b, prop) thy = |
325 fun add_axiom (b, prop) thy = |
326 let |
326 let |
327 val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b; |
327 val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b; |
328 val thy' = thy |> Theory.add_axioms_i [(b', prop)]; |
328 val thy' = thy |> Theory.add_axioms_i [(b', prop)]; |
329 val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b')); |
329 val axm = unvarify_global (Thm.axiom thy' (Sign.full_name thy' b')); |
330 in (axm, thy') end; |
330 in (axm, thy') end; |
331 |
331 |
332 fun add_def unchecked overloaded (b, prop) thy = |
332 fun add_def unchecked overloaded (b, prop) thy = |
333 let |
333 let |
334 val tfrees = rev (map TFree (Term.add_tfrees prop [])); |
334 val tfrees = rev (map TFree (Term.add_tfrees prop [])); |
335 val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); |
335 val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); |
336 val strip_sorts = tfrees ~~ tfrees'; |
336 val strip_sorts = tfrees ~~ tfrees'; |
337 val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees); |
337 val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global)) (tfrees' ~~ tfrees); |
338 |
338 |
339 val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop; |
339 val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop; |
340 val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy; |
340 val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy; |
341 val axm' = Thm.axiom thy' (Sign.full_name thy' b); |
341 val axm' = Thm.axiom thy' (Sign.full_name thy' b); |
342 val thm = unvarify (Thm.instantiate (recover_sorts, []) axm'); |
342 val thm = unvarify_global (Thm.instantiate (recover_sorts, []) axm'); |
343 in (thm, thy') end; |
343 in (thm, thy') end; |
344 |
344 |
345 |
345 |
346 |
346 |
347 (** attributes **) |
347 (** attributes **) |