equal
deleted
inserted
replaced
1 (* Title: ZF/trancl.ML |
1 (* Title: ZF/trancl.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 For trancl.thy. Transitive closure of a relation |
6 Transitive closure of a relation |
7 *) |
7 *) |
8 |
8 |
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 1); |
14 by (Blast_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 (!claset addIs [r_into_rtrancl]) 1); |
54 by (blast_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 (!claset addIs [r_into_rtrancl] |
58 by (blast_tac (!claset addIs [r_into_rtrancl] |
59 addSDs [rtrancl_type RS subsetD]) 1); |
59 addSDs [rtrancl_type RS subsetD]) 1); |
60 qed "rtrancl_field"; |
60 qed "rtrancl_field"; |
61 |
61 |
62 |
62 |
63 (** standard induction rule **) |
63 (** standard induction rule **) |
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 (!claset addIs [r_into_trancl]) 1); |
134 by (blast_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 1); |
162 by (Blast_tac 1); |
163 by (etac rtrancl_induct 1); |
163 by (etac rtrancl_induct 1); |
164 by (ALLGOALS (fast_tac (!claset 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*) |
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 (!claset 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 (!claset addIs [rtrancl_into_trancl1]))); |
177 by (ALLGOALS (blast_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 (!claset addEs [rtrancl_type RS subsetD RS SigmaE2]) 1); |
181 by (blast_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"; |