author | wenzelm |
Tue, 17 May 2005 09:58:40 +0200 | |
changeset 15967 | f9163c6f69d6 |
parent 15577 | e16da3068ad6 |
child 16070 | 4a83dd540b88 |
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 |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
|
15577 | 7 |
header {* The unit domain *} |
8 |
||
9 |
theory One |
|
10 |
imports Lift |
|
11 |
begin |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
13 |
types one = "unit lift" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
|
3717 | 15 |
constdefs |
16 |
ONE :: "one" |
|
17 |
"ONE == Def ()" |
|
2640 | 18 |
|
19 |
translations |
|
3717 | 20 |
"one" <= (type) "unit lift" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
21 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
22 |
(* Title: HOLCF/One.ML |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
23 |
ID: $Id$ |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
24 |
Author: Oscar Slotosch |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
25 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
26 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
27 |
The unit domain. |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
28 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
29 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
30 |
(* ------------------------------------------------------------------------ *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
31 |
(* Exhaustion and Elimination for type one *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
32 |
(* ------------------------------------------------------------------------ *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
33 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
34 |
lemma Exh_one: "t=UU | t = ONE" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
35 |
apply (unfold ONE_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
36 |
apply (induct t) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
37 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
38 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
39 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
40 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
41 |
lemma oneE: "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
42 |
apply (rule Exh_one [THEN disjE]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
43 |
apply fast |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
44 |
apply fast |
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 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
47 |
lemma dist_less_one [simp]: "~ONE << UU" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
48 |
apply (unfold ONE_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
49 |
apply (simp add: inst_lift_po) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
50 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
51 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
52 |
lemma dist_eq_one [simp]: "ONE~=UU" "UU~=ONE" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
53 |
apply (unfold ONE_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
54 |
apply (simp_all add: inst_lift_po) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
55 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
56 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
57 |
end |