1.1 --- a/src/HOL/IsaMakefile	Thu Nov 17 18:44:56 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Nov 17 19:01:05 2011 +0100
     1.3 @@ -1507,7 +1507,8 @@
     1.4  $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
     1.5    Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
     1.6    Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
     1.7 -  Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy
     1.8 +  Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
     1.9 +  Quotient_Examples/Lift_Set.thy
    1.10  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
    1.11  
    1.12  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Thu Nov 17 19:01:05 2011 +0100
     2.3 @@ -0,0 +1,43 @@
     2.4 +(*  Title:      HOL/Quotient.thy
     2.5 +    Author:     Lukas Bulwahn and Ondrey Kuncar
     2.6 +*)
     2.7 +
     2.8 +header {* Example of lifting definitions with the quotient infrastructure *}
     2.9 +
    2.10 +theory Lift_Set
    2.11 +imports Main
    2.12 +begin
    2.13 +
    2.14 +typedef 'a set = "(UNIV :: ('a => bool) => bool)"
    2.15 +morphisms member Set by auto
    2.16 +
    2.17 +text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
    2.18 +
    2.19 +local_setup {* fn lthy =>
    2.20 +let
    2.21 +  val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
    2.22 +  val qty_full_name = @{type_name "set"}
    2.23 +
    2.24 +  fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    2.25 +  in lthy
    2.26 +    |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.27 +        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
    2.28 +       #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
    2.29 +  end
    2.30 +*}
    2.31 +
    2.32 +text {* Now, we can employ quotient_definition to lift definitions. *}
    2.33 +
    2.34 +quotient_definition empty where "empty :: 'a set"
    2.35 +is "Set.empty"
    2.36 +
    2.37 +term "Lift_Set.empty"
    2.38 +thm Lift_Set.empty_def
    2.39 +
    2.40 +quotient_definition insert where "insert :: 'a => 'a set => 'a set"
    2.41 +is "Set.insert"
    2.42 +
    2.43 +term "Lift_Set.insert"
    2.44 +thm Lift_Set.insert_def
    2.45 +
    2.46 +end

     3.1 --- a/src/HOL/Quotient_Examples/ROOT.ML	Thu Nov 17 18:44:56 2011 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML	Thu Nov 17 19:01:05 2011 +0100
     3.3 @@ -4,5 +4,5 @@
     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"];
     3.8 +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset", "Lift_Set"];
     3.9