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