# HG changeset patch # User haftmann # Date 1245591974 -7200 # Node ID 41788a3ffd6a70ca345a5a468a4bee9c48e13dd3 # Parent 052399f580cfe701625c16b8248aa61a9532c573# Parent 002da20f442e91b7654cf35080c7b717dfba253a merged diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Nominal/nominal.ML --- a/src/HOL/Nominal/nominal.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Nominal/nominal.ML Sun Jun 21 15:46:14 2009 +0200 @@ -6,7 +6,7 @@ signature NOMINAL = sig - val add_nominal_datatype : DatatypeAux.datatype_config -> string list -> + val add_nominal_datatype : Datatype.config -> string list -> (string list * bstring * mixfix * (bstring * string list * mixfix) list) list -> theory -> theory type descr @@ -2084,7 +2084,7 @@ val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args; val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in add_nominal_datatype DatatypeAux.default_datatype_config names specs end; + in add_nominal_datatype Datatype.default_config names specs end; val _ = OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 15:46:14 2009 +0200 @@ -102,7 +102,7 @@ fold_map (fn ak => fn thy => let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)]) val ({inject,case_thms,...},thy1) = Datatype.add_datatype - DatatypeAux.default_datatype_config [ak] [dt] thy + Datatype.default_config [ak] [dt] thy val inject_flat = flat inject val ak_type = Type (Sign.intern_type thy1 ak,[]) val ak_sign = Sign.intern_const thy1 ak diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/datatype_package/datatype.ML --- a/src/HOL/Tools/datatype_package/datatype.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype.ML Sun Jun 21 15:46:14 2009 +0200 @@ -6,26 +6,7 @@ signature DATATYPE = sig - type datatype_config = DatatypeAux.datatype_config - type datatype_info = DatatypeAux.datatype_info - type descr = DatatypeAux.descr - val get_datatypes : theory -> datatype_info Symtab.table - val get_datatype : theory -> string -> datatype_info option - val the_datatype : theory -> string -> datatype_info - val datatype_of_constr : theory -> string -> datatype_info option - val datatype_of_case : theory -> string -> datatype_info option - val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list - val the_datatype_descr : theory -> string list - -> descr * (string * sort) list * string list - * (string list * string list) * (typ list * typ list) - val get_datatype_constrs : theory -> string -> (string * typ) list option - val distinct_simproc : simproc - val make_case : Proof.context -> bool -> string list -> term -> - (term * term) list -> term * (term * (int * bool)) list - val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option - val read_typ: theory -> - (typ list * (string * sort) list) * string -> typ list * (string * sort) list - val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory + include DATATYPE_COMMON type rules = {distinct : thm list list, inject : thm list list, exhaustion : thm list, @@ -34,15 +15,31 @@ split_thms : (thm * thm) list, induction : thm, simps : thm list} - val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context) - -> string list option -> term list -> theory -> Proof.state; - val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state - val add_datatype : datatype_config -> string list -> (string list * binding * mixfix * + val add_datatype : config -> string list -> (string list * binding * mixfix * (binding * typ list * mixfix) list) list -> theory -> rules * theory - val add_datatype_cmd : string list -> (string list * binding * mixfix * - (binding * string list * mixfix) list) list -> theory -> rules * theory + val datatype_cmd : string list -> (string list * binding * mixfix * + (binding * string list * mixfix) list) list -> theory -> theory + val rep_datatype : config -> (rules -> Proof.context -> Proof.context) + -> string list option -> term list -> theory -> Proof.state + val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state + val get_datatypes : theory -> info Symtab.table + val get_datatype : theory -> string -> info option + val the_datatype : theory -> string -> info + val datatype_of_constr : theory -> string -> info option + val datatype_of_case : theory -> string -> info option + val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list + val the_datatype_descr : theory -> string list + -> descr * (string * sort) list * string list + * (string list * string list) * (typ list * typ list) + val get_datatype_constrs : theory -> string -> (string * typ) list option + val interpretation : (config -> string list -> theory -> theory) -> theory -> theory + val distinct_simproc : simproc + val make_case : Proof.context -> bool -> string list -> term -> + (term * term) list -> term * (term * (int * bool)) list + val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option + val read_typ: theory -> + (typ list * (string * sort) list) * string -> typ list * (string * sort) list val setup: theory -> theory - val print_datatypes : theory -> unit end; structure Datatype : DATATYPE = @@ -56,9 +53,9 @@ structure DatatypesData = TheoryDataFun ( type T = - {types: datatype_info Symtab.table, - constrs: datatype_info Symtab.table, - cases: datatype_info Symtab.table}; + {types: info Symtab.table, + constrs: info Symtab.table, + cases: info Symtab.table}; val empty = {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty}; @@ -75,14 +72,10 @@ val get_datatypes = #types o DatatypesData.get; val map_datatypes = DatatypesData.map; -fun print_datatypes thy = - Pretty.writeln (Pretty.strs ("datatypes:" :: - map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy)))); - (** theory information about datatypes **) -fun put_dt_infos (dt_infos : (string * datatype_info) list) = +fun put_dt_infos (dt_infos : (string * info) list) = map_datatypes (fn {types, constrs, cases} => {types = fold Symtab.update dt_infos types, constrs = fold Symtab.default (*conservative wrt. overloaded constructors*) @@ -207,7 +200,7 @@ let val inducts = ProjectRule.projections (ProofContext.init thy) induction; - fun named_rules (name, {index, exhaustion, ...}: datatype_info) = + fun named_rules (name, {index, exhaustion, ...}: info) = [((Binding.empty, nth inducts index), [Induct.induct_type name]), ((Binding.empty, exhaustion), [Induct.cases_type name])]; fun unnamed_rule i = @@ -351,13 +344,13 @@ simps : thm list} structure DatatypeInterpretation = InterpretationFun - (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =); + (type T = config * string list val eq: T * T -> bool = eq_snd op =); fun interpretation f = DatatypeInterpretation.interpretation (uncurry f); (******************* definitional introduction of datatypes *******************) -fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info +fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy = let val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names); @@ -414,7 +407,7 @@ (*********************** declare existing type as datatype *********************) -fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy = +fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy = let val ((_, [induct']), _) = Variable.importT_thms [induct] (Variable.thm_context induct); @@ -487,7 +480,7 @@ simps = simps}, thy11) end; -fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy = +fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy = let fun constr_of_term (Const (c, T)) = (c, T) | constr_of_term t = @@ -553,13 +546,13 @@ end; val rep_datatype = gen_rep_datatype Sign.cert_term; -val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I); +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I); (******************************** add datatype ********************************) -fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy = +fun gen_add_datatype prep_typ (config : config) new_type_names dts thy = let val _ = Theory.requires thy "Datatype" "datatype definitions"; @@ -627,12 +620,12 @@ val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts); in add_datatype_def - (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info + (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy end; val add_datatype = gen_add_datatype cert_typ; -val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config; +val datatype_cmd = snd ooo gen_add_datatype read_typ default_config; @@ -649,23 +642,29 @@ (* outer syntax *) -local structure P = OuterParse and K = OuterKeyword in +local -val datatype_decl = - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix -- - (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)); +structure P = OuterParse and K = OuterKeyword -fun mk_datatype args = +fun prep_datatype_decls args = let val names = map (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args; val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in snd o add_datatype_cmd names specs end; + in (names, specs) end; + +val parse_datatype_decl = + (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix -- + (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix))); + +val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls; + +in val _ = OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl - (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype)); + (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs))); val _ = OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/datatype_package/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 15:46:14 2009 +0200 @@ -14,24 +14,22 @@ signature DATATYPE_ABS_PROOFS = sig - type datatype_config = DatatypeAux.datatype_config - type descr = DatatypeAux.descr - type datatype_info = DatatypeAux.datatype_info - val prove_casedist_thms : datatype_config -> string list -> + include DATATYPE_COMMON + val prove_casedist_thms : config -> string list -> descr list -> (string * sort) list -> thm -> attribute list -> theory -> thm list * theory - val prove_primrec_thms : datatype_config -> string list -> + val prove_primrec_thms : config -> string list -> descr list -> (string * sort) list -> - datatype_info Symtab.table -> thm list list -> thm list list -> + info Symtab.table -> thm list list -> thm list list -> simpset -> thm -> theory -> (string list * thm list) * theory - val prove_case_thms : datatype_config -> string list -> + val prove_case_thms : config -> string list -> descr list -> (string * sort) list -> string list -> thm list -> theory -> (thm list list * string list) * theory - val prove_split_thms : datatype_config -> string list -> + val prove_split_thms : config -> string list -> descr list -> (string * sort) list -> thm list list -> thm list list -> thm list -> thm list list -> theory -> (thm * thm) list * theory - val prove_nchotomys : datatype_config -> string list -> descr list -> + val prove_nchotomys : config -> string list -> descr list -> (string * sort) list -> thm list -> theory -> thm list * theory val prove_weak_case_congs : string list -> descr list -> (string * sort) list -> theory -> thm list * theory @@ -47,7 +45,7 @@ (************************ case distinction theorems ***************************) -fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy = +fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy = let val _ = message config "Proving case distinction theorems ..."; @@ -89,8 +87,8 @@ (*************************** primrec combinators ******************************) -fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts - (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy = +fun prove_primrec_thms (config : config) new_type_names descr sorts + (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy = let val _ = message config "Constructing primrec combinators ..."; @@ -275,7 +273,7 @@ (***************************** case combinators *******************************) -fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy = +fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy = let val _ = message config "Proving characteristic theorems for case combinators ..."; @@ -349,7 +347,7 @@ (******************************* case splitting *******************************) -fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites +fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy = let val _ = message config "Proving equations for case splitting ..."; @@ -398,7 +396,7 @@ (************************* additional theorems for TFL ************************) -fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy = +fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy = let val _ = message config "Proving additional theorems for TFL ..."; diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/datatype_package/datatype_aux.ML --- a/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 15:46:14 2009 +0200 @@ -4,11 +4,23 @@ Auxiliary functions for defining datatypes. *) +signature DATATYPE_COMMON = +sig + type config + val default_config : config + datatype dtyp = + DtTFree of string + | DtType of string * (dtyp list) + | DtRec of int; + type descr + type info +end + signature DATATYPE_AUX = sig - type datatype_config - val default_datatype_config : datatype_config - val message : datatype_config -> string -> unit + include DATATYPE_COMMON + + val message : config -> string -> unit val add_path : bool -> string -> theory -> theory val parent_path : bool -> theory -> theory @@ -33,12 +45,6 @@ datatype simproc_dist = FewConstrs of thm list | ManyConstrs of thm * simpset; - datatype dtyp = - DtTFree of string - | DtType of string * (dtyp list) - | DtRec of int; - type descr - type datatype_info exception Datatype exception Datatype_Empty of string @@ -61,7 +67,7 @@ -> ((string * Term.typ list) * (string * 'a list) list) list val check_nonempty : descr list -> unit val unfold_datatypes : - theory -> descr -> (string * sort) list -> datatype_info Symtab.table -> + theory -> descr -> (string * sort) list -> info Symtab.table -> descr -> int -> descr list * int end; @@ -70,10 +76,10 @@ (* datatype option flags *) -type datatype_config = { strict: bool, flat_names: bool, quiet: bool }; -val default_datatype_config : datatype_config = +type config = { strict: bool, flat_names: bool, quiet: bool }; +val default_config : config = { strict = true, flat_names = false, quiet = false }; -fun message ({ quiet, ...} : datatype_config) s = +fun message ({ quiet, ...} : config) s = if quiet then () else writeln s; fun add_path flat_names s = if flat_names then I else Sign.add_path s; @@ -186,7 +192,7 @@ (* index, datatype name, type arguments, constructor name, types of constructor's arguments *) type descr = (int * (string * dtyp list * (string * dtyp list) list)) list; -type datatype_info = +type info = {index : int, alt_names : string list option, descr : descr, @@ -317,7 +323,7 @@ (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *) (* need to be unfolded *) -fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i = +fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i = let fun typ_error T msg = error ("Non-admissible type expression\n" ^ Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg); diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/datatype_package/datatype_case.ML --- a/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 15:46:14 2009 +0200 @@ -7,16 +7,16 @@ signature DATATYPE_CASE = sig - val make_case: (string -> DatatypeAux.datatype_info option) -> + val make_case: (string -> DatatypeAux.info option) -> Proof.context -> bool -> string list -> term -> (term * term) list -> term * (term * (int * bool)) list - val dest_case: (string -> DatatypeAux.datatype_info option) -> bool -> + val dest_case: (string -> DatatypeAux.info option) -> bool -> string list -> term -> (term * (term * term) list) option - val strip_case: (string -> DatatypeAux.datatype_info option) -> bool -> + val strip_case: (string -> DatatypeAux.info option) -> bool -> term -> (term * (term * term) list) option - val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option) + val case_tr: bool -> (theory -> string -> DatatypeAux.info option) -> Proof.context -> term list -> term - val case_tr': (theory -> string -> DatatypeAux.datatype_info option) -> + val case_tr': (theory -> string -> DatatypeAux.info option) -> string -> Proof.context -> term list -> term end; @@ -31,7 +31,7 @@ * Get information about datatypes *---------------------------------------------------------------------------*) -fun ty_info (tab : string -> DatatypeAux.datatype_info option) s = +fun ty_info (tab : string -> DatatypeAux.info option) s = case tab s of SOME {descr, case_name, index, sorts, ...} => let diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/datatype_package/datatype_codegen.ML --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 15:46:14 2009 +0200 @@ -6,7 +6,7 @@ signature DATATYPE_CODEGEN = sig - val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option + val find_shortest_path: Datatype.descr -> int -> (string * int) option val mk_eq_eqns: theory -> string -> (thm * bool) list val mk_case_cert: theory -> string -> thm val setup: theory -> theory @@ -17,7 +17,7 @@ (** find shortest path to constructor with no recursive arguments **) -fun find_nonempty (descr: DatatypeAux.descr) is i = +fun find_nonempty (descr: Datatype.descr) is i = let val (_, _, constrs) = the (AList.lookup (op =) descr i); fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i @@ -42,7 +42,7 @@ (* datatype definition *) -fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr = +fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr = let val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/datatype_package/datatype_realizer.ML --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 15:46:14 2009 +0200 @@ -7,7 +7,7 @@ signature DATATYPE_REALIZER = sig - val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory + val add_dt_realizers: Datatype.config -> string list -> theory -> theory val setup: theory -> theory end; @@ -38,7 +38,7 @@ fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT); -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy = +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy = let val recTs = get_rec_types descr sorts; val pnames = if length descr = 1 then ["P"] @@ -157,7 +157,7 @@ in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy = +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy = let val cert = cterm_of thy; val rT = TFree ("'P", HOLogic.typeS); diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/datatype_package/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 15:46:14 2009 +0200 @@ -11,12 +11,10 @@ signature DATATYPE_REP_PROOFS = sig - type datatype_config = DatatypeAux.datatype_config - type descr = DatatypeAux.descr - type datatype_info = DatatypeAux.datatype_info + include DATATYPE_COMMON val distinctness_limit : int Config.T val distinctness_limit_setup : theory -> theory - val representation_proofs : datatype_config -> datatype_info Symtab.table -> + val representation_proofs : config -> info Symtab.table -> string list -> descr list -> (string * sort) list -> (binding * mixfix) list -> (binding * mixfix) list list -> attribute -> theory -> (thm list list * thm list list * thm list list * @@ -43,12 +41,12 @@ val myinv_f_f = thm "myinv_f_f"; -fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = +fun exh_thm_of (dt_info : info Symtab.table) tname = #exhaustion (the (Symtab.lookup dt_info tname)); (******************************************************************************) -fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table) +fun representation_proofs (config : config) (dt_info : info Symtab.table) new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = let val Datatype_thy = ThyInfo.the_theory "Datatype" thy; diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/function_package/size.ML Sun Jun 21 15:46:14 2009 +0200 @@ -57,7 +57,7 @@ val app = curry (list_comb o swap); -fun prove_size_thms (info : datatype_info) new_type_names thy = +fun prove_size_thms (info : info) new_type_names thy = let val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info; val l = length new_type_names; diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/hologic.ML Sun Jun 21 15:46:14 2009 +0200 @@ -603,8 +603,11 @@ val typerepT = Type ("Typerep.typerep", []); -fun mk_typerep T = Const ("Typerep.typerep_class.typerep", - Term.itselfT T --> typerepT) $ Logic.mk_type T; +fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep", + literalT --> listT typerepT --> typerepT) $ mk_literal tyco + $ mk_list typerepT (map mk_typerep Ts) + | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep", + Term.itselfT T --> typerepT) $ Logic.mk_type T; val termT = Type ("Code_Eval.term", []); diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Sun Jun 21 15:46:14 2009 +0200 @@ -221,7 +221,7 @@ (* find datatypes which contain all datatypes in tnames' *) -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = [] +fun find_dts (dt_info : info Symtab.table) _ [] = [] | find_dts dt_info tnames' (tname::tnames) = (case Symtab.lookup dt_info tname of NONE => primrec_err (quote tname ^ " is not a datatype") @@ -230,7 +230,7 @@ (tname, dt)::(find_dts dt_info tnames' tnames) else find_dts dt_info tnames' tnames); -fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns = +fun prepare_induct ({descr, induction, ...}: info) rec_eqns = let fun constrs_of (_, (_, _, cs)) = map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs; diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/primrec.ML Sun Jun 21 15:46:14 2009 +0200 @@ -203,7 +203,7 @@ (* find datatypes which contain all datatypes in tnames' *) -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = [] +fun find_dts (dt_info : info Symtab.table) _ [] = [] | find_dts dt_info tnames' (tname::tnames) = (case Symtab.lookup dt_info tname of NONE => primrec_error (quote tname ^ " is not a datatype") diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 15:46:14 2009 +0200 @@ -12,10 +12,10 @@ -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed val ensure_random_typecopy: string -> theory -> theory val random_aux_specification: string -> term list -> local_theory -> local_theory - val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list + val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list -> string list -> string list * string list -> typ list * typ list -> string * (term list * (term * term) list) - val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory + val ensure_random_datatype: Datatype.config -> string list -> theory -> theory val eval_ref: (unit -> int -> seed -> term list option * seed) option ref val setup: theory -> theory end; diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/refute.ML Sun Jun 21 15:46:14 2009 +0200 @@ -73,7 +73,7 @@ val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term val string_of_typ : Term.typ -> string val typ_of_dtyp : - DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp + Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp -> Term.typ end; (* signature REFUTE *) @@ -411,15 +411,6 @@ (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) -(* ------------------------------------------------------------------------- *) -(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *) -(* ('Term.typ'), given type parameters for the data type's type *) -(* arguments *) -(* ------------------------------------------------------------------------- *) - - (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> - DatatypeAux.dtyp -> Term.typ *) - fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = (* replace a 'DtTFree' variable by the associated type *) the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a)) @@ -1660,10 +1651,6 @@ (* their arguments) of the size of the argument types *) (* ------------------------------------------------------------------------- *) - (* theory -> (Term.typ * int) list -> DatatypeAux.descr -> - (DatatypeAux.dtyp * Term.typ) list -> - (string * DatatypeAux.dtyp list) list -> int *) - fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = sum (map (fn (_, dtyps) => product (map (size_of_type thy (typ_sizes, []) o @@ -2144,7 +2131,6 @@ (* decrement depth for the IDT 'T' *) val typs' = (case AList.lookup (op =) typs T of NONE => typs | SOME n => AList.update (op =) (T, n-1) typs) - (* Term.term list -> DatatypeAux.dtyp list -> Term.term list *) fun constructor_terms terms [] = terms | constructor_terms terms (d::ds) = let @@ -2241,7 +2227,6 @@ else () (* returns an interpretation where everything is mapped to *) (* an "undefined" element of the datatype *) - (* DatatypeAux.dtyp list -> interpretation *) fun make_undef [] = Leaf (replicate total False) | make_undef (d::ds) = @@ -2253,7 +2238,6 @@ Node (replicate size (make_undef ds)) end (* returns the interpretation for a constructor *) - (* int * DatatypeAux.dtyp list -> int * interpretation *) fun make_constr (offset, []) = if offset - (DatatypeAux.dtyp * Term.typ) list -> - (DatatypeAux.dtyp * Term.typ) list *) fun rec_typ_assoc acc [] = acc | rec_typ_assoc acc ((d, T)::xs) = @@ -2458,7 +2439,6 @@ else raise REFUTE ("IDT_recursion_interpreter", "different type associations for the same dtyp")) - (* (DatatypeAux.dtyp * Term.typ) list *) val typ_assoc = filter (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false) (rec_typ_assoc [] @@ -2613,7 +2593,6 @@ val rec_dtyps_args = List.filter (DatatypeAux.is_rec_type o fst) (dtyps ~~ args) (* map those indices to interpretations *) - (* (DatatypeAux.dtyp * interpretation) list *) val rec_dtyps_intrs = map (fn (dtyp, arg) => let val dT = typ_of_dtyp descr typ_assoc dtyp @@ -2625,8 +2604,6 @@ (* takes the dtyp and interpretation of an element, *) (* and computes the interpretation for the *) (* corresponding recursive argument *) - (* DatatypeAux.dtyp -> interpretation -> - interpretation *) fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) = (* recursive argument is "rec_i params elem" *) compute_array_entry i (find_index_eq True xs) @@ -3252,8 +3229,6 @@ (* constructor generates the datatype's element that is given by *) (* 'element', returns the constructor (as a term) as well as the *) (* indices of the arguments *) - (* string * DatatypeAux.dtyp list -> - (Term.term * int list) option *) fun get_constr_args (cname, cargs) = let val cTerm = Const (cname, @@ -3281,7 +3256,6 @@ in Option.map (fn args => (cTerm, cargs, args)) (get_args iC) end - (* Term.term * DatatypeAux.dtyp list * int list *) val (cTerm, cargs, args) = (* we could speed things up by computing the correct *) (* constructor directly (rather than testing all *) diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/typecopy.ML --- a/src/HOL/Tools/typecopy.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/typecopy.ML Sun Jun 21 15:46:14 2009 +0200 @@ -6,21 +6,13 @@ signature TYPECOPY = sig - type info = { - vs: (string * sort) list, - constr: string, - typ: typ, - inject: thm, - proj: string * typ, - proj_def: thm - } + type info = { vs: (string * sort) list, constr: string, typ: typ, + inject: thm, proj: string * typ, proj_def: thm } val typecopy: binding * string list -> typ -> (binding * binding) option -> theory -> (string * info) * theory - val get_typecopies: theory -> string list val get_info: theory -> string -> info option val interpretation: (string -> theory -> theory) -> theory -> theory val add_default_code: string -> theory -> theory - val print_typecopies: theory -> unit val setup: theory -> theory end; @@ -47,22 +39,6 @@ fun merge _ = Symtab.merge (K true); ); -fun print_typecopies thy = - let - val tab = TypecopyData.get thy; - fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) = - (Pretty.block o Pretty.breaks) [ - Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)), - Pretty.str "=", - (Pretty.str o Sign.extern_const thy) constr, - Syntax.pretty_typ_global thy typ, - Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]]; - in - (Pretty.writeln o Pretty.block o Pretty.fbreaks) - (Pretty.str "type copies:" :: map mk (Symtab.dest tab)) - end; - -val get_typecopies = Symtab.keys o TypecopyData.get; val get_info = Symtab.lookup o TypecopyData.get; @@ -72,7 +48,7 @@ val interpretation = TypecopyInterpretation.interpretation; -(* declaring typecopies *) +(* introducing typecopies *) fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy = let diff -r 052399f580cf -r 41788a3ffd6a src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/Tools/typedef.ML Sun Jun 21 15:46:14 2009 +0200 @@ -12,13 +12,13 @@ type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm} - val get_info: theory -> string -> info option val add_typedef: bool -> binding option -> binding * string list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory val typedef: (bool * binding) * (binding * string list * mixfix) * term * (binding * binding) option -> theory -> Proof.state val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string * (binding * binding) option -> theory -> Proof.state + val get_info: theory -> string -> info option val interpretation: (string -> theory -> theory) -> theory -> theory val setup: theory -> theory end; diff -r 052399f580cf -r 41788a3ffd6a src/HOL/ex/Codegenerator_Candidates.thy --- a/src/HOL/ex/Codegenerator_Candidates.thy Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Sun Jun 21 15:46:14 2009 +0200 @@ -25,20 +25,6 @@ "~~/src/HOL/ex/Records" begin -(*temporary Haskell workaround*) -declare typerep_fun_def [code inline] -declare typerep_prod_def [code inline] -declare typerep_sum_def [code inline] -declare typerep_cpoint_ext_type_def [code inline] -declare typerep_itself_def [code inline] -declare typerep_list_def [code inline] -declare typerep_option_def [code inline] -declare typerep_point_ext_type_def [code inline] -declare typerep_point'_ext_type_def [code inline] -declare typerep_point''_ext_type_def [code inline] -declare typerep_pol_def [code inline] -declare typerep_polex_def [code inline] - (*avoid popular infixes*) code_reserved SML union inter upto diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOLCF/Fixrec.thy Sun Jun 21 15:46:14 2009 +0200 @@ -6,7 +6,7 @@ theory Fixrec imports Sprod Ssum Up One Tr Fix -uses ("Tools/fixrec_package.ML") +uses ("Tools/fixrec.ML") begin subsection {* Maybe monad type *} @@ -599,12 +599,12 @@ subsection {* Initializing the fixrec package *} -use "Tools/fixrec_package.ML" +use "Tools/fixrec.ML" -setup {* FixrecPackage.setup *} +setup {* Fixrec.setup *} setup {* - FixrecPackage.add_matchers + Fixrec.add_matchers [ (@{const_name up}, @{const_name match_up}), (@{const_name sinl}, @{const_name match_sinl}), (@{const_name sinr}, @{const_name match_sinr}), diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 15:46:14 2009 +0200 @@ -6,7 +6,7 @@ theory Abstraction imports LiveIOA -uses ("ioa_package.ML") +uses ("ioa.ML") begin defaultsort type @@ -613,6 +613,6 @@ method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} "" -use "ioa_package.ML" +use "ioa.ML" end diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/IOA/meta_theory/ioa.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/ioa.ML Sun Jun 21 15:46:14 2009 +0200 @@ -0,0 +1,536 @@ +(* Title: HOLCF/IOA/meta_theory/ioa.ML + Author: Tobias Hamberger, TU Muenchen +*) + +signature IOA = +sig + val add_ioa: string -> string + -> (string) list -> (string) list -> (string) list + -> (string * string) list -> string + -> (string * string * (string * string)list) list + -> theory -> theory + val add_composition : string -> (string)list -> theory -> theory + val add_hiding : string -> string -> (string)list -> theory -> theory + val add_restriction : string -> string -> (string)list -> theory -> theory + val add_rename : string -> string -> string -> theory -> theory +end; + +structure Ioa: IOA = +struct + +val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global; +val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global; + +exception malformed; + +(* stripping quotes *) +fun strip [] = [] | +strip ("\""::r) = strip r | +strip (a::r) = a :: (strip r); +fun strip_quote s = implode(strip(explode(s))); + +(* used by *_of_varlist *) +fun extract_first (a,b) = strip_quote a; +fun extract_second (a,b) = strip_quote b; +(* following functions producing sth from a varlist *) +fun comma_list_of_varlist [] = "" | +comma_list_of_varlist [a] = extract_first a | +comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r); +fun primed_comma_list_of_varlist [] = "" | +primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" | +primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^ + (primed_comma_list_of_varlist r); +fun type_product_of_varlist [] = "" | +type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | +type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r; + +(* listing a list *) +fun list_elements_of [] = "" | +list_elements_of (a::r) = a ^ " " ^ (list_elements_of r); + +(* extracting type parameters from a type list *) +(* fun param_tupel thy [] res = res | +param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res | +param_tupel thy ((TFree(a,_))::r) res = +if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) | +param_tupel thy (a::r) res = +error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a)); +*) + +(* used by constr_list *) +fun extract_constrs thy [] = [] | +extract_constrs thy (a::r) = +let +fun delete_bold [] = [] +| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs)) + then (let val (_::_::_::s) = xs in delete_bold s end) + else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) + then (let val (_::_::_::s) = xs in delete_bold s end) + else (x::delete_bold xs)); +fun delete_bold_string s = implode(delete_bold(explode s)); +(* from a constructor term in *.induct (with quantifiers, +"Trueprop" and ?P stripped away) delivers the head *) +fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r | +extract_hd (Const("Trueprop",_) $ r) = extract_hd r | +extract_hd (Var(_,_) $ r) = extract_hd r | +extract_hd (a $ b) = extract_hd a | +extract_hd (Const(s,_)) = s | +extract_hd _ = raise malformed; +(* delivers constructor term string from a prem of *.induct *) +fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))| +extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | +extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) | +extract_constr _ _ = raise malformed; +in +(extract_hd a,extract_constr thy a) :: (extract_constrs thy r) +end; + +(* delivering list of constructor terms of a datatype *) +fun constr_list thy atyp = +let +fun act_name thy (Type(s,_)) = s | +act_name _ s = +error("malformed action type: " ^ (string_of_typ thy s)); +fun afpl ("." :: a) = [] | +afpl [] = [] | +afpl (a::r) = a :: (afpl r); +fun unqualify s = implode(rev(afpl(rev(explode s)))); +val q_atypstr = act_name thy atyp; +val uq_atypstr = unqualify q_atypstr; +val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct")); +in +extract_constrs thy prem +handle malformed => +error("malformed theorem : " ^ uq_atypstr ^ ".induct") +end; + +fun check_for_constr thy atyp (a $ b) = +let +fun all_free (Free(_,_)) = true | +all_free (a $ b) = if (all_free a) then (all_free b) else false | +all_free _ = false; +in +if (all_free b) then (check_for_constr thy atyp a) else false +end | +check_for_constr thy atyp (Const(a,_)) = +let +val cl = constr_list thy atyp; +fun fstmem a [] = false | +fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r) +in +if (fstmem a cl) then true else false +end | +check_for_constr _ _ _ = false; + +(* delivering the free variables of a constructor term *) +fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) | +free_vars_of (Const(_,_)) = [] | +free_vars_of (Free(a,_)) = [a] | +free_vars_of _ = raise malformed; + +(* making a constructor set from a constructor term (of signature) *) +fun constr_set_string thy atyp ctstr = +let +val trm = OldGoals.simple_read_term thy atyp ctstr; +val l = free_vars_of trm +in +if (check_for_constr thy atyp trm) then +(if (l=[]) then ("{" ^ ctstr ^ "}") +else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") +else (raise malformed) +handle malformed => +error("malformed action term: " ^ (string_of_term thy trm)) +end; + +(* extracting constructor heads *) +fun constructor_head thy atypstr s = +let +fun hd_of (Const(a,_)) = a | +hd_of (t $ _) = hd_of t | +hd_of _ = raise malformed; +val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; +in +hd_of trm handle malformed => +error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) +end; +fun constructor_head_list _ _ [] = [] | +constructor_head_list thy atypstr (a::r) = + (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r); + +(* producing an action set *) +(*FIXME*) +fun action_set_string thy atyp [] = "Set.empty" | +action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) | +action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^ + " Un " ^ (action_set_string thy atyp r); + +(* used by extend *) +fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" | +pstr s ((a,b)::r) = +if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r); +fun poststring [] l = "" | +poststring [(a,b)] l = pstr a l | +poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l); + +(* extends a (action string,condition,assignlist) tupel by a +(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list +(where bool indicates whether there is a precondition *) +fun extend thy atyp statetupel (actstr,r,[]) = +let +val trm = OldGoals.simple_read_term thy atyp actstr; +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r; +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true +in +if (check_for_constr thy atyp trm) +then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) +else +error("transition " ^ actstr ^ " is not a pure constructor term") +end | +extend thy atyp statetupel (actstr,r,(a,b)::c) = +let +fun pseudo_poststring [] = "" | +pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | +pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); +val trm = OldGoals.simple_read_term thy atyp actstr; +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r; +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true +in +if (check_for_constr thy atyp trm) then +(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) +(* the case with transrel *) + else + (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), + "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) +else +error("transition " ^ actstr ^ " is not a pure constructor term") +end; +(* used by make_alt_string *) +fun extended_list _ _ _ [] = [] | +extended_list thy atyp statetupel (a::r) = + (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); + +(* used by write_alts *) +fun write_alt thy (chead,tr) inp out int [] = +if (chead mem inp) then +( +error("Input action " ^ tr ^ " was not specified") +) else ( +if (chead mem (out@int)) then +(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else (); +(tr ^ " => False",tr ^ " => False")) | +write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = +let +fun hd_of (Const(a,_)) = a | +hd_of (t $ _) = hd_of t | +hd_of _ = raise malformed; +fun occurs_again c [] = false | +occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); +in +if (chead=(hd_of a)) then +(if ((chead mem inp) andalso e) then ( +error("Input action " ^ b ^ " has a precondition") +) else (if (chead mem (inp@out@int)) then + (if (occurs_again chead r) then ( +error("Two specifications for action: " ^ b) + ) else (b ^ " => " ^ c,b ^ " => " ^ d)) + else ( +error("Action " ^ b ^ " is not in automaton signature") +))) else (write_alt thy (chead,ctrm) inp out int r) +handle malformed => +error ("malformed action term: " ^ (string_of_term thy a)) +end; + +(* used by make_alt_string *) +fun write_alts thy (a,b) inp out int [] ttr = (a,b) | +write_alts thy (a,b) inp out int [c] ttr = +let +val wa = write_alt thy c inp out int ttr +in + (a ^ (fst wa),b ^ (snd wa)) +end | +write_alts thy (a,b) inp out int (c::r) ttr = +let +val wa = write_alt thy c inp out int ttr +in + write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr +end; + +fun make_alt_string thy inp out int atyp statetupel trans = +let +val cl = constr_list thy atyp; +val ttr = extended_list thy atyp statetupel trans; +in +write_alts thy ("","") inp out int cl ttr +end; + +(* used in add_ioa *) +fun check_free_primed (Free(a,_)) = +let +val (f::r) = rev(explode a) +in +if (f="'") then [a] else [] +end | +check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) | +check_free_primed (Abs(_,_,t)) = check_free_primed t | +check_free_primed _ = []; + +fun overlap [] _ = true | +overlap (a::r) l = if (a mem l) then ( +error("Two occurences of action " ^ a ^ " in automaton signature") +) else (overlap r l); + +(* delivering some types of an automaton *) +fun aut_type_of thy aut_name = +let +fun left_of (( _ $ left) $ _) = left | +left_of _ = raise malformed; +val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def")); +in +(#T(rep_cterm(cterm_of thy (left_of aut_def)))) +handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") +end; + +fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp | +act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ +(string_of_typ thy t)); +fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp | +st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ +(string_of_typ thy t)); + +fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | +comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | +comp_st_type_of _ _ = error "empty automaton list"; + +(* checking consistency of action types (for composition) *) +fun check_ac thy (a::r) = +let +fun ch_f_a thy acttyp [] = acttyp | +ch_f_a thy acttyp (a::r) = +let +val auttyp = aut_type_of thy a; +val ac = (act_type_of thy auttyp); +in +if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A") +end; +val auttyp = aut_type_of thy a; +val acttyp = (act_type_of thy auttyp); +in +ch_f_a thy acttyp r +end | +check_ac _ [] = error "empty automaton list"; + +fun clist [] = "" | +clist [a] = a | +clist (a::r) = a ^ " || " ^ (clist r); + +val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name)); + + +(* add_ioa *) + +fun add_ioa automaton_name action_type inp out int statetupel ini trans thy = +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); +let +val state_type_string = type_product_of_varlist(statetupel); +val styp = Syntax.read_typ_global thy state_type_string; +val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")"; +val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")"; +val atyp = Syntax.read_typ_global thy action_type; +val inp_set_string = action_set_string thy atyp inp; +val out_set_string = action_set_string thy atyp out; +val int_set_string = action_set_string thy atyp int; +val inp_head_list = constructor_head_list thy action_type inp; +val out_head_list = constructor_head_list thy action_type out; +val int_head_list = constructor_head_list thy action_type int; +val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); +val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list + atyp statetupel trans; +val thy2 = (thy +|> Sign.add_consts +[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn), +(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn), +(Binding.name (automaton_name ^ "_trans"), + "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), +(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] +|> add_defs +[(automaton_name ^ "_initial_def", +automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), +(automaton_name ^ "_asig_def", +automaton_name ^ "_asig == (" ^ + inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), +(automaton_name ^ "_trans_def", +automaton_name ^ "_trans == {(" ^ + state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^ +"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), +(automaton_name ^ "_def", +automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ +"_initial, " ^ automaton_name ^ "_trans,{},{})") +]) +val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[])) +( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string)))) +in +( +if (chk_prime_list = []) then thy2 +else ( +error("Precondition or assignment terms in postconditions contain following primed variables:\n" + ^ (list_elements_of chk_prime_list))) +) +end) + +fun add_composition automaton_name aut_list thy = +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); +let +val acttyp = check_ac thy aut_list; +val st_typ = comp_st_type_of thy aut_list; +val comp_list = clist aut_list; +in +thy +|> Sign.add_consts_i +[(Binding.name automaton_name, +Type("*", +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), + Type("*",[Type("set",[st_typ]), + Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), + Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) +,NoSyn)] +|> add_defs +[(automaton_name ^ "_def", +automaton_name ^ " == " ^ comp_list)] +end) + +fun add_restriction automaton_name aut_source actlist thy = +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); +let +val auttyp = aut_type_of thy aut_source; +val acttyp = act_type_of thy auttyp; +val rest_set = action_set_string thy acttyp actlist +in +thy +|> Sign.add_consts_i +[(Binding.name automaton_name, auttyp,NoSyn)] +|> add_defs +[(automaton_name ^ "_def", +automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] +end) +fun add_hiding automaton_name aut_source actlist thy = +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); +let +val auttyp = aut_type_of thy aut_source; +val acttyp = act_type_of thy auttyp; +val hid_set = action_set_string thy acttyp actlist +in +thy +|> Sign.add_consts_i +[(Binding.name automaton_name, auttyp,NoSyn)] +|> add_defs +[(automaton_name ^ "_def", +automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] +end) + +fun ren_act_type_of thy funct = + (case Term.fastype_of (Syntax.read_term_global thy funct) of + Type ("fun", [a, b]) => a + | _ => error "could not extract argument type of renaming function term"); + +fun add_rename automaton_name aut_source fun_name thy = +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); +let +val auttyp = aut_type_of thy aut_source; +val st_typ = st_type_of thy auttyp; +val acttyp = ren_act_type_of thy fun_name +in +thy +|> Sign.add_consts_i +[(Binding.name automaton_name, +Type("*", +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), + Type("*",[Type("set",[st_typ]), + Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), + Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) +,NoSyn)] +|> add_defs +[(automaton_name ^ "_def", +automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] +end) + + +(** outer syntax **) + +(* prepare results *) + +(*encoding transition specifications with a element of ParseTrans*) +datatype ParseTrans = Rel of string | PP of string*(string*string)list; +fun mk_trans_of_rel s = Rel(s); +fun mk_trans_of_prepost (s,l) = PP(s,l); + +fun trans_of (a, Rel b) = (a, b, [("", "")]) + | trans_of (a, PP (b, l)) = (a, b, l); + + +fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = + add_ioa aut action_type inp out int states initial (map trans_of trans); + +fun mk_composition_decl (aut, autlist) = + add_composition aut autlist; + +fun mk_hiding_decl (aut, (actlist, source_aut)) = + add_hiding aut source_aut actlist; + +fun mk_restriction_decl (aut, (source_aut, actlist)) = + add_restriction aut source_aut actlist; + +fun mk_rename_decl (aut, (source_aut, rename_f)) = + add_rename aut source_aut rename_f; + + +(* outer syntax *) + +local structure P = OuterParse and K = OuterKeyword in + +val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs", + "outputs", "internals", "states", "initially", "transitions", "pre", + "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", + "rename"]; + +val actionlist = P.list1 P.term; +val inputslist = P.$$$ "inputs" |-- P.!!! actionlist; +val outputslist = P.$$$ "outputs" |-- P.!!! actionlist; +val internalslist = P.$$$ "internals" |-- P.!!! actionlist; +val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ)); +val initial = P.$$$ "initially" |-- P.!!! P.term; +val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term); +val pre = P.$$$ "pre" |-- P.!!! P.term; +val post = P.$$$ "post" |-- P.!!! assign_list; +val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; +val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; +val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel; +val transition = P.term -- (transrel || pre1 || post1); +val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition); + +val ioa_decl = + (P.name -- (P.$$$ "=" |-- + (P.$$$ "signature" |-- + P.!!! (P.$$$ "actions" |-- + (P.typ -- + (Scan.optional inputslist []) -- + (Scan.optional outputslist []) -- + (Scan.optional internalslist []) -- + stateslist -- + (Scan.optional initial "True") -- + translist))))) >> mk_ioa_decl || + (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name)))) + >> mk_composition_decl || + (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- + P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl || + (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- + P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl || + (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term)))))) + >> mk_rename_decl; + +val _ = + OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl + (ioa_decl >> Toplevel.theory); + +end; + +end; diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 11:50:26 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,537 +0,0 @@ -(* Title: HOLCF/IOA/meta_theory/ioa_package.ML - ID: $Id$ - Author: Tobias Hamberger, TU Muenchen -*) - -signature IOA_PACKAGE = -sig - val add_ioa: string -> string - -> (string) list -> (string) list -> (string) list - -> (string * string) list -> string - -> (string * string * (string * string)list) list - -> theory -> theory - val add_composition : string -> (string)list -> theory -> theory - val add_hiding : string -> string -> (string)list -> theory -> theory - val add_restriction : string -> string -> (string)list -> theory -> theory - val add_rename : string -> string -> string -> theory -> theory -end; - -structure IoaPackage: IOA_PACKAGE = -struct - -val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global; -val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global; - -exception malformed; - -(* stripping quotes *) -fun strip [] = [] | -strip ("\""::r) = strip r | -strip (a::r) = a :: (strip r); -fun strip_quote s = implode(strip(explode(s))); - -(* used by *_of_varlist *) -fun extract_first (a,b) = strip_quote a; -fun extract_second (a,b) = strip_quote b; -(* following functions producing sth from a varlist *) -fun comma_list_of_varlist [] = "" | -comma_list_of_varlist [a] = extract_first a | -comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r); -fun primed_comma_list_of_varlist [] = "" | -primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" | -primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^ - (primed_comma_list_of_varlist r); -fun type_product_of_varlist [] = "" | -type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | -type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r; - -(* listing a list *) -fun list_elements_of [] = "" | -list_elements_of (a::r) = a ^ " " ^ (list_elements_of r); - -(* extracting type parameters from a type list *) -(* fun param_tupel thy [] res = res | -param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res | -param_tupel thy ((TFree(a,_))::r) res = -if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) | -param_tupel thy (a::r) res = -error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a)); -*) - -(* used by constr_list *) -fun extract_constrs thy [] = [] | -extract_constrs thy (a::r) = -let -fun delete_bold [] = [] -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs)) - then (let val (_::_::_::s) = xs in delete_bold s end) - else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) - then (let val (_::_::_::s) = xs in delete_bold s end) - else (x::delete_bold xs)); -fun delete_bold_string s = implode(delete_bold(explode s)); -(* from a constructor term in *.induct (with quantifiers, -"Trueprop" and ?P stripped away) delivers the head *) -fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r | -extract_hd (Const("Trueprop",_) $ r) = extract_hd r | -extract_hd (Var(_,_) $ r) = extract_hd r | -extract_hd (a $ b) = extract_hd a | -extract_hd (Const(s,_)) = s | -extract_hd _ = raise malformed; -(* delivers constructor term string from a prem of *.induct *) -fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))| -extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | -extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) | -extract_constr _ _ = raise malformed; -in -(extract_hd a,extract_constr thy a) :: (extract_constrs thy r) -end; - -(* delivering list of constructor terms of a datatype *) -fun constr_list thy atyp = -let -fun act_name thy (Type(s,_)) = s | -act_name _ s = -error("malformed action type: " ^ (string_of_typ thy s)); -fun afpl ("." :: a) = [] | -afpl [] = [] | -afpl (a::r) = a :: (afpl r); -fun unqualify s = implode(rev(afpl(rev(explode s)))); -val q_atypstr = act_name thy atyp; -val uq_atypstr = unqualify q_atypstr; -val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct")); -in -extract_constrs thy prem -handle malformed => -error("malformed theorem : " ^ uq_atypstr ^ ".induct") -end; - -fun check_for_constr thy atyp (a $ b) = -let -fun all_free (Free(_,_)) = true | -all_free (a $ b) = if (all_free a) then (all_free b) else false | -all_free _ = false; -in -if (all_free b) then (check_for_constr thy atyp a) else false -end | -check_for_constr thy atyp (Const(a,_)) = -let -val cl = constr_list thy atyp; -fun fstmem a [] = false | -fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r) -in -if (fstmem a cl) then true else false -end | -check_for_constr _ _ _ = false; - -(* delivering the free variables of a constructor term *) -fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) | -free_vars_of (Const(_,_)) = [] | -free_vars_of (Free(a,_)) = [a] | -free_vars_of _ = raise malformed; - -(* making a constructor set from a constructor term (of signature) *) -fun constr_set_string thy atyp ctstr = -let -val trm = OldGoals.simple_read_term thy atyp ctstr; -val l = free_vars_of trm -in -if (check_for_constr thy atyp trm) then -(if (l=[]) then ("{" ^ ctstr ^ "}") -else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") -else (raise malformed) -handle malformed => -error("malformed action term: " ^ (string_of_term thy trm)) -end; - -(* extracting constructor heads *) -fun constructor_head thy atypstr s = -let -fun hd_of (Const(a,_)) = a | -hd_of (t $ _) = hd_of t | -hd_of _ = raise malformed; -val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; -in -hd_of trm handle malformed => -error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) -end; -fun constructor_head_list _ _ [] = [] | -constructor_head_list thy atypstr (a::r) = - (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r); - -(* producing an action set *) -(*FIXME*) -fun action_set_string thy atyp [] = "Set.empty" | -action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) | -action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^ - " Un " ^ (action_set_string thy atyp r); - -(* used by extend *) -fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" | -pstr s ((a,b)::r) = -if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r); -fun poststring [] l = "" | -poststring [(a,b)] l = pstr a l | -poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l); - -(* extends a (action string,condition,assignlist) tupel by a -(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list -(where bool indicates whether there is a precondition *) -fun extend thy atyp statetupel (actstr,r,[]) = -let -val trm = OldGoals.simple_read_term thy atyp actstr; -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r; -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true -in -if (check_for_constr thy atyp trm) -then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) -else -error("transition " ^ actstr ^ " is not a pure constructor term") -end | -extend thy atyp statetupel (actstr,r,(a,b)::c) = -let -fun pseudo_poststring [] = "" | -pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | -pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); -val trm = OldGoals.simple_read_term thy atyp actstr; -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r; -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true -in -if (check_for_constr thy atyp trm) then -(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) -(* the case with transrel *) - else - (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), - "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) -else -error("transition " ^ actstr ^ " is not a pure constructor term") -end; -(* used by make_alt_string *) -fun extended_list _ _ _ [] = [] | -extended_list thy atyp statetupel (a::r) = - (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); - -(* used by write_alts *) -fun write_alt thy (chead,tr) inp out int [] = -if (chead mem inp) then -( -error("Input action " ^ tr ^ " was not specified") -) else ( -if (chead mem (out@int)) then -(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else (); -(tr ^ " => False",tr ^ " => False")) | -write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = -let -fun hd_of (Const(a,_)) = a | -hd_of (t $ _) = hd_of t | -hd_of _ = raise malformed; -fun occurs_again c [] = false | -occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); -in -if (chead=(hd_of a)) then -(if ((chead mem inp) andalso e) then ( -error("Input action " ^ b ^ " has a precondition") -) else (if (chead mem (inp@out@int)) then - (if (occurs_again chead r) then ( -error("Two specifications for action: " ^ b) - ) else (b ^ " => " ^ c,b ^ " => " ^ d)) - else ( -error("Action " ^ b ^ " is not in automaton signature") -))) else (write_alt thy (chead,ctrm) inp out int r) -handle malformed => -error ("malformed action term: " ^ (string_of_term thy a)) -end; - -(* used by make_alt_string *) -fun write_alts thy (a,b) inp out int [] ttr = (a,b) | -write_alts thy (a,b) inp out int [c] ttr = -let -val wa = write_alt thy c inp out int ttr -in - (a ^ (fst wa),b ^ (snd wa)) -end | -write_alts thy (a,b) inp out int (c::r) ttr = -let -val wa = write_alt thy c inp out int ttr -in - write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr -end; - -fun make_alt_string thy inp out int atyp statetupel trans = -let -val cl = constr_list thy atyp; -val ttr = extended_list thy atyp statetupel trans; -in -write_alts thy ("","") inp out int cl ttr -end; - -(* used in add_ioa *) -fun check_free_primed (Free(a,_)) = -let -val (f::r) = rev(explode a) -in -if (f="'") then [a] else [] -end | -check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) | -check_free_primed (Abs(_,_,t)) = check_free_primed t | -check_free_primed _ = []; - -fun overlap [] _ = true | -overlap (a::r) l = if (a mem l) then ( -error("Two occurences of action " ^ a ^ " in automaton signature") -) else (overlap r l); - -(* delivering some types of an automaton *) -fun aut_type_of thy aut_name = -let -fun left_of (( _ $ left) $ _) = left | -left_of _ = raise malformed; -val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def")); -in -(#T(rep_cterm(cterm_of thy (left_of aut_def)))) -handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") -end; - -fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp | -act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ -(string_of_typ thy t)); -fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp | -st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ -(string_of_typ thy t)); - -fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | -comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | -comp_st_type_of _ _ = error "empty automaton list"; - -(* checking consistency of action types (for composition) *) -fun check_ac thy (a::r) = -let -fun ch_f_a thy acttyp [] = acttyp | -ch_f_a thy acttyp (a::r) = -let -val auttyp = aut_type_of thy a; -val ac = (act_type_of thy auttyp); -in -if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A") -end; -val auttyp = aut_type_of thy a; -val acttyp = (act_type_of thy auttyp); -in -ch_f_a thy acttyp r -end | -check_ac _ [] = error "empty automaton list"; - -fun clist [] = "" | -clist [a] = a | -clist (a::r) = a ^ " || " ^ (clist r); - -val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name)); - - -(* add_ioa *) - -fun add_ioa automaton_name action_type inp out int statetupel ini trans thy = -(writeln("Constructing automaton " ^ automaton_name ^ " ..."); -let -val state_type_string = type_product_of_varlist(statetupel); -val styp = Syntax.read_typ_global thy state_type_string; -val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")"; -val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")"; -val atyp = Syntax.read_typ_global thy action_type; -val inp_set_string = action_set_string thy atyp inp; -val out_set_string = action_set_string thy atyp out; -val int_set_string = action_set_string thy atyp int; -val inp_head_list = constructor_head_list thy action_type inp; -val out_head_list = constructor_head_list thy action_type out; -val int_head_list = constructor_head_list thy action_type int; -val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); -val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list - atyp statetupel trans; -val thy2 = (thy -|> Sign.add_consts -[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn), -(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn), -(Binding.name (automaton_name ^ "_trans"), - "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), -(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] -|> add_defs -[(automaton_name ^ "_initial_def", -automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), -(automaton_name ^ "_asig_def", -automaton_name ^ "_asig == (" ^ - inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), -(automaton_name ^ "_trans_def", -automaton_name ^ "_trans == {(" ^ - state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^ -"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), -(automaton_name ^ "_def", -automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ -"_initial, " ^ automaton_name ^ "_trans,{},{})") -]) -val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[])) -( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string)))) -in -( -if (chk_prime_list = []) then thy2 -else ( -error("Precondition or assignment terms in postconditions contain following primed variables:\n" - ^ (list_elements_of chk_prime_list))) -) -end) - -fun add_composition automaton_name aut_list thy = -(writeln("Constructing automaton " ^ automaton_name ^ " ..."); -let -val acttyp = check_ac thy aut_list; -val st_typ = comp_st_type_of thy aut_list; -val comp_list = clist aut_list; -in -thy -|> Sign.add_consts_i -[(Binding.name automaton_name, -Type("*", -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), - Type("*",[Type("set",[st_typ]), - Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), - Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) -,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == " ^ comp_list)] -end) - -fun add_restriction automaton_name aut_source actlist thy = -(writeln("Constructing automaton " ^ automaton_name ^ " ..."); -let -val auttyp = aut_type_of thy aut_source; -val acttyp = act_type_of thy auttyp; -val rest_set = action_set_string thy acttyp actlist -in -thy -|> Sign.add_consts_i -[(Binding.name automaton_name, auttyp,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] -end) -fun add_hiding automaton_name aut_source actlist thy = -(writeln("Constructing automaton " ^ automaton_name ^ " ..."); -let -val auttyp = aut_type_of thy aut_source; -val acttyp = act_type_of thy auttyp; -val hid_set = action_set_string thy acttyp actlist -in -thy -|> Sign.add_consts_i -[(Binding.name automaton_name, auttyp,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] -end) - -fun ren_act_type_of thy funct = - (case Term.fastype_of (Syntax.read_term_global thy funct) of - Type ("fun", [a, b]) => a - | _ => error "could not extract argument type of renaming function term"); - -fun add_rename automaton_name aut_source fun_name thy = -(writeln("Constructing automaton " ^ automaton_name ^ " ..."); -let -val auttyp = aut_type_of thy aut_source; -val st_typ = st_type_of thy auttyp; -val acttyp = ren_act_type_of thy fun_name -in -thy -|> Sign.add_consts_i -[(Binding.name automaton_name, -Type("*", -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), - Type("*",[Type("set",[st_typ]), - Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), - Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) -,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] -end) - - -(** outer syntax **) - -(* prepare results *) - -(*encoding transition specifications with a element of ParseTrans*) -datatype ParseTrans = Rel of string | PP of string*(string*string)list; -fun mk_trans_of_rel s = Rel(s); -fun mk_trans_of_prepost (s,l) = PP(s,l); - -fun trans_of (a, Rel b) = (a, b, [("", "")]) - | trans_of (a, PP (b, l)) = (a, b, l); - - -fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = - add_ioa aut action_type inp out int states initial (map trans_of trans); - -fun mk_composition_decl (aut, autlist) = - add_composition aut autlist; - -fun mk_hiding_decl (aut, (actlist, source_aut)) = - add_hiding aut source_aut actlist; - -fun mk_restriction_decl (aut, (source_aut, actlist)) = - add_restriction aut source_aut actlist; - -fun mk_rename_decl (aut, (source_aut, rename_f)) = - add_rename aut source_aut rename_f; - - -(* outer syntax *) - -local structure P = OuterParse and K = OuterKeyword in - -val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs", - "outputs", "internals", "states", "initially", "transitions", "pre", - "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", - "rename"]; - -val actionlist = P.list1 P.term; -val inputslist = P.$$$ "inputs" |-- P.!!! actionlist; -val outputslist = P.$$$ "outputs" |-- P.!!! actionlist; -val internalslist = P.$$$ "internals" |-- P.!!! actionlist; -val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ)); -val initial = P.$$$ "initially" |-- P.!!! P.term; -val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term); -val pre = P.$$$ "pre" |-- P.!!! P.term; -val post = P.$$$ "post" |-- P.!!! assign_list; -val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; -val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; -val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel; -val transition = P.term -- (transrel || pre1 || post1); -val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition); - -val ioa_decl = - (P.name -- (P.$$$ "=" |-- - (P.$$$ "signature" |-- - P.!!! (P.$$$ "actions" |-- - (P.typ -- - (Scan.optional inputslist []) -- - (Scan.optional outputslist []) -- - (Scan.optional internalslist []) -- - stateslist -- - (Scan.optional initial "True") -- - translist))))) >> mk_ioa_decl || - (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name)))) - >> mk_composition_decl || - (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- - P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl || - (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- - P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl || - (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term)))))) - >> mk_rename_decl; - -val _ = - OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl - (ioa_decl >> Toplevel.theory); - -end; - -end; diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOLCF/IsaMakefile Sun Jun 21 15:46:14 2009 +0200 @@ -67,8 +67,8 @@ Tools/domain/domain_library.ML \ Tools/domain/domain_syntax.ML \ Tools/domain/domain_theorems.ML \ - Tools/fixrec_package.ML \ - Tools/pcpodef_package.ML \ + Tools/fixrec.ML \ + Tools/pcpodef.ML \ holcf_logic.ML \ document/root.tex @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF @@ -127,7 +127,7 @@ IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ - IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML + IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML @cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Pcpodef.thy --- a/src/HOLCF/Pcpodef.thy Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOLCF/Pcpodef.thy Sun Jun 21 15:46:14 2009 +0200 @@ -6,7 +6,7 @@ theory Pcpodef imports Adm -uses ("Tools/pcpodef_package.ML") +uses ("Tools/pcpodef.ML") begin subsection {* Proving a subtype is a partial order *} @@ -303,6 +303,6 @@ subsection {* HOLCF type definition package *} -use "Tools/pcpodef_package.ML" +use "Tools/pcpodef.ML" end diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 15:46:14 2009 +0200 @@ -6,7 +6,7 @@ signature DOMAIN_AXIOMS = sig - val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term + val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term val calc_axioms : string -> Domain_Library.eq list -> int -> Domain_Library.eq -> @@ -171,7 +171,7 @@ val mat_names = map mat_name con_names; fun qualify n = Sign.full_name thy (Binding.name n); val ms = map qualify con_names ~~ map qualify mat_names; - in FixrecPackage.add_matchers ms thy end; + in Fixrec.add_matchers ms thy end; fun add_axioms comp_dnam (eqs : eq list) thy' = let diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 11:50:26 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 15:46:14 2009 +0200 @@ -135,10 +135,10 @@ eqtype arg; type cons = string * arg list; type eq = (string * typ list) * cons list; - val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg; + val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg; val is_lazy : arg -> bool; val rec_of : arg -> int; - val dtyp_of : arg -> DatatypeAux.dtyp; + val dtyp_of : arg -> Datatype.dtyp; val sel_of : arg -> string option; val vname : arg -> string; val upd_vname : (string -> string) -> arg -> arg; @@ -154,7 +154,7 @@ val idx_name : 'a list -> string -> int -> string; val app_rec_arg : (int -> term) -> arg -> term; val con_app : string -> arg list -> term; - val dtyp_of_eq : eq -> DatatypeAux.dtyp; + val dtyp_of_eq : eq -> Datatype.dtyp; (* Name mangling *) @@ -215,7 +215,7 @@ (* ----- constructor list handling ----- *) type arg = - (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *) + (bool * Datatype.dtyp) * (* (lazy, recursive element) *) string option * (* selector name *) string; (* argument name *) diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Tools/fixrec.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/fixrec.ML Sun Jun 21 15:46:14 2009 +0200 @@ -0,0 +1,435 @@ +(* Title: HOLCF/Tools/fixrec.ML + Author: Amber Telfer and Brian Huffman + +Recursive function definition package for HOLCF. +*) + +signature FIXREC = +sig + val add_fixrec: bool -> (binding * typ option * mixfix) list + -> (Attrib.binding * term) list -> local_theory -> local_theory + val add_fixrec_cmd: bool -> (binding * string option * mixfix) list + -> (Attrib.binding * string) list -> local_theory -> local_theory + val add_fixpat: Thm.binding * term list -> theory -> theory + val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory + val add_matchers: (string * string) list -> theory -> theory + val setup: theory -> theory +end; + +structure Fixrec :> FIXREC = +struct + +val def_cont_fix_eq = @{thm def_cont_fix_eq}; +val def_cont_fix_ind = @{thm def_cont_fix_ind}; + + +fun fixrec_err s = error ("fixrec definition error:\n" ^ s); +fun fixrec_eq_err thy s eq = + fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)); + +(*************************************************************************) +(***************************** building types ****************************) +(*************************************************************************) + +(* ->> is taken from holcf_logic.ML *) +fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]); + +infixr 6 ->>; val (op ->>) = cfunT; + +fun cfunsT (Ts, U) = foldr cfunT U Ts; + +fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) + | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); + +fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U + | binder_cfun _ = []; + +fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U + | body_cfun T = T; + +fun strip_cfun T : typ list * typ = + (binder_cfun T, body_cfun T); + +fun maybeT T = Type(@{type_name "maybe"}, [T]); + +fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T + | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []); + +fun tupleT [] = HOLogic.unitT + | tupleT [T] = T + | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); + +fun matchT (T, U) = + body_cfun T ->> cfunsT (binder_cfun T, U) ->> U; + + +(*************************************************************************) +(***************************** building terms ****************************) +(*************************************************************************) + +val mk_trp = HOLogic.mk_Trueprop; + +(* splits a cterm into the right and lefthand sides of equality *) +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); + +(* similar to Thm.head_of, but for continuous application *) +fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f + | chead_of u = u; + +fun capply_const (S, T) = + Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); + +fun cabs_const (S, T) = + Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); + +fun mk_cabs t = + let val T = Term.fastype_of t + in cabs_const (Term.domain_type T, Term.range_type T) $ t end + +fun mk_capply (t, u) = + let val (S, T) = + case Term.fastype_of t of + Type(@{type_name "->"}, [S, T]) => (S, T) + | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); + in capply_const (S, T) $ t $ u end; + +infix 0 ==; val (op ==) = Logic.mk_equals; +infix 1 ===; val (op ===) = HOLogic.mk_eq; +infix 9 ` ; val (op `) = mk_capply; + +(* builds the expression (LAM v. rhs) *) +fun big_lambda v rhs = + cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; + +(* builds the expression (LAM v1 v2 .. vn. rhs) *) +fun big_lambdas [] rhs = rhs + | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); + +fun mk_return t = + let val T = Term.fastype_of t + in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end; + +fun mk_bind (t, u) = + let val (T, mU) = dest_cfunT (Term.fastype_of u); + val bindT = maybeT T ->> (T ->> mU) ->> mU; + in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end; + +fun mk_mplus (t, u) = + let val mT = Term.fastype_of t + in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end; + +fun mk_run t = + let val mT = Term.fastype_of t + val T = dest_maybeT mT + in Const(@{const_name Fixrec.run}, mT ->> T) ` t end; + +fun mk_fix t = + let val (T, _) = dest_cfunT (Term.fastype_of t) + in Const(@{const_name fix}, (T ->> T) ->> T) ` t end; + +fun mk_cont t = + let val T = Term.fastype_of t + in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end; + +val mk_fst = HOLogic.mk_fst +val mk_snd = HOLogic.mk_snd + +(* builds the expression (v1,v2,..,vn) *) +fun mk_tuple [] = HOLogic.unit +| mk_tuple (t::[]) = t +| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); + +(* builds the expression (%(v1,v2,..,vn). rhs) *) +fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs + | lambda_tuple (v::[]) rhs = Term.lambda v rhs + | lambda_tuple (v::vs) rhs = + HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); + + +(*************************************************************************) +(************* fixed-point definitions and unfolding theorems ************) +(*************************************************************************) + +fun add_fixdefs + (fixes : ((binding * typ) * mixfix) list) + (spec : (Attrib.binding * term) list) + (lthy : local_theory) = + let + val thy = ProofContext.theory_of lthy; + val names = map (Binding.name_of o fst o fst) fixes; + val all_names = space_implode "_" names; + val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec); + val functional = lambda_tuple lhss (mk_tuple rhss); + val fixpoint = mk_fix (mk_cabs functional); + + val cont_thm = + Goal.prove lthy [] [] (mk_trp (mk_cont functional)) + (K (simp_tac (local_simpset_of lthy) 1)); + + fun one_def (l as Free(n,_)) r = + let val b = Long_Name.base_name n + in ((Binding.name (b^"_def"), []), r) end + | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; + fun defs [] _ = [] + | defs (l::[]) r = [one_def l r] + | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r); + val fixdefs = defs lhss fixpoint; + val define_all = fold_map (LocalTheory.define Thm.definitionK); + val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy + |> define_all (map (apfst fst) fixes ~~ fixdefs); + fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; + val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms); + val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT); + val predicate = lambda_tuple lhss (list_comb (P, lhss)); + val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm]) + |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)] + |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict}; + val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm]) + |> LocalDefs.unfold lthy' @{thms split_conv}; + fun unfolds [] thm = [] + | unfolds (n::[]) thm = [(n^"_unfold", thm)] + | unfolds (n::ns) thm = let + val thmL = thm RS @{thm Pair_eqD1}; + val thmR = thm RS @{thm Pair_eqD2}; + in (n^"_unfold", thmL) :: unfolds ns thmR end; + val unfold_thms = unfolds names tuple_unfold_thm; + fun mk_note (n, thm) = ((Binding.name n, []), [thm]); + val (thmss, lthy'') = lthy' + |> fold_map (LocalTheory.note Thm.generatedK o mk_note) + ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms); + in + (lthy'', names, fixdef_thms, map snd unfold_thms) + end; + +(*************************************************************************) +(*********** monadic notation and pattern matching compilation ***********) +(*************************************************************************) + +structure FixrecMatchData = TheoryDataFun ( + type T = string Symtab.table; + val empty = Symtab.empty; + val copy = I; + val extend = I; + fun merge _ tabs : T = Symtab.merge (K true) tabs; +); + +(* associate match functions with pattern constants *) +fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms); + +fun taken_names (t : term) : bstring list = + let + fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs + | taken (Free(a,_) , bs) = insert (op =) a bs + | taken (f $ u , bs) = taken (f, taken (u, bs)) + | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) + | taken (_ , bs) = bs; + in + taken (t, []) + end; + +(* builds a monadic term for matching a constructor pattern *) +fun pre_build match_name pat rhs vs taken = + case pat of + Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) => + pre_build match_name f rhs (v::vs) taken + | Const(@{const_name Rep_CFun},_)$f$x => + let val (rhs', v, taken') = pre_build match_name x rhs [] taken; + in pre_build match_name f rhs' (v::vs) taken' end + | Const(c,T) => + let + val n = Name.variant taken "v"; + fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs + | result_type T _ = T; + val v = Free(n, result_type T vs); + val m = Const(match_name c, matchT (T, fastype_of rhs)); + val k = big_lambdas vs rhs; + in + (m`v`k, v, n::taken) + end + | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) + | _ => fixrec_err "pre_build: invalid pattern"; + +(* builds a monadic term for matching a function definition pattern *) +(* returns (name, arity, matcher) *) +fun building match_name pat rhs vs taken = + case pat of + Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) => + building match_name f rhs (v::vs) taken + | Const(@{const_name Rep_CFun}, _)$f$x => + let val (rhs', v, taken') = pre_build match_name x rhs [] taken; + in building match_name f rhs' (v::vs) taken' end + | Free(_,_) => ((pat, length vs), big_lambdas vs rhs) + | Const(_,_) => ((pat, length vs), big_lambdas vs rhs) + | _ => fixrec_err ("function is not declared as constant in theory: " + ^ ML_Syntax.print_term pat); + +fun strip_alls t = + if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t; + +fun match_eq match_name eq = + let + val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)); + in + building match_name lhs (mk_return rhs) [] (taken_names eq) + end; + +(* returns the sum (using +++) of the terms in ms *) +(* also applies "run" to the result! *) +fun fatbar arity ms = + let + fun LAM_Ts 0 t = ([], Term.fastype_of t) + | LAM_Ts n (_ $ Abs(_,T,t)) = + let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end + | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; + fun unLAM 0 t = t + | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t + | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; + fun reLAM ([], U) t = t + | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t)); + val msum = foldr1 mk_mplus (map (unLAM arity) ms); + val (Ts, U) = LAM_Ts arity (hd ms) + in + reLAM (rev Ts, dest_maybeT U) (mk_run msum) + end; + +(* this is the pattern-matching compiler function *) +fun compile_pats match_name eqs = + let + val (((n::names),(a::arities)),mats) = + apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs)); + val cname = if forall (fn x => n=x) names then n + else fixrec_err "all equations in block must define the same function"; + val arity = if forall (fn x => a=x) arities then a + else fixrec_err "all equations in block must have the same arity"; + val rhs = fatbar arity mats; + in + mk_trp (cname === rhs) + end; + +(*************************************************************************) +(********************** Proving associated theorems **********************) +(*************************************************************************) + +(* proves a block of pattern matching equations as theorems, using unfold *) +fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) = + let + val tacs = + [rtac (unfold_thm RS @{thm ssubst_lhs}) 1, + asm_simp_tac (local_simpset_of lthy) 1]; + fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs)); + fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t); + in + map prove_eqn eqns + end; + +(*************************************************************************) +(************************* Main fixrec function **************************) +(*************************************************************************) + +local +(* code adapted from HOL/Tools/primrec.ML *) + +fun gen_fixrec + (set_group : bool) + prep_spec + (strict : bool) + raw_fixes + raw_spec + (lthy : local_theory) = + let + val (fixes : ((binding * typ) * mixfix) list, + spec : (Attrib.binding * term) list) = + fst (prep_spec raw_fixes raw_spec lthy); + val chead_of_spec = + chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd; + fun name_of (Free (n, _)) = n + | name_of t = fixrec_err ("unknown term"); + val all_names = map (name_of o chead_of_spec) spec; + val names = distinct (op =) all_names; + fun block_of_name n = + map_filter + (fn (m,eq) => if m = n then SOME eq else NONE) + (all_names ~~ spec); + val blocks = map block_of_name names; + + val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy); + fun match_name c = + case Symtab.lookup matcher_tab c of SOME m => m + | NONE => fixrec_err ("unknown pattern constructor: " ^ c); + + val matches = map (compile_pats match_name) (map (map snd) blocks); + val spec' = map (pair Attrib.empty_binding) matches; + val (lthy', cnames, fixdef_thms, unfold_thms) = + add_fixdefs fixes spec' lthy; + in + if strict then let (* only prove simp rules if strict = true *) + val simps : (Attrib.binding * thm) list list = + map (make_simps lthy') (unfold_thms ~~ blocks); + fun mk_bind n : Attrib.binding = + (Binding.name (n ^ "_simps"), + [Attrib.internal (K Simplifier.simp_add)]); + val simps1 : (Attrib.binding * thm list) list = + map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps); + val simps2 : (Attrib.binding * thm list) list = + map (apsnd (fn thm => [thm])) (List.concat simps); + val (_, lthy'') = lthy' + |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2); + in + lthy'' + end + else lthy' + end; + +in + +val add_fixrec = gen_fixrec false Specification.check_spec; +val add_fixrec_cmd = gen_fixrec true Specification.read_spec; + +end; (* local *) + +(*************************************************************************) +(******************************** Fixpat *********************************) +(*************************************************************************) + +fun fix_pat thy t = + let + val T = fastype_of t; + val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); + val cname = case chead_of t of Const(c,_) => c | _ => + fixrec_err "function is not declared as constant in theory"; + val unfold_thm = PureThy.get_thm thy (cname^"_unfold"); + val simp = Goal.prove_global thy [] [] eq + (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); + in simp end; + +fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = + let + val atts = map (prep_attrib thy) srcs; + val ts = map (prep_term thy) strings; + val simps = map (fix_pat thy) ts; + in + (snd o PureThy.add_thmss [((name, simps), atts)]) thy + end; + +val add_fixpat = gen_add_fixpat Sign.cert_term (K I); +val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute; + + +(*************************************************************************) +(******************************** Parsers ********************************) +(*************************************************************************) + +local structure P = OuterParse and K = OuterKeyword in + +val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl + ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs + >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs)); + +val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl + (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd)); + +end; + +val setup = FixrecMatchData.init; + +end; diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 11:50:26 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,435 +0,0 @@ -(* Title: HOLCF/Tools/fixrec_package.ML - Author: Amber Telfer and Brian Huffman - -Recursive function definition package for HOLCF. -*) - -signature FIXREC_PACKAGE = -sig - val add_fixrec: bool -> (binding * typ option * mixfix) list - -> (Attrib.binding * term) list -> local_theory -> local_theory - val add_fixrec_cmd: bool -> (binding * string option * mixfix) list - -> (Attrib.binding * string) list -> local_theory -> local_theory - val add_fixpat: Thm.binding * term list -> theory -> theory - val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory - val add_matchers: (string * string) list -> theory -> theory - val setup: theory -> theory -end; - -structure FixrecPackage :> FIXREC_PACKAGE = -struct - -val def_cont_fix_eq = @{thm def_cont_fix_eq}; -val def_cont_fix_ind = @{thm def_cont_fix_ind}; - - -fun fixrec_err s = error ("fixrec definition error:\n" ^ s); -fun fixrec_eq_err thy s eq = - fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)); - -(*************************************************************************) -(***************************** building types ****************************) -(*************************************************************************) - -(* ->> is taken from holcf_logic.ML *) -fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]); - -infixr 6 ->>; val (op ->>) = cfunT; - -fun cfunsT (Ts, U) = foldr cfunT U Ts; - -fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) - | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); - -fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U - | binder_cfun _ = []; - -fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U - | body_cfun T = T; - -fun strip_cfun T : typ list * typ = - (binder_cfun T, body_cfun T); - -fun maybeT T = Type(@{type_name "maybe"}, [T]); - -fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T - | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []); - -fun tupleT [] = HOLogic.unitT - | tupleT [T] = T - | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); - -fun matchT (T, U) = - body_cfun T ->> cfunsT (binder_cfun T, U) ->> U; - - -(*************************************************************************) -(***************************** building terms ****************************) -(*************************************************************************) - -val mk_trp = HOLogic.mk_Trueprop; - -(* splits a cterm into the right and lefthand sides of equality *) -fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); - -(* similar to Thm.head_of, but for continuous application *) -fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f - | chead_of u = u; - -fun capply_const (S, T) = - Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); - -fun cabs_const (S, T) = - Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); - -fun mk_cabs t = - let val T = Term.fastype_of t - in cabs_const (Term.domain_type T, Term.range_type T) $ t end - -fun mk_capply (t, u) = - let val (S, T) = - case Term.fastype_of t of - Type(@{type_name "->"}, [S, T]) => (S, T) - | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); - in capply_const (S, T) $ t $ u end; - -infix 0 ==; val (op ==) = Logic.mk_equals; -infix 1 ===; val (op ===) = HOLogic.mk_eq; -infix 9 ` ; val (op `) = mk_capply; - -(* builds the expression (LAM v. rhs) *) -fun big_lambda v rhs = - cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; - -(* builds the expression (LAM v1 v2 .. vn. rhs) *) -fun big_lambdas [] rhs = rhs - | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); - -fun mk_return t = - let val T = Term.fastype_of t - in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end; - -fun mk_bind (t, u) = - let val (T, mU) = dest_cfunT (Term.fastype_of u); - val bindT = maybeT T ->> (T ->> mU) ->> mU; - in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end; - -fun mk_mplus (t, u) = - let val mT = Term.fastype_of t - in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end; - -fun mk_run t = - let val mT = Term.fastype_of t - val T = dest_maybeT mT - in Const(@{const_name Fixrec.run}, mT ->> T) ` t end; - -fun mk_fix t = - let val (T, _) = dest_cfunT (Term.fastype_of t) - in Const(@{const_name fix}, (T ->> T) ->> T) ` t end; - -fun mk_cont t = - let val T = Term.fastype_of t - in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end; - -val mk_fst = HOLogic.mk_fst -val mk_snd = HOLogic.mk_snd - -(* builds the expression (v1,v2,..,vn) *) -fun mk_tuple [] = HOLogic.unit -| mk_tuple (t::[]) = t -| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); - -(* builds the expression (%(v1,v2,..,vn). rhs) *) -fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs - | lambda_tuple (v::[]) rhs = Term.lambda v rhs - | lambda_tuple (v::vs) rhs = - HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); - - -(*************************************************************************) -(************* fixed-point definitions and unfolding theorems ************) -(*************************************************************************) - -fun add_fixdefs - (fixes : ((binding * typ) * mixfix) list) - (spec : (Attrib.binding * term) list) - (lthy : local_theory) = - let - val thy = ProofContext.theory_of lthy; - val names = map (Binding.name_of o fst o fst) fixes; - val all_names = space_implode "_" names; - val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec); - val functional = lambda_tuple lhss (mk_tuple rhss); - val fixpoint = mk_fix (mk_cabs functional); - - val cont_thm = - Goal.prove lthy [] [] (mk_trp (mk_cont functional)) - (K (simp_tac (local_simpset_of lthy) 1)); - - fun one_def (l as Free(n,_)) r = - let val b = Long_Name.base_name n - in ((Binding.name (b^"_def"), []), r) end - | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; - fun defs [] _ = [] - | defs (l::[]) r = [one_def l r] - | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r); - val fixdefs = defs lhss fixpoint; - val define_all = fold_map (LocalTheory.define Thm.definitionK); - val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy - |> define_all (map (apfst fst) fixes ~~ fixdefs); - fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; - val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms); - val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT); - val predicate = lambda_tuple lhss (list_comb (P, lhss)); - val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm]) - |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)] - |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict}; - val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm]) - |> LocalDefs.unfold lthy' @{thms split_conv}; - fun unfolds [] thm = [] - | unfolds (n::[]) thm = [(n^"_unfold", thm)] - | unfolds (n::ns) thm = let - val thmL = thm RS @{thm Pair_eqD1}; - val thmR = thm RS @{thm Pair_eqD2}; - in (n^"_unfold", thmL) :: unfolds ns thmR end; - val unfold_thms = unfolds names tuple_unfold_thm; - fun mk_note (n, thm) = ((Binding.name n, []), [thm]); - val (thmss, lthy'') = lthy' - |> fold_map (LocalTheory.note Thm.generatedK o mk_note) - ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms); - in - (lthy'', names, fixdef_thms, map snd unfold_thms) - end; - -(*************************************************************************) -(*********** monadic notation and pattern matching compilation ***********) -(*************************************************************************) - -structure FixrecMatchData = TheoryDataFun ( - type T = string Symtab.table; - val empty = Symtab.empty; - val copy = I; - val extend = I; - fun merge _ tabs : T = Symtab.merge (K true) tabs; -); - -(* associate match functions with pattern constants *) -fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms); - -fun taken_names (t : term) : bstring list = - let - fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs - | taken (Free(a,_) , bs) = insert (op =) a bs - | taken (f $ u , bs) = taken (f, taken (u, bs)) - | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) - | taken (_ , bs) = bs; - in - taken (t, []) - end; - -(* builds a monadic term for matching a constructor pattern *) -fun pre_build match_name pat rhs vs taken = - case pat of - Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) => - pre_build match_name f rhs (v::vs) taken - | Const(@{const_name Rep_CFun},_)$f$x => - let val (rhs', v, taken') = pre_build match_name x rhs [] taken; - in pre_build match_name f rhs' (v::vs) taken' end - | Const(c,T) => - let - val n = Name.variant taken "v"; - fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs - | result_type T _ = T; - val v = Free(n, result_type T vs); - val m = Const(match_name c, matchT (T, fastype_of rhs)); - val k = big_lambdas vs rhs; - in - (m`v`k, v, n::taken) - end - | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) - | _ => fixrec_err "pre_build: invalid pattern"; - -(* builds a monadic term for matching a function definition pattern *) -(* returns (name, arity, matcher) *) -fun building match_name pat rhs vs taken = - case pat of - Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) => - building match_name f rhs (v::vs) taken - | Const(@{const_name Rep_CFun}, _)$f$x => - let val (rhs', v, taken') = pre_build match_name x rhs [] taken; - in building match_name f rhs' (v::vs) taken' end - | Free(_,_) => ((pat, length vs), big_lambdas vs rhs) - | Const(_,_) => ((pat, length vs), big_lambdas vs rhs) - | _ => fixrec_err ("function is not declared as constant in theory: " - ^ ML_Syntax.print_term pat); - -fun strip_alls t = - if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t; - -fun match_eq match_name eq = - let - val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)); - in - building match_name lhs (mk_return rhs) [] (taken_names eq) - end; - -(* returns the sum (using +++) of the terms in ms *) -(* also applies "run" to the result! *) -fun fatbar arity ms = - let - fun LAM_Ts 0 t = ([], Term.fastype_of t) - | LAM_Ts n (_ $ Abs(_,T,t)) = - let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end - | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; - fun unLAM 0 t = t - | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t - | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; - fun reLAM ([], U) t = t - | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t)); - val msum = foldr1 mk_mplus (map (unLAM arity) ms); - val (Ts, U) = LAM_Ts arity (hd ms) - in - reLAM (rev Ts, dest_maybeT U) (mk_run msum) - end; - -(* this is the pattern-matching compiler function *) -fun compile_pats match_name eqs = - let - val (((n::names),(a::arities)),mats) = - apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs)); - val cname = if forall (fn x => n=x) names then n - else fixrec_err "all equations in block must define the same function"; - val arity = if forall (fn x => a=x) arities then a - else fixrec_err "all equations in block must have the same arity"; - val rhs = fatbar arity mats; - in - mk_trp (cname === rhs) - end; - -(*************************************************************************) -(********************** Proving associated theorems **********************) -(*************************************************************************) - -(* proves a block of pattern matching equations as theorems, using unfold *) -fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) = - let - val tacs = - [rtac (unfold_thm RS @{thm ssubst_lhs}) 1, - asm_simp_tac (local_simpset_of lthy) 1]; - fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs)); - fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t); - in - map prove_eqn eqns - end; - -(*************************************************************************) -(************************* Main fixrec function **************************) -(*************************************************************************) - -local -(* code adapted from HOL/Tools/primrec_package.ML *) - -fun gen_fixrec - (set_group : bool) - prep_spec - (strict : bool) - raw_fixes - raw_spec - (lthy : local_theory) = - let - val (fixes : ((binding * typ) * mixfix) list, - spec : (Attrib.binding * term) list) = - fst (prep_spec raw_fixes raw_spec lthy); - val chead_of_spec = - chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd; - fun name_of (Free (n, _)) = n - | name_of t = fixrec_err ("unknown term"); - val all_names = map (name_of o chead_of_spec) spec; - val names = distinct (op =) all_names; - fun block_of_name n = - map_filter - (fn (m,eq) => if m = n then SOME eq else NONE) - (all_names ~~ spec); - val blocks = map block_of_name names; - - val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy); - fun match_name c = - case Symtab.lookup matcher_tab c of SOME m => m - | NONE => fixrec_err ("unknown pattern constructor: " ^ c); - - val matches = map (compile_pats match_name) (map (map snd) blocks); - val spec' = map (pair Attrib.empty_binding) matches; - val (lthy', cnames, fixdef_thms, unfold_thms) = - add_fixdefs fixes spec' lthy; - in - if strict then let (* only prove simp rules if strict = true *) - val simps : (Attrib.binding * thm) list list = - map (make_simps lthy') (unfold_thms ~~ blocks); - fun mk_bind n : Attrib.binding = - (Binding.name (n ^ "_simps"), - [Attrib.internal (K Simplifier.simp_add)]); - val simps1 : (Attrib.binding * thm list) list = - map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps); - val simps2 : (Attrib.binding * thm list) list = - map (apsnd (fn thm => [thm])) (List.concat simps); - val (_, lthy'') = lthy' - |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2); - in - lthy'' - end - else lthy' - end; - -in - -val add_fixrec = gen_fixrec false Specification.check_spec; -val add_fixrec_cmd = gen_fixrec true Specification.read_spec; - -end; (* local *) - -(*************************************************************************) -(******************************** Fixpat *********************************) -(*************************************************************************) - -fun fix_pat thy t = - let - val T = fastype_of t; - val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); - val cname = case chead_of t of Const(c,_) => c | _ => - fixrec_err "function is not declared as constant in theory"; - val unfold_thm = PureThy.get_thm thy (cname^"_unfold"); - val simp = Goal.prove_global thy [] [] eq - (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); - in simp end; - -fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = - let - val atts = map (prep_attrib thy) srcs; - val ts = map (prep_term thy) strings; - val simps = map (fix_pat thy) ts; - in - (snd o PureThy.add_thmss [((name, simps), atts)]) thy - end; - -val add_fixpat = gen_add_fixpat Sign.cert_term (K I); -val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute; - - -(*************************************************************************) -(******************************** Parsers ********************************) -(*************************************************************************) - -local structure P = OuterParse and K = OuterKeyword in - -val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl - ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs - >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs)); - -val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl - (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd)); - -end; - -val setup = FixrecMatchData.init; - -end; diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Tools/pcpodef.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/pcpodef.ML Sun Jun 21 15:46:14 2009 +0200 @@ -0,0 +1,201 @@ +(* Title: HOLCF/Tools/pcpodef.ML + Author: Brian Huffman + +Primitive domain definitions for HOLCF, similar to Gordon/HOL-style +typedef (see also ~~/src/HOL/Tools/typedef.ML). +*) + +signature PCPODEF = +sig + val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term + * (binding * binding) option -> theory -> Proof.state + val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string + * (binding * binding) option -> theory -> Proof.state + val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term + * (binding * binding) option -> theory -> Proof.state + val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string + * (binding * binding) option -> theory -> Proof.state +end; + +structure Pcpodef :> PCPODEF = +struct + +(** type definitions **) + +(* prepare_cpodef *) + +fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); + +fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); +fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); + +fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = + let + val _ = Theory.requires thy "Pcpodef" "pcpodefs"; + val ctxt = ProofContext.init thy; + + val full = Sign.full_name thy; + val full_name = full name; + val bname = Binding.name_of name; + + (*rhs*) + val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; + val setT = Term.fastype_of set; + val rhs_tfrees = Term.add_tfrees set []; + val oldT = HOLogic.dest_setT setT handle TYPE _ => + error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); + + (*goal*) + val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); + val goal_nonempty = + HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); + val goal_admissible = + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); + + (*lhs*) + val defS = Sign.defaultS thy; + val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; + val lhs_sorts = map snd lhs_tfrees; + + val tname = Binding.map_name (Syntax.type_name mx) t; + val full_tname = full tname; + val newT = Type (full_tname, map TFree lhs_tfrees); + + val (Rep_name, Abs_name) = + (case opt_morphs of + NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) + | SOME morphs => morphs); + val RepC = Const (full Rep_name, newT --> oldT); + fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT); + val below_def = Logic.mk_equals (belowC newT, + Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); + + fun make_po tac thy1 = + let + val ((_, {type_definition, set_def, ...}), thy2) = thy1 + |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac; + val lthy3 = thy2 + |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po}); + val below_def' = Syntax.check_term lthy3 below_def; + val ((_, (_, below_definition')), lthy4) = lthy3 + |> Specification.definition (NONE, + ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def')); + val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); + val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition'; + val thy5 = lthy4 + |> Class.prove_instantiation_instance + (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1)) + |> LocalTheory.exit_global; + in ((type_definition, below_definition, set_def), thy5) end; + + fun make_cpo admissible (type_def, below_def, set_def) theory = + let + val admissible' = fold_rule (the_list set_def) admissible; + val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible']; + val theory' = theory + |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) + (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1); + val cpo_thms' = map (Thm.transfer theory') cpo_thms; + in + theory' + |> Sign.add_path (Binding.name_of name) + |> PureThy.add_thms + ([((Binding.prefix_name "adm_" name, admissible'), []), + ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []), + ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []), + ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []), + ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []), + ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])]) + |> snd + |> Sign.parent_path + end; + + fun make_pcpo UU_mem (type_def, below_def, set_def) theory = + let + val UU_mem' = fold_rule (the_list set_def) UU_mem; + val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem']; + val theory' = theory + |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) + (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1); + val pcpo_thms' = map (Thm.transfer theory') pcpo_thms; + in + theory' + |> Sign.add_path (Binding.name_of name) + |> PureThy.add_thms + ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []), + ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []), + ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []), + ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []), + ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []), + ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])]) + |> snd + |> Sign.parent_path + end; + + fun pcpodef_result UU_mem admissible = + make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1) + #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs); + + fun cpodef_result nonempty admissible = + make_po (Tactic.rtac nonempty 1) + #-> make_cpo admissible; + in + if pcpo + then (goal_UU_mem, goal_admissible, pcpodef_result) + else (goal_nonempty, goal_admissible, cpodef_result) + end + handle ERROR msg => + cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)); + + +(* proof interface *) + +local + +fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = + let + val (goal1, goal2, make_result) = + prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; + fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2); + in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; + +in + +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x; +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x; + +fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x; +fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x; + +end; + + + +(** outer syntax **) + +local structure P = OuterParse and K = OuterKeyword in + +val typedef_proof_decl = + Scan.optional (P.$$$ "(" |-- + ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) + --| P.$$$ ")") (true, NONE) -- + (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); + +fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = + (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) + ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs); + +val _ = + OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal + (typedef_proof_decl >> + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); + +val _ = + OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal + (typedef_proof_decl >> + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); + +end; + +end; diff -r 052399f580cf -r 41788a3ffd6a src/HOLCF/Tools/pcpodef_package.ML --- a/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 11:50:26 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,201 +0,0 @@ -(* Title: HOLCF/Tools/pcpodef_package.ML - Author: Brian Huffman - -Primitive domain definitions for HOLCF, similar to Gordon/HOL-style -typedef (see also ~~/src/HOL/Tools/typedef_package.ML). -*) - -signature PCPODEF_PACKAGE = -sig - val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term - * (binding * binding) option -> theory -> Proof.state - val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string - * (binding * binding) option -> theory -> Proof.state - val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term - * (binding * binding) option -> theory -> Proof.state - val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string - * (binding * binding) option -> theory -> Proof.state -end; - -structure PcpodefPackage :> PCPODEF_PACKAGE = -struct - -(** type definitions **) - -(* prepare_cpodef *) - -fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); - -fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); -fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); - -fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = - let - val _ = Theory.requires thy "Pcpodef" "pcpodefs"; - val ctxt = ProofContext.init thy; - - val full = Sign.full_name thy; - val full_name = full name; - val bname = Binding.name_of name; - - (*rhs*) - val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; - val setT = Term.fastype_of set; - val rhs_tfrees = Term.add_tfrees set []; - val oldT = HOLogic.dest_setT setT handle TYPE _ => - error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); - - (*goal*) - val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); - val goal_nonempty = - HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); - val goal_admissible = - HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); - - (*lhs*) - val defS = Sign.defaultS thy; - val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; - val lhs_sorts = map snd lhs_tfrees; - - val tname = Binding.map_name (Syntax.type_name mx) t; - val full_tname = full tname; - val newT = Type (full_tname, map TFree lhs_tfrees); - - val (Rep_name, Abs_name) = - (case opt_morphs of - NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) - | SOME morphs => morphs); - val RepC = Const (full Rep_name, newT --> oldT); - fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT); - val below_def = Logic.mk_equals (belowC newT, - Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); - - fun make_po tac thy1 = - let - val ((_, {type_definition, set_def, ...}), thy2) = thy1 - |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac; - val lthy3 = thy2 - |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po}); - val below_def' = Syntax.check_term lthy3 below_def; - val ((_, (_, below_definition')), lthy4) = lthy3 - |> Specification.definition (NONE, - ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def')); - val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); - val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition'; - val thy5 = lthy4 - |> Class.prove_instantiation_instance - (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1)) - |> LocalTheory.exit_global; - in ((type_definition, below_definition, set_def), thy5) end; - - fun make_cpo admissible (type_def, below_def, set_def) theory = - let - val admissible' = fold_rule (the_list set_def) admissible; - val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible']; - val theory' = theory - |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) - (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1); - val cpo_thms' = map (Thm.transfer theory') cpo_thms; - in - theory' - |> Sign.add_path (Binding.name_of name) - |> PureThy.add_thms - ([((Binding.prefix_name "adm_" name, admissible'), []), - ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []), - ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []), - ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []), - ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []), - ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])]) - |> snd - |> Sign.parent_path - end; - - fun make_pcpo UU_mem (type_def, below_def, set_def) theory = - let - val UU_mem' = fold_rule (the_list set_def) UU_mem; - val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem']; - val theory' = theory - |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) - (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1); - val pcpo_thms' = map (Thm.transfer theory') pcpo_thms; - in - theory' - |> Sign.add_path (Binding.name_of name) - |> PureThy.add_thms - ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []), - ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []), - ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []), - ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []), - ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []), - ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])]) - |> snd - |> Sign.parent_path - end; - - fun pcpodef_result UU_mem admissible = - make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1) - #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs); - - fun cpodef_result nonempty admissible = - make_po (Tactic.rtac nonempty 1) - #-> make_cpo admissible; - in - if pcpo - then (goal_UU_mem, goal_admissible, pcpodef_result) - else (goal_nonempty, goal_admissible, cpodef_result) - end - handle ERROR msg => - cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)); - - -(* proof interface *) - -local - -fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = - let - val (goal1, goal2, make_result) = - prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; - fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2); - in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; - -in - -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x; -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x; - -fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x; -fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x; - -end; - - - -(** outer syntax **) - -local structure P = OuterParse and K = OuterKeyword in - -val typedef_proof_decl = - Scan.optional (P.$$$ "(" |-- - ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) - --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- - Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); - -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = - (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) - ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs); - -val _ = - OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal - (typedef_proof_decl >> - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); - -val _ = - OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal - (typedef_proof_decl >> - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); - -end; - -end;