--- 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
--- 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
--- 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
--- 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 ...";
--- 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);
--- 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
--- 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)) =>
--- 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);
--- 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;
--- 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;
--- 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", []);
--- 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;
--- 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")
--- 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;
--- 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<total then
(offset+1, Leaf ((replicate offset False) @ True ::
@@ -2421,9 +2405,6 @@
(* mutually recursive types must have the same type *)
(* parameters, unless the mutual recursion comes from *)
(* indirect recursion *)
- (* (DatatypeAux.dtyp * Term.typ) list ->
- (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 *)
--- 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
--- 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;
--- 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
--- 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}),
--- 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
--- /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;
--- 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;
--- 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
--- 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
--- 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
--- 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 *)
--- /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;
--- 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;
--- /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;
--- 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;