src/HOL/RelPow.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5183 89f162de39cf
child 5316 7a8975451a89
permissions -rw-r--r--
even more tidying of Goal commands
     1 (*  Title:      HOL/RelPow.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     5 *)
     6 
     7 open RelPow;
     8 
     9 Goal "!!R:: ('a*'a)set. R^1 = R";
    10 by (Simp_tac 1);
    11 qed "rel_pow_1";
    12 Addsimps [rel_pow_1];
    13 
    14 Goal "(x,x) : R^0";
    15 by (Simp_tac 1);
    16 qed "rel_pow_0_I";
    17 
    18 Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    19 by (Simp_tac  1);
    20 by (Blast_tac 1);
    21 qed "rel_pow_Suc_I";
    22 
    23 Goal "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    24 by (nat_ind_tac "n" 1);
    25 by (Simp_tac  1);
    26 by (Asm_full_simp_tac 1);
    27 by (Blast_tac 1);
    28 qed_spec_mp "rel_pow_Suc_I2";
    29 
    30 Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
    31 by (Asm_full_simp_tac 1);
    32 qed "rel_pow_0_E";
    33 
    34 val [major,minor] = goal RelPow.thy
    35   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
    36 by (cut_facts_tac [major] 1);
    37 by (Asm_full_simp_tac  1);
    38 by (blast_tac (claset() addIs [minor]) 1);
    39 qed "rel_pow_Suc_E";
    40 
    41 val [p1,p2,p3] = goal RelPow.thy
    42     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    43 \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
    44 \    |] ==> P";
    45 by (cut_facts_tac [p1] 1);
    46 by (exhaust_tac "n" 1);
    47 by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
    48 by (Asm_full_simp_tac 1);
    49 by (etac compEpair 1);
    50 by (REPEAT(ares_tac [p3] 1));
    51 qed "rel_pow_E";
    52 
    53 Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
    54 by (nat_ind_tac "n" 1);
    55 by (blast_tac (claset() addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    56 by (blast_tac (claset() addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    57 qed_spec_mp "rel_pow_Suc_D2";
    58 
    59 
    60 Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
    61 by (nat_ind_tac "n" 1);
    62 by (fast_tac (claset() addss (simpset())) 1);
    63 by (fast_tac (claset() addss (simpset())) 1);
    64 qed_spec_mp "rel_pow_Suc_D2'";
    65 
    66 val [p1,p2,p3] = goal RelPow.thy
    67     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    68 \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
    69 \    |] ==> P";
    70 by (cut_facts_tac [p1] 1);
    71 by (exhaust_tac "n" 1);
    72 by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
    73 by (Asm_full_simp_tac 1);
    74 by (etac compEpair 1);
    75 by (dtac (conjI RS rel_pow_Suc_D2') 1);
    76 by (assume_tac 1);
    77 by (etac exE 1);
    78 by (etac p3 1);
    79 by (etac conjunct1 1);
    80 by (etac conjunct2 1);
    81 qed "rel_pow_E2";
    82 
    83 Goal "!!p. p:R^* ==> p : (UN n. R^n)";
    84 by (split_all_tac 1);
    85 by (etac rtrancl_induct 1);
    86 by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I])));
    87 qed "rtrancl_imp_UN_rel_pow";
    88 
    89 Goal "!y. (x,y):R^n --> (x,y):R^*";
    90 by (nat_ind_tac "n" 1);
    91 by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
    92 by (blast_tac (claset() addEs [rel_pow_Suc_E]
    93                        addIs [rtrancl_into_rtrancl]) 1);
    94 val lemma = result() RS spec RS mp;
    95 
    96 Goal "!!p. p:R^n ==> p:R^*";
    97 by (split_all_tac 1);
    98 by (etac lemma 1);
    99 qed "rel_pow_imp_rtrancl";
   100 
   101 Goal "R^* = (UN n. R^n)";
   102 by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
   103 qed "rtrancl_is_UN_rel_pow";
   104 
   105 
   106 Goal "!!r::('a * 'a)set. Univalent r ==> Univalent (r^n)";
   107 by (rtac UnivalentI 1);
   108 by (induct_tac "n" 1);
   109  by (Simp_tac 1);
   110 by (fast_tac (claset() addDs [UnivalentD] addEs [rel_pow_Suc_E]) 1);
   111 qed_spec_mp "Univalent_rel_pow";
   112 
   113 
   114 
   115