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;

1515

10 
Addsimps [rel_pow_0];

1496

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

1515

17 
by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);

1496

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

1515

23 
by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);

1496

24 
by(fast_tac comp_cs 1);

1515

25 
by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);

1496

26 
by(fast_tac comp_cs 1);


27 
qed_spec_mp "rel_pow_Suc_I2";


28 

1515

29 
goal RelPow.thy "!!R. [ (x,y) : R^0; x=y ==> P ] ==> P";


30 
by(Asm_full_simp_tac 1);


31 
qed "rel_pow_0_E";


32 


33 
val [major,minor] = goal RelPow.thy


34 
"[ (x,z) : R^(Suc n); !!y. [ (x,y) : R^n; (y,z) : R ] ==> P ] ==> P";


35 
by(cut_facts_tac [major] 1);


36 
by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);


37 
by(fast_tac (comp_cs addIs [minor]) 1);


38 
qed "rel_pow_Suc_E";


39 


40 
val [p1,p2,p3] = goal RelPow.thy


41 
"[ (x,z) : R^n; [ n=0; x = z ] ==> P; \


42 
\ !!y m. [ n = Suc m; (x,y) : R^m; (y,z) : R ] ==> P \


43 
\ ] ==> P";


44 
by(res_inst_tac [("n","n")] natE 1);


45 
by(cut_facts_tac [p1] 1);


46 
by(asm_full_simp_tac (!simpset addsimps [p2]) 1);


47 
by(cut_facts_tac [p1] 1);


48 
by(Asm_full_simp_tac 1);


49 
be rel_pow_Suc_E 1;


50 
by(REPEAT(ares_tac [p3] 1));


51 
qed "rel_pow_E";


52 

1496

53 
goal RelPow.thy "!x z. (x,z):R^(Suc n) > (? y. (x,y):R & (y,z):R^n)";


54 
by(nat_ind_tac "n" 1);

1515

55 
by(fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);


56 
by(fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);


57 
qed_spec_mp "rel_pow_Suc_D2";

1496

58 


59 
val [p1,p2,p3] = goal RelPow.thy


60 
"[ (x,z) : R^n; [ n=0; x = z ] ==> P; \


61 
\ !!y m. [ n = Suc m; (x,y) : R; (y,z) : R^m ] ==> P \


62 
\ ] ==> P";

1515

63 
by(res_inst_tac [("n","n")] natE 1);


64 
by(cut_facts_tac [p1] 1);


65 
by(asm_full_simp_tac (!simpset addsimps [p2]) 1);


66 
by(cut_facts_tac [p1] 1);


67 
by(Asm_full_simp_tac 1);


68 
bd rel_pow_Suc_D2 1;


69 
be exE 1;


70 
be p3 1;


71 
be conjunct1 1;


72 
be conjunct2 1;


73 
qed "rel_pow_E2";

1496

74 


75 
goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";


76 
by(split_all_tac 1);


77 
be rtrancl_induct 1;


78 
by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));


79 
qed "rtrancl_imp_UN_rel_pow";


80 


81 
goal RelPow.thy "!y. (x,y):R^n > (x,y):R^*";


82 
by(nat_ind_tac "n" 1);

1515

83 
by(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);


84 
by(fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);

1496

85 
val lemma = result() RS spec RS mp;


86 


87 
goal RelPow.thy "!!p. p:R^n ==> p:R^*";


88 
by(split_all_tac 1);


89 
be lemma 1;

1515

90 
qed "rel_pow_imp_rtrancl";

1496

91 


92 
goal RelPow.thy "R^* = (UN n. R^n)";

1515

93 
by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);

1496

94 
qed "rtrancl_is_UN_rel_pow";
