# HG changeset patch
# User bulwahn
# Date 1321552865 -3600
# Node ID 5b0b1dc2e40f30f99d21adf06fed1a54d5837a6c
# Parent  fbad87611fae2335a015271d948f7031d97f1a40
adding a preliminary example to show how the quotient_definition package can be generalized

diff -r fbad87611fae -r 5b0b1dc2e40f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Nov 17 18:44:56 2011 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 17 19:01:05 2011 +0100
@@ -1507,7 +1507,8 @@
 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
   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/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
+  Quotient_Examples/Lift_Set.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
 
 
diff -r fbad87611fae -r 5b0b1dc2e40f src/HOL/Quotient_Examples/Lift_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Thu Nov 17 19:01:05 2011 +0100
@@ -0,0 +1,43 @@
+(*  Title:      HOL/Quotient.thy
+    Author:     Lukas Bulwahn and Ondrey Kuncar
+*)
+
+header {* Example of lifting definitions with the quotient infrastructure *}
+
+theory Lift_Set
+imports Main
+begin
+
+typedef 'a set = "(UNIV :: ('a => bool) => bool)"
+morphisms member Set by auto
+
+text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
+
+local_setup {* fn lthy =>
+let
+  val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+  val qty_full_name = @{type_name "set"}
+
+  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 "Set"}, rep = @{term "member"}}))
+  end
+*}
+
+text {* Now, we can employ quotient_definition to lift definitions. *}
+
+quotient_definition empty where "empty :: 'a set"
+is "Set.empty"
+
+term "Lift_Set.empty"
+thm Lift_Set.empty_def
+
+quotient_definition insert where "insert :: 'a => 'a set => 'a set"
+is "Set.insert"
+
+term "Lift_Set.insert"
+thm Lift_Set.insert_def
+
+end
diff -r fbad87611fae -r 5b0b1dc2e40f src/HOL/Quotient_Examples/ROOT.ML
--- a/src/HOL/Quotient_Examples/ROOT.ML	Thu Nov 17 18:44:56 2011 +0100
+++ b/src/HOL/Quotient_Examples/ROOT.ML	Thu Nov 17 19:01:05 2011 +0100
@@ -4,5 +4,5 @@
 Testing the quotient package.
 *)
 
-use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset"];
+use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset", "Lift_Set"];