src/HOL/Quotient_Examples/Lift_Set.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47308 9caab698dbe4
child 49834 b27bbb021df1
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45576
6ea2bba2694a improving header
bulwahn
parents: 45536
diff changeset
     1
(*  Title:      HOL/Quotient_Examples/Lift_Set.thy
45609
2c0c8ce96f4a misspelled name
kuncar
parents: 45576
diff changeset
     2
    Author:     Lukas Bulwahn and Ondrej Kuncar
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
     3
*)
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
     4
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
     5
header {* Example of lifting definitions with the lifting infrastructure *}
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
     6
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
     7
theory Lift_Set
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
     8
imports Main
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
     9
begin
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    10
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45694
diff changeset
    11
definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45609
diff changeset
    12
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45694
diff changeset
    13
typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45609
diff changeset
    14
  morphisms member Set
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45609
diff changeset
    15
  unfolding set_def by auto
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    16
47097
987cb55cac44 fix example files
kuncar
parents: 47092
diff changeset
    17
setup_lifting type_definition_set[unfolded set_def]
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    18
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    19
text {* Now, we can employ lift_definition to lift definitions. *}
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    20
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    21
lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    22
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    23
term "Lift_Set.empty"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    24
thm Lift_Set.empty_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    25
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    26
lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done 
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    27
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    28
term "Lift_Set.insert"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    29
thm Lift_Set.insert_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    30
47097
987cb55cac44 fix example files
kuncar
parents: 47092
diff changeset
    31
export_code empty insert in SML
987cb55cac44 fix example files
kuncar
parents: 47092
diff changeset
    32
45536
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
diff changeset
    33
end
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45694
diff changeset
    34