author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 58249  180f1b3508ed 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Discrete.thy 
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

2 
Author: Tobias Nipkow 
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

3 
*) 
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

4 

15578  5 
header {* Discrete cpo types *} 
6 

15555  7 
theory Discrete 
19105  8 
imports Cont 
15555  9 
begin 
10 

11 
datatype 'a discr = Discr "'a :: type" 

12 

40434  13 
subsection {* Discrete cpo class instance *} 
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

14 

40434  15 
instantiation discr :: (type) discrete_cpo 
25902  16 
begin 
15555  17 

25902  18 
definition 
40434  19 
"(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)" 
25902  20 

40434  21 
instance 
22 
by default (simp add: below_discr_def) 

15555  23 

40434  24 
end 
15555  25 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
31076
diff
changeset

26 
subsection {* \emph{undiscr} *} 
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

27 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

28 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

29 
undiscr :: "('a::type)discr => 'a" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

30 
"undiscr x = (case x of Discr y => y)" 
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

31 

26025  32 
lemma undiscr_Discr [simp]: "undiscr (Discr x) = x" 
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

33 
by (simp add: undiscr_def) 
15555  34 

26025  35 
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y" 
36 
by (induct y) simp 

37 

2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

38 
end 