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 

1693

12 
goal RelPow.thy "R^1 = R";


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


14 
qed "rel_pow_1";


15 
Addsimps [rel_pow_1];


16 

1496

17 
goal RelPow.thy "(x,x) : R^0";

1552

18 
by (Simp_tac 1);

1496

19 
qed "rel_pow_0_I";


20 


21 
goal RelPow.thy "!!R. [ (x,y) : R^n; (y,z):R ] ==> (x,z):R^(Suc n)";

1552

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


23 
by (fast_tac comp_cs 1);

1496

24 
qed "rel_pow_Suc_I";


25 


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

1552

27 
by (nat_ind_tac "n" 1);


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


29 
by (fast_tac comp_cs 1);


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


31 
by (fast_tac comp_cs 1);

1496

32 
qed_spec_mp "rel_pow_Suc_I2";


33 

1515

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

1552

35 
by (Asm_full_simp_tac 1);

1515

36 
qed "rel_pow_0_E";


37 


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


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

1552

40 
by (cut_facts_tac [major] 1);


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


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

1515

43 
qed "rel_pow_Suc_E";


44 


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


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


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


48 
\ ] ==> P";

1552

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


50 
by (cut_facts_tac [p1] 1);


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


52 
by (cut_facts_tac [p1] 1);


53 
by (Asm_full_simp_tac 1);


54 
by (etac rel_pow_Suc_E 1);


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

1515

56 
qed "rel_pow_E";


57 

1496

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

1552

59 
by (nat_ind_tac "n" 1);


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


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

1515

62 
qed_spec_mp "rel_pow_Suc_D2";

1496

63 


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


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


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


67 
\ ] ==> P";

1552

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


69 
by (cut_facts_tac [p1] 1);


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


71 
by (cut_facts_tac [p1] 1);


72 
by (Asm_full_simp_tac 1);


73 
by (dtac rel_pow_Suc_D2 1);


74 
by (etac exE 1);


75 
by (etac p3 1);


76 
by (etac conjunct1 1);


77 
by (etac conjunct2 1);

1515

78 
qed "rel_pow_E2";

1496

79 


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

1552

81 
by (split_all_tac 1);


82 
by (etac rtrancl_induct 1);


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

1496

84 
qed "rtrancl_imp_UN_rel_pow";


85 


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

1552

87 
by (nat_ind_tac "n" 1);


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


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

1496

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


91 


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

1552

93 
by (split_all_tac 1);


94 
by (etac lemma 1);

1515

95 
qed "rel_pow_imp_rtrancl";

1496

96 


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

1552

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

1496

99 
qed "rtrancl_is_UN_rel_pow";
