5 *) |
5 *) |
6 |
6 |
7 open RelPow; |
7 open RelPow; |
8 |
8 |
9 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def; |
9 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def; |
10 Addsimps [rel_pow_0, rel_pow_Suc]; |
10 Addsimps [rel_pow_0]; |
11 |
11 |
12 goal RelPow.thy "(x,x) : R^0"; |
12 goal RelPow.thy "(x,x) : R^0"; |
13 by(Simp_tac 1); |
13 by(Simp_tac 1); |
14 qed "rel_pow_0_I"; |
14 qed "rel_pow_0_I"; |
15 |
15 |
16 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"; |
16 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"; |
17 by(Simp_tac 1); |
17 by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
18 by(fast_tac comp_cs 1); |
18 by(fast_tac comp_cs 1); |
19 qed "rel_pow_Suc_I"; |
19 qed "rel_pow_Suc_I"; |
20 |
20 |
21 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; |
21 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; |
22 by(nat_ind_tac "n" 1); |
22 by(nat_ind_tac "n" 1); |
23 by(Simp_tac 1); |
23 by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
24 by(fast_tac comp_cs 1); |
24 by(fast_tac comp_cs 1); |
25 by(Asm_full_simp_tac 1); |
25 by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
26 by(fast_tac comp_cs 1); |
26 by(fast_tac comp_cs 1); |
27 qed_spec_mp "rel_pow_Suc_I2"; |
27 qed_spec_mp "rel_pow_Suc_I2"; |
28 |
28 |
|
29 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P"; |
|
30 by(Asm_full_simp_tac 1); |
|
31 qed "rel_pow_0_E"; |
|
32 |
|
33 val [major,minor] = goal RelPow.thy |
|
34 "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"; |
|
35 by(cut_facts_tac [major] 1); |
|
36 by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
|
37 by(fast_tac (comp_cs addIs [minor]) 1); |
|
38 qed "rel_pow_Suc_E"; |
|
39 |
|
40 val [p1,p2,p3] = goal RelPow.thy |
|
41 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ |
|
42 \ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P \ |
|
43 \ |] ==> P"; |
|
44 by(res_inst_tac [("n","n")] natE 1); |
|
45 by(cut_facts_tac [p1] 1); |
|
46 by(asm_full_simp_tac (!simpset addsimps [p2]) 1); |
|
47 by(cut_facts_tac [p1] 1); |
|
48 by(Asm_full_simp_tac 1); |
|
49 be rel_pow_Suc_E 1; |
|
50 by(REPEAT(ares_tac [p3] 1)); |
|
51 qed "rel_pow_E"; |
|
52 |
29 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)"; |
53 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); |
54 by(nat_ind_tac "n" 1); |
31 by(Simp_tac 1); |
55 by(fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1); |
32 by(fast_tac comp_cs 1); |
56 by(fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1); |
33 by(Asm_full_simp_tac 1); |
57 qed_spec_mp "rel_pow_Suc_D2"; |
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 |
58 |
46 val [p1,p2,p3] = goal RelPow.thy |
59 val [p1,p2,p3] = goal RelPow.thy |
47 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ |
60 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ |
48 \ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \ |
61 \ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \ |
49 \ |] ==> P"; |
62 \ |] ==> P"; |
50 br (p1 RS lemma) 1; |
63 by(res_inst_tac [("n","n")] natE 1); |
51 by(REPEAT(ares_tac [impI,p2] 1)); |
64 by(cut_facts_tac [p1] 1); |
52 by(REPEAT(ares_tac [allI,impI,p3] 1)); |
65 by(asm_full_simp_tac (!simpset addsimps [p2]) 1); |
53 qed "UN_rel_powE2"; |
66 by(cut_facts_tac [p1] 1); |
|
67 by(Asm_full_simp_tac 1); |
|
68 bd rel_pow_Suc_D2 1; |
|
69 be exE 1; |
|
70 be p3 1; |
|
71 be conjunct1 1; |
|
72 be conjunct2 1; |
|
73 qed "rel_pow_E2"; |
54 |
74 |
55 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)"; |
75 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)"; |
56 by(split_all_tac 1); |
76 by(split_all_tac 1); |
57 be rtrancl_induct 1; |
77 be rtrancl_induct 1; |
58 by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I]))); |
78 by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I]))); |
59 qed "rtrancl_imp_UN_rel_pow"; |
79 qed "rtrancl_imp_UN_rel_pow"; |
60 |
80 |
61 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*"; |
81 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*"; |
62 by(nat_ind_tac "n" 1); |
82 by(nat_ind_tac "n" 1); |
63 by(Simp_tac 1); |
83 by(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1); |
64 by(fast_tac (HOL_cs addIs [rtrancl_refl]) 1); |
84 by(fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 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; |
85 val lemma = result() RS spec RS mp; |
68 |
86 |
69 goal RelPow.thy "!!p. p:R^n ==> p:R^*"; |
87 goal RelPow.thy "!!p. p:R^n ==> p:R^*"; |
70 by(split_all_tac 1); |
88 by(split_all_tac 1); |
71 be lemma 1; |
89 be lemma 1; |
72 qed "UN_rel_pow_imp_rtrancl"; |
90 qed "rel_pow_imp_rtrancl"; |
73 |
91 |
74 goal RelPow.thy "R^* = (UN n. R^n)"; |
92 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); |
93 by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1); |
76 qed "rtrancl_is_UN_rel_pow"; |
94 qed "rtrancl_is_UN_rel_pow"; |