src/HOL/RelPow.ML
author paulson
Thu Sep 26 12:47:47 1996 +0200 (1996-09-26)
changeset 2031 03a843f0f447
parent 1760 6f41a494f3b1
child 2056 93c093620c28
permissions -rw-r--r--
Ran expandshort
     1 (*  Title:      HOL/RelPow.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     5 *)
     6 
     7 open RelPow;
     8 
     9 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
    10 Addsimps [rel_pow_0];
    11 
    12 goal RelPow.thy "R^1 = R";
    13 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    14 qed "rel_pow_1";
    15 Addsimps [rel_pow_1];
    16 
    17 goal RelPow.thy "(x,x) : R^0";
    18 by (Simp_tac 1);
    19 qed "rel_pow_0_I";
    20 
    21 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    22 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    23 by (Fast_tac 1);
    24 qed "rel_pow_Suc_I";
    25 
    26 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    27 by (nat_ind_tac "n" 1);
    28 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    29 by (Fast_tac 1);
    30 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    31 by (Fast_tac 1);
    32 qed_spec_mp "rel_pow_Suc_I2";
    33 
    34 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
    35 by (Asm_full_simp_tac 1);
    36 qed "rel_pow_0_E";
    37 
    38 val [major,minor] = goal RelPow.thy
    39   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
    40 by (cut_facts_tac [major] 1);
    41 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    42 by (fast_tac (!claset addIs [minor]) 1);
    43 qed "rel_pow_Suc_E";
    44 
    45 val [p1,p2,p3] = goal RelPow.thy
    46     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    47 \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
    48 \    |] ==> P";
    49 by (res_inst_tac [("n","n")] natE 1);
    50 by (cut_facts_tac [p1] 1);
    51 by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
    52 by (cut_facts_tac [p1] 1);
    53 by (Asm_full_simp_tac 1);
    54 by (etac rel_pow_Suc_E 1);
    55 by (REPEAT(ares_tac [p3] 1));
    56 qed "rel_pow_E";
    57 
    58 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
    59 by (nat_ind_tac "n" 1);
    60 by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    61 by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    62 qed_spec_mp "rel_pow_Suc_D2";
    63 
    64 val [p1,p2,p3] = goal RelPow.thy
    65     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    66 \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
    67 \    |] ==> P";
    68 by (res_inst_tac [("n","n")] natE 1);
    69 by (cut_facts_tac [p1] 1);
    70 by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
    71 by (cut_facts_tac [p1] 1);
    72 by (Asm_full_simp_tac 1);
    73 by (dtac rel_pow_Suc_D2 1);
    74 by (etac exE 1);
    75 by (etac p3 1);
    76 by (etac conjunct1 1);
    77 by (etac conjunct2 1);
    78 qed "rel_pow_E2";
    79 
    80 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
    81 by (split_all_tac 1);
    82 by (etac rtrancl_induct 1);
    83 by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
    84 qed "rtrancl_imp_UN_rel_pow";
    85 
    86 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
    87 by (nat_ind_tac "n" 1);
    88 by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
    89 by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
    90 val lemma = result() RS spec RS mp;
    91 
    92 goal RelPow.thy "!!p. p:R^n ==> p:R^*";
    93 by (split_all_tac 1);
    94 by (etac lemma 1);
    95 qed "rel_pow_imp_rtrancl";
    96 
    97 goal RelPow.thy "R^* = (UN n. R^n)";
    98 by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
    99 qed "rtrancl_is_UN_rel_pow";