|
1 (* Title: HOLCF/one.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for one.thy |
|
7 *) |
|
8 |
|
9 open One; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* Exhaustion and Elimination for type one *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val Exh_one = prove_goalw One.thy [one_def] "z=UU | z = one" |
|
16 (fn prems => |
|
17 [ |
|
18 (res_inst_tac [("p","rep_one[z]")] liftE1 1), |
|
19 (rtac disjI1 1), |
|
20 (rtac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict ) |
|
21 RS conjunct2 RS subst) 1), |
|
22 (rtac (abs_one_iso RS subst) 1), |
|
23 (etac cfun_arg_cong 1), |
|
24 (rtac disjI2 1), |
|
25 (rtac (abs_one_iso RS subst) 1), |
|
26 (rtac cfun_arg_cong 1), |
|
27 (rtac (unique_void2 RS subst) 1), |
|
28 (atac 1) |
|
29 ]); |
|
30 |
|
31 val oneE = prove_goal One.thy |
|
32 "[| p=UU ==> Q; p = one ==>Q|] ==>Q" |
|
33 (fn prems => |
|
34 [ |
|
35 (rtac (Exh_one RS disjE) 1), |
|
36 (eresolve_tac prems 1), |
|
37 (eresolve_tac prems 1) |
|
38 ]); |
|
39 |
|
40 (* ------------------------------------------------------------------------ *) |
|
41 (* distinctness for type one : stored in a list *) |
|
42 (* ------------------------------------------------------------------------ *) |
|
43 |
|
44 val dist_less_one = [ |
|
45 prove_goalw One.thy [one_def] "~one << UU" |
|
46 (fn prems => |
|
47 [ |
|
48 (rtac classical3 1), |
|
49 (rtac less_lift4b 1), |
|
50 (rtac (rep_one_iso RS subst) 1), |
|
51 (rtac (rep_one_iso RS subst) 1), |
|
52 (rtac monofun_cfun_arg 1), |
|
53 (etac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict ) |
|
54 RS conjunct2 RS ssubst) 1) |
|
55 ]) |
|
56 ]; |
|
57 |
|
58 val dist_eq_one = [prove_goal One.thy "~one=UU" |
|
59 (fn prems => |
|
60 [ |
|
61 (rtac not_less2not_eq 1), |
|
62 (resolve_tac dist_less_one 1) |
|
63 ])]; |
|
64 |
|
65 val dist_eq_one = dist_eq_one @ (map (fn thm => (thm RS not_sym)) dist_eq_one); |
|
66 |
|
67 (* ------------------------------------------------------------------------ *) |
|
68 (* one is flat *) |
|
69 (* ------------------------------------------------------------------------ *) |
|
70 |
|
71 val prems = goalw One.thy [flat_def] "flat(one)"; |
|
72 by (rtac allI 1); |
|
73 by (rtac allI 1); |
|
74 by (res_inst_tac [("p","x")] oneE 1); |
|
75 by (asm_simp_tac ccc1_ss 1); |
|
76 by (res_inst_tac [("p","y")] oneE 1); |
|
77 by (asm_simp_tac (ccc1_ss addsimps dist_less_one) 1); |
|
78 by (asm_simp_tac ccc1_ss 1); |
|
79 val flat_one = result(); |
|
80 |
|
81 |
|
82 (* ------------------------------------------------------------------------ *) |
|
83 (* properties of one_when *) |
|
84 (* here I tried a generic prove procedure *) |
|
85 (* ------------------------------------------------------------------------ *) |
|
86 |
|
87 fun prover s = prove_goalw One.thy [one_when_def,one_def] s |
|
88 (fn prems => |
|
89 [ |
|
90 (simp_tac (ccc1_ss addsimps [(rep_one_iso ), |
|
91 (abs_one_iso RS allI) RS ((rep_one_iso RS allI) |
|
92 RS iso_strict) RS conjunct1] )1) |
|
93 ]); |
|
94 |
|
95 val one_when = map prover ["one_when[x][UU] = UU","one_when[x][one] = x"]; |
|
96 |