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