src/HOL/Lambda/Commutation.ML
author paulson
Wed, 23 Apr 1997 11:20:18 +0200
changeset 3024 005d899b5c48
parent 2922 580647a879cf
child 3439 54785105178c
permissions -rw-r--r--
Necessary inclusion of depth bound into blast_tac call
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Lambda/Commutation.thy
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     2
    ID:         $Id$
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     4
    Copyright   1995 TU Muenchen
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     5
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     6
Basic commutation lemmas.
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     7
*)
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     8
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     9
open Commutation;
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    10
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    11
(*** square ***)
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    12
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    13
goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    14
by (Blast_tac 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    15
qed "square_sym";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    16
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    17
goalw Commutation.thy [square_def]
1431
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    18
  "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    19
by (Blast_tac 1);
1431
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    20
qed "square_subset";
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    21
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    22
goalw Commutation.thy [square_def]
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    23
  "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    24
by (Blast_tac 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    25
qed "square_reflcl";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    26
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    27
goalw Commutation.thy [square_def]
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    28
  "!!R. square R S S T ==> square (R^*) S S (T^*)";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1974
diff changeset
    29
by (strip_tac 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1431
diff changeset
    30
by (etac rtrancl_induct 1);
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    31
by (Blast_tac 1);
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    32
by (blast_tac (!claset addIs [rtrancl_into_rtrancl]) 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    33
qed "square_rtrancl";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    34
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    35
goalw Commutation.thy [commute_def]
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    36
 "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1974
diff changeset
    37
by (fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl]
1974
b50f96543dec Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents: 1641
diff changeset
    38
                     addEs [r_into_rtrancl]
b50f96543dec Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents: 1641
diff changeset
    39
                     addss !simpset) 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    40
qed "square_rtrancl_reflcl_commute";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    41
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    42
(*** commute ***)
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    43
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    44
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    45
by (blast_tac (!claset addIs [square_sym]) 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    46
qed "commute_sym";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    47
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    48
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    49
by (blast_tac (!claset addIs [square_rtrancl,square_sym]) 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    50
qed "commute_rtrancl";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    51
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    52
goalw Commutation.thy [commute_def,square_def]
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    53
  "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    54
by (Blast_tac 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    55
qed "commute_Un";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    56
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    57
(*** diamond, confluence and union ***)
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    58
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    59
goalw Commutation.thy [diamond_def]
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    60
  "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1974
diff changeset
    61
by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    62
qed "diamond_Un";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    63
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    64
goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)";
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1431
diff changeset
    65
by (etac commute_rtrancl 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    66
qed "diamond_confluent";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    67
1431
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    68
goalw Commutation.thy [diamond_def]
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    69
  "!!R. square R R (R^=) (R^=) ==> confluent R";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    70
by (fast_tac (!claset addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    71
                      addEs [square_subset]) 1);
1431
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    72
qed "square_reflcl_confluent";
be7c6d77e19c Polished proofs.
nipkow
parents: 1302
diff changeset
    73
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    74
goal Commutation.thy
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    75
 "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    76
\      ==> confluent(R Un S)";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1974
diff changeset
    77
by (rtac (rtrancl_Un_rtrancl RS subst) 1);
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    78
by (blast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    79
qed "confluent_Un";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    80
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    81
goal Commutation.thy
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    82
  "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1974
diff changeset
    83
by (fast_tac (!claset addIs [diamond_confluent]
1974
b50f96543dec Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents: 1641
diff changeset
    84
                    addDs [rtrancl_subset RS sym] addss !simpset) 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    85
qed "diamond_to_confluence";
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    86
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    87
(*** Church_Rosser ***)
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    88
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    89
goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def]
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    90
  "Church_Rosser(R) = confluent(R)";
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    91
by (safe_tac HOL_cs);
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    92
 by (blast_tac (HOL_cs addIs
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    93
      [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    94
       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1431
diff changeset
    95
by (etac rtrancl_induct 1);
2897
27dc4862751b Now calls blast_tac
paulson
parents: 2057
diff changeset
    96
 by (Blast_tac 1);
3024
005d899b5c48 Necessary inclusion of depth bound into blast_tac call
paulson
parents: 2922
diff changeset
    97
by (Blast.depth_tac (!claset delrules [rtrancl_refl] 
005d899b5c48 Necessary inclusion of depth bound into blast_tac call
paulson
parents: 2922
diff changeset
    98
                       addIs [r_into_rtrancl, rtrancl_trans]) 12 1);
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    99
qed "Church_Rosser_confluent";