|
1 (* Title: HOL/RelPow.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1996 TU Muenchen |
|
5 *) |
|
6 |
|
7 open RelPow; |
|
8 |
|
9 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def; |
|
10 Addsimps [rel_pow_0, rel_pow_Suc]; |
|
11 |
|
12 goal RelPow.thy "(x,x) : R^0"; |
|
13 by(Simp_tac 1); |
|
14 qed "rel_pow_0_I"; |
|
15 |
|
16 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"; |
|
17 by(Simp_tac 1); |
|
18 by(fast_tac comp_cs 1); |
|
19 qed "rel_pow_Suc_I"; |
|
20 |
|
21 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; |
|
22 by(nat_ind_tac "n" 1); |
|
23 by(Simp_tac 1); |
|
24 by(fast_tac comp_cs 1); |
|
25 by(Asm_full_simp_tac 1); |
|
26 by(fast_tac comp_cs 1); |
|
27 qed_spec_mp "rel_pow_Suc_I2"; |
|
28 |
|
29 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)"; |
|
30 by(nat_ind_tac "n" 1); |
|
31 by(Simp_tac 1); |
|
32 by(fast_tac comp_cs 1); |
|
33 by(Asm_full_simp_tac 1); |
|
34 by(fast_tac comp_cs 1); |
|
35 val lemma = result() RS spec RS spec RS mp; |
|
36 |
|
37 goal RelPow.thy |
|
38 "(x,z) : R^n --> (n=0 --> x=z --> P) --> \ |
|
39 \ (!y m. n = Suc m --> (x,y):R --> (y,z):R^m --> P) --> P"; |
|
40 by(res_inst_tac [("n","n")] natE 1); |
|
41 by(Asm_simp_tac 1); |
|
42 by(hyp_subst_tac 1); |
|
43 by(fast_tac (HOL_cs addDs [lemma]) 1); |
|
44 val lemma = result() RS mp RS mp RS mp; |
|
45 |
|
46 val [p1,p2,p3] = goal RelPow.thy |
|
47 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ |
|
48 \ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \ |
|
49 \ |] ==> P"; |
|
50 br (p1 RS lemma) 1; |
|
51 by(REPEAT(ares_tac [impI,p2] 1)); |
|
52 by(REPEAT(ares_tac [allI,impI,p3] 1)); |
|
53 qed "UN_rel_powE2"; |
|
54 |
|
55 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)"; |
|
56 by(split_all_tac 1); |
|
57 be rtrancl_induct 1; |
|
58 by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I]))); |
|
59 qed "rtrancl_imp_UN_rel_pow"; |
|
60 |
|
61 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*"; |
|
62 by(nat_ind_tac "n" 1); |
|
63 by(Simp_tac 1); |
|
64 by(fast_tac (HOL_cs addIs [rtrancl_refl]) 1); |
|
65 by(Simp_tac 1); |
|
66 by(fast_tac (trancl_cs addEs [rtrancl_into_rtrancl]) 1); |
|
67 val lemma = result() RS spec RS mp; |
|
68 |
|
69 goal RelPow.thy "!!p. p:R^n ==> p:R^*"; |
|
70 by(split_all_tac 1); |
|
71 be lemma 1; |
|
72 qed "UN_rel_pow_imp_rtrancl"; |
|
73 |
|
74 goal RelPow.thy "R^* = (UN n. R^n)"; |
|
75 by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,UN_rel_pow_imp_rtrancl]) 1); |
|
76 qed "rtrancl_is_UN_rel_pow"; |