--- a/src/HOL/BNF/BNF_Util.thy Thu Nov 14 19:54:10 2013 +0100
+++ b/src/HOL/BNF/BNF_Util.thy Thu Nov 14 20:55:09 2013 +0100
@@ -9,7 +9,7 @@
header {* Library for Bounded Natural Functors *}
theory BNF_Util
-imports Ctr_Sugar "../Cardinals/Cardinal_Arithmetic"
+imports "../Cardinals/Cardinal_Arithmetic"
begin
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML Thu Nov 14 19:54:10 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Thu Nov 14 20:55:09 2013 +0100
@@ -49,7 +49,7 @@
SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
| _ => not_datatype s);
- val fp_sugar0 as {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1;
+ val {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1;
val fpT_names' = map (fst o dest_Type) fpTs0;
val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
@@ -82,7 +82,7 @@
fold add_nested_types_of subTs (seen @ mutual_Ts)
end
| NONE => error ("Unsupported recursion via type constructor " ^ quote s ^
- " not associated with new-style datatype (cf. \"datatype_new\")"));
+ " not corresponding to new-style datatype (cf. \"datatype_new\")"));
val Ts = add_nested_types_of fpT1 [];
val b_names = map base_name_of_typ Ts;
@@ -92,7 +92,7 @@
val nn_fp = length fpTs;
val nn = length Ts;
val get_indices = K [];
- val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
+ val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
val callssss = map (fn fp_sugar0 => indexify_callsss fp_sugar0 []) fp_sugars0;
val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
@@ -105,15 +105,13 @@
fp_sugars;
val inducts = conj_dests nn induct;
- val frozen_Ts = map Type.legacy_freeze_type Ts;
- val mk_dtyp = dtyp_of_typ frozen_Ts;
+ val mk_dtyp = dtyp_of_typ Ts;
- fun mk_ctr_descr (Const (s, T)) =
- (s, map mk_dtyp (binder_types (Type.legacy_freeze_type T)));
+ fun mk_ctr_descr Ts = mk_ctr Ts #> dest_Const ##> (binder_types #> map mk_dtyp);
fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
- (index, (T_name, map mk_dtyp Ts, map mk_ctr_descr ctrs));
+ (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
- val descr = map3 mk_typ_descr (0 upto nn - 1) frozen_Ts ctr_sugars;
+ val descr = map3 mk_typ_descr (0 upto nn - 1) Ts ctr_sugars;
val recs = map (fst o dest_Const o co_rec_of) co_iterss;
val rec_thms = flat (map co_rec_of iter_thmsss);
--- a/src/HOL/BNF/Tools/bnf_util.ML Thu Nov 14 19:54:10 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_util.ML Thu Nov 14 20:55:09 2013 +0100
@@ -54,7 +54,6 @@
term list list list list * Proof.context
val nonzero_string_of_int: int -> string
val retype_free: typ -> term -> term
- val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
val binder_fun_types: typ -> typ list
val body_fun_type: typ -> typ
@@ -307,14 +306,6 @@
val mk_TFreess = fold_map mk_TFrees;
-(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
-fun typ_subst_nonatomic [] = I
- | typ_subst_nonatomic inst =
- let
- fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts))
- | subst T = perhaps (AList.lookup (op =) inst) T;
- in subst end;
-
fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
--- a/src/HOL/Cardinals/Wellfounded_More_Base.thy Thu Nov 14 19:54:10 2013 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More_Base.thy Thu Nov 14 20:55:09 2013 +0100
@@ -8,7 +8,7 @@
header {* More on Well-Founded Relations (Base) *}
theory Wellfounded_More_Base
-imports Wellfounded Order_Relation_More_Base "~~/src/HOL/Library/Wfrec"
+imports Order_Relation_More_Base "~~/src/HOL/Library/Wfrec"
begin
--- a/src/HOL/Tools/ctr_sugar.ML Thu Nov 14 19:54:10 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML Thu Nov 14 20:55:09 2013 +0100
@@ -210,16 +210,16 @@
fun mk_ctr Ts t =
let val Type (_, Ts0) = body_type (fastype_of t) in
- Term.subst_atomic_types (Ts0 ~~ Ts) t
+ subst_nonatomic_types (Ts0 ~~ Ts) t
end;
fun mk_case Ts T t =
let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
- Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
+ subst_nonatomic_types ((body, T) :: (Ts0 ~~ Ts)) t
end;
fun mk_disc_or_sel Ts t =
- Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+ subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
fun name_of_const what t =
(case head_of t of
--- a/src/HOL/Tools/ctr_sugar_util.ML Thu Nov 14 19:54:10 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar_util.ML Thu Nov 14 20:55:09 2013 +0100
@@ -36,6 +36,9 @@
(string * sort) list * Proof.context
val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
+ val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
+ val subst_nonatomic_types: (typ * typ) list -> term -> term
+
val mk_predT: typ list -> typ
val mk_pred1T: typ -> typ
@@ -143,6 +146,17 @@
apfst (map TFree) o
variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
+(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
+fun typ_subst_nonatomic [] = I
+ | typ_subst_nonatomic inst =
+ let
+ fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts))
+ | subst T = perhaps (AList.lookup (op =) inst) T;
+ in subst end;
+
+fun subst_nonatomic_types [] = I
+ | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst);
+
fun mk_predT Ts = Ts ---> HOLogic.boolT;
fun mk_pred1T T = mk_predT [T];