Main renaming + fixes for new Isabelle in IntEx2.
(* Title: quotient_def.thy+ −
Author: Cezary Kaliszyk and Christian Urban+ −
+ −
Definitions for constants on quotient types.+ −
+ −
*)+ −
+ −
signature QUOTIENT_DEF =+ −
sig+ −
val quotient_def: mixfix -> Attrib.binding -> term -> term ->+ −
local_theory -> (term * thm) * local_theory+ −
+ −
val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->+ −
local_theory -> local_theory+ −
end;+ −
+ −
structure Quotient_Def: QUOTIENT_DEF =+ −
struct+ −
+ −
open Quotient_Info;+ −
open Quotient_Term;+ −
+ −
(* wrapper for define *)+ −
fun define name mx attr rhs lthy =+ −
let+ −
val ((rhs, (_ , thm)), lthy') =+ −
Local_Theory.define ((name, mx), (attr, rhs)) lthy+ −
in+ −
((rhs, thm), lthy')+ −
end+ −
+ −
+ −
(** Interface and Syntax Setup **)+ −
+ −
(* The ML-interface for a quotient definition takes+ −
as argument:+ −
+ −
- the mixfix annotation+ −
- name and attributes+ −
- the new constant as term+ −
- the rhs of the definition as term+ −
+ −
It returns the defined constant and its definition+ −
theorem; stores the data in the qconsts data slot.+ −
+ −
Restriction: At the moment the right-hand side must+ −
be a terms composed of constant. Similarly the+ −
left-hand side must be a single constant.+ −
*)+ −
fun quotient_def mx attr lhs rhs lthy =+ −
let+ −
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."+ −
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"+ −
+ −
val qconst_bname = Binding.name lhs_str+ −
val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs+ −
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)+ −
val (_, prop') = LocalDefs.cert_def lthy prop+ −
val (_, newrhs) = Primitive_Defs.abs_def prop'+ −
+ −
val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy+ −
+ −
(* data storage *)+ −
fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}+ −
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)+ −
val lthy'' = Local_Theory.declaration true+ −
(fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'+ −
in+ −
((trm, thm), lthy'')+ −
end+ −
+ −
fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =+ −
let+ −
val lhs = Syntax.read_term lthy lhs_str+ −
val rhs = Syntax.read_term lthy rhs_str+ −
val lthy' = Variable.declare_term lhs lthy+ −
val lthy'' = Variable.declare_term rhs lthy'+ −
in+ −
quotient_def mx attr lhs rhs lthy'' |> snd+ −
end+ −
+ −
val _ = OuterKeyword.keyword "as";+ −
+ −
val quotdef_parser =+ −
(SpecParse.opt_thm_name ":" --+ −
OuterParse.term) --+ −
(OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --+ −
OuterParse.term)+ −
+ −
val _ = OuterSyntax.local_theory "quotient_definition"+ −
"definition for constants over the quotient type"+ −
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)+ −
+ −
end; (* structure *)+ −