# HG changeset patch
# User nipkow
# Date 824368236 -3600
# Node ID c443b2adaf52b7d0f588be7b2d32a0aee635cbd8
# Parent  b8b54847c77f3d8ac4286d6f0cc18885d9c8c38e
Added a few thms and the new theory RelPow.

diff -r b8b54847c77f -r c443b2adaf52 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Feb 13 17:16:06 1996 +0100
+++ b/src/HOL/Arith.ML	Thu Feb 15 08:10:36 1996 +0100
@@ -151,6 +151,7 @@
 
 qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+Addsimps [diff_self_eq_0];
 
 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
 val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
diff -r b8b54847c77f -r c443b2adaf52 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Feb 13 17:16:06 1996 +0100
+++ b/src/HOL/ROOT.ML	Thu Feb 15 08:10:36 1996 +0100
@@ -27,10 +27,9 @@
 use_thy "subset";
 use     "hologic.ML";
 use     "typedef.ML";
-use_thy "Prod";
 use_thy "Sum";
 use_thy "Gfp";
-use_thy "Nat";
+use_thy "RelPow";
 
 use "datatype.ML";
 use "ind_syntax.ML";
diff -r b8b54847c77f -r c443b2adaf52 src/HOL/RelPow.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/RelPow.ML	Thu Feb 15 08:10:36 1996 +0100
@@ -0,0 +1,76 @@
+(*  Title:      HOL/RelPow.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996  TU Muenchen
+*)
+
+open RelPow;
+
+val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
+Addsimps [rel_pow_0, rel_pow_Suc];
+
+goal RelPow.thy "(x,x) : R^0";
+by(Simp_tac 1);
+qed "rel_pow_0_I";
+
+goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
+by(Simp_tac 1);
+by(fast_tac comp_cs 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 1);
+by(fast_tac comp_cs 1);
+by(Asm_full_simp_tac 1);
+by(fast_tac comp_cs 1);
+qed_spec_mp "rel_pow_Suc_I2";
+
+goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
+by(nat_ind_tac "n" 1);
+by(Simp_tac 1);
+by(fast_tac comp_cs 1);
+by(Asm_full_simp_tac 1);
+by(fast_tac comp_cs 1);
+val lemma = result() RS spec RS spec RS mp;
+
+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) --> P";
+by(res_inst_tac [("n","n")] natE 1);
+by(Asm_simp_tac 1);
+by(hyp_subst_tac 1);
+by(fast_tac (HOL_cs addDs [lemma]) 1);
+val lemma = result() RS mp RS mp RS mp;
+
+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  \
+\    |] ==> P";
+br (p1 RS lemma) 1;
+by(REPEAT(ares_tac [impI,p2] 1));
+by(REPEAT(ares_tac [allI,impI,p3] 1));
+qed "UN_rel_powE2";
+
+goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
+by(split_all_tac 1);
+be rtrancl_induct 1;
+by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
+qed "rtrancl_imp_UN_rel_pow";
+
+goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
+by(nat_ind_tac "n" 1);
+by(Simp_tac 1);
+by(fast_tac (HOL_cs addIs [rtrancl_refl]) 1);
+by(Simp_tac 1);
+by(fast_tac (trancl_cs addEs [rtrancl_into_rtrancl]) 1);
+val lemma = result() RS spec RS mp;
+
+goal RelPow.thy "!!p. p:R^n ==> p:R^*";
+by(split_all_tac 1);
+be lemma 1;
+qed "UN_rel_pow_imp_rtrancl";
+
+goal RelPow.thy "R^* = (UN n. R^n)";
+by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,UN_rel_pow_imp_rtrancl]) 1);
+qed "rtrancl_is_UN_rel_pow";
diff -r b8b54847c77f -r c443b2adaf52 src/HOL/RelPow.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/RelPow.thy	Thu Feb 15 08:10:36 1996 +0100
@@ -0,0 +1,15 @@
+(*  Title:      HOL/RelPow.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996  TU Muenchen
+
+R^n = R O ... O R, the n-fold composition of R
+*)
+
+RelPow = Nat +
+
+consts
+  "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100)
+defs
+  rel_pow_def "R^n == nat_rec n id (%m S. R O S)"
+end
diff -r b8b54847c77f -r c443b2adaf52 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Tue Feb 13 17:16:06 1996 +0100
+++ b/src/HOL/Trancl.ML	Thu Feb 15 08:10:36 1996 +0100
@@ -86,6 +86,16 @@
 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
 qed "rtranclE";
 
+goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*";
+be rtrancl_induct 1;
+by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
+by(fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
+val lemma = result();
+
+goal Trancl.thy  "!!R. [| (x,y) : R;  (y,z) : R^* |] ==> (x,z) : R^*";
+by(fast_tac (HOL_cs addDs [lemma]) 1);
+qed "rtrancl_into_rtrancl2";
+
 
 (**** The relation trancl ****)