author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 19105  3aabd46340e0 
child 25131  2c8caac48ade 
permissions  rwrr 
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

1 
(* Title: HOLCF/Discrete.thy 
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

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

4 

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

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

7 

15578  8 
header {* Discrete cpo types *} 
9 

15555  10 
theory Discrete 
19105  11 
imports Cont 
15555  12 
begin 
13 

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

15 

15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

16 
subsection {* Type @{typ "'a discr"} is a partial order *} 
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

17 

15555  18 
instance discr :: (type) sq_ord .. 
19 

20 
defs (overloaded) 

21 
less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool) == op =" 

22 

23 
lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)" 

15639  24 
by (unfold less_discr_def) (rule refl) 
15555  25 

26 
instance discr :: (type) po 

27 
proof 

28 
fix x y z :: "'a discr" 

29 
show "x << x" by simp 

30 
{ assume "x << y" and "y << x" thus "x = y" by simp } 

31 
{ assume "x << y" and "y << z" thus "x << z" by simp } 

32 
qed 

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

33 

15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

34 
subsection {* Type @{typ "'a discr"} is a cpo *} 
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

35 

15555  36 
lemma discr_chain0: 
37 
"!!S::nat=>('a::type)discr. chain S ==> S i = S 0" 

38 
apply (unfold chain_def) 

39 
apply (induct_tac "i") 

40 
apply (rule refl) 

41 
apply (erule subst) 

42 
apply (rule sym) 

43 
apply fast 

44 
done 

45 

15639  46 
lemma discr_chain_range0 [simp]: 
15555  47 
"!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}" 
15639  48 
by (fast elim: discr_chain0) 
15555  49 

50 
lemma discr_cpo: 

51 
"!!S. chain S ==> ? x::('a::type)discr. range(S) << x" 

15639  52 
by (unfold is_lub_def is_ub_def) simp 
15555  53 

15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

54 
instance discr :: (type) cpo 
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

55 
by intro_classes (rule discr_cpo) 
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

56 

17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

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

58 

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

59 
constdefs 
15555  60 
undiscr :: "('a::type)discr => 'a" 
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset

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

62 

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

64 
by (simp add: undiscr_def) 
15555  65 

66 
lemma discr_chain_f_range0: 

67 
"!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}" 

15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

68 
by (fast dest: discr_chain0 elim: arg_cong) 
15555  69 

70 
lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)" 

16213  71 
apply (unfold cont_def is_lub_def is_ub_def) 
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset

72 
apply (simp add: discr_chain_f_range0) 
15555  73 
done 
74 

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

75 
end 