- Datatype package now also supports arbitrarily branching datatypes
(using function types).
- Added new simplification procedure for proving distinctness of
constructors.
- dtK is now a reference.
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Jul 16 12:14:04 1999 +0200
@@ -25,13 +25,10 @@
val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
- thm -> theory -> theory * string list * thm list
+ simpset -> thm -> theory -> theory * string list * thm list
val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
string list -> thm list -> theory -> theory * string list * thm list list
- val prove_distinctness_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- thm list list -> thm list list -> theory -> theory * thm list list
val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
thm list list -> thm list list -> thm list -> thm list list -> theory ->
@@ -97,10 +94,14 @@
(*************************** primrec combinators ******************************)
fun prove_primrec_thms flat_names new_type_names descr sorts
- (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
+ (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
let
val _ = message "Constructing primrec combinators ...";
+ val fun_rel_comp_name = Sign.intern_const (sign_of Relation.thy) "fun_rel_comp";
+ val [fun_rel_comp_def, o_def] =
+ map (get_thm Relation.thy) ["fun_rel_comp_def", "o_def"];
+
val big_name = space_implode "_" new_type_names;
val thy0 = add_path flat_names big_name thy;
@@ -123,9 +124,14 @@
val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let
- val recs = filter is_rec_type cargs;
- val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
- (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+
+ fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
+ | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
+ T --> nth_elem (k, rec_result_Ts);
+
+ val argTs = Ts @ map mk_argT recs
in argTs ---> nth_elem (i, rec_result_Ts)
end) constrs) descr');
@@ -141,22 +147,27 @@
fun make_rec_intr T set_name ((rec_intr_ts, l), (cname, cargs)) =
let
- fun mk_prem (dt, (j, k, prems, t1s, t2s)) =
- let
- val T = typ_of_dtyp descr' sorts dt;
- val free1 = mk_Free "x" T j
- in (case dt of
- DtRec m =>
+ fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
+ let val free1 = mk_Free "x" U j
+ in (case (dt, U) of
+ (DtRec m, _) =>
let val free2 = mk_Free "y" (nth_elem (m, rec_result_Ts)) k
in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem
(HOLogic.mk_prod (free1, free2), nth_elem (m, rec_sets))))::prems,
free1::t1s, free2::t2s)
end
+ | (DtType ("fun", [_, DtRec m]), U' as Type ("fun", [T', _])) =>
+ let val free2 = mk_Free "y" (T' --> nth_elem (m, rec_result_Ts)) k
+ in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem (free2,
+ Const (fun_rel_comp_name, [U', snd (strip_type (nth_elem (m, rec_set_Ts)))] --->
+ HOLogic.mk_setT (T' --> nth_elem (m, rec_result_Ts))) $
+ free1 $ nth_elem (m, rec_sets))))::prems, free1::t1s, free2::t2s)
+ end
| _ => (j + 1, k, prems, free1::t1s, t2s))
end;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs, (1, 1, [], [], []))
+ val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
(HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
@@ -170,7 +181,7 @@
val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
(InductivePackage.add_inductive_i false true big_rec_name' false false true
- rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
+ rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
(* prove uniqueness and termination of primrec combinators *)
@@ -181,9 +192,7 @@
val distinct_tac = (etac Pair_inject 1) THEN
(if i < length newTs then
full_simp_tac (HOL_ss addsimps (nth_elem (i, dist_rewrites))) 1
- else full_simp_tac (HOL_ss addsimps
- ((#distinct (the (Symtab.lookup (dt_info, tname)))) @
- [Suc_Suc_eq, Suc_not_Zero, Zero_not_Suc])) 1);
+ else full_simp_tac dist_ss 1);
val inject = map (fn r => r RS iffD1)
(if i < length newTs then nth_elem (i, constr_inject)
@@ -194,6 +203,7 @@
val k = length (filter is_rec_type cargs)
in (EVERY [DETERM tac,
+ REPEAT (dtac fun_rel_comp_unique 1),
REPEAT (etac ex1E 1), rtac ex1I 1,
DEPTH_SOLVE_1 (ares_tac [intr] 1),
REPEAT_DETERM_N k (etac thin 1),
@@ -252,10 +262,9 @@
(Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
Theory.add_defs_i (map (fn ((((name, comb), set), T), T') =>
- ((Sign.base_name name) ^ "_def", Logic.mk_equals
- (comb $ Free ("x", T),
+ ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
- HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))
+ HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
parent_path flat_names;
@@ -270,7 +279,8 @@
[rtac select1_equality 1,
resolve_tac rec_unique_thms 1,
resolve_tac rec_intrs 1,
- REPEAT (resolve_tac rec_total_thms 1)]))
+ rewrite_goals_tac [o_def, fun_rel_comp_def],
+ REPEAT ((rtac CollectI 1 THEN rtac allI 1) ORELSE resolve_tac rec_total_thms 1)]))
(DatatypeProp.make_primrecs new_type_names descr sorts thy2)
in
@@ -294,10 +304,13 @@
val newTs = take (length (hd descr), recTs);
val T' = TFree (variant used "'t", HOLogic.termS);
+ fun mk_dummyT (DtRec _) = T'
+ | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
+
val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val Ts' = replicate (length (filter is_rec_type cargs)) T'
+ val Ts' = map mk_dummyT (filter is_rec_type cargs)
in Const ("arbitrary", Ts @ Ts' ---> T')
end) constrs) descr';
@@ -312,7 +325,7 @@
val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val Ts' = Ts @ (replicate (length (filter is_rec_type cargs)) T');
+ val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
val frees = take (length cargs, frees');
val free = mk_Free "f" (Ts ---> T') j
@@ -350,80 +363,6 @@
(store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
end;
-(************************ distinctness of constructors ************************)
-
-fun prove_distinctness_thms flat_names new_type_names descr sorts dist_rewrites case_thms thy =
- let
- val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
-
- val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
- val newTs = take (length (hd descr), recTs);
-
- (*--------------------------------------------------------------------*)
- (* define t_ord - functions for proving distinctness of constructors: *)
- (* t_ord C_i ... = i *)
- (*--------------------------------------------------------------------*)
-
- fun define_ord ((thy, ord_defs), (((_, (_, _, constrs)), T), tname)) =
- if length constrs < DatatypeProp.dtK then (thy, ord_defs)
- else
- let
- val Tss = map ((map (typ_of_dtyp descr' sorts)) o snd) constrs;
- val ts = map HOLogic.mk_nat (0 upto length constrs - 1);
- val mk_abs = foldr (fn (T, t') => Abs ("x", T, t'));
- val fs = map mk_abs (Tss ~~ ts);
- val fTs = map (fn Ts => Ts ---> HOLogic.natT) Tss;
- val ord_name = Sign.full_name (Theory.sign_of thy) (tname ^ "_ord");
- val case_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_case");
- val ordT = T --> HOLogic.natT;
- val caseT = fTs ---> ordT;
- val defpair = (tname ^ "_ord_def", Logic.mk_equals
- (Const (ord_name, ordT), list_comb (Const (case_name, caseT), fs)));
- val thy' = thy |>
- Theory.add_consts_i [(tname ^ "_ord", ordT, NoSyn)] |>
- Theory.add_defs_i [defpair];
- val def = get_def thy' (tname ^ "_ord")
-
- in (thy', ord_defs @ [def]) end;
-
- val (thy2, ord_defs) =
- foldl define_ord ((thy1, []), (hd descr) ~~ newTs ~~ new_type_names);
-
- (**** number of constructors < dtK ****)
-
- fun prove_distinct_thms _ [] = []
- | prove_distinct_thms dist_rewrites' (t::_::ts) =
- let
- val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy2) t) (fn _ =>
- [simp_tac (HOL_ss addsimps dist_rewrites') 1])
- in dist_thm::(standard (dist_thm RS not_sym))::
- (prove_distinct_thms dist_rewrites' ts)
- end;
-
- val distinct_thms = map (fn ((((_, (_, _, constrs)), ts),
- dist_rewrites'), case_thms) =>
- if length constrs < DatatypeProp.dtK then
- prove_distinct_thms dist_rewrites' ts
- else
- let
- val t::ts' = rev ts;
- val (_ $ (_ $ (_ $ (f $ _) $ _))) = hd (Logic.strip_imp_prems t);
- val cert = cterm_of (Theory.sign_of thy2);
- val distinct_lemma' = cterm_instantiate
- [(cert distinct_f, cert f)] distinct_lemma;
- val rewrites = ord_defs @ (map mk_meta_eq case_thms)
- in
- (map (fn t => prove_goalw_cterm rewrites (cert t)
- (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma']
- end) ((hd descr) ~~ (DatatypeProp.make_distincts new_type_names
- descr sorts thy2) ~~ dist_rewrites ~~ case_thms)
-
- in
- (thy2 |> parent_path flat_names |>
- store_thmss "distinct" new_type_names distinct_thms,
- distinct_thms)
- end;
(******************************* case splitting *******************************)
@@ -465,6 +404,11 @@
(******************************* size functions *******************************)
fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
+ if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
+ (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) (flat descr)
+ then
+ (thy, [])
+ else
let
val _ = message "Proving equations for size function ...";
@@ -475,7 +419,7 @@
val recTs = get_rec_types descr' sorts;
val big_size_name = space_implode "_" new_type_names ^ "_size";
- val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy1))) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
val size_names = replicate (length (hd descr)) size_name @
map (Sign.full_name (Theory.sign_of thy1))
(if length (flat (tl descr)) = 1 then [big_size_name] else
--- a/src/HOL/Tools/datatype_aux.ML Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Fri Jul 16 12:14:04 1999 +0200
@@ -13,8 +13,6 @@
val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
- val get_thy : string -> theory -> theory option
-
val add_path : bool -> string -> theory -> theory
val parent_path : bool -> theory -> theory
@@ -28,6 +26,10 @@
val indtac : thm -> int -> tactic
val exh_tac : (string -> thm) -> int -> tactic
+ datatype simproc_dist = QuickAndDirty
+ | FewConstrs of thm list
+ | ManyConstrs of thm * simpset;
+
datatype dtyp =
DtTFree of string
| DtType of string * (dtyp list)
@@ -35,6 +37,7 @@
type datatype_info
+ exception Datatype
val dtyp_of_typ : (string * string list) list -> typ -> dtyp
val mk_Free : string -> typ -> int -> term
val is_rec_type : dtyp -> bool
@@ -46,14 +49,16 @@
val dest_conj : term -> term list
val get_nonrec_types : (int * (string * dtyp list *
(string * dtyp list) list)) list -> (string * sort) list -> typ list
+ val get_branching_types : (int * (string * dtyp list *
+ (string * dtyp list) list)) list -> (string * sort) list -> typ list
val get_rec_types : (int * (string * dtyp list *
(string * dtyp list) list)) list -> (string * sort) list -> typ list
val check_nonempty : (int * (string * dtyp list *
(string * dtyp list) list)) list list -> unit
val unfold_datatypes :
- datatype_info Symtab.table ->
- (int * (string * dtyp list *
- (string * dtyp list) list)) list -> int ->
+ Sign.sg -> (int * (string * dtyp list * (string * dtyp list) list)) list ->
+ (string * sort) list -> datatype_info Symtab.table ->
+ (int * (string * dtyp list * (string * dtyp list) list)) list -> int ->
(int * (string * dtyp list *
(string * dtyp list) list)) list list * int
end;
@@ -67,9 +72,6 @@
(* FIXME: move to library ? *)
fun foldl1 f (x::xs) = foldl f (x, xs);
-fun get_thy name thy = find_first
- (equal name o Sign.name_of o Theory.sign_of) (Theory.ancestors_of thy);
-
fun add_path flat_names s = if flat_names then I else Theory.add_path s;
fun parent_path flat_names = if flat_names then I else Theory.parent_path;
@@ -92,7 +94,7 @@
(* split theorem thm_1 & ... & thm_n into n theorems *)
fun split_conj_thm th =
- ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle _ => [th];
+ ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
val mk_conj = foldr1 (HOLogic.mk_binop "op &");
val mk_disj = foldr1 (HOLogic.mk_binop "op |");
@@ -138,6 +140,12 @@
in compose_tac (false, exhaustion', nprems_of exhaustion) i state
end;
+(* handling of distinctness theorems *)
+
+datatype simproc_dist = QuickAndDirty
+ | FewConstrs of thm list
+ | ManyConstrs of thm * simpset;
+
(********************** Internal description of datatypes *********************)
datatype dtyp =
@@ -157,7 +165,7 @@
case_rewrites : thm list,
induction : thm,
exhaustion : thm,
- distinct : thm list,
+ distinct : simproc_dist,
inject : thm list,
nchotomy : thm,
case_cong : thm};
@@ -172,8 +180,13 @@
DtType (name, map (subst_DtTFree i substs) ts)
| subst_DtTFree i _ (DtRec j) = DtRec (i + j);
-fun dest_DtTFree (DtTFree a) = a;
-fun dest_DtRec (DtRec i) = i;
+exception Datatype;
+
+fun dest_DtTFree (DtTFree a) = a
+ | dest_DtTFree _ = raise Datatype;
+
+fun dest_DtRec (DtRec i) = i
+ | dest_DtRec _ = raise Datatype;
fun is_rec_type (DtType (_, dts)) = exists is_rec_type dts
| is_rec_type (DtRec _) = true
@@ -201,6 +214,7 @@
fun get_nonrec_types descr sorts =
let fun add (Ts, T as DtTFree _) = T ins Ts
+ | add (Ts, T as DtType ("fun", [_, DtRec _])) = Ts
| add (Ts, T as DtType _) = T ins Ts
| add (Ts, _) = Ts
in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
@@ -213,6 +227,16 @@
fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
+(* get all branching types *)
+
+fun get_branching_types descr sorts =
+ let fun add (Ts, DtType ("fun", [T, DtRec _])) = T ins Ts
+ | add (Ts, _) = Ts
+ in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
+ foldl (fn (Ts', (_, cargs)) =>
+ foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
+ end;
+
(* nonemptiness check for datatypes *)
fun check_nonempty descr =
@@ -223,6 +247,7 @@
val (_, _, constrs) = the (assoc (descr', i));
fun arg_nonempty (DtRec i) = if i mem is then false
else is_nonempty_dt (i::is) i
+ | arg_nonempty (DtType ("fun", [_, T])) = arg_nonempty T
| arg_nonempty _ = true;
in exists ((forall arg_nonempty) o snd) constrs
end
@@ -234,16 +259,19 @@
(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
(* need to be unfolded *)
-fun unfold_datatypes (dt_info : datatype_info Symtab.table) descr i =
+fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
let
- fun get_dt_descr i tname dts =
+ fun typ_error T msg = error ("Non-admissible type expression\n" ^
+ Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
+
+ fun get_dt_descr T i tname dts =
(case Symtab.lookup (dt_info, tname) of
- None => error (tname ^ " is not a datatype - can't use it in\
- \ indirect recursion")
+ None => typ_error T (tname ^ " is not a datatype - can't use it in\
+ \ nested recursion")
| (Some {index, descr, ...}) =>
let val (_, vars, _) = the (assoc (descr, index));
- val subst = ((map dest_DtTFree vars) ~~ dts) handle _ =>
- error ("Type constructor " ^ tname ^ " used with wrong\
+ val subst = ((map dest_DtTFree vars) ~~ dts) handle LIST _ =>
+ typ_error T ("Type constructor " ^ tname ^ " used with wrong\
\ number of arguments")
in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
(tn, map (subst_DtTFree i subst) args,
@@ -254,9 +282,18 @@
fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
if is_rec_type T then
- let val (index, descr) = get_dt_descr i tname dts;
- val (descr', i') = unfold_datatypes dt_info descr (i + length descr)
- in (i', Ts @ [DtRec index], descrs @ descr') end
+ if tname = "fun" then
+ if is_rec_type (hd dts) then
+ typ_error T "Non-strictly positive recursive occurrence of type"
+ else
+ (case hd (tl dts) of
+ DtType ("fun", _) => typ_error T "Curried function types not allowed"
+ | T' => let val (i', [T''], descrs') = unfold_arg ((i, [], descrs), T')
+ in (i', Ts @ [DtType (tname, [hd dts, T''])], descrs') end)
+ else
+ let val (index, descr) = get_dt_descr T i tname dts;
+ val (descr', i') = unfold_datatypes sign orig_descr sorts dt_info descr (i + length descr)
+ in (i', Ts @ [DtRec index], descrs @ descr') end
else (i, Ts @ [T], descrs)
| unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
--- a/src/HOL/Tools/datatype_package.ML Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Jul 16 12:14:04 1999 +0200
@@ -11,6 +11,7 @@
val mutual_induct_tac : string list -> int -> tactic
val induct_tac : string -> int -> tactic
val exhaust_tac : string -> int -> tactic
+ val distinct_simproc : simproc
end;
signature DATATYPE_PACKAGE =
@@ -63,9 +64,12 @@
simps : thm list}
val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
val print_datatypes : theory -> unit
- val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info
- val datatype_info : theory -> string -> DatatypeAux.datatype_info
+ val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info option
+ val datatype_info : theory -> string -> DatatypeAux.datatype_info option
+ val datatype_info_sg_err : Sign.sg -> string -> DatatypeAux.datatype_info
+ val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
val constrs_of : theory -> string -> term list option
+ val constrs_of_sg : Sign.sg -> string -> term list option
val case_const_of : theory -> string -> term option
val setup: (theory -> theory) list
end;
@@ -104,28 +108,31 @@
(** theory information about datatypes **)
-fun datatype_info_sg sg name =
- (case Symtab.lookup (get_datatypes_sg sg, name) of
- Some info => info
- | None => error ("Unknown datatype " ^ quote name));
+fun datatype_info_sg sg name = Symtab.lookup (get_datatypes_sg sg, name);
+
+fun datatype_info_sg_err sg name = (case datatype_info_sg sg name of
+ Some info => info
+ | None => error ("Unknown datatype " ^ quote name));
val datatype_info = datatype_info_sg o Theory.sign_of;
-fun constrs_of thy tname =
- let
- val {index, descr, ...} = datatype_info thy tname;
- val (_, _, constrs) = the (assoc (descr, index))
- in
- Some (map (fn (cname, _) =>
- Const (cname, the (Sign.const_type (Theory.sign_of thy) cname))) constrs)
- end handle _ => None;
+fun datatype_info_err thy name = (case datatype_info thy name of
+ Some info => info
+ | None => error ("Unknown datatype " ^ quote name));
-fun case_const_of thy tname =
- let
- val {case_name, ...} = datatype_info thy tname;
- in
- Some (Const (case_name, the (Sign.const_type (Theory.sign_of thy) case_name)))
- end handle _ => None;
+fun constrs_of_sg sg tname = (case datatype_info_sg sg tname of
+ Some {index, descr, ...} =>
+ let val (_, _, constrs) = the (assoc (descr, index))
+ in Some (map (fn (cname, _) => Const (cname, the (Sign.const_type sg cname))) constrs)
+ end
+ | _ => None);
+
+val constrs_of = constrs_of_sg o Theory.sign_of;
+
+fun case_const_of thy tname = (case datatype_info thy tname of
+ Some {case_name, ...} => Some (Const (case_name, the (Sign.const_type
+ (Theory.sign_of thy) case_name)))
+ | _ => None);
fun find_tname var Bi =
let val frees = map dest_Free (term_frees Bi)
@@ -168,7 +175,7 @@
val (_, _, Bi, _) = dest_state (state, i);
val {sign, ...} = rep_thm state;
val tn = find_tname (hd vars) Bi;
- val {induction, ...} = datatype_info_sg sign tn;
+ val {induction, ...} = datatype_info_sg_err sign tn;
val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
implode (tl (explode (Syntax.string_of_vname ixn))))
(dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
@@ -186,7 +193,7 @@
let
val {sign, ...} = rep_thm state;
val tn = infer_tname state sign i aterm;
- val {exhaustion, ...} = datatype_info_sg sign tn;
+ val {exhaustion, ...} = datatype_info_sg_err sign tn;
val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
(hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
@@ -195,6 +202,61 @@
end;
+(**** simplification procedure for showing distinctness of constructors ****)
+
+(* oracle *)
+
+val distinctN = "constr_distinct";
+
+exception ConstrDistinct of term;
+
+
+fun distinct_proc sg _ (t as Const ("op =", _) $ t1 $ t2) =
+ (case (pairself strip_comb (t1, t2)) of
+ ((Const (cname1, _), xs), (Const (cname2, _), ys)) =>
+ (case (fastype_of t1, fastype_of t2) of
+ (Type (tname1, _), Type (tname2, _)) =>
+ if tname1 = tname2 andalso not (cname1 = cname2) then
+ (case (constrs_of_sg sg tname1) of
+ Some constrs => let val cnames = map (fst o dest_Const) constrs
+ in if cname1 mem cnames andalso cname2 mem cnames then
+ let val eq_t = Logic.mk_equals (t, Const ("False", HOLogic.boolT));
+ val eq_ct = cterm_of sg eq_t;
+ val Datatype_thy = theory "Datatype";
+ val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
+ map (get_thm Datatype_thy)
+ ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
+ in (case (#distinct (datatype_info_sg_err sg tname1)) of
+ QuickAndDirty => Some (Thm.invoke_oracle
+ Datatype_thy distinctN (sg, ConstrDistinct eq_t))
+ | FewConstrs thms => Some (prove_goalw_cterm [] eq_ct (K
+ [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
+ atac 2, resolve_tac thms 1, etac FalseE 1]))
+ | ManyConstrs (thm, ss) => Some (prove_goalw_cterm [] eq_ct (K
+ [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
+ full_simp_tac ss 1,
+ REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
+ eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
+ etac FalseE 1])))
+ end
+ else None
+ end
+ | None => None)
+ else None
+ | _ => None)
+ | _ => None)
+ | distinct_proc sg _ _ = None;
+
+val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termTVar)];
+val distinct_simproc = mk_simproc "distinct_simproc" distinct_pats distinct_proc;
+
+val dist_ss = HOL_ss addsimprocs [distinct_simproc];
+
+val simproc_setup =
+ [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
+ fn thy => (simpset_ref_of thy := simpset_of thy addsimprocs [distinct_simproc]; thy)];
+
+
(* prepare types *)
fun read_typ sign ((Ts, sorts), str) =
@@ -240,7 +302,7 @@
fun clasimp addDistinct ([], _) = clasimp
| clasimp addDistinct (thms::thmss, (_, (_, _, constrs))::descr) =
- if length constrs < DatatypeProp.dtK then
+ if length constrs < !DatatypeProp.dtK then
clasimp addIffs thms addDistinct (thmss, descr)
else
clasimp addsimps2 thms addDistinct (thmss, descr);
@@ -275,6 +337,9 @@
val used = foldr add_typ_tfree_names (recTs, []);
val newTs = take (length (hd descr), recTs);
+ val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
+ (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) descr';
+
(**** declare new types and constants ****)
val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
@@ -290,9 +355,14 @@
val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let
- val recs = filter is_rec_type cargs;
- val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
- (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+
+ fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
+ | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
+ T --> nth_elem (k, rec_result_Ts);
+
+ val argTs = Ts @ map mk_argT recs
in argTs ---> nth_elem (i, rec_result_Ts)
end) constrs) descr');
@@ -341,19 +411,11 @@
val thy2 = thy2' |>
- (** t_ord functions **)
-
- Theory.add_consts_i
- (foldr (fn ((((_, (_, _, constrs)), tname), T), decls) =>
- if length constrs < DatatypeProp.dtK then decls
- else (tname ^ "_ord", T --> HOLogic.natT, NoSyn)::decls)
- ((hd descr) ~~ new_type_names ~~ newTs, [])) |>
-
(** size functions **)
- Theory.add_consts_i (map (fn (s, T) =>
+ (if no_size then I else Theory.add_consts_i (map (fn (s, T) =>
(Sign.base_name s, T --> HOLogic.natT, NoSyn))
- (size_names ~~ drop (length (hd descr), recTs))) |>
+ (size_names ~~ drop (length (hd descr), recTs)))) |>
(** constructors **)
@@ -370,19 +432,19 @@
(**** introduction of axioms ****)
val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
- val size_axs = DatatypeProp.make_size new_type_names descr sorts thy2;
+ val size_axs = if no_size then [] else DatatypeProp.make_size new_type_names descr sorts thy2;
val (thy3, inject) = thy2 |>
Theory.add_path (space_implode "_" new_type_names) |>
PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
- PureThy.add_axiomss_i [(("size", size_axs), [])] |>
+ (if no_size then I else PureThy.add_axiomss_i [(("size", size_axs), [])]) |>
Theory.parent_path |>
add_and_get_axiomss "inject" new_type_names
(DatatypeProp.make_injs descr sorts);
val induct = get_axiom thy3 "induct";
val rec_thms = get_thms thy3 "recs";
- val size_thms = get_thms thy3 "size";
+ val size_thms = if no_size then [] else get_thms thy3 "size";
val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
(DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
@@ -401,7 +463,8 @@
val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
- exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+ exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
+ nchotomys ~~ case_congs);
val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
@@ -413,7 +476,7 @@
val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
- addIffs flat inject addDistinct (distinct, hd descr));
+ addIffs flat (inject @ distinct));
in
(thy11,
@@ -435,18 +498,16 @@
let
val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
- val (thy2, inject, dist_rewrites, induct) = thy |>
+ val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |>
DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
types_syntax constr_syntax;
val (thy3, casedist_thms) =
DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
- flat_names new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
- val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
+ flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
+ val (thy6, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
- val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
- flat_names new_type_names descr sorts dist_rewrites case_thms thy5;
val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
descr sorts inject dist_rewrites casedist_thms case_thms thy6;
val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
@@ -458,7 +519,7 @@
val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
- casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+ casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs);
val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
@@ -470,7 +531,7 @@
val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
- addIffs flat inject addDistinct (distinct, hd descr));
+ addIffs flat (inject @ distinct));
in
(thy11,
@@ -505,7 +566,7 @@
Sign.string_of_term sign t);
fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
- ((tname, map dest_TFree Ts) handle _ => err t)
+ ((tname, map dest_TFree Ts) handle TERM _ => err t)
| get_typ t = err t;
val dtnames = map get_typ (dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
@@ -535,7 +596,7 @@
val (thy2, casedist_thms) = thy1 |>
DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
- false new_type_names [descr] sorts dt_info inject distinct induction thy2;
+ false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
new_type_names [descr] sorts reccomb_names rec_thms thy3;
val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
@@ -552,7 +613,7 @@
val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
- casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+ casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs);
val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
@@ -564,7 +625,7 @@
val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
- addIffs flat inject addDistinct (distinct, descr));
+ addIffs flat (inject @ distinct));
in
(thy9,
@@ -641,10 +702,10 @@
end;
val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
+ val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
val dt_info = get_datatypes thy;
- val (descr, _) = unfold_datatypes dt_info dts' i;
+ val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
val _ = check_nonempty descr;
- val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
in
(if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
@@ -659,7 +720,7 @@
(* setup theory *)
-val setup = [DatatypesData.init];
+val setup = [DatatypesData.init] @ simproc_setup;
(* outer syntax *)
--- a/src/HOL/Tools/datatype_prop.ML Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Fri Jul 16 12:14:04 1999 +0200
@@ -8,7 +8,7 @@
signature DATATYPE_PROP =
sig
- val dtK : int
+ val dtK : int ref
val make_injs : (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
term list list
@@ -46,7 +46,7 @@
open DatatypeAux;
(*the kind of distinctiveness axioms depends on number of constructors*)
-val dtK = 7;
+val dtK = ref 7;
fun make_tnames Ts =
let
@@ -110,14 +110,19 @@
fun make_ind_prem k T (cname, cargs) =
let
+ fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
+ (make_pred k T $ Free (s, T))
+ | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
+ HOLogic.mk_Trueprop (HOLogic.all_const T $
+ Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0)));
+
val recs = filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val recTs' = map (typ_of_dtyp descr' sorts) recs;
val tnames = variantlist (make_tnames Ts, pnames);
val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
- val prems = map (fn ((r, s), T) => HOLogic.mk_Trueprop
- (make_pred (dest_DtRec r) T $ Free (s, T))) (recs ~~ rec_tnames ~~ recTs');
+ val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
in list_all_free (frees, Logic.list_implies (prems,
HOLogic.mk_Trueprop (make_pred k T $
@@ -162,6 +167,8 @@
fun make_primrecs new_type_names descr sorts thy =
let
+ val o_name = Sign.intern_const (sign_of Fun.thy) "op o";
+
val sign = Theory.sign_of thy;
val descr' = flat descr;
@@ -174,9 +181,14 @@
val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let
- val recs = filter is_rec_type cargs;
- val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
- (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+
+ fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
+ | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
+ T --> nth_elem (k, rec_result_Ts);
+
+ val argTs = Ts @ map mk_argT recs
in argTs ---> nth_elem (i, rec_result_Ts)
end) constrs) descr');
@@ -201,7 +213,14 @@
val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (rec_tnames ~~ recTs');
- val reccombs' = map (fn (DtRec i) => nth_elem (i, reccombs)) recs
+
+ fun mk_reccomb (DtRec i, _) = nth_elem (i, reccombs)
+ | mk_reccomb (DtType ("fun", [_, DtRec i]), Type ("fun", [T, U])) =
+ let val T' = nth_elem (i, rec_result_Ts)
+ in Const (o_name, [U --> T', T --> U, T] ---> T') $ nth_elem (i, reccombs)
+ end;
+
+ val reccombs' = map mk_reccomb (recs ~~ recTs')
in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
(comb_t $ list_comb (Const (cname, Ts ---> T), frees),
@@ -292,35 +311,12 @@
in (make_distincts' constrs) @ (make_distincts_1 T constrs)
end;
- (**** number of constructors >= dtK : t_ord C_i ... = i ****)
-
- fun make_distincts_2 T tname i constrs =
- let
- val ord_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_ord");
- val ord_t = Const (ord_name, T --> HOLogic.natT)
-
- in (case constrs of
- [] => [Logic.mk_implies (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
- (ord_t $ Free ("x", T), ord_t $ Free ("y", T))),
- HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
- (Free ("x", T), Free ("y", T))))]
- | ((cname, cargs)::constrs) =>
- let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val frees = map Free ((make_tnames Ts) ~~ Ts);
- in
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (ord_t $
- list_comb (Const (cname, Ts ---> T), frees), HOLogic.mk_nat i)))::
- (make_distincts_2 T tname (i + 1) constrs)
- end)
- end;
-
in map (fn (((_, (_, _, constrs)), T), tname) =>
- if length constrs < dtK then make_distincts_1 T constrs
- else make_distincts_2 T tname 0 constrs)
+ if length constrs < !dtK then make_distincts_1 T constrs else [])
((hd descr) ~~ newTs ~~ new_type_names)
end;
+
(*************************** the "split" - equations **************************)
fun make_splits new_type_names descr sorts thy =
@@ -403,7 +399,7 @@
val recTs = get_rec_types descr' sorts;
val big_size_name = space_implode "_" new_type_names ^ "_size";
- val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy))) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
val size_names = replicate (length (hd descr)) size_name @
map (Sign.intern_const (Theory.sign_of thy))
(if length (flat (tl descr)) = 1 then [big_size_name] else
--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Jul 16 12:14:04 1999 +0200
@@ -12,13 +12,16 @@
*)
+val foo = ref [TrueI];
+
signature DATATYPE_REP_PROOFS =
sig
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
(string * mixfix) list -> (string * mixfix) list list -> theory ->
- theory * thm list list * thm list list * thm
+ theory * thm list list * thm list list * thm list list *
+ DatatypeAux.simproc_dist list * thm
end;
structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -43,15 +46,22 @@
fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
new_type_names descr sorts types_syntax constr_syntax thy =
let
- val Univ_thy = the (get_thy "Univ" thy);
- val node_name = Sign.intern_tycon (Theory.sign_of Univ_thy) "node";
- val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name] =
- map (Sign.intern_const (Theory.sign_of Univ_thy))
- ["In0", "In1", "Scons", "Leaf", "Numb"];
+ val Datatype_thy = theory "Datatype";
+ val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
+ val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
+ Funs_name, o_name] =
+ map (Sign.intern_const (Theory.sign_of Datatype_thy))
+ ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"];
+
val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
- In0_not_In1, In1_not_In0] = map (get_thm Univ_thy)
- ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq",
- "In1_eq", "In0_not_In1", "In1_not_In0"];
+ In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
+ Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy)
+ ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
+ "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
+ "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"];
+
+ val Funs_IntE = (Int_lower2 RS Funs_mono RS
+ (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
val descr' = flat descr;
@@ -65,19 +75,23 @@
val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
val leafTs' = get_nonrec_types descr' sorts;
- val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs', []);
+ val branchTs = get_branching_types descr' sorts;
+ val branchT = if null branchTs then HOLogic.unitT
+ else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
+ val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
val recTs = get_rec_types descr' sorts;
val newTs = take (length (hd descr), recTs);
val oldTs = drop (length (hd descr), recTs);
val sumT = if null leafTs then HOLogic.unitT
else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
- val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT]));
+ val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
val UnivT = HOLogic.mk_setT Univ_elT;
val In0 = Const (In0_name, Univ_elT --> Univ_elT);
val In1 = Const (In1_name, Univ_elT --> Univ_elT);
val Leaf = Const (Leaf_name, sumT --> Univ_elT);
+ val Lim = Const (Lim_name, (branchT --> Univ_elT) --> Univ_elT);
(* make injections needed for embedding types in leaves *)
@@ -103,6 +117,25 @@
else
foldr1 (HOLogic.mk_binop Scons_name) ts);
+ (* function spaces *)
+
+ fun mk_fun_inj T' x =
+ let
+ fun mk_inj T n i =
+ if n = 1 then x else
+ let
+ val n2 = n div 2;
+ val Type (_, [T1, T2]) = T;
+ val sum_case = Const ("sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
+ in
+ if i <= n2 then
+ sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
+ else
+ sum_case $ Const ("arbitrary", T1 --> Univ_elT) $ mk_inj T2 (n - n2) (i - n2)
+ end
+ in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
+ end;
+
(************** generate introduction rules for representing set **********)
val _ = message "Constructing representing sets ...";
@@ -116,6 +149,14 @@
in (j + 1, (HOLogic.mk_mem (free_t,
Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
end
+ | mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) =
+ let val T' = typ_of_dtyp descr' sorts T;
+ val free_t = mk_Free "x" (T' --> Univ_elT) j
+ in (j + 1, (HOLogic.mk_mem (free_t,
+ Const (Funs_name, UnivT --> HOLogic.mk_setT (T' --> Univ_elT)) $
+ Const (nth_elem (k, rep_set_names), UnivT)))::prems,
+ Lim $ mk_fun_inj T' free_t::ts)
+ end
| mk_prem (dt, (j, prems, ts)) =
let val T = typ_of_dtyp descr' sorts dt
in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
@@ -136,16 +177,17 @@
val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
(InductivePackage.add_inductive_i false true big_rec_name false true false
- consts [] (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
+ consts [] (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
(********************************* typedef ********************************)
val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
setmp TypedefPackage.quiet_mode true
(TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
- (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1)))) thy)
- (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
- new_type_names));
+ (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1)
+ (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy)
+ (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
+ (take (length newTs, consts)) ~~ new_type_names));
(*********************** definition of constructors ***********************)
@@ -171,6 +213,13 @@
in (case dt of
DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
T --> Univ_elT) $ free_t)::r_args)
+ | DtType ("fun", [T', DtRec m]) =>
+ let val ([T''], T''') = strip_type T
+ in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T''
+ (Const (o_name, [T''' --> Univ_elT, T, T''] ---> Univ_elT) $
+ Const (nth_elem (m, all_rep_names), T''' --> Univ_elT) $ free_t))::r_args)
+ end
+
| _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
end;
@@ -200,8 +249,8 @@
val sg = Theory.sign_of thy;
val rep_const = cterm_of sg
(Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
- val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
- val dist = cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma;
+ val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong);
+ val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma);
val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
in
@@ -282,23 +331,34 @@
val rep_const = Const (rep_name, T --> Univ_elT);
val constr = Const (cname, argTs ---> T);
- fun process_arg ks' ((i2, i2', ts), dt) =
+ fun process_arg ks' ((i2, i2', ts, Ts), dt) =
let val T' = typ_of_dtyp descr' sorts dt
in (case dt of
DtRec j => if j mem ks' then
- (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'])
+ (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT])
else
(i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
- T' --> Univ_elT) $ mk_Free "x" T' i2])
- | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)]))
+ T' --> Univ_elT) $ mk_Free "x" T' i2], Ts)
+ | (DtType ("fun", [_, DtRec j])) =>
+ let val ([T''], T''') = strip_type T'
+ in if j mem ks' then
+ (i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T''
+ (mk_Free "y" (T'' --> Univ_elT) i2')], Ts @ [T'' --> Univ_elT])
+ else
+ (i2 + 1, i2', ts @ [Lim $ mk_fun_inj T''
+ (Const (o_name, [T''' --> Univ_elT, T', T''] ---> Univ_elT) $
+ Const (nth_elem (j, all_rep_names), T''' --> Univ_elT) $
+ mk_Free "x" T' i2)], Ts)
+ end
+ | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
end;
- val (i2, i2', ts) = foldl (process_arg ks) ((1, 1, []), cargs);
+ val (i2, i2', ts, Ts) = foldl (process_arg ks) ((1, 1, [], []), cargs);
val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
- val ys = map (mk_Free "y" Univ_elT) (1 upto (i2' - 1));
+ val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
- val (_, _, ts') = foldl (process_arg []) ((1, 1, []), cargs);
+ val (_, _, ts', _) = foldl (process_arg []) ((1, 1, [], []), cargs);
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
(rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i))
@@ -340,6 +400,21 @@
(* prove isomorphism properties *)
+ fun mk_funs_inv thm =
+ let
+ val [_, t] = prems_of Funs_inv;
+ val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t;
+ val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t;
+ val [_ $ (_ $ _ $ R')] = prems_of thm;
+ val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm;
+ val inv' = cterm_instantiate (map
+ ((pairself (cterm_of (sign_of_thm thm))) o
+ (apsnd (map_term_types (incr_tvar 1))))
+ [(R, R'), (r, r'), (a, a')]) Funs_inv
+ in
+ rule_by_tactic (atac 2) (thm RSN (2, inv'))
+ end;
+
(* prove x : dt_rep_set_i --> x : range dt_Rep_i *)
fun mk_iso_t (((set_name, iso_name), i), T) =
@@ -355,8 +430,6 @@
val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
(rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
- val newT_Abs_inverse_thms = map (fn (iso, _, _) => iso RS subst) newT_iso_axms;
-
(* all the theorems are proved by one single simultaneous induction *)
val iso_thms = if length descr = 1 then [] else
@@ -365,14 +438,19 @@
[indtac rep_induct 1,
REPEAT (rtac TrueI 1),
REPEAT (EVERY
- [REPEAT (etac rangeE 1),
- REPEAT (eresolve_tac newT_Abs_inverse_thms 1),
+ [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
+ REPEAT (etac Funs_IntE 1),
+ REPEAT (eresolve_tac [rangeE, Funs_rangeE] 1),
+ REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
+ map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
TRY (hyp_subst_tac 1),
rtac (sym RS range_eqI) 1,
resolve_tac iso_char_thms 1])])));
- val Abs_inverse_thms = newT_Abs_inverse_thms @ (map (fn r =>
- r RS mp RS f_inv_f RS subst) iso_thms);
+ val Abs_inverse_thms' = (map #1 newT_iso_axms) @ map (fn r => r RS mp RS f_inv_f) iso_thms;
+
+ val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
+ map mk_funs_inv Abs_inverse_thms');
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *)
@@ -395,7 +473,7 @@
val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
val rewrites = map mk_meta_eq iso_char_thms;
- val inj_thms' = map (fn r => r RS injD) inj_thms;
+ val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o]) inj_thms);
val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
(HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
@@ -411,8 +489,9 @@
ORELSE (EVERY
[REPEAT (etac Scons_inject 1),
REPEAT (dresolve_tac
- (inj_thms' @ [Leaf_inject, Inl_inject, Inr_inject]) 1),
- REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
+ (inj_thms' @ [Leaf_inject, Lim_inject, Inl_inject, Inr_inject]) 1),
+ REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
+ (dtac inj_fun_lemma 1 THEN atac 1)),
TRY (hyp_subst_tac 1),
rtac refl 1])])])]);
@@ -425,11 +504,11 @@
(HOLogic.mk_Trueprop (mk_conj ind_concl2)))
(fn _ =>
[indtac induction 1,
- rewrite_goals_tac rewrites,
+ rewrite_goals_tac (o_def :: rewrites),
REPEAT (EVERY
[resolve_tac rep_intrs 1,
- REPEAT ((atac 1) ORELSE
- (resolve_tac elem_thms 1))])]);
+ REPEAT (FIRST [atac 1, etac spec 1,
+ resolve_tac (FunsI :: elem_thms) 1])])]);
in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm))
end;
@@ -446,19 +525,18 @@
fun prove_constr_rep_thm eqn =
let
val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
- val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
+ val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
rtac refl 1,
resolve_tac rep_intrs 2,
- REPEAT (resolve_tac iso_elem_thms 1)])
+ REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)])
end;
(*--------------------------------------------------------------*)
(* constr_rep_thms and rep_congs are used to prove distinctness *)
- (* of constructors internally. *)
- (* the external version uses dt_case which is not defined yet *)
+ (* of constructors. *)
(*--------------------------------------------------------------*)
val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns;
@@ -467,27 +545,45 @@
dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
(constr_rep_thms ~~ dist_lemmas);
+ fun prove_distinct_thms (_, []) = []
+ | prove_distinct_thms (dist_rewrites', t::_::ts) =
+ let
+ val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
+ [simp_tac (HOL_ss addsimps dist_rewrites') 1])
+ in dist_thm::(standard (dist_thm RS not_sym))::
+ (prove_distinct_thms (dist_rewrites', ts))
+ end;
+
+ val distinct_thms = map prove_distinct_thms (dist_rewrites ~~
+ DatatypeProp.make_distincts new_type_names descr sorts thy5);
+
+ val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
+ if length constrs < !DatatypeProp.dtK then FewConstrs dists
+ else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
+ constr_rep_thms ~~ rep_congs ~~ distinct_thms);
+
(* prove injectivity of constructors *)
fun prove_constr_inj_thm rep_thms t =
- let val inj_thms = Scons_inject::(map make_elim
+ let val inj_thms = Scons_inject::sum_case_inject::(map make_elim
((map (fn r => r RS injD) iso_inj_thms) @
- [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject]))
+ [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject]))
in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
[rtac iffI 1,
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
dresolve_tac rep_congs 1, dtac box_equals 1,
- REPEAT (resolve_tac rep_thms 1),
+ REPEAT (resolve_tac rep_thms 1), rewrite_goals_tac [o_def],
REPEAT (eresolve_tac inj_thms 1),
- hyp_subst_tac 1,
- REPEAT (resolve_tac [conjI, refl] 1)])
+ REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
+ eresolve_tac inj_thms 1, atac 1]))])
end;
val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
- val thy6 = store_thmss "inject" new_type_names
- constr_inject (parent_path flat_names thy5);
+ val thy6 = thy5 |> parent_path flat_names |>
+ store_thmss "inject" new_type_names constr_inject |>
+ store_thmss "distinct" new_type_names distinct_thms;
(*************************** induction theorem ****************************)
@@ -538,17 +634,18 @@
(DatatypeProp.make_ind descr sorts)) (fn prems =>
[rtac indrule_lemma' 1, indtac rep_induct 1,
EVERY (map (fn (prem, r) => (EVERY
- [REPEAT (eresolve_tac Abs_inverse_thms 1),
+ [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
- DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
- (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
+ DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewrite_goals_tac [o_def],
+ rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
+ (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
val thy7 = thy6 |>
Theory.add_path big_name |>
PureThy.add_thms [(("induct", dt_induct), [])] |>
Theory.parent_path;
- in (thy7, constr_inject, dist_rewrites, dt_induct)
+ in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct)
end;
end;