author | wenzelm |
Sat, 29 Mar 2008 19:14:16 +0100 | |
changeset 26494 | 6816ca8b48ef |
parent 25131 | 2c8caac48ade |
child 27293 | de9a2fd0eab4 |
permissions | -rw-r--r-- |
2640 | 1 |
(* Title: HOLCF/One.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order 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 Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order 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 Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
14 |
types one = "unit lift" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
15 |
translations |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
16 |
"one" <= (type) "unit lift" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
|
3717 | 18 |
constdefs |
19 |
ONE :: "one" |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
20 |
"ONE == Def ()" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
21 |
|
16747 | 22 |
text {* Exhaustion and Elimination for type @{typ one} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
23 |
|
16747 | 24 |
lemma Exh_one: "t = \<bottom> \<or> t = ONE" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
25 |
apply (unfold ONE_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
26 |
apply (induct t) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
27 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
28 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
29 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
30 |
|
16747 | 31 |
lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
32 |
apply (rule Exh_one [THEN disjE]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
33 |
apply fast |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
34 |
apply fast |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
35 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
36 |
|
16747 | 37 |
lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
38 |
apply (unfold ONE_def) |
16747 | 39 |
apply simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
40 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
41 |
|
16747 | 42 |
lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
43 |
apply (unfold ONE_def) |
16747 | 44 |
apply simp_all |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
45 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
46 |
|
17838 | 47 |
lemma compact_ONE [simp]: "compact ONE" |
48 |
by (rule compact_chfin) |
|
49 |
||
18080 | 50 |
text {* Case analysis function for type @{typ one} *} |
51 |
||
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
52 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
53 |
one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
54 |
"one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))" |
18080 | 55 |
|
56 |
translations |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
57 |
"case x of CONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x" |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18111
diff
changeset
|
58 |
"\<Lambda> (CONST ONE). t" == "CONST one_when\<cdot>t" |
18080 | 59 |
|
18111 | 60 |
lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>" |
18080 | 61 |
by (simp add: one_when_def) |
62 |
||
18111 | 63 |
lemma one_when2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t" |
18080 | 64 |
by (simp add: one_when_def) |
65 |
||
18111 | 66 |
lemma one_when3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x" |
18080 | 67 |
by (rule_tac p=x in oneE, simp_all) |
68 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
69 |
end |