1.1 --- a/src/HOL/IsaMakefile	Fri Nov 18 13:42:07 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Nov 18 13:50:01 2011 +0100
     1.3 @@ -1508,7 +1508,7 @@
     1.4    Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
     1.5    Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
     1.6    Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
     1.7 -  Quotient_Examples/Lift_Set.thy
     1.8 +  Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy
     1.9  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
    1.10  
    1.11  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Nov 18 13:50:01 2011 +0100
     2.3 @@ -0,0 +1,135 @@
     2.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
     2.5 +
     2.6 +header {* Lifting operations of RBT trees *}
     2.7 +
     2.8 +theory Lift_RBT 
     2.9 +imports Main "~~/src/HOL/Library/RBT_Impl"
    2.10 +begin
    2.11 +
    2.12 +subsection {* Type definition *}
    2.13 +
    2.14 +typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    2.15 +  morphisms impl_of RBT
    2.16 +proof -
    2.17 +  have "RBT_Impl.Empty \<in> ?rbt" by simp
    2.18 +  then show ?thesis ..
    2.19 +qed
    2.20 +
    2.21 +local_setup {* fn lthy =>
    2.22 +let
    2.23 +  val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"},
    2.24 +    equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
    2.25 +  val qty_full_name = @{type_name "rbt"}
    2.26 +
    2.27 +  fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    2.28 +  in lthy
    2.29 +    |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.30 +        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
    2.31 +       #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi
    2.32 +         {abs = @{term "RBT"}, rep = @{term "impl_of"}}))
    2.33 +  end
    2.34 +*}
    2.35 +
    2.36 +lemma rbt_eq_iff:
    2.37 +  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
    2.38 +  by (simp add: impl_of_inject)
    2.39 +
    2.40 +lemma rbt_eqI:
    2.41 +  "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
    2.42 +  by (simp add: rbt_eq_iff)
    2.43 +
    2.44 +lemma is_rbt_impl_of [simp, intro]:
    2.45 +  "is_rbt (impl_of t)"
    2.46 +  using impl_of [of t] by simp
    2.47 +
    2.48 +lemma RBT_impl_of [simp, code abstype]:
    2.49 +  "RBT (impl_of t) = t"
    2.50 +  by (simp add: impl_of_inverse)
    2.51 +
    2.52 +
    2.53 +subsection {* Primitive operations *}
    2.54 +
    2.55 +quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
    2.56 +
    2.57 +declare lookup_def[unfolded map_fun_def comp_def id_def, code]
    2.58 +
    2.59 +(* FIXME: some bug in quotient?*)
    2.60 +(*
    2.61 +quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
    2.62 +is "RBT_Impl.Empty"
    2.63 +*)
    2.64 +
    2.65 +definition empty :: "('a\<Colon>linorder, 'b) rbt" where
    2.66 +  "empty = RBT RBT_Impl.Empty"
    2.67 +
    2.68 +lemma impl_of_empty [code abstract]:
    2.69 +  "impl_of empty = RBT_Impl.Empty"
    2.70 +  by (simp add: empty_def RBT_inverse)
    2.71 +
    2.72 +quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    2.73 +is "RBT_Impl.insert"
    2.74 +
    2.75 +lemma impl_of_insert [code abstract]:
    2.76 +  "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
    2.77 +  by (simp add: insert_def RBT_inverse)
    2.78 +
    2.79 +quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    2.80 +is "RBT_Impl.delete"
    2.81 +
    2.82 +lemma impl_of_delete [code abstract]:
    2.83 +  "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
    2.84 +  by (simp add: delete_def RBT_inverse)
    2.85 +
    2.86 +(* FIXME: bug in quotient? *)
    2.87 +(*
    2.88 +quotient_definition entries where "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
    2.89 +is "RBT_Impl.entries"
    2.90 +*)
    2.91 +definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where
    2.92 +  [code]: "entries t = RBT_Impl.entries (impl_of t)"
    2.93 +
    2.94 +(* FIXME: bug in quotient? *)
    2.95 +(*
    2.96 +quotient_definition keys where "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
    2.97 +is "RBT_Impl.keys"
    2.98 +*)
    2.99 +
   2.100 +quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
   2.101 +is "RBT_Impl.bulkload"
   2.102 +
   2.103 +lemma impl_of_bulkload [code abstract]:
   2.104 +  "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
   2.105 +  by (simp add: bulkload_def RBT_inverse)
   2.106 +
   2.107 +quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   2.108 +is "RBT_Impl.map_entry"
   2.109 +
   2.110 +lemma impl_of_map_entry [code abstract]:
   2.111 +  "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
   2.112 +  by (simp add: map_entry_def RBT_inverse)
   2.113 +
   2.114 +(* Another bug: map is supposed to be a new definition, not using the old one.
   2.115 +quotient_definition "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   2.116 +is "RBT_Impl.map"
   2.117 +*)
   2.118 +(* But this works, and then shows the other bug... *)
   2.119 +(*
   2.120 +quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   2.121 +is "RBT_Impl.map"
   2.122 +*)
   2.123 +definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
   2.124 +  "map f t = RBT (RBT_Impl.map f (impl_of t))"
   2.125 +
   2.126 +lemma impl_of_map [code abstract]:
   2.127 +  "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
   2.128 +  by (simp add: map_def RBT_inverse)
   2.129 +(* FIXME: bug?
   2.130 +quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is "RBT_Impl.fold"
   2.131 +*)
   2.132 +(*FIXME: definition of fold should have the code attribute. *)
   2.133 +
   2.134 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
   2.135 +  [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
   2.136 +
   2.137 +
   2.138 +end
   2.139 \ No newline at end of file

     3.1 --- a/src/HOL/Quotient_Examples/ROOT.ML	Fri Nov 18 13:42:07 2011 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML	Fri Nov 18 13:50:01 2011 +0100
     3.3 @@ -4,5 +4,6 @@
     3.4  Testing the quotient package.
     3.5  *)
     3.6  
     3.7 -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset", "Lift_Set"];
     3.8 +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset",
     3.9 +  "List_Quotient_Cset", "Lift_Set", "Lift_RBT"];
    3.10