# HG changeset patch # User wenzelm # Date 1269722770 -3600 # Node ID 95e67639ac27657acabb603ed992b7f3ab334fd7 # Parent 26e820d27e0a6e821de41964d636ae5980a263a6# Parent 9cc3df9a606e1ac66c16ea5a561e546b4757f1ad merged diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Import/proof_kernel.ML Sat Mar 27 21:46:10 2010 +0100 @@ -2098,7 +2098,7 @@ (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2 - val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 + val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4 val fulltyname = Sign.intern_type thy' tycname val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' @@ -2195,7 +2195,7 @@ [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))] typedef_hol2hollight - val th4 = (#type_definition typedef_info) RS typedef_hol2hollight' + val th4 = (#type_definition (#2 typedef_info)) RS typedef_hol2hollight' val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse raise ERR "type_introduction" "no type variables expected any more" val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Mar 27 21:46:10 2010 +0100 @@ -640,9 +640,9 @@ new_type_names); val perm_defs = map snd typedefs; - val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs; - val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs; - val Rep_thms = map (collect_simp o #Rep o fst) typedefs; + val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs; + val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs; + val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs; (** prove that new types are in class pt_ **) @@ -826,8 +826,8 @@ new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax) (thy7, [], [], []); - val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs - val rep_inject_thms = map (#Rep_inject o fst) typedefs + val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs + val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs (* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *) diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Sat Mar 27 21:46:10 2010 +0100 @@ -276,11 +276,11 @@ val _ = message config "Proving isomorphism properties ..."; - val newT_iso_axms = map (fn (_, td) => + val newT_iso_axms = map (fn (_, (_, td)) => (collect_simp (#Abs_inverse td), #Rep_inverse td, collect_simp (#Rep td))) typedefs; - val newT_iso_inj_thms = map (fn (_, td) => + val newT_iso_inj_thms = map (fn (_, (_, td)) => (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs; (********* isomorphisms between existing types and "unfolded" types *******) diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 27 21:46:10 2010 +0100 @@ -570,8 +570,8 @@ set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} else case Typedef.get_info_global thy s of (* FIXME handle multiple typedef interpretations (!??) *) - [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse, - Rep_inverse, ...}] => + [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse, + Rep_inverse, ...})] => SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Sat Mar 27 21:46:10 2010 +0100 @@ -89,7 +89,7 @@ (* tactic to prove the quot_type theorem for the new type *) -fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = +fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) = let val rep_thm = #Rep typedef_info RS mem_def1 val rep_inv = #Rep_inverse typedef_info @@ -143,10 +143,10 @@ val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy (* abs and rep functions from the typedef *) - val Abs_ty = #abs_type typedef_info - val Rep_ty = #rep_type typedef_info - val Abs_name = #Abs_name typedef_info - val Rep_name = #Rep_name typedef_info + val Abs_ty = #abs_type (#1 typedef_info) + val Rep_ty = #rep_type (#1 typedef_info) + val Abs_name = #Abs_name (#1 typedef_info) + val Rep_name = #Rep_name (#1 typedef_info) val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Tools/record.ML Sat Mar 27 21:46:10 2010 +0100 @@ -104,12 +104,12 @@ let fun get_thms thy name = let - val [{Rep_inject = rep_inject, Abs_name = absN, abs_type = absT, - Abs_inverse = abs_inverse, ...}] = Typedef.get_info_global thy name; + val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] = + Typedef.get_info_global thy name; val rewrite_rule = MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}]; in - (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT) + (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT) end; in thy diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Tools/typecopy.ML --- a/src/HOL/Tools/typecopy.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Tools/typecopy.ML Sat Mar 27 21:46:10 2010 +0100 @@ -55,9 +55,9 @@ val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs; val tac = Tactic.rtac UNIV_witness 1; - fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, - Rep_name = c_rep, Abs_inject = inject, - Abs_inverse = inverse, ... } : Typedef.info ) thy = + fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, + Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... }) + : Typedef.info) thy = let val exists_thm = UNIV_I @@ -94,7 +94,7 @@ val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs, typ = ty_rep, ... } = get_info thy tyco; (* FIXME handle multiple typedef interpretations (!??) *) - val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco; + val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco; val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c)); val ty = Type (tyco, map TFree vs); val proj = Const (proj, ty --> ty_rep); diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Tools/typedef.ML Sat Mar 27 21:46:10 2010 +0100 @@ -8,8 +8,8 @@ signature TYPEDEF = sig type info = - {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm, - type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, + {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} * + {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm} val transform_info: morphism -> info -> info @@ -35,26 +35,26 @@ (* theory data *) type info = - {(*global part*) - rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, + (*global part*) + {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} * (*local part*) - inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, - Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, - Rep_induct: thm, Abs_induct: thm}; + {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, + Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, + Rep_induct: thm, Abs_induct: thm}; fun transform_info phi (info: info) = let val thm = Morphism.thm phi; - val {rep_type, abs_type, Rep_name, Abs_name, inhabited, type_definition, + val (global_info, {inhabited, type_definition, set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, - Rep_cases, Abs_cases, Rep_induct, Abs_induct} = info; + Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info; in - {rep_type = rep_type, abs_type = abs_type, Rep_name = Rep_name, Abs_name = Abs_name, - inhabited = thm inhabited, type_definition = thm type_definition, - set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse, - Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject, - Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct, - Abs_induct = thm Abs_induct} + (global_info, + {inhabited = thm inhabited, type_definition = thm type_definition, + set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse, + Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject, + Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct, + Abs_induct = thm Abs_induct}) end; structure Data = Generic_Data @@ -235,12 +235,13 @@ [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]), make @{thm type_definition.Abs_induct}); - val info = {rep_type = oldT, abs_type = newT, - Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC), - inhabited = inhabited, type_definition = type_definition, set_def = set_def, + val info = + ({rep_type = oldT, abs_type = newT, + Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC)}, + {inhabited = inhabited, type_definition = type_definition, set_def = set_def, Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, - Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; + Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}); in lthy2 |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info)) diff -r 26e820d27e0a -r 95e67639ac27 src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOL/Tools/typedef_codegen.ML Sat Mar 27 21:46:10 2010 +0100 @@ -31,10 +31,10 @@ in (case strip_comb t of (Const (s, Type ("fun", [T, U])), ts) => - if lookup #Rep_name T = s andalso + if lookup (#Rep_name o #1) T = s andalso is_none (Codegen.get_assoc_type thy (get_name T)) then mk_fun s T ts - else if lookup #Abs_name U = s andalso + else if lookup (#Abs_name o #1) U = s andalso is_none (Codegen.get_assoc_type thy (get_name U)) then mk_fun s U ts else NONE @@ -48,7 +48,7 @@ fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr = (case Typedef.get_info_global thy s of (* FIXME handle multiple typedef interpretations (!??) *) - [{abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}] => + [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] => if is_some (Codegen.get_assoc_type thy tname) then NONE else let diff -r 26e820d27e0a -r 95e67639ac27 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Sat Mar 27 21:46:10 2010 +0100 @@ -193,10 +193,10 @@ fun add_podef def opt_name typ set opt_morphs tac thy = let val name = the_default (#1 typ) opt_name; - val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy + val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac; - val oldT = #rep_type info; - val newT = #abs_type info; + val oldT = #rep_type (#1 info); + val newT = #abs_type (#1 info); val lhs_tfrees = map dest_TFree (snd (dest_Type newT)); val RepC = Const (Rep_name, newT --> oldT); @@ -235,7 +235,7 @@ fun cpodef_result nonempty admissible thy = let - val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy + val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1); val (cpo_info, thy3) = thy2 |> prove_cpo name newT morphs type_definition set_def below_def admissible; @@ -270,7 +270,7 @@ fun pcpodef_result UU_mem admissible thy = let val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1; - val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy + val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy |> add_podef def (SOME name) typ set opt_morphs tac; val (cpo_info, thy3) = thy2 |> prove_cpo name newT morphs type_definition set_def below_def admissible; diff -r 26e820d27e0a -r 95e67639ac27 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Sat Mar 27 21:34:28 2010 +0100 +++ b/src/HOLCF/Tools/repdef.ML Sat Mar 27 21:46:10 2010 +0100 @@ -95,8 +95,8 @@ |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); (*definitions*) - val Rep_const = Const (#Rep_name info, newT --> udomT); - val Abs_const = Const (#Abs_name info, udomT --> newT); + val Rep_const = Const (#Rep_name (#1 info), newT --> udomT); + val Abs_const = Const (#Abs_name (#1 info), udomT --> newT); val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const); val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $ Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); @@ -125,8 +125,8 @@ val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef; val type_definition_thm = MetaSimplifier.rewrite_rule - (the_list (#set_def info)) - (#type_definition info); + (the_list (#set_def (#2 info))) + (#type_definition (#2 info)); val typedef_thms = [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def]; val thy = lthy