src/HOL/Quotient_Examples/Lift_Set.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 63167 0909deb8059b
child 70009 435fb018e8ee
permissions -rw-r--r--
more fundamental definition of div and mod on int
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
wenzelm@63167
     5
section \<open>Example of lifting definitions with the lifting infrastructure\<close>
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
blanchet@55584
    15
  unfolding set_def by (rule UNIV_witness)
bulwahn@45536
    16
kuncar@47097
    17
setup_lifting type_definition_set[unfolded set_def]
bulwahn@45536
    18
wenzelm@63167
    19
text \<open>Now, we can employ lift_definition to lift definitions.\<close>
bulwahn@45536
    20
blanchet@55584
    21
lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" .
bulwahn@45536
    22
bulwahn@45536
    23
term "Lift_Set.empty"
bulwahn@45536
    24
thm Lift_Set.empty_def
bulwahn@45536
    25
blanchet@55584
    26
lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" . 
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