1 (* Title: HOLCF/tr1.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for tr1.thy |
|
7 *) |
|
8 |
|
9 open Tr1; |
|
10 |
|
11 (* -------------------------------------------------------------------------- *) |
|
12 (* distinctness for type tr *) |
|
13 (* -------------------------------------------------------------------------- *) |
|
14 |
|
15 val dist_less_tr = [ |
|
16 prove_goalw Tr1.thy [TT_def] "~TT << UU" |
|
17 (fn prems => |
|
18 [ |
|
19 (rtac classical2 1), |
|
20 (rtac defined_sinl 1), |
|
21 (rtac not_less2not_eq 1), |
|
22 (rtac dist_less_one 1), |
|
23 (rtac (rep_tr_iso RS subst) 1), |
|
24 (rtac (rep_tr_iso RS subst) 1), |
|
25 (rtac cfun_arg_cong 1), |
|
26 (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1), |
|
27 (etac (eq_UU_iff RS ssubst) 1) |
|
28 ]), |
|
29 prove_goalw Tr1.thy [FF_def] "~FF << UU" |
|
30 (fn prems => |
|
31 [ |
|
32 (rtac classical2 1), |
|
33 (rtac defined_sinr 1), |
|
34 (rtac not_less2not_eq 1), |
|
35 (rtac dist_less_one 1), |
|
36 (rtac (rep_tr_iso RS subst) 1), |
|
37 (rtac (rep_tr_iso RS subst) 1), |
|
38 (rtac cfun_arg_cong 1), |
|
39 (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1), |
|
40 (etac (eq_UU_iff RS ssubst) 1) |
|
41 ]), |
|
42 prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF" |
|
43 (fn prems => |
|
44 [ |
|
45 (rtac classical2 1), |
|
46 (rtac (less_ssum4c RS iffD1) 2), |
|
47 (rtac not_less2not_eq 1), |
|
48 (rtac dist_less_one 1), |
|
49 (rtac (rep_tr_iso RS subst) 1), |
|
50 (rtac (rep_tr_iso RS subst) 1), |
|
51 (etac monofun_cfun_arg 1) |
|
52 ]), |
|
53 prove_goalw Tr1.thy [FF_def,TT_def] "~FF << TT" |
|
54 (fn prems => |
|
55 [ |
|
56 (rtac classical2 1), |
|
57 (rtac (less_ssum4d RS iffD1) 2), |
|
58 (rtac not_less2not_eq 1), |
|
59 (rtac dist_less_one 1), |
|
60 (rtac (rep_tr_iso RS subst) 1), |
|
61 (rtac (rep_tr_iso RS subst) 1), |
|
62 (etac monofun_cfun_arg 1) |
|
63 ]) |
|
64 ]; |
|
65 |
|
66 fun prover s = prove_goal Tr1.thy s |
|
67 (fn prems => |
|
68 [ |
|
69 (rtac not_less2not_eq 1), |
|
70 (resolve_tac dist_less_tr 1) |
|
71 ]); |
|
72 |
|
73 val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"]; |
|
74 val dist_eq_tr = dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr); |
|
75 |
|
76 (* ------------------------------------------------------------------------ *) |
|
77 (* Exhaustion and elimination for type tr *) |
|
78 (* ------------------------------------------------------------------------ *) |
|
79 |
|
80 qed_goalw "Exh_tr" Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF" |
|
81 (fn prems => |
|
82 [ |
|
83 (res_inst_tac [("p","rep_tr`t")] ssumE 1), |
|
84 (rtac disjI1 1), |
|
85 (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) |
|
86 RS conjunct2 RS subst) 1), |
|
87 (rtac (abs_tr_iso RS subst) 1), |
|
88 (etac cfun_arg_cong 1), |
|
89 (rtac disjI2 1), |
|
90 (rtac disjI1 1), |
|
91 (rtac (abs_tr_iso RS subst) 1), |
|
92 (rtac cfun_arg_cong 1), |
|
93 (etac trans 1), |
|
94 (rtac cfun_arg_cong 1), |
|
95 (rtac (Exh_one RS disjE) 1), |
|
96 (contr_tac 1), |
|
97 (atac 1), |
|
98 (rtac disjI2 1), |
|
99 (rtac disjI2 1), |
|
100 (rtac (abs_tr_iso RS subst) 1), |
|
101 (rtac cfun_arg_cong 1), |
|
102 (etac trans 1), |
|
103 (rtac cfun_arg_cong 1), |
|
104 (rtac (Exh_one RS disjE) 1), |
|
105 (contr_tac 1), |
|
106 (atac 1) |
|
107 ]); |
|
108 |
|
109 |
|
110 qed_goal "trE" Tr1.thy |
|
111 "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q" |
|
112 (fn prems => |
|
113 [ |
|
114 (rtac (Exh_tr RS disjE) 1), |
|
115 (eresolve_tac prems 1), |
|
116 (etac disjE 1), |
|
117 (eresolve_tac prems 1), |
|
118 (eresolve_tac prems 1) |
|
119 ]); |
|
120 |
|
121 |
|
122 (* ------------------------------------------------------------------------ *) |
|
123 (* type tr is flat *) |
|
124 (* ------------------------------------------------------------------------ *) |
|
125 |
|
126 qed_goalw "flat_tr" Tr1.thy [flat_def] "flat TT" |
|
127 (fn prems => |
|
128 [ |
|
129 (rtac allI 1), |
|
130 (rtac allI 1), |
|
131 (res_inst_tac [("p","x")] trE 1), |
|
132 (Asm_simp_tac 1), |
|
133 (res_inst_tac [("p","y")] trE 1), |
|
134 (asm_simp_tac (!simpset addsimps dist_less_tr) 1), |
|
135 (asm_simp_tac (!simpset addsimps dist_less_tr) 1), |
|
136 (asm_simp_tac (!simpset addsimps dist_less_tr) 1), |
|
137 (res_inst_tac [("p","y")] trE 1), |
|
138 (asm_simp_tac (!simpset addsimps dist_less_tr) 1), |
|
139 (asm_simp_tac (!simpset addsimps dist_less_tr) 1), |
|
140 (asm_simp_tac (!simpset addsimps dist_less_tr) 1) |
|
141 ]); |
|
142 |
|
143 |
|
144 (* ------------------------------------------------------------------------ *) |
|
145 (* properties of tr_when *) |
|
146 (* ------------------------------------------------------------------------ *) |
|
147 |
|
148 fun prover s = prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s (fn prems => [ |
|
149 (Simp_tac 1), |
|
150 (simp_tac (!simpset addsimps [rep_tr_iso, |
|
151 (abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) |
|
152 RS iso_strict) RS conjunct1]) 1)]); |
|
153 |
|
154 val tr_when = map prover [ |
|
155 "tr_when`x`y`UU = UU", |
|
156 "tr_when`x`y`TT = x", |
|
157 "tr_when`x`y`FF = y" |
|
158 ]; |
|
159 |
|