src/HOL/RelPow.ML
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8709 483a3eb96c7e
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/RelPow.ML
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     5
*)
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     6
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     7
open RelPow;
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
     8
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
     9
Goal "!!R:: ('a*'a)set. R^1 = R";
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    10
by (Simp_tac 1);
1693
7083f6b05423 Added R^1 = R
nipkow
parents: 1552
diff changeset
    11
qed "rel_pow_1";
7083f6b05423 Added R^1 = R
nipkow
parents: 1552
diff changeset
    12
Addsimps [rel_pow_1];
7083f6b05423 Added R^1 = R
nipkow
parents: 1552
diff changeset
    13
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
    14
Goal "(x,x) : R^0";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    15
by (Simp_tac 1);
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    16
qed "rel_pow_0_I";
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    17
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    18
Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    19
by (Simp_tac  1);
2922
580647a879cf Using Blast_tac
paulson
parents: 2741
diff changeset
    20
by (Blast_tac 1);
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    21
qed "rel_pow_Suc_I";
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    22
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
    23
Goal "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
8709
483a3eb96c7e stopped using the obsolete "nat_ind_tac"
paulson
parents: 8442
diff changeset
    24
by (induct_tac "n" 1);
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    25
by (Simp_tac  1);
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    26
by (Asm_full_simp_tac 1);
2922
580647a879cf Using Blast_tac
paulson
parents: 2741
diff changeset
    27
by (Blast_tac 1);
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    28
qed_spec_mp "rel_pow_Suc_I2";
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    29
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
    30
Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    31
by (Asm_full_simp_tac 1);
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    32
qed "rel_pow_0_E";
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    33
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    34
val [major,minor] = Goal
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    35
  "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    36
by (cut_facts_tac [major] 1);
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    37
by (Asm_full_simp_tac  1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    38
by (blast_tac (claset() addIs [minor]) 1);
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    39
qed "rel_pow_Suc_E";
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    40
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    41
val [p1,p2,p3] = Goal
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    42
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    43
\       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    44
\    |] ==> P";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    45
by (cut_facts_tac [p1] 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    46
by (case_tac "n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    47
by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    48
by (Asm_full_simp_tac 1);
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    49
by (etac compEpair 1);
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    50
by (REPEAT(ares_tac [p3] 1));
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    51
qed "rel_pow_E";
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    52
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
    53
Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
8709
483a3eb96c7e stopped using the obsolete "nat_ind_tac"
paulson
parents: 8442
diff changeset
    54
by (induct_tac "n" 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    55
by (blast_tac (claset() addIs [rel_pow_0_I] 
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    56
	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    57
by (blast_tac (claset() addIs [rel_pow_Suc_I]  
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    58
	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    59
qed_spec_mp "rel_pow_Suc_D2";
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    60
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    61
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5183
diff changeset
    62
Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
8709
483a3eb96c7e stopped using the obsolete "nat_ind_tac"
paulson
parents: 8442
diff changeset
    63
by (induct_tac "n" 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    64
by (ALLGOALS Asm_simp_tac);
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    65
by (Blast_tac 1);
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    66
qed_spec_mp "rel_pow_Suc_D2'";
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    67
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
    68
val [p1,p2,p3] = Goal
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    69
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    70
\       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    71
\    |] ==> P";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    72
by (cut_facts_tac [p1] 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    73
by (case_tac "n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    74
by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    75
by (Asm_full_simp_tac 1);
3023
01364e2f30ad Ran expandshort
paulson
parents: 2935
diff changeset
    76
by (etac compEpair 1);
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
    77
by (dtac (conjI RS rel_pow_Suc_D2') 1);
3023
01364e2f30ad Ran expandshort
paulson
parents: 2935
diff changeset
    78
by (assume_tac 1);
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    79
by (etac exE 1);
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    80
by (etac p3 1);
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    81
by (etac conjunct1 1);
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    82
by (etac conjunct2 1);
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
    83
qed "rel_pow_E2";
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    84
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
    85
Goal "!!p. p:R^* ==> p : (UN n. R^n)";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    86
by (split_all_tac 1);
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    87
by (etac rtrancl_induct 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    88
by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I])));
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    89
qed "rtrancl_imp_UN_rel_pow";
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    90
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
    91
Goal "!y. (x,y):R^n --> (x,y):R^*";
8709
483a3eb96c7e stopped using the obsolete "nat_ind_tac"
paulson
parents: 8442
diff changeset
    92
by (induct_tac "n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    93
by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    94
by (blast_tac (claset() addEs [rel_pow_Suc_E]
3023
01364e2f30ad Ran expandshort
paulson
parents: 2935
diff changeset
    95
                       addIs [rtrancl_into_rtrancl]) 1);
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    96
val lemma = result() RS spec RS mp;
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
    97
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
    98
Goal "!!p. p:R^n ==> p:R^*";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
    99
by (split_all_tac 1);
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
   100
by (etac lemma 1);
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1496
diff changeset
   101
qed "rel_pow_imp_rtrancl";
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
   102
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4759
diff changeset
   103
Goal "R^* = (UN n. R^n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   104
by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
1496
c443b2adaf52 Added a few thms and the new theory RelPow.
nipkow
parents:
diff changeset
   105
qed "rtrancl_is_UN_rel_pow";
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
   106
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
   107
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 5316
diff changeset
   108
Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)";
722074b93cdd renamed Univalent to univalent
oheimb
parents: 5316
diff changeset
   109
by (rtac univalentI 1);
4759
33a03e70e641 added Univalent_rel_pow
oheimb
parents: 4089
diff changeset
   110
by (induct_tac "n" 1);
33a03e70e641 added Univalent_rel_pow
oheimb
parents: 4089
diff changeset
   111
 by (Simp_tac 1);
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 5316
diff changeset
   112
by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1);
722074b93cdd renamed Univalent to univalent
oheimb
parents: 5316
diff changeset
   113
qed_spec_mp "univalent_rel_pow";
2741
2b7f72cbe51f Minor changes due to primrec definition for ^
pusch
parents: 2056
diff changeset
   114
4759
33a03e70e641 added Univalent_rel_pow
oheimb
parents: 4089
diff changeset
   115
33a03e70e641 added Univalent_rel_pow
oheimb
parents: 4089
diff changeset
   116
33a03e70e641 added Univalent_rel_pow
oheimb
parents: 4089
diff changeset
   117