13 |
13 |
14 (* ------------------------------------------------------------------------ *) |
14 (* ------------------------------------------------------------------------ *) |
15 (* A non-emptyness result for Void *) |
15 (* A non-emptyness result for Void *) |
16 (* ------------------------------------------------------------------------ *) |
16 (* ------------------------------------------------------------------------ *) |
17 |
17 |
18 val VoidI = prove_goalw Void.thy [UU_void_Rep_def,Void_def] |
18 qed_goalw "VoidI" Void.thy [UU_void_Rep_def,Void_def] |
19 " UU_void_Rep : Void" |
19 " UU_void_Rep : Void" |
20 (fn prems => |
20 (fn prems => |
21 [ |
21 [ |
22 (rtac (mem_Collect_eq RS ssubst) 1), |
22 (rtac (mem_Collect_eq RS ssubst) 1), |
23 (rtac refl 1) |
23 (rtac refl 1) |
25 |
25 |
26 (* ------------------------------------------------------------------------ *) |
26 (* ------------------------------------------------------------------------ *) |
27 (* less_void is a partial ordering on void *) |
27 (* less_void is a partial ordering on void *) |
28 (* ------------------------------------------------------------------------ *) |
28 (* ------------------------------------------------------------------------ *) |
29 |
29 |
30 val refl_less_void = prove_goalw Void.thy [ less_void_def ] "less_void(x,x)" |
30 qed_goalw "refl_less_void" Void.thy [ less_void_def ] "less_void(x,x)" |
31 (fn prems => |
31 (fn prems => |
32 [ |
32 [ |
33 (fast_tac HOL_cs 1) |
33 (fast_tac HOL_cs 1) |
34 ]); |
34 ]); |
35 |
35 |
36 val antisym_less_void = prove_goalw Void.thy [ less_void_def ] |
36 qed_goalw "antisym_less_void" Void.thy [ less_void_def ] |
37 "[|less_void(x,y); less_void(y,x)|] ==> x = y" |
37 "[|less_void(x,y); less_void(y,x)|] ==> x = y" |
38 (fn prems => |
38 (fn prems => |
39 [ |
39 [ |
40 (cut_facts_tac prems 1), |
40 (cut_facts_tac prems 1), |
41 (rtac (Rep_Void_inverse RS subst) 1), |
41 (rtac (Rep_Void_inverse RS subst) 1), |
42 (etac subst 1), |
42 (etac subst 1), |
43 (rtac (Rep_Void_inverse RS sym) 1) |
43 (rtac (Rep_Void_inverse RS sym) 1) |
44 ]); |
44 ]); |
45 |
45 |
46 val trans_less_void = prove_goalw Void.thy [ less_void_def ] |
46 qed_goalw "trans_less_void" Void.thy [ less_void_def ] |
47 "[|less_void(x,y); less_void(y,z)|] ==> less_void(x,z)" |
47 "[|less_void(x,y); less_void(y,z)|] ==> less_void(x,z)" |
48 (fn prems => |
48 (fn prems => |
49 [ |
49 [ |
50 (cut_facts_tac prems 1), |
50 (cut_facts_tac prems 1), |
51 (fast_tac HOL_cs 1) |
51 (fast_tac HOL_cs 1) |
54 (* ------------------------------------------------------------------------ *) |
54 (* ------------------------------------------------------------------------ *) |
55 (* a technical lemma about void: *) |
55 (* a technical lemma about void: *) |
56 (* every element in void is represented by UU_void_Rep *) |
56 (* every element in void is represented by UU_void_Rep *) |
57 (* ------------------------------------------------------------------------ *) |
57 (* ------------------------------------------------------------------------ *) |
58 |
58 |
59 val unique_void = prove_goal Void.thy "Rep_Void(x) = UU_void_Rep" |
59 qed_goal "unique_void" Void.thy "Rep_Void(x) = UU_void_Rep" |
60 (fn prems => |
60 (fn prems => |
61 [ |
61 [ |
62 (rtac (mem_Collect_eq RS subst) 1), |
62 (rtac (mem_Collect_eq RS subst) 1), |
63 (fold_goals_tac [Void_def]), |
63 (fold_goals_tac [Void_def]), |
64 (rtac Rep_Void 1) |
64 (rtac Rep_Void 1) |