--- 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)
--- 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 \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
where
"option_pred R None = True"
--- 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 \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
--- 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 (\<lambda>A. Ball A P)"
unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast
--- 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 \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
where
"sum_pred R1 R2 (Inl a) = R1 a"
--- 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"
--- 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:"
--- 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
--- 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;