author kuncar Fri, 23 Mar 2012 14:18:43 +0100 changeset 47093 0516a6c1ea59 parent 47092 fa3538d6004b child 47094 1a7ad2601cb5
store the quotient theorem for every quotient
```--- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:17:29 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:18:43 2012 +0100
@@ -6,30 +6,15 @@
imports Main "~~/src/HOL/Library/RBT_Impl"
begin

+definition inv :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+  where [simp]: "inv R = (\<lambda>x y. R x \<and> x = y)"
+
subsection {* Type definition *}

-typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
-  morphisms impl_of RBT
-proof -
-  have "RBT_Impl.Empty \<in> ?rbt" by simp
-  then show ?thesis ..
-qed
+quotient_type ('a, 'b) rbt = "('a\<Colon>linorder, 'b) RBT_Impl.rbt" / "inv is_rbt" morphisms impl_of RBT
+sorry

-local_setup {* fn lthy =>
-let
-  val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"},
-    equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
-  val qty_full_name = @{type_name "rbt"}
-
-  fun qinfo phi = Quotient_Info.transform_quotients phi quotients
-  in lthy
-    |> Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
-       #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi
-         {abs = @{term "RBT"}, rep = @{term "impl_of"}}))
-  end
-*}
-
+(*
lemma rbt_eq_iff:
"t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
@@ -45,12 +30,12 @@
lemma RBT_impl_of [simp, code abstype]:
"RBT (impl_of t) = t"
-
+*)

subsection {* Primitive operations *}

quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
-done
+by simp

declare lookup_def[unfolded map_fun_def comp_def id_def, code]
```
```--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:17:29 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:18:43 2012 +0100
@@ -18,7 +18,7 @@
val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
val print_abs_rep: Proof.context -> unit

-  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
val transform_quotients: morphism -> quotients -> quotients
val lookup_quotients: Proof.context -> string -> quotients option
val lookup_quotients_global: theory -> string -> quotients option
@@ -125,7 +125,7 @@
end

(* info about quotient types *)
-type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}

structure Quotients = Generic_Data
(
@@ -135,11 +135,12 @@
fun merge data = Symtab.merge (K true) data
)

-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
+fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
{qtyp = Morphism.typ phi qtyp,
rtyp = Morphism.typ phi rtyp,
equiv_rel = Morphism.term phi equiv_rel,
-   equiv_thm = Morphism.thm phi equiv_thm}
+   equiv_thm = Morphism.thm phi equiv_thm,
+   quot_thm = Morphism.thm phi quot_thm}

val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
@@ -151,7 +152,7 @@

fun print_quotients ctxt =
let
-    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
+    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
Pretty.block (separate (Pretty.brk 2)
[Pretty.str "quotient type:",
Syntax.pretty_typ ctxt qtyp,
@@ -160,7 +161,9 @@
Pretty.str "relation:",
Syntax.pretty_term ctxt equiv_rel,
Pretty.str "equiv. thm:",
-        Syntax.pretty_term ctxt (prop_of equiv_thm)])
+        Syntax.pretty_term ctxt (prop_of equiv_thm),
+        Pretty.str "quot. thm:",
+        Syntax.pretty_term ctxt (prop_of quot_thm)])
in
map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
|> Pretty.big_list "quotients:"```
```--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:17:29 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:18:43 2012 +0100
@@ -126,7 +126,8 @@
val equiv_thm_name = Binding.suffix_name "_equivp" qty_name

(* storing the quotients *)
-    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
+    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm,
+      quot_thm = quotient_thm}

fun qinfo phi = Quotient_Info.transform_quotients phi quotients
fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}```