|
1 (* Title: HOL/Relation_Power.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1996 TU Muenchen |
|
5 *) |
|
6 |
|
7 Goal "!!R:: ('a*'a)set. R^1 = R"; |
|
8 by (Simp_tac 1); |
|
9 qed "rel_pow_1"; |
|
10 Addsimps [rel_pow_1]; |
|
11 |
|
12 Goal "(x,x) : R^0"; |
|
13 by (Simp_tac 1); |
|
14 qed "rel_pow_0_I"; |
|
15 |
|
16 Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"; |
|
17 by (Simp_tac 1); |
|
18 by (Blast_tac 1); |
|
19 qed "rel_pow_Suc_I"; |
|
20 |
|
21 Goal "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; |
|
22 by (induct_tac "n" 1); |
|
23 by (Simp_tac 1); |
|
24 by (Asm_full_simp_tac 1); |
|
25 by (Blast_tac 1); |
|
26 qed_spec_mp "rel_pow_Suc_I2"; |
|
27 |
|
28 Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P"; |
|
29 by (Asm_full_simp_tac 1); |
|
30 qed "rel_pow_0_E"; |
|
31 |
|
32 val [major,minor] = Goal |
|
33 "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"; |
|
34 by (cut_facts_tac [major] 1); |
|
35 by (Asm_full_simp_tac 1); |
|
36 by (blast_tac (claset() addIs [minor]) 1); |
|
37 qed "rel_pow_Suc_E"; |
|
38 |
|
39 val [p1,p2,p3] = Goal |
|
40 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ |
|
41 \ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P \ |
|
42 \ |] ==> P"; |
|
43 by (cut_facts_tac [p1] 1); |
|
44 by (case_tac "n" 1); |
|
45 by (asm_full_simp_tac (simpset() addsimps [p2]) 1); |
|
46 by (Asm_full_simp_tac 1); |
|
47 by (etac compEpair 1); |
|
48 by (REPEAT(ares_tac [p3] 1)); |
|
49 qed "rel_pow_E"; |
|
50 |
|
51 Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)"; |
|
52 by (induct_tac "n" 1); |
|
53 by (blast_tac (claset() addIs [rel_pow_0_I] |
|
54 addEs [rel_pow_0_E,rel_pow_Suc_E]) 1); |
|
55 by (blast_tac (claset() addIs [rel_pow_Suc_I] |
|
56 addEs [rel_pow_0_E,rel_pow_Suc_E]) 1); |
|
57 qed_spec_mp "rel_pow_Suc_D2"; |
|
58 |
|
59 |
|
60 Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)"; |
|
61 by (induct_tac "n" 1); |
|
62 by (ALLGOALS Asm_simp_tac); |
|
63 by (Blast_tac 1); |
|
64 qed_spec_mp "rel_pow_Suc_D2'"; |
|
65 |
|
66 val [p1,p2,p3] = Goal |
|
67 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ |
|
68 \ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \ |
|
69 \ |] ==> P"; |
|
70 by (cut_facts_tac [p1] 1); |
|
71 by (case_tac "n" 1); |
|
72 by (asm_full_simp_tac (simpset() addsimps [p2]) 1); |
|
73 by (Asm_full_simp_tac 1); |
|
74 by (etac compEpair 1); |
|
75 by (dtac (conjI RS rel_pow_Suc_D2') 1); |
|
76 by (assume_tac 1); |
|
77 by (etac exE 1); |
|
78 by (etac p3 1); |
|
79 by (etac conjunct1 1); |
|
80 by (etac conjunct2 1); |
|
81 qed "rel_pow_E2"; |
|
82 |
|
83 Goal "!!p. p:R^* ==> p : (UN n. R^n)"; |
|
84 by (split_all_tac 1); |
|
85 by (etac rtrancl_induct 1); |
|
86 by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I]))); |
|
87 qed "rtrancl_imp_UN_rel_pow"; |
|
88 |
|
89 Goal "!y. (x,y):R^n --> (x,y):R^*"; |
|
90 by (induct_tac "n" 1); |
|
91 by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1); |
|
92 by (blast_tac (claset() addEs [rel_pow_Suc_E] |
|
93 addIs [rtrancl_into_rtrancl]) 1); |
|
94 val lemma = result() RS spec RS mp; |
|
95 |
|
96 Goal "!!p. p:R^n ==> p:R^*"; |
|
97 by (split_all_tac 1); |
|
98 by (etac lemma 1); |
|
99 qed "rel_pow_imp_rtrancl"; |
|
100 |
|
101 Goal "R^* = (UN n. R^n)"; |
|
102 by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1); |
|
103 qed "rtrancl_is_UN_rel_pow"; |
|
104 |
|
105 |
|
106 Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)"; |
|
107 by (rtac univalentI 1); |
|
108 by (induct_tac "n" 1); |
|
109 by (Simp_tac 1); |
|
110 by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1); |
|
111 qed_spec_mp "univalent_rel_pow"; |
|
112 |
|
113 |
|
114 |
|
115 |