Minor changes due to primrec definition for ^
authorpusch
Thu Mar 06 16:06:31 1997 +0100 (1997-03-06)
changeset 27412b7f72cbe51f
parent 2740 2c549ae2563b
child 2742 b70d7b032e62
Minor changes due to primrec definition for ^
src/HOL/RelPow.ML
     1.1 --- a/src/HOL/RelPow.ML	Thu Mar 06 16:06:08 1997 +0100
     1.2 +++ b/src/HOL/RelPow.ML	Thu Mar 06 16:06:31 1997 +0100
     1.3 @@ -6,11 +6,8 @@
     1.4  
     1.5  open RelPow;
     1.6  
     1.7 -val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
     1.8 -Addsimps [rel_pow_0];
     1.9 -
    1.10  goal RelPow.thy "R^1 = R";
    1.11 -by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.12 +by (Simp_tac 1);
    1.13  qed "rel_pow_1";
    1.14  Addsimps [rel_pow_1];
    1.15  
    1.16 @@ -19,14 +16,14 @@
    1.17  qed "rel_pow_0_I";
    1.18  
    1.19  goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    1.20 -by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.21 +by (Simp_tac  1);
    1.22  by (Fast_tac 1);
    1.23  qed "rel_pow_Suc_I";
    1.24  
    1.25  goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    1.26  by (nat_ind_tac "n" 1);
    1.27 -by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.28 -by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.29 +by (Simp_tac  1);
    1.30 +by (Asm_full_simp_tac 1);
    1.31  by (Fast_tac 1);
    1.32  qed_spec_mp "rel_pow_Suc_I2";
    1.33  
    1.34 @@ -37,7 +34,7 @@
    1.35  val [major,minor] = goal RelPow.thy
    1.36    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
    1.37  by (cut_facts_tac [major] 1);
    1.38 -by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.39 +by (Asm_full_simp_tac  1);
    1.40  by (fast_tac (!claset addIs [minor]) 1);
    1.41  qed "rel_pow_Suc_E";
    1.42  
    1.43 @@ -50,7 +47,7 @@
    1.44  by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
    1.45  by (cut_facts_tac [p1] 1);
    1.46  by (Asm_full_simp_tac 1);
    1.47 -by (etac rel_pow_Suc_E 1);
    1.48 +by (etac compEpair 1);
    1.49  by (REPEAT(ares_tac [p3] 1));
    1.50  qed "rel_pow_E";
    1.51  
    1.52 @@ -60,6 +57,14 @@
    1.53  by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    1.54  qed_spec_mp "rel_pow_Suc_D2";
    1.55  
    1.56 +
    1.57 +goal RelPow.thy
    1.58 +"!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
    1.59 +by (nat_ind_tac "n" 1);
    1.60 +by (fast_tac (!claset addss (!simpset)) 1);
    1.61 +by (fast_tac (!claset addss (!simpset)) 1);
    1.62 +qed_spec_mp "rel_pow_Suc_D2'";
    1.63 +
    1.64  val [p1,p2,p3] = goal RelPow.thy
    1.65      "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    1.66  \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
    1.67 @@ -69,7 +74,9 @@
    1.68  by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
    1.69  by (cut_facts_tac [p1] 1);
    1.70  by (Asm_full_simp_tac 1);
    1.71 -by (dtac rel_pow_Suc_D2 1);
    1.72 +be compEpair 1;
    1.73 +by (dtac (conjI RS rel_pow_Suc_D2') 1);
    1.74 +ba 1;
    1.75  by (etac exE 1);
    1.76  by (etac p3 1);
    1.77  by (etac conjunct1 1);
    1.78 @@ -96,3 +103,6 @@
    1.79  goal RelPow.thy "R^* = (UN n. R^n)";
    1.80  by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
    1.81  qed "rtrancl_is_UN_rel_pow";
    1.82 +
    1.83 +
    1.84 +