src/HOL/RelPow.ML
author paulson
Wed Mar 06 12:52:11 1996 +0100 (1996-03-06)
changeset 1552 6f71b5d46700
parent 1515 4ed79ebab64d
child 1693 7083f6b05423
permissions -rw-r--r--
Ran expandshort
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@1496
    12
goal RelPow.thy "(x,x) : R^0";
paulson@1552
    13
by (Simp_tac 1);
nipkow@1496
    14
qed "rel_pow_0_I";
nipkow@1496
    15
nipkow@1496
    16
goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
paulson@1552
    17
by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
paulson@1552
    18
by (fast_tac comp_cs 1);
nipkow@1496
    19
qed "rel_pow_Suc_I";
nipkow@1496
    20
nipkow@1496
    21
goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
paulson@1552
    22
by (nat_ind_tac "n" 1);
paulson@1552
    23
by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
paulson@1552
    24
by (fast_tac comp_cs 1);
paulson@1552
    25
by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
paulson@1552
    26
by (fast_tac comp_cs 1);
nipkow@1496
    27
qed_spec_mp "rel_pow_Suc_I2";
nipkow@1496
    28
nipkow@1515
    29
goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
paulson@1552
    30
by (Asm_full_simp_tac 1);
nipkow@1515
    31
qed "rel_pow_0_E";
nipkow@1515
    32
nipkow@1515
    33
val [major,minor] = goal RelPow.thy
nipkow@1515
    34
  "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
paulson@1552
    35
by (cut_facts_tac [major] 1);
paulson@1552
    36
by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
paulson@1552
    37
by (fast_tac (comp_cs addIs [minor]) 1);
nipkow@1515
    38
qed "rel_pow_Suc_E";
nipkow@1515
    39
nipkow@1515
    40
val [p1,p2,p3] = goal RelPow.thy
nipkow@1515
    41
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
nipkow@1515
    42
\       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
nipkow@1515
    43
\    |] ==> P";
paulson@1552
    44
by (res_inst_tac [("n","n")] natE 1);
paulson@1552
    45
by (cut_facts_tac [p1] 1);
paulson@1552
    46
by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
paulson@1552
    47
by (cut_facts_tac [p1] 1);
paulson@1552
    48
by (Asm_full_simp_tac 1);
paulson@1552
    49
by (etac rel_pow_Suc_E 1);
paulson@1552
    50
by (REPEAT(ares_tac [p3] 1));
nipkow@1515
    51
qed "rel_pow_E";
nipkow@1515
    52
nipkow@1496
    53
goal RelPow.thy "!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@1552
    55
by (fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
paulson@1552
    56
by (fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
nipkow@1515
    57
qed_spec_mp "rel_pow_Suc_D2";
nipkow@1496
    58
nipkow@1496
    59
val [p1,p2,p3] = goal RelPow.thy
nipkow@1496
    60
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
nipkow@1496
    61
\       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
nipkow@1496
    62
\    |] ==> P";
paulson@1552
    63
by (res_inst_tac [("n","n")] natE 1);
paulson@1552
    64
by (cut_facts_tac [p1] 1);
paulson@1552
    65
by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
paulson@1552
    66
by (cut_facts_tac [p1] 1);
paulson@1552
    67
by (Asm_full_simp_tac 1);
paulson@1552
    68
by (dtac rel_pow_Suc_D2 1);
paulson@1552
    69
by (etac exE 1);
paulson@1552
    70
by (etac p3 1);
paulson@1552
    71
by (etac conjunct1 1);
paulson@1552
    72
by (etac conjunct2 1);
nipkow@1515
    73
qed "rel_pow_E2";
nipkow@1496
    74
nipkow@1496
    75
goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
paulson@1552
    76
by (split_all_tac 1);
paulson@1552
    77
by (etac rtrancl_induct 1);
paulson@1552
    78
by (ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
nipkow@1496
    79
qed "rtrancl_imp_UN_rel_pow";
nipkow@1496
    80
nipkow@1496
    81
goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
paulson@1552
    82
by (nat_ind_tac "n" 1);
paulson@1552
    83
by (fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
paulson@1552
    84
by (fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
nipkow@1496
    85
val lemma = result() RS spec RS mp;
nipkow@1496
    86
nipkow@1496
    87
goal RelPow.thy "!!p. p:R^n ==> p:R^*";
paulson@1552
    88
by (split_all_tac 1);
paulson@1552
    89
by (etac lemma 1);
nipkow@1515
    90
qed "rel_pow_imp_rtrancl";
nipkow@1496
    91
nipkow@1496
    92
goal RelPow.thy "R^* = (UN n. R^n)";
paulson@1552
    93
by (fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
nipkow@1496
    94
qed "rtrancl_is_UN_rel_pow";