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