Quotient_Info stores only relation maps
authorkuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802b16f976db515
parent 45801 5616fbda86e6
child 45806 0f1c049c147e
Quotient_Info stores only relation maps
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_info.ML
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Dec 09 16:08:32 2011 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Dec 09 18:07:04 2011 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Main Quotient_Syntax
     1.5  begin
     1.6  
     1.7 -declare [[map list = (map, list_all2)]]
     1.8 +declare [[map list = list_all2]]
     1.9  
    1.10  lemma map_id [id_simps]:
    1.11    "map id = id"
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Dec 09 16:08:32 2011 +0100
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Dec 09 18:07:04 2011 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  | "option_rel R None (Some x) = False"
     2.5  | "option_rel R (Some x) (Some y) = R x y"
     2.6  
     2.7 -declare [[map option = (Option.map, option_rel)]]
     2.8 +declare [[map option = option_rel]]
     2.9  
    2.10  lemma option_rel_unfold:
    2.11    "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Dec 09 16:08:32 2011 +0100
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Dec 09 18:07:04 2011 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  where
     3.5    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
     3.6  
     3.7 -declare [[map prod = (map_pair, prod_rel)]]
     3.8 +declare [[map prod = prod_rel]]
     3.9  
    3.10  lemma prod_rel_apply [simp]:
    3.11    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
     4.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 16:08:32 2011 +0100
     4.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 18:07:04 2011 +0100
     4.3 @@ -16,7 +16,7 @@
     4.4  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
     4.5  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
     4.6  
     4.7 -declare [[map sum = (sum_map, sum_rel)]]
     4.8 +declare [[map sum = sum_rel]]
     4.9  
    4.10  lemma sum_rel_unfold:
    4.11    "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
     5.1 --- a/src/HOL/Quotient.thy	Fri Dec 09 16:08:32 2011 +0100
     5.2 +++ b/src/HOL/Quotient.thy	Fri Dec 09 18:07:04 2011 +0100
     5.3 @@ -671,8 +671,8 @@
     5.4  use "Tools/Quotient/quotient_info.ML"
     5.5  setup Quotient_Info.setup
     5.6  
     5.7 -declare [[map "fun" = (map_fun, fun_rel)]]
     5.8 -declare [[map set = (vimage, set_rel)]]
     5.9 +declare [[map "fun" = fun_rel]]
    5.10 +declare [[map set = set_rel]]
    5.11  
    5.12  lemmas [quot_thm] = fun_quotient
    5.13  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
     6.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Dec 09 16:08:32 2011 +0100
     6.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Dec 09 18:07:04 2011 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  signature QUOTIENT_INFO =
     6.6  sig
     6.7 -  type quotmaps = {mapfun: string, relmap: string}
     6.8 +  type quotmaps = {relmap: string}
     6.9    val lookup_quotmaps: Proof.context -> string -> quotmaps option
    6.10    val lookup_quotmaps_global: theory -> string -> quotmaps option
    6.11    val print_quotmaps: Proof.context -> unit
    6.12 @@ -54,7 +54,7 @@
    6.13  (* FIXME just one data slot (record) per program unit *)
    6.14  
    6.15  (* info about map- and rel-functions for a type *)
    6.16 -type quotmaps = {mapfun: string, relmap: string}
    6.17 +type quotmaps = {relmap: string}
    6.18  
    6.19  structure Quotmaps = Generic_Data
    6.20  (
    6.21 @@ -72,20 +72,18 @@
    6.22  val quotmaps_attribute_setup =
    6.23    Attrib.setup @{binding map}
    6.24      ((Args.type_name false --| Scan.lift (Parse.$$$ "=")) --  (* FIXME Args.type_name true (requires "set" type) *)
    6.25 -      (Scan.lift (Parse.$$$ "(") |-- Args.const_proper true --| Scan.lift (Parse.$$$ ",") --
    6.26 -        Args.const_proper true --| Scan.lift (Parse.$$$ ")")) >>
    6.27 -      (fn (tyname, (mapname, relname)) =>
    6.28 -        let val minfo = {mapfun = mapname, relmap = relname}
    6.29 +      Args.const_proper true >>
    6.30 +      (fn (tyname, relname) =>
    6.31 +        let val minfo = {relmap = relname}
    6.32          in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
    6.33      "declaration of map information"
    6.34  
    6.35  fun print_quotmaps ctxt =
    6.36    let
    6.37 -    fun prt_map (ty_name, {mapfun, relmap}) =
    6.38 +    fun prt_map (ty_name, {relmap}) =
    6.39        Pretty.block (separate (Pretty.brk 2)
    6.40          (map Pretty.str
    6.41           ["type:", ty_name,
    6.42 -          "map:", mapfun,
    6.43            "relation map:", relmap]))
    6.44    in
    6.45      map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))