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