author  huffman 
Sun, 19 Dec 2010 18:11:20 0800  
changeset 41295  5b5388d4ccc9 
parent 41182  717404c7d59a 
child 42151  4da4fc77664b 
permissions  rwrr 
2640  1 
(* Title: HOLCF/One.thy 
2 
Author: Oscar Slotosch 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

3 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

4 

15577  5 
header {* The unit domain *} 
6 

7 
theory One 

8 
imports Lift 

9 
begin 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

10 

41295  11 
type_synonym 
12 
one = "unit lift" 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

13 

41295  14 
translations 
15 
(type) "one" <= (type) "unit lift" 

16 

17 
definition ONE :: "one" 

18 
where "ONE == Def ()" 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

19 

16747  20 
text {* Exhaustion and Elimination for type @{typ one} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

21 

16747  22 
lemma Exh_one: "t = \<bottom> \<or> t = ONE" 
27293  23 
unfolding ONE_def by (induct t) simp_all 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

24 

35783  25 
lemma oneE [case_names bottom ONE]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
27293  26 
unfolding ONE_def by (induct p) simp_all 
27 

35783  28 
lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x" 
27293  29 
by (cases x rule: oneE) simp_all 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

30 

41182  31 
lemma dist_below_one [simp]: "ONE \<notsqsubseteq> \<bottom>" 
27293  32 
unfolding ONE_def by simp 
33 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30911
diff
changeset

34 
lemma below_ONE [simp]: "x \<sqsubseteq> ONE" 
27293  35 
by (induct x rule: one_induct) simp_all 
36 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30911
diff
changeset

37 
lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE" 
27293  38 
by (induct x rule: one_induct) simp_all 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

39 

30911
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
29141
diff
changeset

40 
lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>" 
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
29141
diff
changeset

41 
unfolding ONE_def by simp 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

42 

27293  43 
lemma one_neq_iffs [simp]: 
44 
"x \<noteq> ONE \<longleftrightarrow> x = \<bottom>" 

45 
"ONE \<noteq> x \<longleftrightarrow> x = \<bottom>" 

46 
"x \<noteq> \<bottom> \<longleftrightarrow> x = ONE" 

47 
"\<bottom> \<noteq> x \<longleftrightarrow> x = ONE" 

48 
by (induct x rule: one_induct) simp_all 

49 

50 
lemma compact_ONE: "compact ONE" 

17838  51 
by (rule compact_chfin) 
52 

18080  53 
text {* Case analysis function for type @{typ one} *} 
54 

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

55 
definition 
40212  56 
one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40212
diff
changeset

57 
"one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)" 
18080  58 

59 
translations 

40212  60 
"case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x" 
61 
"\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t" 

18080  62 

40212  63 
lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>" 
64 
by (simp add: one_case_def) 

18080  65 

40212  66 
lemma one_case2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t" 
67 
by (simp add: one_case_def) 

18080  68 

40212  69 
lemma one_case3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x" 
27293  70 
by (induct x rule: one_induct) simp_all 
18080  71 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

72 
end 