src/HOL/RelPow.ML
author nipkow
Thu Feb 15 08:10:36 1996 +0100 (1996-02-15)
changeset 1496 c443b2adaf52
child 1515 4ed79ebab64d
permissions -rw-r--r--
Added a few thms and the new theory RelPow.
     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";