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'
bulwahn@45576
     1
(*  Title:      HOL/Quotient_Examples/Lift_Set.thy
kuncar@45609
     2
    Author:     Lukas Bulwahn and Ondrej Kuncar
bulwahn@45536
     3
*)
bulwahn@45536
     4
kuncar@47308
     5
header {* Example of lifting definitions with the lifting infrastructure *}
bulwahn@45536
     6
bulwahn@45536
     7
theory Lift_Set
bulwahn@45536
     8
imports Main
bulwahn@45536
     9
begin
bulwahn@45536
    10
haftmann@45970
    11
definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
wenzelm@45694
    12
wenzelm@49834
    13
typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
wenzelm@45694
    14
  morphisms member Set
wenzelm@45694
    15
  unfolding set_def by auto
bulwahn@45536
    16
kuncar@47097
    17
setup_lifting type_definition_set[unfolded set_def]
bulwahn@45536
    18
kuncar@47308
    19
text {* Now, we can employ lift_definition to lift definitions. *}
bulwahn@45536
    20
kuncar@47308
    21
lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
bulwahn@45536
    22
bulwahn@45536
    23
term "Lift_Set.empty"
bulwahn@45536
    24
thm Lift_Set.empty_def
bulwahn@45536
    25
kuncar@47308
    26
lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done 
bulwahn@45536
    27
bulwahn@45536
    28
term "Lift_Set.insert"
bulwahn@45536
    29
thm Lift_Set.insert_def
bulwahn@45536
    30
kuncar@47097
    31
export_code empty insert in SML
kuncar@47097
    32
bulwahn@45536
    33
end
haftmann@45970
    34