equal
deleted
inserted
replaced
46 done |
46 done |
47 |
47 |
48 lemma compact_ONE [simp]: "compact ONE" |
48 lemma compact_ONE [simp]: "compact ONE" |
49 by (rule compact_chfin) |
49 by (rule compact_chfin) |
50 |
50 |
|
51 text {* Case analysis function for type @{typ one} *} |
|
52 |
|
53 constdefs |
|
54 one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" |
|
55 "one_when \<equiv> \<Lambda> a. strictify\<cdot>(\<Lambda> _. a)" |
|
56 |
|
57 translations |
|
58 "\<Lambda> ONE. t" == "one_when\<cdot>t" |
|
59 |
|
60 lemma one_when1 [simp]: "(\<Lambda> ONE. t)\<cdot>\<bottom> = \<bottom>" |
|
61 by (simp add: one_when_def) |
|
62 |
|
63 lemma one_when2 [simp]: "(\<Lambda> ONE. t)\<cdot>ONE = t" |
|
64 by (simp add: one_when_def) |
|
65 |
|
66 lemma one_when3 [simp]: "(\<Lambda> ONE. ONE)\<cdot>x = x" |
|
67 by (rule_tac p=x in oneE, simp_all) |
|
68 |
51 end |
69 end |