# HG changeset patch # User kuncar # Date 1335434518 -7200 # Node ID f29e7dcd7c40d9d04242213cf67410b5586ab7b0 # Parent 024cf0f7fb6de29059acd14d9882a93b52d8ba1a use a quot_map theorem attribute instead of the complicated map attribute diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Library/Quotient_List.thy Thu Apr 26 12:01:58 2012 +0200 @@ -178,7 +178,7 @@ subsection {* Setup for lifting package *} -lemma Quotient_list: +lemma Quotient_list[quot_map]: assumes "Quotient R Abs Rep T" shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)" proof (unfold Quotient_alt_def, intro conjI allI impI) @@ -199,8 +199,6 @@ by (induct xs ys rule: list_induct2', simp_all, metis 3) qed -declare [[map list = (list_all2, Quotient_list)]] - lemma list_invariant_commute [invariant_commute]: "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)" apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Thu Apr 26 12:01:58 2012 +0200 @@ -101,15 +101,13 @@ subsection {* Setup for lifting package *} -lemma Quotient_option: +lemma Quotient_option[quot_map]: assumes "Quotient R Abs Rep T" shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep) (option_rel T)" using assms unfolding Quotient_alt_def option_rel_unfold by (simp split: option.split) -declare [[map option = (option_rel, Quotient_option)]] - fun option_pred :: "('a \ bool) \ 'a option \ bool" where "option_pred R None = True" diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Thu Apr 26 12:01:58 2012 +0200 @@ -84,15 +84,13 @@ subsection {* Setup for lifting package *} -lemma Quotient_prod: +lemma Quotient_prod[quot_map]: assumes "Quotient R1 Abs1 Rep1 T1" assumes "Quotient R2 Abs2 Rep2 T2" shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2) (prod_rel T1 T2)" using assms unfolding Quotient_alt_def by auto -declare [[map prod = (prod_rel, Quotient_prod)]] - definition prod_pred :: "('a \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" where "prod_pred R1 R2 = (\(a, b). R1 a \ R2 b)" diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Thu Apr 26 12:01:58 2012 +0200 @@ -185,7 +185,7 @@ subsection {* Setup for lifting package *} -lemma Quotient_set: +lemma Quotient_set[quot_map]: assumes "Quotient R Abs Rep T" shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)" using assms unfolding Quotient_alt_def4 @@ -193,8 +193,6 @@ apply (simp add: set_rel_def, fast) done -declare [[map set = (set_rel, Quotient_set)]] - lemma set_invariant_commute [invariant_commute]: "set_rel (Lifting.invariant P) = Lifting.invariant (\A. Ball A P)" unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Thu Apr 26 12:01:58 2012 +0200 @@ -92,7 +92,7 @@ subsection {* Setup for lifting package *} -lemma Quotient_sum: +lemma Quotient_sum[quot_map]: assumes "Quotient R1 Abs1 Rep1 T1" assumes "Quotient R2 Abs2 Rep2 T2" shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) @@ -100,8 +100,6 @@ using assms unfolding Quotient_alt_def by (simp add: split_sum_all) -declare [[map sum = (sum_rel, Quotient_sum)]] - fun sum_pred :: "('a \ bool) \ ('b \ bool) \ 'a + 'b \ bool" where "sum_pred R1 R2 (Inl a) = R1 a" diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Lifting.thy Thu Apr 26 12:01:58 2012 +0200 @@ -360,7 +360,7 @@ use "Tools/Lifting/lifting_info.ML" setup Lifting_Info.setup -declare [[map "fun" = (fun_rel, fun_quotient)]] +declare fun_quotient[quot_map] use "Tools/Lifting/lifting_term.ML" diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu Apr 26 12:01:58 2012 +0200 @@ -6,7 +6,7 @@ signature LIFTING_INFO = sig - type quotmaps = {relmap: string, quot_thm: thm} + type quotmaps = {rel_quot_thm: thm} val lookup_quotmaps: Proof.context -> string -> quotmaps option val lookup_quotmaps_global: theory -> string -> quotmaps option val print_quotmaps: Proof.context -> unit @@ -27,10 +27,12 @@ structure Lifting_Info: LIFTING_INFO = struct +open Lifting_Util + (** data containers **) -(* info about map- and rel-functions for a type *) -type quotmaps = {relmap: string, quot_thm: thm} +(* info about Quotient map theorems *) +type quotmaps = {rel_quot_thm: thm} structure Quotmaps = Generic_Data ( @@ -45,26 +47,28 @@ (* FIXME export proper internal update operation!? *) +fun add_quot_map rel_quot_thm ctxt = + let + val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm + val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl + val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs + val minfo = {rel_quot_thm = rel_quot_thm} + in + Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt + end + val quotmaps_attribute_setup = - Attrib.setup @{binding map} - ((Args.type_name true --| Scan.lift @{keyword "="}) -- - (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} -- - Attrib.thm --| Scan.lift @{keyword ")"}) >> - (fn (tyname, (relname, qthm)) => - let val minfo = {relmap = relname, quot_thm = qthm} - in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) - "declaration of map information" + Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map)) + "declaration of the Quotient map theorem" fun print_quotmaps ctxt = let - fun prt_map (ty_name, {relmap, quot_thm}) = + fun prt_map (ty_name, {rel_quot_thm}) = Pretty.block (separate (Pretty.brk 2) [Pretty.str "type:", Pretty.str ty_name, - Pretty.str "relation map:", - Pretty.str relmap, Pretty.str "quot. theorem:", - Syntax.pretty_term ctxt (prop_of quot_thm)]) + Syntax.pretty_term ctxt (prop_of rel_quot_thm)]) in map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) |> Pretty.big_list "maps for type constructors:" diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Apr 26 12:01:58 2012 +0200 @@ -76,7 +76,7 @@ val thy = Proof_Context.theory_of ctxt in (case Lifting_Info.lookup_quotmaps ctxt s of - SOME map_data => Thm.transfer thy (#quot_thm map_data) + SOME map_data => Thm.transfer thy (#rel_quot_thm map_data) | NONE => raise QUOT_THM_INTERNAL (Pretty.block [Pretty.str ("No relator for the type " ^ quote s), Pretty.brk 1, @@ -85,10 +85,6 @@ fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient}) -fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr) - = (rel, abs, rep, cr) - | dest_Quotient t = raise TERM ("dest_Quotient", [t]) - fun quot_thm_rel quot_thm = case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of (rel, _, _, _) => rel diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Thu Apr 26 12:01:58 2012 +0200 @@ -8,6 +8,7 @@ sig val MRSL: thm list * thm -> thm val Trueprop_conv: conv -> conv + val dest_Quotient: term -> term * term * term * term end; @@ -23,4 +24,8 @@ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct | _ => raise CTERM ("Trueprop_conv", [ct])) +fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr) + = (rel, abs, rep, cr) + | dest_Quotient t = raise TERM ("dest_Quotient", [t]) + end;