author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8709  483a3eb96c7e 
permissions  rwrr 
1496  1 
(* Title: HOL/RelPow.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1996 TU Muenchen 

5 
*) 

6 

7 
open RelPow; 

8 

5069  9 
Goal "!!R:: ('a*'a)set. R^1 = R"; 
2741  10 
by (Simp_tac 1); 
1693  11 
qed "rel_pow_1"; 
12 
Addsimps [rel_pow_1]; 

13 

5069  14 
Goal "(x,x) : R^0"; 
1552  15 
by (Simp_tac 1); 
1496  16 
qed "rel_pow_0_I"; 
17 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

18 
Goal "[ (x,y) : R^n; (y,z):R ] ==> (x,z):R^(Suc n)"; 
2741  19 
by (Simp_tac 1); 
2922  20 
by (Blast_tac 1); 
1496  21 
qed "rel_pow_Suc_I"; 
22 

5069  23 
Goal "!z. (x,y) : R > (y,z):R^n > (x,z):R^(Suc n)"; 
8709  24 
by (induct_tac "n" 1); 
2741  25 
by (Simp_tac 1); 
26 
by (Asm_full_simp_tac 1); 

2922  27 
by (Blast_tac 1); 
1496  28 
qed_spec_mp "rel_pow_Suc_I2"; 
29 

5069  30 
Goal "!!R. [ (x,y) : R^0; x=y ==> P ] ==> P"; 
1552  31 
by (Asm_full_simp_tac 1); 
1515  32 
qed "rel_pow_0_E"; 
33 

5316  34 
val [major,minor] = Goal 
1515  35 
"[ (x,z) : R^(Suc n); !!y. [ (x,y) : R^n; (y,z) : R ] ==> P ] ==> P"; 
1552  36 
by (cut_facts_tac [major] 1); 
2741  37 
by (Asm_full_simp_tac 1); 
4089  38 
by (blast_tac (claset() addIs [minor]) 1); 
1515  39 
qed "rel_pow_Suc_E"; 
40 

5316  41 
val [p1,p2,p3] = Goal 
1515  42 
"[ (x,z) : R^n; [ n=0; x = z ] ==> P; \ 
43 
\ !!y m. [ n = Suc m; (x,y) : R^m; (y,z) : R ] ==> P \ 

44 
\ ] ==> P"; 

1552  45 
by (cut_facts_tac [p1] 1); 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

46 
by (case_tac "n" 1); 
4089  47 
by (asm_full_simp_tac (simpset() addsimps [p2]) 1); 
1552  48 
by (Asm_full_simp_tac 1); 
2741  49 
by (etac compEpair 1); 
1552  50 
by (REPEAT(ares_tac [p3] 1)); 
1515  51 
qed "rel_pow_E"; 
52 

5069  53 
Goal "!x z. (x,z):R^(Suc n) > (? y. (x,y):R & (y,z):R^n)"; 
8709  54 
by (induct_tac "n" 1); 
5316  55 
by (blast_tac (claset() addIs [rel_pow_0_I] 
56 
addEs [rel_pow_0_E,rel_pow_Suc_E]) 1); 

57 
by (blast_tac (claset() addIs [rel_pow_Suc_I] 

58 
addEs [rel_pow_0_E,rel_pow_Suc_E]) 1); 

1515  59 
qed_spec_mp "rel_pow_Suc_D2"; 
1496  60 

2741  61 

5278  62 
Goal "!x y z. (x,y) : R^n & (y,z) : R > (? w. (x,w) : R & (w,z) : R^n)"; 
8709  63 
by (induct_tac "n" 1); 
5316  64 
by (ALLGOALS Asm_simp_tac); 
65 
by (Blast_tac 1); 

2741  66 
qed_spec_mp "rel_pow_Suc_D2'"; 
67 

5316  68 
val [p1,p2,p3] = Goal 
1496  69 
"[ (x,z) : R^n; [ n=0; x = z ] ==> P; \ 
70 
\ !!y m. [ n = Suc m; (x,y) : R; (y,z) : R^m ] ==> P \ 

71 
\ ] ==> P"; 

1552  72 
by (cut_facts_tac [p1] 1); 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

73 
by (case_tac "n" 1); 
4089  74 
by (asm_full_simp_tac (simpset() addsimps [p2]) 1); 
1552  75 
by (Asm_full_simp_tac 1); 
3023  76 
by (etac compEpair 1); 
2741  77 
by (dtac (conjI RS rel_pow_Suc_D2') 1); 
3023  78 
by (assume_tac 1); 
1552  79 
by (etac exE 1); 
80 
by (etac p3 1); 

81 
by (etac conjunct1 1); 

82 
by (etac conjunct2 1); 

1515  83 
qed "rel_pow_E2"; 
1496  84 

5069  85 
Goal "!!p. p:R^* ==> p : (UN n. R^n)"; 
1552  86 
by (split_all_tac 1); 
87 
by (etac rtrancl_induct 1); 

4089  88 
by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I]))); 
1496  89 
qed "rtrancl_imp_UN_rel_pow"; 
90 

5069  91 
Goal "!y. (x,y):R^n > (x,y):R^*"; 
8709  92 
by (induct_tac "n" 1); 
4089  93 
by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1); 
94 
by (blast_tac (claset() addEs [rel_pow_Suc_E] 

3023  95 
addIs [rtrancl_into_rtrancl]) 1); 
1496  96 
val lemma = result() RS spec RS mp; 
97 

5069  98 
Goal "!!p. p:R^n ==> p:R^*"; 
1552  99 
by (split_all_tac 1); 
100 
by (etac lemma 1); 

1515  101 
qed "rel_pow_imp_rtrancl"; 
1496  102 

5069  103 
Goal "R^* = (UN n. R^n)"; 
4089  104 
by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1); 
1496  105 
qed "rtrancl_is_UN_rel_pow"; 
2741  106 

107 

8268  108 
Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)"; 
109 
by (rtac univalentI 1); 

4759  110 
by (induct_tac "n" 1); 
111 
by (Simp_tac 1); 

8268  112 
by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1); 
113 
qed_spec_mp "univalent_rel_pow"; 

2741  114 

4759  115 

116 

117 