author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 18111  2b56f74fd605 
child 25131  2c8caac48ade 
permissions  rwrr 
2640  1 
(* Title: HOLCF/One.thy 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
2640  3 
Author: Oscar Slotosch 
16070
4a83dd540b88
removed LICENCE note  everything is subject to Isabelle licence as
wenzelm
parents:
15577
diff
changeset

4 

4a83dd540b88
removed LICENCE note  everything is subject to Isabelle licence as
wenzelm
parents:
15577
diff
changeset

5 
The unit domain. 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

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

7 

15577  8 
header {* The unit domain *} 
9 

10 
theory One 

11 
imports Lift 

12 
begin 

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

13 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

14 
types one = "unit lift" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

15 

3717  16 
constdefs 
17 
ONE :: "one" 

16747  18 
"ONE \<equiv> Def ()" 
2640  19 

20 
translations 

3717  21 
"one" <= (type) "unit lift" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

22 

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

24 

16747  25 
lemma Exh_one: "t = \<bottom> \<or> t = ONE" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

26 
apply (unfold ONE_def) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

27 
apply (induct t) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

28 
apply simp 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

29 
apply simp 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

30 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

31 

16747  32 
lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

33 
apply (rule Exh_one [THEN disjE]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

34 
apply fast 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

35 
apply fast 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

36 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

37 

16747  38 
lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

39 
apply (unfold ONE_def) 
16747  40 
apply simp 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

41 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

42 

16747  43 
lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

44 
apply (unfold ONE_def) 
16747  45 
apply simp_all 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

46 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

47 

17838  48 
lemma compact_ONE [simp]: "compact ONE" 
49 
by (rule compact_chfin) 

50 

18080  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 

18111  58 
"case x of ONE \<Rightarrow> t" == "one_when\<cdot>t\<cdot>x" 
18080  59 
"\<Lambda> ONE. t" == "one_when\<cdot>t" 
60 

18111  61 
lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>" 
18080  62 
by (simp add: one_when_def) 
63 

18111  64 
lemma one_when2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t" 
18080  65 
by (simp add: one_when_def) 
66 

18111  67 
lemma one_when3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x" 
18080  68 
by (rule_tac p=x in oneE, simp_all) 
69 

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

70 
end 