author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47308  9caab698dbe4 
child 49834  b27bbb021df1 
permissions  rwrr 
45576  1 
(* Title: HOL/Quotient_Examples/Lift_Set.thy 
45609  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  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  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  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  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  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  31 
export_code empty insert in SML 
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 