# HG changeset patch # User blanchet # Date 1384458909 -3600 # Node ID 4a655e62ad34d2fad0ea25081a1da6dae5c90c26 # Parent e275d520f49d634c8692b8a41f830320280a54b0 fixed type variable confusion in 'datatype_new_compat' diff -r e275d520f49d -r 4a655e62ad34 src/HOL/BNF/BNF_Util.thy --- 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 \ A \ (B \ {x \ A. P x}) = (\x \ B. P x)" diff -r e275d520f49d -r 4a655e62ad34 src/HOL/BNF/Tools/bnf_lfp_compat.ML --- 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); diff -r e275d520f49d -r 4a655e62ad34 src/HOL/BNF/Tools/bnf_util.ML --- 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; diff -r e275d520f49d -r 4a655e62ad34 src/HOL/Cardinals/Wellfounded_More_Base.thy --- 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 diff -r e275d520f49d -r 4a655e62ad34 src/HOL/Tools/ctr_sugar.ML --- 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 diff -r e275d520f49d -r 4a655e62ad34 src/HOL/Tools/ctr_sugar_util.ML --- 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];