use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
authorblanchet
Thu Apr 03 10:51:22 2014 +0200 (2014-04-03)
changeset 5637532e0da92c786
parent 56374 dfc7a46c2900
child 56376 5a93b8f928a2
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
src/HOL/HOL.thy
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/typedef.ML
src/HOL/Wellfounded.thy
src/Pure/Isar/code.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Apr 03 10:51:20 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Apr 03 10:51:22 2014 +0200
     1.3 @@ -2017,4 +2017,3 @@
     1.4  hide_const (open) eq equal
     1.5  
     1.6  end
     1.7 -
     2.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Apr 03 10:51:20 2014 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Apr 03 10:51:22 2014 +0200
     2.3 @@ -265,7 +265,15 @@
     2.4    type T = Datatype_Aux.config * string list;
     2.5    val eq: T * T -> bool = eq_snd (op =);
     2.6  );
     2.7 -fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
     2.8 +
     2.9 +fun with_repaired_path f config (type_names as name :: _) thy =
    2.10 +  thy
    2.11 +  |> Sign.root_path
    2.12 +  |> Sign.add_path (Long_Name.qualifier name)
    2.13 +  |> f config type_names
    2.14 +  |> Sign.restore_naming thy;
    2.15 +
    2.16 +fun interpretation f = Datatype_Interpretation.interpretation (uncurry (with_repaired_path f));
    2.17  val interpretation_data = Datatype_Interpretation.data;
    2.18  
    2.19  
     3.1 --- a/src/HOL/Tools/Function/size.ML	Thu Apr 03 10:51:20 2014 +0200
     3.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Apr 03 10:51:22 2014 +0200
     3.3 @@ -220,8 +220,7 @@
     3.4  fun add_size_thms config (new_type_names as name :: _) thy =
     3.5    let
     3.6      val info as {descr, ...} = Datatype_Data.the_info thy name;
     3.7 -    val prefix =
     3.8 -      Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name;
     3.9 +    val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
    3.10      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
    3.11        Datatype_Aux.is_rec_type dt andalso
    3.12          not (null (fst (Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
    3.13 @@ -229,7 +228,6 @@
    3.14      if no_size then thy
    3.15      else
    3.16        thy
    3.17 -      |> Sign.root_path
    3.18        |> Sign.add_path prefix
    3.19        |> prove_size_thms info new_type_names
    3.20        |> Sign.restore_naming thy
     4.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 03 10:51:20 2014 +0200
     4.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 03 10:51:22 2014 +0200
     4.3 @@ -405,9 +405,9 @@
     4.4      val algebra = Sign.classes_of thy;
     4.5      val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
     4.6      val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
     4.7 -    fun insts_of sort constr  = (map (rpair sort) o flat o maps snd o maps snd)
     4.8 +    fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
     4.9        (Datatype_Aux.interpret_construction descr vs constr)
    4.10 -    val insts = insts_of sort  { atyp = single, dtyp = (K o K o K) [] }
    4.11 +    val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
    4.12        @ insts_of aux_sort { atyp = K [], dtyp = K o K }
    4.13      val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos;
    4.14    in if has_inst then thy
     5.1 --- a/src/HOL/Tools/typedef.ML	Thu Apr 03 10:51:20 2014 +0200
     5.2 +++ b/src/HOL/Tools/typedef.ML	Thu Apr 03 10:51:22 2014 +0200
     5.3 @@ -73,7 +73,15 @@
     5.4  (* global interpretation *)
     5.5  
     5.6  structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
     5.7 -val interpretation = Typedef_Interpretation.interpretation;
     5.8 +
     5.9 +fun with_repaired_path f name thy =
    5.10 +  thy
    5.11 +  |> Sign.root_path
    5.12 +  |> Sign.add_path (Long_Name.qualifier name)
    5.13 +  |> f name
    5.14 +  |> Sign.restore_naming thy;
    5.15 +
    5.16 +fun interpretation f = Typedef_Interpretation.interpretation (with_repaired_path f);
    5.17  
    5.18  val setup = Typedef_Interpretation.init;
    5.19  
    5.20 @@ -154,8 +162,7 @@
    5.21        |> Typedecl.typedecl (name, args, mx)
    5.22        ||> Variable.declare_term set;
    5.23  
    5.24 -    val Type (full_name, type_args) = newT;
    5.25 -    val lhs_tfrees = map Term.dest_TFree type_args;
    5.26 +    val Type (full_name, _) = newT;
    5.27  
    5.28  
    5.29      (* axiomatization *)
    5.30 @@ -183,7 +190,6 @@
    5.31  
    5.32      fun typedef_result inhabited lthy1 =
    5.33        let
    5.34 -        val cert = Thm.cterm_of (Proof_Context.theory_of lthy1);
    5.35          val typedef' = inhabited RS typedef;
    5.36          fun make th = Goal.norm_result lthy1 (typedef' RS th);
    5.37          val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
     6.1 --- a/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:20 2014 +0200
     6.2 +++ b/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:22 2014 +0200
     6.3 @@ -859,7 +859,7 @@
     6.4  lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
     6.5    by (induct n) simp_all
     6.6  
     6.7 -declare "prod.size" [no_atp]
     6.8 +declare prod.size [no_atp]
     6.9  
    6.10  
    6.11  hide_const (open) acc accp
     7.1 --- a/src/Pure/Isar/code.ML	Thu Apr 03 10:51:20 2014 +0200
     7.2 +++ b/src/Pure/Isar/code.ML	Thu Apr 03 10:51:22 2014 +0200
     7.3 @@ -1232,8 +1232,15 @@
     7.4  structure Datatype_Interpretation =
     7.5    Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
     7.6  
     7.7 +fun with_repaired_path f (tyco, serial) thy =
     7.8 +  thy
     7.9 +  |> Sign.root_path
    7.10 +  |> Sign.add_path (Long_Name.qualifier tyco)
    7.11 +  |> f (tyco, serial)
    7.12 +  |> Sign.restore_naming thy;
    7.13 +
    7.14  fun datatype_interpretation f = Datatype_Interpretation.interpretation
    7.15 -  (fn (tyco, _) => fn thy => f (tyco, fst (get_type thy tyco)) thy);
    7.16 +  (fn (tyco, _) => fn thy => with_repaired_path f (tyco, fst (get_type thy tyco)) thy);
    7.17  
    7.18  fun add_datatype proto_constrs thy =
    7.19    let