full name of a type as key in bnf table
authortraytel
Sun Sep 09 21:13:15 2012 +0200 (2012-09-09)
changeset 49236632f68beff2a
parent 49235 f9fc2b64c599
child 49237 fe22b6a5740b
full name of a type as key in bnf table
src/HOL/Codatatype/Basic_BNFs.thy
src/HOL/Codatatype/Tools/bnf_comp.ML
src/HOL/Codatatype/Tools/bnf_def.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
     1.1 --- a/src/HOL/Codatatype/Basic_BNFs.thy	Sun Sep 09 19:57:20 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Basic_BNFs.thy	Sun Sep 09 21:13:15 2012 +0200
     1.3 @@ -572,10 +572,6 @@
     1.4    qed
     1.5  qed auto
     1.6  
     1.7 -bnf_def deadlist = "map id" [] "\<lambda>_::'a list. |lists (UNIV :: 'a set)|" ["[]"]
     1.8 -by (auto simp add: cinfinite_def wpull_def infinite_UNIV_listI map.id
     1.9 -  ordLeq_transitive ctwo_def card_of_card_order_on Field_card_of card_of_mono1 ordLeq_cexp2)
    1.10 -
    1.11  (* Finite sets *)
    1.12  abbreviation afset where "afset \<equiv> abs_fset"
    1.13  abbreviation rfset where "rfset \<equiv> rep_fset"
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 19:57:20 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 21:13:15 2012 +0200
     2.3 @@ -726,7 +726,7 @@
     2.4    | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
     2.5      let
     2.6        val tfrees = Term.add_tfreesT T [];
     2.7 -      val bnf_opt = if null tfrees then NONE else bnf_of lthy (Long_Name.base_name C);
     2.8 +      val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
     2.9      in
    2.10        (case bnf_opt of
    2.11          NONE => ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy))
    2.12 @@ -746,9 +746,7 @@
    2.13            in ((bnf, deads_lives), (unfold', lthy)) end
    2.14          else
    2.15            let
    2.16 -            (* FIXME: we should allow several BNFs with the same base name *)
    2.17 -            val Tname = Long_Name.base_name C;
    2.18 -            val name = Binding.name_of b ^ "_" ^ Tname;
    2.19 +            val name = Binding.name_of b;
    2.20              fun qualify i bind =
    2.21                let val namei = if i > 0 then name ^ string_of_int i else name;
    2.22                in
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Sun Sep 09 19:57:20 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Sun Sep 09 21:13:15 2012 +0200
     3.3 @@ -631,7 +631,10 @@
     3.4      val dead = length deads;
     3.5  
     3.6      (*FIXME: check DUP here, not in after_qed*)
     3.7 -    val key = Name_Space.full_name Name_Space.default_naming b;
     3.8 +    val key =
     3.9 +      (case (CA, Binding.eq_name (qualify b, b)) of
    3.10 +        (Type (C, _), True) => C
    3.11 +      | _ => Name_Space.full_name Name_Space.default_naming b);
    3.12  
    3.13      (*TODO: further checks of type of bnf_map*)
    3.14      (*TODO: check types of bnf_sets*)
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:57:20 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 21:13:15 2012 +0200
     4.3 @@ -166,8 +166,7 @@
     4.4        in snd oo add end;
     4.5  
     4.6      val nested_bnfs =
     4.7 -      map_filter (bnf_of lthy o Long_Name.base_name)
     4.8 -        (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
     4.9 +      map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
    4.10  
    4.11      val timer = time (Timer.startRealTimer ());
    4.12  
    4.13 @@ -456,7 +455,7 @@
    4.14  
    4.15      fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
    4.16        let
    4.17 -        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    4.18 +        val map0 = map_of_bnf (the (bnf_of lthy s));
    4.19          val mapx = mk_map Ts Us map0;
    4.20          val TUs = map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    4.21          val args = map build_arg TUs;