9 open Trancl; |
9 open Trancl; |
10 |
10 |
11 goal Trancl.thy "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"; |
11 goal Trancl.thy "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"; |
12 by (rtac bnd_monoI 1); |
12 by (rtac bnd_monoI 1); |
13 by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2)); |
13 by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2)); |
14 by (fast_tac comp_cs 1); |
14 by (Fast_tac 1); |
15 qed "rtrancl_bnd_mono"; |
15 qed "rtrancl_bnd_mono"; |
16 |
16 |
17 val [prem] = goalw Trancl.thy [rtrancl_def] "r<=s ==> r^* <= s^*"; |
17 val [prem] = goalw Trancl.thy [rtrancl_def] "r<=s ==> r^* <= s^*"; |
18 by (rtac lfp_mono 1); |
18 by (rtac lfp_mono 1); |
19 by (REPEAT (resolve_tac [rtrancl_bnd_mono, prem, subset_refl, id_mono, |
19 by (REPEAT (resolve_tac [rtrancl_bnd_mono, prem, subset_refl, id_mono, |
49 qed "r_into_rtrancl"; |
49 qed "r_into_rtrancl"; |
50 |
50 |
51 (*The premise ensures that r consists entirely of pairs*) |
51 (*The premise ensures that r consists entirely of pairs*) |
52 val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^*"; |
52 val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^*"; |
53 by (cut_facts_tac prems 1); |
53 by (cut_facts_tac prems 1); |
54 by (fast_tac (ZF_cs addIs [r_into_rtrancl]) 1); |
54 by (fast_tac (!claset addIs [r_into_rtrancl]) 1); |
55 qed "r_subset_rtrancl"; |
55 qed "r_subset_rtrancl"; |
56 |
56 |
57 goal Trancl.thy "field(r^*) = field(r)"; |
57 goal Trancl.thy "field(r^*) = field(r)"; |
58 by (fast_tac (eq_cs addIs [r_into_rtrancl] |
58 by (fast_tac (eq_cs addIs [r_into_rtrancl] |
59 addSDs [rtrancl_type RS subsetD]) 1); |
59 addSDs [rtrancl_type RS subsetD]) 1); |
66 "[| <a,b> : r^*; \ |
66 "[| <a,b> : r^*; \ |
67 \ !!x. x: field(r) ==> P(<x,x>); \ |
67 \ !!x. x: field(r) ==> P(<x,x>); \ |
68 \ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \ |
68 \ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \ |
69 \ ==> P(<a,b>)"; |
69 \ ==> P(<a,b>)"; |
70 by (rtac ([rtrancl_def, rtrancl_bnd_mono, major] MRS def_induct) 1); |
70 by (rtac ([rtrancl_def, rtrancl_bnd_mono, major] MRS def_induct) 1); |
71 by (fast_tac (ZF_cs addIs prems addSEs [idE,compE]) 1); |
71 by (fast_tac (!claset addIs prems) 1); |
72 qed "rtrancl_full_induct"; |
72 qed "rtrancl_full_induct"; |
73 |
73 |
74 (*nice induction rule. |
74 (*nice induction rule. |
75 Tried adding the typing hypotheses y,z:field(r), but these |
75 Tried adding the typing hypotheses y,z:field(r), but these |
76 caused expensive case splits!*) |
76 caused expensive case splits!*) |
83 by (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)" 1); |
83 by (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)" 1); |
84 (*now solve first subgoal: this formula is sufficient*) |
84 (*now solve first subgoal: this formula is sufficient*) |
85 by (EVERY1 [etac (spec RS mp), rtac refl]); |
85 by (EVERY1 [etac (spec RS mp), rtac refl]); |
86 (*now do the induction*) |
86 (*now do the induction*) |
87 by (resolve_tac [major RS rtrancl_full_induct] 1); |
87 by (resolve_tac [major RS rtrancl_full_induct] 1); |
88 by (ALLGOALS (fast_tac (ZF_cs addIs prems))); |
88 by (ALLGOALS (fast_tac (!claset addIs prems))); |
89 qed "rtrancl_induct"; |
89 qed "rtrancl_induct"; |
90 |
90 |
91 (*transitivity of transitive closure!! -- by induction.*) |
91 (*transitivity of transitive closure!! -- by induction.*) |
92 goalw Trancl.thy [trans_def] "trans(r^*)"; |
92 goalw Trancl.thy [trans_def] "trans(r^*)"; |
93 by (REPEAT (resolve_tac [allI,impI] 1)); |
93 by (REPEAT (resolve_tac [allI,impI] 1)); |
101 \ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \ |
101 \ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \ |
102 \ ==> P"; |
102 \ ==> P"; |
103 by (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r)" 1); |
103 by (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r)" 1); |
104 (*see HOL/trancl*) |
104 (*see HOL/trancl*) |
105 by (rtac (major RS rtrancl_induct) 2); |
105 by (rtac (major RS rtrancl_induct) 2); |
106 by (ALLGOALS (fast_tac (ZF_cs addSEs prems))); |
106 by (ALLGOALS (fast_tac (!claset addSEs prems))); |
107 qed "rtranclE"; |
107 qed "rtranclE"; |
108 |
108 |
109 |
109 |
110 (**** The relation trancl ****) |
110 (**** The relation trancl ****) |
111 |
111 |
112 (*Transitivity of r^+ is proved by transitivity of r^* *) |
112 (*Transitivity of r^+ is proved by transitivity of r^* *) |
113 goalw Trancl.thy [trans_def,trancl_def] "trans(r^+)"; |
113 goalw Trancl.thy [trans_def,trancl_def] "trans(r^+)"; |
114 by (safe_tac comp_cs); |
114 by (safe_tac (!claset)); |
115 by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1); |
115 by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1); |
116 by (REPEAT (assume_tac 1)); |
116 by (REPEAT (assume_tac 1)); |
117 qed "trans_trancl"; |
117 qed "trans_trancl"; |
118 |
118 |
119 (** Conversions between trancl and rtrancl **) |
119 (** Conversions between trancl and rtrancl **) |
129 qed "r_into_trancl"; |
129 qed "r_into_trancl"; |
130 |
130 |
131 (*The premise ensures that r consists entirely of pairs*) |
131 (*The premise ensures that r consists entirely of pairs*) |
132 val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^+"; |
132 val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^+"; |
133 by (cut_facts_tac prems 1); |
133 by (cut_facts_tac prems 1); |
134 by (fast_tac (ZF_cs addIs [r_into_trancl]) 1); |
134 by (fast_tac (!claset addIs [r_into_trancl]) 1); |
135 qed "r_subset_trancl"; |
135 qed "r_subset_trancl"; |
136 |
136 |
137 (*intro rule by definition: from r^* and r *) |
137 (*intro rule by definition: from r^* and r *) |
138 val prems = goalw Trancl.thy [trancl_def] |
138 val prems = goalw Trancl.thy [trancl_def] |
139 "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+"; |
139 "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+"; |
157 \ |] ==> P(b)"; |
157 \ |] ==> P(b)"; |
158 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); |
158 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); |
159 (*by induction on this formula*) |
159 (*by induction on this formula*) |
160 by (subgoal_tac "ALL z. <y,z> : r --> P(z)" 1); |
160 by (subgoal_tac "ALL z. <y,z> : r --> P(z)" 1); |
161 (*now solve first subgoal: this formula is sufficient*) |
161 (*now solve first subgoal: this formula is sufficient*) |
162 by (fast_tac ZF_cs 1); |
162 by (Fast_tac 1); |
163 by (etac rtrancl_induct 1); |
163 by (etac rtrancl_induct 1); |
164 by (ALLGOALS (fast_tac (ZF_cs addIs (rtrancl_into_trancl1::prems)))); |
164 by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems)))); |
165 qed "trancl_induct"; |
165 qed "trancl_induct"; |
166 |
166 |
167 (*elimination of r^+ -- NOT an induction rule*) |
167 (*elimination of r^+ -- NOT an induction rule*) |
168 val major::prems = goal Trancl.thy |
168 val major::prems = goal Trancl.thy |
169 "[| <a,b> : r^+; \ |
169 "[| <a,b> : r^+; \ |
170 \ <a,b> : r ==> P; \ |
170 \ <a,b> : r ==> P; \ |
171 \ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \ |
171 \ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \ |
172 \ |] ==> P"; |
172 \ |] ==> P"; |
173 by (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r)" 1); |
173 by (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r)" 1); |
174 by (fast_tac (ZF_cs addIs prems) 1); |
174 by (fast_tac (!claset addIs prems) 1); |
175 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); |
175 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); |
176 by (etac rtranclE 1); |
176 by (etac rtranclE 1); |
177 by (ALLGOALS (fast_tac (ZF_cs addIs [rtrancl_into_trancl1]))); |
177 by (ALLGOALS (fast_tac (!claset addIs [rtrancl_into_trancl1]))); |
178 qed "tranclE"; |
178 qed "tranclE"; |
179 |
179 |
180 goalw Trancl.thy [trancl_def] "r^+ <= field(r)*field(r)"; |
180 goalw Trancl.thy [trancl_def] "r^+ <= field(r)*field(r)"; |
181 by (fast_tac (ZF_cs addEs [compE, rtrancl_type RS subsetD RS SigmaE2]) 1); |
181 by (fast_tac (!claset addEs [rtrancl_type RS subsetD RS SigmaE2]) 1); |
182 qed "trancl_type"; |
182 qed "trancl_type"; |
183 |
183 |
184 val [prem] = goalw Trancl.thy [trancl_def] "r<=s ==> r^+ <= s^+"; |
184 val [prem] = goalw Trancl.thy [trancl_def] "r<=s ==> r^+ <= s^+"; |
185 by (REPEAT (resolve_tac [prem, comp_mono, rtrancl_mono] 1)); |
185 by (REPEAT (resolve_tac [prem, comp_mono, rtrancl_mono] 1)); |
186 qed "trancl_mono"; |
186 qed "trancl_mono"; |