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