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