Added a few thms and the new theory RelPow.
authornipkow
Thu Feb 15 08:10:36 1996 +0100 (1996-02-15)
changeset 1496c443b2adaf52
parent 1495 b8b54847c77f
child 1497 41a1b0426b2e
Added a few thms and the new theory RelPow.
src/HOL/Arith.ML
src/HOL/ROOT.ML
src/HOL/RelPow.ML
src/HOL/RelPow.thy
src/HOL/Trancl.ML
     1.1 --- a/src/HOL/Arith.ML	Tue Feb 13 17:16:06 1996 +0100
     1.2 +++ b/src/HOL/Arith.ML	Thu Feb 15 08:10:36 1996 +0100
     1.3 @@ -151,6 +151,7 @@
     1.4  
     1.5  qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
     1.6   (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
     1.7 +Addsimps [diff_self_eq_0];
     1.8  
     1.9  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
    1.10  val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
     2.1 --- a/src/HOL/ROOT.ML	Tue Feb 13 17:16:06 1996 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Thu Feb 15 08:10:36 1996 +0100
     2.3 @@ -27,10 +27,9 @@
     2.4  use_thy "subset";
     2.5  use     "hologic.ML";
     2.6  use     "typedef.ML";
     2.7 -use_thy "Prod";
     2.8  use_thy "Sum";
     2.9  use_thy "Gfp";
    2.10 -use_thy "Nat";
    2.11 +use_thy "RelPow";
    2.12  
    2.13  use "datatype.ML";
    2.14  use "ind_syntax.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/RelPow.ML	Thu Feb 15 08:10:36 1996 +0100
     3.3 @@ -0,0 +1,76 @@
     3.4 +(*  Title:      HOL/RelPow.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow
     3.7 +    Copyright   1996  TU Muenchen
     3.8 +*)
     3.9 +
    3.10 +open RelPow;
    3.11 +
    3.12 +val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
    3.13 +Addsimps [rel_pow_0, rel_pow_Suc];
    3.14 +
    3.15 +goal RelPow.thy "(x,x) : R^0";
    3.16 +by(Simp_tac 1);
    3.17 +qed "rel_pow_0_I";
    3.18 +
    3.19 +goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    3.20 +by(Simp_tac 1);
    3.21 +by(fast_tac comp_cs 1);
    3.22 +qed "rel_pow_Suc_I";
    3.23 +
    3.24 +goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    3.25 +by(nat_ind_tac "n" 1);
    3.26 +by(Simp_tac 1);
    3.27 +by(fast_tac comp_cs 1);
    3.28 +by(Asm_full_simp_tac 1);
    3.29 +by(fast_tac comp_cs 1);
    3.30 +qed_spec_mp "rel_pow_Suc_I2";
    3.31 +
    3.32 +goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
    3.33 +by(nat_ind_tac "n" 1);
    3.34 +by(Simp_tac 1);
    3.35 +by(fast_tac comp_cs 1);
    3.36 +by(Asm_full_simp_tac 1);
    3.37 +by(fast_tac comp_cs 1);
    3.38 +val lemma = result() RS spec RS spec RS mp;
    3.39 +
    3.40 +goal RelPow.thy
    3.41 +  "(x,z) : R^n --> (n=0 --> x=z --> P) --> \
    3.42 +\     (!y m. n = Suc m --> (x,y):R --> (y,z):R^m --> P) --> P";
    3.43 +by(res_inst_tac [("n","n")] natE 1);
    3.44 +by(Asm_simp_tac 1);
    3.45 +by(hyp_subst_tac 1);
    3.46 +by(fast_tac (HOL_cs addDs [lemma]) 1);
    3.47 +val lemma = result() RS mp RS mp RS mp;
    3.48 +
    3.49 +val [p1,p2,p3] = goal RelPow.thy
    3.50 +    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    3.51 +\       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
    3.52 +\    |] ==> P";
    3.53 +br (p1 RS lemma) 1;
    3.54 +by(REPEAT(ares_tac [impI,p2] 1));
    3.55 +by(REPEAT(ares_tac [allI,impI,p3] 1));
    3.56 +qed "UN_rel_powE2";
    3.57 +
    3.58 +goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
    3.59 +by(split_all_tac 1);
    3.60 +be rtrancl_induct 1;
    3.61 +by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
    3.62 +qed "rtrancl_imp_UN_rel_pow";
    3.63 +
    3.64 +goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
    3.65 +by(nat_ind_tac "n" 1);
    3.66 +by(Simp_tac 1);
    3.67 +by(fast_tac (HOL_cs addIs [rtrancl_refl]) 1);
    3.68 +by(Simp_tac 1);
    3.69 +by(fast_tac (trancl_cs addEs [rtrancl_into_rtrancl]) 1);
    3.70 +val lemma = result() RS spec RS mp;
    3.71 +
    3.72 +goal RelPow.thy "!!p. p:R^n ==> p:R^*";
    3.73 +by(split_all_tac 1);
    3.74 +be lemma 1;
    3.75 +qed "UN_rel_pow_imp_rtrancl";
    3.76 +
    3.77 +goal RelPow.thy "R^* = (UN n. R^n)";
    3.78 +by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,UN_rel_pow_imp_rtrancl]) 1);
    3.79 +qed "rtrancl_is_UN_rel_pow";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/RelPow.thy	Thu Feb 15 08:10:36 1996 +0100
     4.3 @@ -0,0 +1,15 @@
     4.4 +(*  Title:      HOL/RelPow.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow
     4.7 +    Copyright   1996  TU Muenchen
     4.8 +
     4.9 +R^n = R O ... O R, the n-fold composition of R
    4.10 +*)
    4.11 +
    4.12 +RelPow = Nat +
    4.13 +
    4.14 +consts
    4.15 +  "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100)
    4.16 +defs
    4.17 +  rel_pow_def "R^n == nat_rec n id (%m S. R O S)"
    4.18 +end
     5.1 --- a/src/HOL/Trancl.ML	Tue Feb 13 17:16:06 1996 +0100
     5.2 +++ b/src/HOL/Trancl.ML	Thu Feb 15 08:10:36 1996 +0100
     5.3 @@ -86,6 +86,16 @@
     5.4  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
     5.5  qed "rtranclE";
     5.6  
     5.7 +goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*";
     5.8 +be rtrancl_induct 1;
     5.9 +by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
    5.10 +by(fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
    5.11 +val lemma = result();
    5.12 +
    5.13 +goal Trancl.thy  "!!R. [| (x,y) : R;  (y,z) : R^* |] ==> (x,z) : R^*";
    5.14 +by(fast_tac (HOL_cs addDs [lemma]) 1);
    5.15 +qed "rtrancl_into_rtrancl2";
    5.16 +
    5.17  
    5.18  (**** The relation trancl ****)
    5.19