src/HOL/RelPow.ML

--- a/src/HOL/RelPow.ML	Thu Mar 06 16:06:08 1997 +0100
+++ b/src/HOL/RelPow.ML	Thu Mar 06 16:06:31 1997 +0100
@@ -6,11 +6,8 @@
 
 open RelPow;
 
-val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
-Addsimps [rel_pow_0];
-
 goal RelPow.thy "R^1 = R";
-by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (Simp_tac 1);
 qed "rel_pow_1";
 Addsimps [rel_pow_1];
 
@@ -19,14 +16,14 @@
 qed "rel_pow_0_I";
 
 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
-by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (Simp_tac  1);
 by (Fast_tac 1);
 qed "rel_pow_Suc_I";
 
 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
 by (nat_ind_tac "n" 1);
-by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (Simp_tac  1);
+by (Asm_full_simp_tac 1);
 by (Fast_tac 1);
 qed_spec_mp "rel_pow_Suc_I2";
 
@@ -37,7 +34,7 @@
 val [major,minor] = goal RelPow.thy
   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
 by (cut_facts_tac [major] 1);
-by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (Asm_full_simp_tac  1);
 by (fast_tac (!claset addIs [minor]) 1);
 qed "rel_pow_Suc_E";
 
@@ -50,7 +47,7 @@
 by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
 by (cut_facts_tac [p1] 1);
 by (Asm_full_simp_tac 1);
-by (etac rel_pow_Suc_E 1);
+by (etac compEpair 1);
 by (REPEAT(ares_tac [p3] 1));
 qed "rel_pow_E";
 
@@ -60,6 +57,14 @@
 by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
 qed_spec_mp "rel_pow_Suc_D2";
 
+
+goal RelPow.thy
+"!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
+by (nat_ind_tac "n" 1);
+by (fast_tac (!claset addss (!simpset)) 1);
+by (fast_tac (!claset addss (!simpset)) 1);
+qed_spec_mp "rel_pow_Suc_D2'";
+
 val [p1,p2,p3] = goal RelPow.thy
     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
 \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
@@ -69,7 +74,9 @@
 by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
 by (cut_facts_tac [p1] 1);
 by (Asm_full_simp_tac 1);
-by (dtac rel_pow_Suc_D2 1);
+be compEpair 1;
+by (dtac (conjI RS rel_pow_Suc_D2') 1);
+ba 1;
 by (etac exE 1);
 by (etac p3 1);
 by (etac conjunct1 1);
@@ -96,3 +103,6 @@
 goal RelPow.thy "R^* = (UN n. R^n)";
 by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";
+
+
+