author | clasohm |
Tue, 30 Jan 1996 13:42:57 +0100 | |
changeset 1461 | 6bcb44e4d6e5 |
parent 1168 | 74be52691d62 |
child 2033 | 639de962ded4 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/void.ML |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
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 |
Lemmas for void.thy. |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
These lemmas are prototype lemmas for class porder |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
see class theory porder.thy |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
open Void; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
(* A non-emptyness result for Void *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
|
892 | 18 |
qed_goalw "VoidI" Void.thy [UU_void_Rep_def,Void_def] |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
" UU_void_Rep : Void" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
20 |
(fn prems => |
1461 | 21 |
[ |
22 |
(rtac (mem_Collect_eq RS ssubst) 1), |
|
23 |
(rtac refl 1) |
|
24 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
26 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
27 |
(* less_void is a partial ordering on void *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
30 |
qed_goalw "refl_less_void" Void.thy [ less_void_def ] "less_void x x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
31 |
(fn prems => |
1461 | 32 |
[ |
33 |
(fast_tac HOL_cs 1) |
|
34 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
|
892 | 36 |
qed_goalw "antisym_less_void" Void.thy [ less_void_def ] |
1461 | 37 |
"[|less_void x y; less_void y x|] ==> x = y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
(fn prems => |
1461 | 39 |
[ |
40 |
(cut_facts_tac prems 1), |
|
41 |
(rtac (Rep_Void_inverse RS subst) 1), |
|
42 |
(etac subst 1), |
|
43 |
(rtac (Rep_Void_inverse RS sym) 1) |
|
44 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
45 |
|
892 | 46 |
qed_goalw "trans_less_void" Void.thy [ less_void_def ] |
1461 | 47 |
"[|less_void x y; less_void y z|] ==> less_void x z" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
48 |
(fn prems => |
1461 | 49 |
[ |
50 |
(cut_facts_tac prems 1), |
|
51 |
(fast_tac HOL_cs 1) |
|
52 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
54 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
(* a technical lemma about void: *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
(* every element in void is represented by UU_void_Rep *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
57 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
|
892 | 59 |
qed_goal "unique_void" Void.thy "Rep_Void(x) = UU_void_Rep" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
60 |
(fn prems => |
1461 | 61 |
[ |
62 |
(rtac (mem_Collect_eq RS subst) 1), |
|
63 |
(fold_goals_tac [Void_def]), |
|
64 |
(rtac Rep_Void 1) |
|
65 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
66 |
|
1461 | 67 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
68 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
69 |