1496
|
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";
|