1.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:17:29 2012 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:18:43 2012 +0100
     1.3 @@ -6,30 +6,15 @@
     1.4  imports Main "~~/src/HOL/Library/RBT_Impl"
     1.5  begin
     1.6  
     1.7 +definition inv :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
     1.8 +  where [simp]: "inv R = (\<lambda>x y. R x \<and> x = y)"
     1.9 +
    1.10  subsection {* Type definition *}
    1.11  
    1.12 -typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    1.13 -  morphisms impl_of RBT
    1.14 -proof -
    1.15 -  have "RBT_Impl.Empty \<in> ?rbt" by simp
    1.16 -  then show ?thesis ..
    1.17 -qed
    1.18 +quotient_type ('a, 'b) rbt = "('a\<Colon>linorder, 'b) RBT_Impl.rbt" / "inv is_rbt" morphisms impl_of RBT
    1.19 +sorry
    1.20  
    1.21 -local_setup {* fn lthy =>
    1.22 -let
    1.23 -  val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"},
    1.24 -    equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
    1.25 -  val qty_full_name = @{type_name "rbt"}
    1.26 -
    1.27 -  fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    1.28 -  in lthy
    1.29 -    |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.30 -        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
    1.31 -       #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi
    1.32 -         {abs = @{term "RBT"}, rep = @{term "impl_of"}}))
    1.33 -  end
    1.34 -*}
    1.35 -
    1.36 +(*
    1.37  lemma rbt_eq_iff:
    1.38    "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
    1.39    by (simp add: impl_of_inject)
    1.40 @@ -45,12 +30,12 @@
    1.41  lemma RBT_impl_of [simp, code abstype]:
    1.42    "RBT (impl_of t) = t"
    1.43    by (simp add: impl_of_inverse)
    1.44 -
    1.45 +*)
    1.46  
    1.47  subsection {* Primitive operations *}
    1.48  
    1.49  quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
    1.50 -done
    1.51 +by simp
    1.52  
    1.53  declare lookup_def[unfolded map_fun_def comp_def id_def, code]
    1.54  

     2.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:17:29 2012 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:18:43 2012 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4    val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
     2.5    val print_abs_rep: Proof.context -> unit
     2.6    
     2.7 -  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
     2.8 +  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
     2.9    val transform_quotients: morphism -> quotients -> quotients
    2.10    val lookup_quotients: Proof.context -> string -> quotients option
    2.11    val lookup_quotients_global: theory -> string -> quotients option
    2.12 @@ -125,7 +125,7 @@
    2.13    end
    2.14  
    2.15  (* info about quotient types *)
    2.16 -type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    2.17 +type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
    2.18  
    2.19  structure Quotients = Generic_Data
    2.20  (
    2.21 @@ -135,11 +135,12 @@
    2.22    fun merge data = Symtab.merge (K true) data
    2.23  )
    2.24  
    2.25 -fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
    2.26 +fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
    2.27    {qtyp = Morphism.typ phi qtyp,
    2.28     rtyp = Morphism.typ phi rtyp,
    2.29     equiv_rel = Morphism.term phi equiv_rel,
    2.30 -   equiv_thm = Morphism.thm phi equiv_thm}
    2.31 +   equiv_thm = Morphism.thm phi equiv_thm,
    2.32 +   quot_thm = Morphism.thm phi quot_thm}
    2.33  
    2.34  val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
    2.35  val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
    2.36 @@ -151,7 +152,7 @@
    2.37  
    2.38  fun print_quotients ctxt =
    2.39    let
    2.40 -    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
    2.41 +    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
    2.42        Pretty.block (separate (Pretty.brk 2)
    2.43         [Pretty.str "quotient type:",
    2.44          Syntax.pretty_typ ctxt qtyp,
    2.45 @@ -160,7 +161,9 @@
    2.46          Pretty.str "relation:",
    2.47          Syntax.pretty_term ctxt equiv_rel,
    2.48          Pretty.str "equiv. thm:",
    2.49 -        Syntax.pretty_term ctxt (prop_of equiv_thm)])
    2.50 +        Syntax.pretty_term ctxt (prop_of equiv_thm),
    2.51 +        Pretty.str "quot. thm:",
    2.52 +        Syntax.pretty_term ctxt (prop_of quot_thm)])
    2.53    in
    2.54      map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
    2.55      |> Pretty.big_list "quotients:"

     3.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:17:29 2012 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:18:43 2012 +0100
     3.3 @@ -126,7 +126,8 @@
     3.4      val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
     3.5  
     3.6      (* storing the quotients *)
     3.7 -    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
     3.8 +    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm, 
     3.9 +      quot_thm = quotient_thm}
    3.10  
    3.11      fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    3.12      fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}