src/HOL/Quotient_Examples/Lift_Set.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 49834 b27bbb021df1
child 55584 a879f14b6f95
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     1 (*  Title:      HOL/Quotient_Examples/Lift_Set.thy
     2     Author:     Lukas Bulwahn and Ondrej Kuncar
     3 *)
     4 
     5 header {* Example of lifting definitions with the lifting infrastructure *}
     6 
     7 theory Lift_Set
     8 imports Main
     9 begin
    10 
    11 definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
    12 
    13 typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
    14   morphisms member Set
    15   unfolding set_def by auto
    16 
    17 setup_lifting type_definition_set[unfolded set_def]
    18 
    19 text {* Now, we can employ lift_definition to lift definitions. *}
    20 
    21 lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
    22 
    23 term "Lift_Set.empty"
    24 thm Lift_Set.empty_def
    25 
    26 lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done 
    27 
    28 term "Lift_Set.insert"
    29 thm Lift_Set.insert_def
    30 
    31 export_code empty insert in SML
    32 
    33 end
    34