store the relational theorem for every relator
authorkuncar
Fri Mar 23 14:20:09 2012 +0100 (2012-03-23)
changeset 470941a7ad2601cb5
parent 47093 0516a6c1ea59
child 47095 b43ddeea727f
store the relational theorem for every relator
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.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 Mar 23 14:18:43 2012 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Mar 23 14:20:09 2012 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  imports Main Quotient_Syntax
     1.5  begin
     1.6  
     1.7 -declare [[map list = list_all2]]
     1.8 -
     1.9  lemma map_id [id_simps]:
    1.10    "map id = id"
    1.11    by (fact List.map.id)
    1.12 @@ -75,6 +73,8 @@
    1.13      by (induct xs ys rule: list_induct2') auto
    1.14  qed
    1.15  
    1.16 +declare [[map list = (list_all2, list_quotient)]]
    1.17 +
    1.18  lemma cons_prs [quot_preserve]:
    1.19    assumes q: "Quotient R Abs Rep"
    1.20    shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Mar 23 14:18:43 2012 +0100
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Mar 23 14:20:09 2012 +0100
     2.3 @@ -16,8 +16,6 @@
     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_rel]]
     2.8 -
     2.9  lemma option_rel_unfold:
    2.10    "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    2.11      | (Some x, Some y) \<Rightarrow> R x y
    2.12 @@ -65,6 +63,8 @@
    2.13    apply (simp add: option_rel_unfold split: option.split)
    2.14    done
    2.15  
    2.16 +declare [[map option = (option_rel, option_quotient)]]
    2.17 +
    2.18  lemma option_None_rsp [quot_respect]:
    2.19    assumes q: "Quotient R Abs Rep"
    2.20    shows "option_rel R None None"
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Mar 23 14:18:43 2012 +0100
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Mar 23 14:20:09 2012 +0100
     3.3 @@ -13,8 +13,6 @@
     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 = prod_rel]]
     3.8 -
     3.9  lemma prod_rel_apply [simp]:
    3.10    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    3.11    by (simp add: prod_rel_def)
    3.12 @@ -45,6 +43,8 @@
    3.13    apply (auto simp add: split_paired_all)
    3.14    done
    3.15  
    3.16 +declare [[map prod = (prod_rel, prod_quotient)]]
    3.17 +
    3.18  lemma Pair_rsp [quot_respect]:
    3.19    assumes q1: "Quotient R1 Abs1 Rep1"
    3.20    assumes q2: "Quotient R2 Abs2 Rep2"
     4.1 --- a/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:18:43 2012 +0100
     4.2 +++ b/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:20:09 2012 +0100
     4.3 @@ -26,6 +26,8 @@
     4.4      by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
     4.5  qed
     4.6  
     4.7 +declare [[map set = (set_rel, set_quotient)]]
     4.8 +
     4.9  lemma empty_set_rsp[quot_respect]:
    4.10    "set_rel R {} {}"
    4.11    unfolding set_rel_def by simp
     5.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Mar 23 14:18:43 2012 +0100
     5.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Mar 23 14:20:09 2012 +0100
     5.3 @@ -16,8 +16,6 @@
     5.4  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
     5.5  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
     5.6  
     5.7 -declare [[map sum = sum_rel]]
     5.8 -
     5.9  lemma sum_rel_unfold:
    5.10    "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    5.11      | (Inr x, Inr y) \<Rightarrow> R2 x y
    5.12 @@ -67,6 +65,8 @@
    5.13    apply (simp add: sum_rel_unfold comp_def split: sum.split)
    5.14    done
    5.15  
    5.16 +declare [[map sum = (sum_rel, sum_quotient)]]
    5.17 +
    5.18  lemma sum_Inl_rsp [quot_respect]:
    5.19    assumes q1: "Quotient R1 Abs1 Rep1"
    5.20    assumes q2: "Quotient R2 Abs2 Rep2"
     6.1 --- a/src/HOL/Quotient.thy	Fri Mar 23 14:18:43 2012 +0100
     6.2 +++ b/src/HOL/Quotient.thy	Fri Mar 23 14:20:09 2012 +0100
     6.3 @@ -686,8 +686,7 @@
     6.4  use "Tools/Quotient/quotient_info.ML"
     6.5  setup Quotient_Info.setup
     6.6  
     6.7 -declare [[map "fun" = fun_rel]]
     6.8 -declare [[map set = set_rel]]
     6.9 +declare [[map "fun" = (fun_rel, fun_quotient)]]
    6.10  
    6.11  lemmas [quot_thm] = fun_quotient
    6.12  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
     7.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:18:43 2012 +0100
     7.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:20:09 2012 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  signature QUOTIENT_INFO =
     7.6  sig
     7.7 -  type quotmaps = {relmap: string}
     7.8 +  type quotmaps = {relmap: string, 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 @@ -54,7 +54,7 @@
    7.13  (* FIXME just one data slot (record) per program unit *)
    7.14  
    7.15  (* info about map- and rel-functions for a type *)
    7.16 -type quotmaps = {relmap: string}
    7.17 +type quotmaps = {relmap: string, quot_thm: thm}
    7.18  
    7.19  structure Quotmaps = Generic_Data
    7.20  (
    7.21 @@ -71,19 +71,24 @@
    7.22  
    7.23  val quotmaps_attribute_setup =
    7.24    Attrib.setup @{binding map}
    7.25 -    ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >>
    7.26 -      (fn (tyname, relname) =>
    7.27 -        let val minfo = {relmap = relname}
    7.28 +    ((Args.type_name true --| Scan.lift (@{keyword "="})) --
    7.29 +      (Scan.lift (@{keyword "("}) |-- Args.const_proper true --| Scan.lift (@{keyword ","}) --
    7.30 +        Attrib.thm --| Scan.lift (@{keyword ")"})) >>
    7.31 +      (fn (tyname, (relname, qthm)) =>
    7.32 +        let val minfo = {relmap = relname, quot_thm = qthm}
    7.33          in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
    7.34      "declaration of map information"
    7.35  
    7.36  fun print_quotmaps ctxt =
    7.37    let
    7.38 -    fun prt_map (ty_name, {relmap}) =
    7.39 +    fun prt_map (ty_name, {relmap, quot_thm}) =
    7.40        Pretty.block (separate (Pretty.brk 2)
    7.41 -        (map Pretty.str
    7.42 -         ["type:", ty_name,
    7.43 -          "relation map:", relmap]))
    7.44 +         [Pretty.str "type:", 
    7.45 +          Pretty.str ty_name,
    7.46 +          Pretty.str "relation map:", 
    7.47 +          Pretty.str relmap,
    7.48 +          Pretty.str "quot. theorem:", 
    7.49 +          Syntax.pretty_term ctxt (prop_of quot_thm)])
    7.50    in
    7.51      map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
    7.52      |> Pretty.big_list "maps for type constructors:"