1.1 --- a/src/HOL/Library/Quotient_List.thy	Thu Apr 26 01:05:06 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Thu Apr 26 12:01:58 2012 +0200
     1.3 @@ -178,7 +178,7 @@
     1.4  
     1.5  subsection {* Setup for lifting package *}
     1.6  
     1.7 -lemma Quotient_list:
     1.8 +lemma Quotient_list[quot_map]:
     1.9    assumes "Quotient R Abs Rep T"
    1.10    shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
    1.11  proof (unfold Quotient_alt_def, intro conjI allI impI)
    1.12 @@ -199,8 +199,6 @@
    1.13      by (induct xs ys rule: list_induct2', simp_all, metis 3)
    1.14  qed
    1.15  
    1.16 -declare [[map list = (list_all2, Quotient_list)]]
    1.17 -
    1.18  lemma list_invariant_commute [invariant_commute]:
    1.19    "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
    1.20    apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) 

     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Thu Apr 26 01:05:06 2012 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Thu Apr 26 12:01:58 2012 +0200
     2.3 @@ -101,15 +101,13 @@
     2.4  
     2.5  subsection {* Setup for lifting package *}
     2.6  
     2.7 -lemma Quotient_option:
     2.8 +lemma Quotient_option[quot_map]:
     2.9    assumes "Quotient R Abs Rep T"
    2.10    shows "Quotient (option_rel R) (Option.map Abs)
    2.11      (Option.map Rep) (option_rel T)"
    2.12    using assms unfolding Quotient_alt_def option_rel_unfold
    2.13    by (simp split: option.split)
    2.14  
    2.15 -declare [[map option = (option_rel, Quotient_option)]]
    2.16 -
    2.17  fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
    2.18  where
    2.19    "option_pred R None = True"

     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Apr 26 01:05:06 2012 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Apr 26 12:01:58 2012 +0200
     3.3 @@ -84,15 +84,13 @@
     3.4  
     3.5  subsection {* Setup for lifting package *}
     3.6  
     3.7 -lemma Quotient_prod:
     3.8 +lemma Quotient_prod[quot_map]:
     3.9    assumes "Quotient R1 Abs1 Rep1 T1"
    3.10    assumes "Quotient R2 Abs2 Rep2 T2"
    3.11    shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
    3.12      (map_pair Rep1 Rep2) (prod_rel T1 T2)"
    3.13    using assms unfolding Quotient_alt_def by auto
    3.14  
    3.15 -declare [[map prod = (prod_rel, Quotient_prod)]]
    3.16 -
    3.17  definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    3.18  where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    3.19  

     4.1 --- a/src/HOL/Library/Quotient_Set.thy	Thu Apr 26 01:05:06 2012 +0200
     4.2 +++ b/src/HOL/Library/Quotient_Set.thy	Thu Apr 26 12:01:58 2012 +0200
     4.3 @@ -185,7 +185,7 @@
     4.4  
     4.5  subsection {* Setup for lifting package *}
     4.6  
     4.7 -lemma Quotient_set:
     4.8 +lemma Quotient_set[quot_map]:
     4.9    assumes "Quotient R Abs Rep T"
    4.10    shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
    4.11    using assms unfolding Quotient_alt_def4
    4.12 @@ -193,8 +193,6 @@
    4.13    apply (simp add: set_rel_def, fast)
    4.14    done
    4.15  
    4.16 -declare [[map set = (set_rel, Quotient_set)]]
    4.17 -
    4.18  lemma set_invariant_commute [invariant_commute]:
    4.19    "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
    4.20    unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast

     5.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Apr 26 01:05:06 2012 +0200
     5.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu Apr 26 12:01:58 2012 +0200
     5.3 @@ -92,7 +92,7 @@
     5.4  
     5.5  subsection {* Setup for lifting package *}
     5.6  
     5.7 -lemma Quotient_sum:
     5.8 +lemma Quotient_sum[quot_map]:
     5.9    assumes "Quotient R1 Abs1 Rep1 T1"
    5.10    assumes "Quotient R2 Abs2 Rep2 T2"
    5.11    shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
    5.12 @@ -100,8 +100,6 @@
    5.13    using assms unfolding Quotient_alt_def
    5.14    by (simp add: split_sum_all)
    5.15  
    5.16 -declare [[map sum = (sum_rel, Quotient_sum)]]
    5.17 -
    5.18  fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    5.19  where
    5.20    "sum_pred R1 R2 (Inl a) = R1 a"

     6.1 --- a/src/HOL/Lifting.thy	Thu Apr 26 01:05:06 2012 +0200
     6.2 +++ b/src/HOL/Lifting.thy	Thu Apr 26 12:01:58 2012 +0200
     6.3 @@ -360,7 +360,7 @@
     6.4  use "Tools/Lifting/lifting_info.ML"
     6.5  setup Lifting_Info.setup
     6.6  
     6.7 -declare [[map "fun" = (fun_rel, fun_quotient)]]
     6.8 +declare fun_quotient[quot_map]
     6.9  
    6.10  use "Tools/Lifting/lifting_term.ML"
    6.11  

     7.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 26 01:05:06 2012 +0200
     7.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 26 12:01:58 2012 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  signature LIFTING_INFO =
     7.6  sig
     7.7 -  type quotmaps = {relmap: string, quot_thm: thm}
     7.8 +  type quotmaps = {rel_quot_thm: thm}
     7.9    val lookup_quotmaps: Proof.context -> string -> quotmaps option
    7.10    val lookup_quotmaps_global: theory -> string -> quotmaps option
    7.11    val print_quotmaps: Proof.context -> unit
    7.12 @@ -27,10 +27,12 @@
    7.13  structure Lifting_Info: LIFTING_INFO =
    7.14  struct
    7.15  
    7.16 +open Lifting_Util
    7.17 +
    7.18  (** data containers **)
    7.19  
    7.20 -(* info about map- and rel-functions for a type *)
    7.21 -type quotmaps = {relmap: string, quot_thm: thm}
    7.22 +(* info about Quotient map theorems *)
    7.23 +type quotmaps = {rel_quot_thm: thm}
    7.24  
    7.25  structure Quotmaps = Generic_Data
    7.26  (
    7.27 @@ -45,26 +47,28 @@
    7.28  
    7.29  (* FIXME export proper internal update operation!? *)
    7.30  
    7.31 +fun add_quot_map rel_quot_thm ctxt = 
    7.32 +  let
    7.33 +    val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm
    7.34 +    val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl
    7.35 +    val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
    7.36 +    val minfo = {rel_quot_thm = rel_quot_thm}
    7.37 +  in
    7.38 +    Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt
    7.39 +  end    
    7.40 +
    7.41  val quotmaps_attribute_setup =
    7.42 -  Attrib.setup @{binding map}
    7.43 -    ((Args.type_name true --| Scan.lift @{keyword "="}) --
    7.44 -      (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
    7.45 -        Attrib.thm --| Scan.lift @{keyword ")"}) >>
    7.46 -      (fn (tyname, (relname, qthm)) =>
    7.47 -        let val minfo = {relmap = relname, quot_thm = qthm}
    7.48 -        in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
    7.49 -    "declaration of map information"
    7.50 +  Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
    7.51 +    "declaration of the Quotient map theorem"
    7.52  
    7.53  fun print_quotmaps ctxt =
    7.54    let
    7.55 -    fun prt_map (ty_name, {relmap, quot_thm}) =
    7.56 +    fun prt_map (ty_name, {rel_quot_thm}) =
    7.57        Pretty.block (separate (Pretty.brk 2)
    7.58           [Pretty.str "type:", 
    7.59            Pretty.str ty_name,
    7.60 -          Pretty.str "relation map:", 
    7.61 -          Pretty.str relmap,
    7.62            Pretty.str "quot. theorem:", 
    7.63 -          Syntax.pretty_term ctxt (prop_of quot_thm)])
    7.64 +          Syntax.pretty_term ctxt (prop_of rel_quot_thm)])
    7.65    in
    7.66      map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
    7.67      |> Pretty.big_list "maps for type constructors:"

     8.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Thu Apr 26 01:05:06 2012 +0200
     8.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Thu Apr 26 12:01:58 2012 +0200
     8.3 @@ -76,7 +76,7 @@
     8.4      val thy = Proof_Context.theory_of ctxt
     8.5    in
     8.6      (case Lifting_Info.lookup_quotmaps ctxt s of
     8.7 -      SOME map_data => Thm.transfer thy (#quot_thm map_data)
     8.8 +      SOME map_data => Thm.transfer thy (#rel_quot_thm map_data)
     8.9      | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    8.10        [Pretty.str ("No relator for the type " ^ quote s), 
    8.11         Pretty.brk 1,
    8.12 @@ -85,10 +85,6 @@
    8.13  
    8.14  fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    8.15  
    8.16 -fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
    8.17 -      = (rel, abs, rep, cr)
    8.18 -  | dest_Quotient t = raise TERM ("dest_Quotient", [t])
    8.19 -
    8.20  fun quot_thm_rel quot_thm =
    8.21    case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
    8.22      (rel, _, _, _) => rel

     9.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Thu Apr 26 01:05:06 2012 +0200
     9.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Thu Apr 26 12:01:58 2012 +0200
     9.3 @@ -8,6 +8,7 @@
     9.4  sig
     9.5    val MRSL: thm list * thm -> thm
     9.6    val Trueprop_conv: conv -> conv
     9.7 +  val dest_Quotient: term -> term * term * term * term
     9.8  end;
     9.9  
    9.10  
    9.11 @@ -23,4 +24,8 @@
    9.12      Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    9.13    | _ => raise CTERM ("Trueprop_conv", [ct]))
    9.14  
    9.15 +fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
    9.16 +      = (rel, abs, rep, cr)
    9.17 +  | dest_Quotient t = raise TERM ("dest_Quotient", [t])
    9.18 +
    9.19  end;