Typedef.info: separate global and local part, only the latter is transformed by morphisms;
authorwenzelm
Sat Mar 27 21:38:38 2010 +0100 (2010-03-27)
changeset 359949cc3df9a606e
parent 35993 380b97496734
child 35996 95e67639ac27
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
src/HOL/Import/proof_kernel.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Quotient/quotient_typ.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typecopy.ML
src/HOL/Tools/typedef.ML
src/HOL/Tools/typedef_codegen.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 27 21:38:38 2010 +0100
     1.3 @@ -2098,7 +2098,7 @@
     1.4                  (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
     1.5              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
     1.6  
     1.7 -            val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
     1.8 +            val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
     1.9  
    1.10              val fulltyname = Sign.intern_type thy' tycname
    1.11              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
    1.12 @@ -2195,7 +2195,7 @@
    1.13                      [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
    1.14                      [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
    1.15                      typedef_hol2hollight
    1.16 -            val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
    1.17 +            val th4 = (#type_definition (#2 typedef_info)) RS typedef_hol2hollight'
    1.18              val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
    1.19                raise ERR "type_introduction" "no type variables expected any more"
    1.20              val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 27 18:43:11 2010 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 27 21:38:38 2010 +0100
     2.3 @@ -640,9 +640,9 @@
     2.4              new_type_names);
     2.5  
     2.6      val perm_defs = map snd typedefs;
     2.7 -    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs;
     2.8 -    val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
     2.9 -    val Rep_thms = map (collect_simp o #Rep o fst) typedefs;
    2.10 +    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
    2.11 +    val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
    2.12 +    val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
    2.13  
    2.14  
    2.15      (** prove that new types are in class pt_<name> **)
    2.16 @@ -826,8 +826,8 @@
    2.17          new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
    2.18        (thy7, [], [], []);
    2.19  
    2.20 -    val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs
    2.21 -    val rep_inject_thms = map (#Rep_inject o fst) typedefs
    2.22 +    val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
    2.23 +    val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
    2.24  
    2.25      (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
    2.26  
     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 27 18:43:11 2010 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 27 21:38:38 2010 +0100
     3.3 @@ -276,11 +276,11 @@
     3.4  
     3.5      val _ = message config "Proving isomorphism properties ...";
     3.6  
     3.7 -    val newT_iso_axms = map (fn (_, td) =>
     3.8 +    val newT_iso_axms = map (fn (_, (_, td)) =>
     3.9        (collect_simp (#Abs_inverse td), #Rep_inverse td,
    3.10         collect_simp (#Rep td))) typedefs;
    3.11  
    3.12 -    val newT_iso_inj_thms = map (fn (_, td) =>
    3.13 +    val newT_iso_inj_thms = map (fn (_, (_, td)) =>
    3.14        (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs;
    3.15  
    3.16      (********* isomorphisms between existing types and "unfolded" types *******)
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 27 18:43:11 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 27 21:38:38 2010 +0100
     4.3 @@ -570,8 +570,8 @@
     4.4            set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
     4.5    else case Typedef.get_info_global thy s of
     4.6      (* FIXME handle multiple typedef interpretations (!??) *)
     4.7 -    [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
     4.8 -          Rep_inverse, ...}] =>
     4.9 +    [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
    4.10 +          Rep_inverse, ...})] =>
    4.11      SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
    4.12            Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
    4.13            set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
     5.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 27 18:43:11 2010 +0100
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 27 21:38:38 2010 +0100
     5.3 @@ -89,7 +89,7 @@
     5.4  
     5.5  
     5.6  (* tactic to prove the quot_type theorem for the new type *)
     5.7 -fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
     5.8 +fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
     5.9  let
    5.10    val rep_thm = #Rep typedef_info RS mem_def1
    5.11    val rep_inv = #Rep_inverse typedef_info
    5.12 @@ -143,10 +143,10 @@
    5.13    val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
    5.14  
    5.15    (* abs and rep functions from the typedef *)
    5.16 -  val Abs_ty = #abs_type typedef_info
    5.17 -  val Rep_ty = #rep_type typedef_info
    5.18 -  val Abs_name = #Abs_name typedef_info
    5.19 -  val Rep_name = #Rep_name typedef_info
    5.20 +  val Abs_ty = #abs_type (#1 typedef_info)
    5.21 +  val Rep_ty = #rep_type (#1 typedef_info)
    5.22 +  val Abs_name = #Abs_name (#1 typedef_info)
    5.23 +  val Rep_name = #Rep_name (#1 typedef_info)
    5.24    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
    5.25    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
    5.26  
     6.1 --- a/src/HOL/Tools/record.ML	Sat Mar 27 18:43:11 2010 +0100
     6.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 27 21:38:38 2010 +0100
     6.3 @@ -104,12 +104,12 @@
     6.4    let
     6.5      fun get_thms thy name =
     6.6        let
     6.7 -        val [{Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
     6.8 -          Abs_inverse = abs_inverse, ...}] = Typedef.get_info_global thy name;
     6.9 +        val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] =
    6.10 +          Typedef.get_info_global thy name;
    6.11          val rewrite_rule =
    6.12            MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
    6.13        in
    6.14 -        (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT)
    6.15 +        (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT)
    6.16        end;
    6.17    in
    6.18      thy
     7.1 --- a/src/HOL/Tools/typecopy.ML	Sat Mar 27 18:43:11 2010 +0100
     7.2 +++ b/src/HOL/Tools/typecopy.ML	Sat Mar 27 21:38:38 2010 +0100
     7.3 @@ -55,9 +55,9 @@
     7.4      val vs =
     7.5        AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
     7.6      val tac = Tactic.rtac UNIV_witness 1;
     7.7 -    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
     7.8 -      Rep_name = c_rep, Abs_inject = inject,
     7.9 -      Abs_inverse = inverse, ... } : Typedef.info ) thy =
    7.10 +    fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
    7.11 +          Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
    7.12 +          : Typedef.info) thy =
    7.13          let
    7.14            val exists_thm =
    7.15              UNIV_I
    7.16 @@ -94,7 +94,7 @@
    7.17      val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
    7.18        typ = ty_rep, ... } = get_info thy tyco;
    7.19      (* FIXME handle multiple typedef interpretations (!??) *)
    7.20 -    val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
    7.21 +    val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco;
    7.22      val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
    7.23      val ty = Type (tyco, map TFree vs);
    7.24      val proj = Const (proj, ty --> ty_rep);
     8.1 --- a/src/HOL/Tools/typedef.ML	Sat Mar 27 18:43:11 2010 +0100
     8.2 +++ b/src/HOL/Tools/typedef.ML	Sat Mar 27 21:38:38 2010 +0100
     8.3 @@ -8,8 +8,8 @@
     8.4  signature TYPEDEF =
     8.5  sig
     8.6    type info =
     8.7 -   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
     8.8 -    type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     8.9 +   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
    8.10 +   {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    8.11      Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    8.12      Rep_induct: thm, Abs_induct: thm}
    8.13    val transform_info: morphism -> info -> info
    8.14 @@ -35,26 +35,26 @@
    8.15  (* theory data *)
    8.16  
    8.17  type info =
    8.18 - {(*global part*)
    8.19 -  rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    8.20 +  (*global part*)
    8.21 +  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
    8.22    (*local part*)
    8.23 -  inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    8.24 -  Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    8.25 -  Rep_induct: thm, Abs_induct: thm};
    8.26 +  {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    8.27 +    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    8.28 +    Rep_induct: thm, Abs_induct: thm};
    8.29  
    8.30  fun transform_info phi (info: info) =
    8.31    let
    8.32      val thm = Morphism.thm phi;
    8.33 -    val {rep_type, abs_type, Rep_name, Abs_name, inhabited, type_definition,
    8.34 +    val (global_info, {inhabited, type_definition,
    8.35        set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
    8.36 -      Rep_cases, Abs_cases, Rep_induct, Abs_induct} = info;
    8.37 +      Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
    8.38    in
    8.39 -   {rep_type = rep_type, abs_type = abs_type, Rep_name = Rep_name, Abs_name = Abs_name,
    8.40 -    inhabited = thm inhabited, type_definition = thm type_definition,
    8.41 -    set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
    8.42 -    Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
    8.43 -    Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
    8.44 -    Abs_induct = thm Abs_induct}
    8.45 +    (global_info,
    8.46 +     {inhabited = thm inhabited, type_definition = thm type_definition,
    8.47 +      set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
    8.48 +      Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
    8.49 +      Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
    8.50 +      Abs_induct = thm Abs_induct})
    8.51    end;
    8.52  
    8.53  structure Data = Generic_Data
    8.54 @@ -235,12 +235,13 @@
    8.55                  [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]),
    8.56                make @{thm type_definition.Abs_induct});
    8.57  
    8.58 -        val info = {rep_type = oldT, abs_type = newT,
    8.59 -          Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC),
    8.60 -            inhabited = inhabited, type_definition = type_definition, set_def = set_def,
    8.61 +        val info =
    8.62 +          ({rep_type = oldT, abs_type = newT,
    8.63 +            Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC)},
    8.64 +           {inhabited = inhabited, type_definition = type_definition, set_def = set_def,
    8.65              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
    8.66              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
    8.67 -          Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
    8.68 +          Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
    8.69        in
    8.70          lthy2
    8.71          |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
     9.1 --- a/src/HOL/Tools/typedef_codegen.ML	Sat Mar 27 18:43:11 2010 +0100
     9.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Sat Mar 27 21:38:38 2010 +0100
     9.3 @@ -31,10 +31,10 @@
     9.4    in
     9.5      (case strip_comb t of
     9.6         (Const (s, Type ("fun", [T, U])), ts) =>
     9.7 -         if lookup #Rep_name T = s andalso
     9.8 +         if lookup (#Rep_name o #1) T = s andalso
     9.9             is_none (Codegen.get_assoc_type thy (get_name T))
    9.10           then mk_fun s T ts
    9.11 -         else if lookup #Abs_name U = s andalso
    9.12 +         else if lookup (#Abs_name o #1) U = s andalso
    9.13             is_none (Codegen.get_assoc_type thy (get_name U))
    9.14           then mk_fun s U ts
    9.15           else NONE
    9.16 @@ -48,7 +48,7 @@
    9.17  fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
    9.18        (case Typedef.get_info_global thy s of
    9.19          (* FIXME handle multiple typedef interpretations (!??) *)
    9.20 -        [{abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}] =>
    9.21 +        [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] =>
    9.22            if is_some (Codegen.get_assoc_type thy tname) then NONE
    9.23            else
    9.24              let
    10.1 --- a/src/HOLCF/Tools/pcpodef.ML	Sat Mar 27 18:43:11 2010 +0100
    10.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Sat Mar 27 21:38:38 2010 +0100
    10.3 @@ -193,10 +193,10 @@
    10.4  fun add_podef def opt_name typ set opt_morphs tac thy =
    10.5    let
    10.6      val name = the_default (#1 typ) opt_name;
    10.7 -    val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
    10.8 +    val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
    10.9        |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
   10.10 -    val oldT = #rep_type info;
   10.11 -    val newT = #abs_type info;
   10.12 +    val oldT = #rep_type (#1 info);
   10.13 +    val newT = #abs_type (#1 info);
   10.14      val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
   10.15  
   10.16      val RepC = Const (Rep_name, newT --> oldT);
   10.17 @@ -235,7 +235,7 @@
   10.18  
   10.19      fun cpodef_result nonempty admissible thy =
   10.20        let
   10.21 -        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
   10.22 +        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
   10.23            |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
   10.24          val (cpo_info, thy3) = thy2
   10.25            |> prove_cpo name newT morphs type_definition set_def below_def admissible;
   10.26 @@ -270,7 +270,7 @@
   10.27      fun pcpodef_result UU_mem admissible thy =
   10.28        let
   10.29          val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
   10.30 -        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
   10.31 +        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
   10.32            |> add_podef def (SOME name) typ set opt_morphs tac;
   10.33          val (cpo_info, thy3) = thy2
   10.34            |> prove_cpo name newT morphs type_definition set_def below_def admissible;
    11.1 --- a/src/HOLCF/Tools/repdef.ML	Sat Mar 27 18:43:11 2010 +0100
    11.2 +++ b/src/HOLCF/Tools/repdef.ML	Sat Mar 27 21:38:38 2010 +0100
    11.3 @@ -95,8 +95,8 @@
    11.4        |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
    11.5  
    11.6      (*definitions*)
    11.7 -    val Rep_const = Const (#Rep_name info, newT --> udomT);
    11.8 -    val Abs_const = Const (#Abs_name info, udomT --> newT);
    11.9 +    val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
   11.10 +    val Abs_const = Const (#Abs_name (#1 info), udomT --> newT);
   11.11      val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
   11.12      val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
   11.13        Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
   11.14 @@ -125,8 +125,8 @@
   11.15      val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef;
   11.16      val type_definition_thm =
   11.17        MetaSimplifier.rewrite_rule
   11.18 -        (the_list (#set_def info))
   11.19 -        (#type_definition info);
   11.20 +        (the_list (#set_def (#2 info)))
   11.21 +        (#type_definition (#2 info));
   11.22      val typedef_thms =
   11.23        [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def];
   11.24      val thy = lthy