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