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