src/HOL/Lambda/Commutation.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2897 27dc4862751b
child 2922 580647a879cf
permissions -rw-r--r--
Dep. on Provers/nat_transitive
nipkow@1278
     1
(*  Title:      HOL/Lambda/Commutation.thy
nipkow@1278
     2
    ID:         $Id$
nipkow@1278
     3
    Author:     Tobias Nipkow
nipkow@1278
     4
    Copyright   1995 TU Muenchen
nipkow@1278
     5
nipkow@1278
     6
Basic commutation lemmas.
nipkow@1278
     7
*)
nipkow@1278
     8
nipkow@1278
     9
open Commutation;
nipkow@1278
    10
nipkow@1278
    11
(*** square ***)
nipkow@1278
    12
nipkow@1278
    13
goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
paulson@2897
    14
by (Blast_tac 1);
nipkow@1278
    15
qed "square_sym";
nipkow@1278
    16
nipkow@1278
    17
goalw Commutation.thy [square_def]
nipkow@1431
    18
  "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
paulson@2897
    19
by (Blast_tac 1);
nipkow@1431
    20
qed "square_subset";
nipkow@1431
    21
nipkow@1431
    22
goalw Commutation.thy [square_def]
nipkow@1278
    23
  "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
paulson@2897
    24
by (Blast_tac 1);
nipkow@1278
    25
qed "square_reflcl";
nipkow@1278
    26
nipkow@1278
    27
goalw Commutation.thy [square_def]
nipkow@1278
    28
  "!!R. square R S S T ==> square (R^*) S S (T^*)";
paulson@2031
    29
by (strip_tac 1);
clasohm@1465
    30
by (etac rtrancl_induct 1);
paulson@2897
    31
by (Blast_tac 1);
paulson@2897
    32
by (blast_tac (!claset addIs [rtrancl_into_rtrancl]) 1);
nipkow@1278
    33
qed "square_rtrancl";
nipkow@1278
    34
nipkow@1278
    35
goalw Commutation.thy [commute_def]
nipkow@1278
    36
 "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
paulson@2031
    37
by (fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl]
nipkow@1974
    38
                     addEs [r_into_rtrancl]
nipkow@1974
    39
                     addss !simpset) 1);
nipkow@1278
    40
qed "square_rtrancl_reflcl_commute";
nipkow@1278
    41
nipkow@1278
    42
(*** commute ***)
nipkow@1278
    43
nipkow@1278
    44
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R";
paulson@2897
    45
by (blast_tac (!claset addIs [square_sym]) 1);
nipkow@1278
    46
qed "commute_sym";
nipkow@1278
    47
nipkow@1278
    48
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
paulson@2897
    49
by (blast_tac (!claset addIs [square_rtrancl,square_sym]) 1);
nipkow@1278
    50
qed "commute_rtrancl";
nipkow@1278
    51
nipkow@1278
    52
goalw Commutation.thy [commute_def,square_def]
nipkow@1278
    53
  "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
paulson@2897
    54
by (Blast_tac 1);
nipkow@1278
    55
qed "commute_Un";
nipkow@1278
    56
nipkow@1278
    57
(*** diamond, confluence and union ***)
nipkow@1278
    58
nipkow@1278
    59
goalw Commutation.thy [diamond_def]
nipkow@1278
    60
  "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
paulson@2031
    61
by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
nipkow@1278
    62
qed "diamond_Un";
nipkow@1278
    63
nipkow@1278
    64
goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)";
clasohm@1465
    65
by (etac commute_rtrancl 1);
nipkow@1278
    66
qed "diamond_confluent";
nipkow@1278
    67
nipkow@1431
    68
goalw Commutation.thy [diamond_def]
nipkow@1431
    69
  "!!R. square R R (R^=) (R^=) ==> confluent R";
paulson@2897
    70
by (fast_tac (!claset addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
paulson@2897
    71
                      addEs [square_subset]) 1);
nipkow@1431
    72
qed "square_reflcl_confluent";
nipkow@1431
    73
nipkow@1278
    74
goal Commutation.thy
nipkow@1278
    75
 "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
nipkow@1278
    76
\      ==> confluent(R Un S)";
paulson@2031
    77
by (rtac (rtrancl_Un_rtrancl RS subst) 1);
paulson@2897
    78
by (blast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1);
nipkow@1278
    79
qed "confluent_Un";
nipkow@1278
    80
nipkow@1278
    81
goal Commutation.thy
nipkow@1278
    82
  "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
paulson@2031
    83
by (fast_tac (!claset addIs [diamond_confluent]
nipkow@1974
    84
                    addDs [rtrancl_subset RS sym] addss !simpset) 1);
nipkow@1278
    85
qed "diamond_to_confluence";
nipkow@1278
    86
nipkow@1278
    87
(*** Church_Rosser ***)
nipkow@1278
    88
nipkow@1278
    89
goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def]
nipkow@1278
    90
  "Church_Rosser(R) = confluent(R)";
paulson@2897
    91
by (safe_tac HOL_cs);
paulson@2897
    92
 by (blast_tac (HOL_cs addIs
nipkow@1278
    93
      [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
nipkow@1278
    94
       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
clasohm@1465
    95
by (etac rtrancl_induct 1);
paulson@2897
    96
 by (Blast_tac 1);
paulson@2031
    97
by (slow_best_tac (!claset addIs [r_into_rtrancl]
nipkow@1302
    98
                    addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
nipkow@1278
    99
qed "Church_Rosser_confluent";