# HG changeset patch # User bulwahn # Date 1321620601 -3600 # Node ID 33b964e117bda276a24e7516641e9aa09ed85ed4 # Parent 6ea2bba2694a0b7e93671fff842aa3c960b3885f adding another example for lifting definitions diff -r 6ea2bba2694a -r 33b964e117bd src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Nov 18 13:42:07 2011 +0100 +++ b/src/HOL/IsaMakefile Fri Nov 18 13:50:01 2011 +0100 @@ -1508,7 +1508,7 @@ Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \ Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \ Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \ - Quotient_Examples/Lift_Set.thy + Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples diff -r 6ea2bba2694a -r 33b964e117bd src/HOL/Quotient_Examples/Lift_RBT.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Nov 18 13:50:01 2011 +0100 @@ -0,0 +1,135 @@ +(* Author: Lukas Bulwahn, TU Muenchen *) + +header {* Lifting operations of RBT trees *} + +theory Lift_RBT +imports Main "~~/src/HOL/Library/RBT_Impl" +begin + +subsection {* Type definition *} + +typedef (open) ('a, 'b) rbt = "{t :: ('a\linorder, 'b) RBT_Impl.rbt. is_rbt t}" + morphisms impl_of RBT +proof - + have "RBT_Impl.Empty \ ?rbt" by simp + then show ?thesis .. +qed + +local_setup {* fn lthy => +let + val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"}, + equiv_rel = @{term "dummy"}, 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 \ impl_of t1 = impl_of t2" + by (simp add: impl_of_inject) + +lemma rbt_eqI: + "impl_of t1 = impl_of t2 \ t1 = t2" + by (simp add: rbt_eq_iff) + +lemma is_rbt_impl_of [simp, intro]: + "is_rbt (impl_of t)" + using impl_of [of t] by simp + +lemma RBT_impl_of [simp, code abstype]: + "RBT (impl_of t) = t" + by (simp add: impl_of_inverse) + + +subsection {* Primitive operations *} + +quotient_definition lookup where "lookup :: ('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" + +declare lookup_def[unfolded map_fun_def comp_def id_def, code] + +(* FIXME: some bug in quotient?*) +(* +quotient_definition empty where "empty :: ('a\linorder, 'b) rbt" +is "RBT_Impl.Empty" +*) + +definition empty :: "('a\linorder, 'b) rbt" where + "empty = RBT RBT_Impl.Empty" + +lemma impl_of_empty [code abstract]: + "impl_of empty = RBT_Impl.Empty" + by (simp add: empty_def RBT_inverse) + +quotient_definition insert where "insert :: 'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" +is "RBT_Impl.insert" + +lemma impl_of_insert [code abstract]: + "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)" + by (simp add: insert_def RBT_inverse) + +quotient_definition delete where "delete :: 'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" +is "RBT_Impl.delete" + +lemma impl_of_delete [code abstract]: + "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)" + by (simp add: delete_def RBT_inverse) + +(* FIXME: bug in quotient? *) +(* +quotient_definition entries where "entries :: ('a\linorder, 'b) rbt \ ('a \ 'b) list" +is "RBT_Impl.entries" +*) +definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" where + [code]: "entries t = RBT_Impl.entries (impl_of t)" + +(* FIXME: bug in quotient? *) +(* +quotient_definition keys where "keys :: ('a\linorder, 'b) rbt \ 'a list" +is "RBT_Impl.keys" +*) + +quotient_definition "bulkload :: ('a\linorder \ 'b) list \ ('a, 'b) rbt" +is "RBT_Impl.bulkload" + +lemma impl_of_bulkload [code abstract]: + "impl_of (bulkload xs) = RBT_Impl.bulkload xs" + by (simp add: bulkload_def RBT_inverse) + +quotient_definition "map_entry :: 'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" +is "RBT_Impl.map_entry" + +lemma impl_of_map_entry [code abstract]: + "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)" + by (simp add: map_entry_def RBT_inverse) + +(* Another bug: map is supposed to be a new definition, not using the old one. +quotient_definition "map :: ('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" +is "RBT_Impl.map" +*) +(* But this works, and then shows the other bug... *) +(* +quotient_definition map where "map :: ('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" +is "RBT_Impl.map" +*) +definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where + "map f t = RBT (RBT_Impl.map f (impl_of t))" + +lemma impl_of_map [code abstract]: + "impl_of (map f t) = RBT_Impl.map f (impl_of t)" + by (simp add: map_def RBT_inverse) +(* FIXME: bug? +quotient_definition fold where "fold :: ('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" is "RBT_Impl.fold" +*) +(*FIXME: definition of fold should have the code attribute. *) + +definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" where + [code]: "fold f t = RBT_Impl.fold f (impl_of t)" + + +end \ No newline at end of file diff -r 6ea2bba2694a -r 33b964e117bd src/HOL/Quotient_Examples/ROOT.ML --- a/src/HOL/Quotient_Examples/ROOT.ML Fri Nov 18 13:42:07 2011 +0100 +++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Nov 18 13:50:01 2011 +0100 @@ -4,5 +4,6 @@ Testing the quotient package. *) -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset", "Lift_Set"]; +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", + "List_Quotient_Cset", "Lift_Set", "Lift_RBT"];