320 |
320 |
321 (** specification primitives **) |
321 (** specification primitives **) |
322 |
322 |
323 (* rules *) |
323 (* rules *) |
324 |
324 |
|
325 fun stripped_sorts thy t = |
|
326 let |
|
327 val tfrees = rev (map TFree (Term.add_tfrees t [])); |
|
328 val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); |
|
329 val strip = tfrees ~~ tfrees'; |
|
330 val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip; |
|
331 val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; |
|
332 in (strip, recover, t') end; |
|
333 |
325 fun add_axiom (b, prop) thy = |
334 fun add_axiom (b, prop) thy = |
326 let |
335 let |
327 val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b; |
336 val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b; |
328 val thy' = thy |> Theory.add_axioms_i [(b', prop)]; |
337 val (strip, recover, prop') = stripped_sorts thy prop; |
329 val axm = unvarify_global (Thm.axiom thy' (Sign.full_name thy' b')); |
338 val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; |
330 in (axm, thy') end; |
339 val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip; |
|
340 val thy' = thy |
|
341 |> Theory.add_axioms_i [(b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop'))]; |
|
342 val axm' = Thm.axiom thy' (Sign.full_name thy' b'); |
|
343 val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts; |
|
344 in (thm, thy') end; |
331 |
345 |
332 fun add_def unchecked overloaded (b, prop) thy = |
346 fun add_def unchecked overloaded (b, prop) thy = |
333 let |
347 let |
334 val tfrees = rev (map TFree (Term.add_tfrees prop [])); |
348 val (strip, recover, prop') = stripped_sorts thy prop; |
335 val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); |
|
336 val strip_sorts = tfrees ~~ tfrees'; |
|
337 val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global)) (tfrees' ~~ tfrees); |
|
338 |
|
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; |
349 val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy; |
341 val axm' = Thm.axiom thy' (Sign.full_name thy' b); |
350 val axm' = Thm.axiom thy' (Sign.full_name thy' b); |
342 val thm = unvarify_global (Thm.instantiate (recover_sorts, []) axm'); |
351 val thm = unvarify_global (Thm.instantiate (recover, []) axm'); |
343 in (thm, thy') end; |
352 in (thm, thy') end; |
344 |
353 |
345 |
354 |
346 |
355 |
347 (** attributes **) |
356 (** attributes **) |