src/HOL/Lambda/Commutation.thy
author haftmann
Fri Mar 09 08:45:50 2007 +0100 (2007-03-09)
changeset 22422 ee19cdb07528
parent 22270 4ccb7e6be929
child 23464 bc2563c37b1a
permissions -rw-r--r--
stepping towards uniform lattice theory development in HOL
clasohm@1476
     1
(*  Title:      HOL/Lambda/Commutation.thy
nipkow@1278
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@1278
     4
    Copyright   1995  TU Muenchen
nipkow@1278
     5
*)
nipkow@1278
     6
wenzelm@9811
     7
header {* Abstract commutation and confluence notions *}
wenzelm@9811
     8
haftmann@16417
     9
theory Commutation imports Main begin
wenzelm@9811
    10
wenzelm@9811
    11
subsection {* Basic definitions *}
wenzelm@9811
    12
wenzelm@19086
    13
definition
berghofe@22270
    14
  square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
wenzelm@19086
    15
  "square R S T U =
berghofe@22270
    16
    (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
wenzelm@9811
    17
wenzelm@21404
    18
definition
berghofe@22270
    19
  commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
wenzelm@19086
    20
  "commute R S = square R S S R"
wenzelm@9811
    21
wenzelm@21404
    22
definition
berghofe@22270
    23
  diamond :: "('a => 'a => bool) => bool" where
wenzelm@19086
    24
  "diamond R = commute R R"
wenzelm@9811
    25
wenzelm@21404
    26
definition
berghofe@22270
    27
  Church_Rosser :: "('a => 'a => bool) => bool" where
wenzelm@19086
    28
  "Church_Rosser R =
haftmann@22422
    29
    (\<forall>x y. (sup R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
wenzelm@9811
    30
wenzelm@19363
    31
abbreviation
berghofe@22270
    32
  confluent :: "('a => 'a => bool) => bool" where
berghofe@22270
    33
  "confluent R == diamond (R^**)"
wenzelm@9811
    34
wenzelm@9811
    35
wenzelm@9811
    36
subsection {* Basic lemmas *}
wenzelm@9811
    37
wenzelm@9811
    38
subsubsection {* square *}
nipkow@1278
    39
wenzelm@9811
    40
lemma square_sym: "square R S T U ==> square S R U T"
wenzelm@9811
    41
  apply (unfold square_def)
wenzelm@9811
    42
  apply blast
wenzelm@9811
    43
  done
wenzelm@9811
    44
wenzelm@9811
    45
lemma square_subset:
berghofe@22270
    46
    "[| square R S T U; T \<le> T' |] ==> square R S T' U"
wenzelm@9811
    47
  apply (unfold square_def)
berghofe@22270
    48
  apply (blast dest: predicate2D)
wenzelm@9811
    49
  done
wenzelm@9811
    50
wenzelm@9811
    51
lemma square_reflcl:
berghofe@22270
    52
    "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
wenzelm@9811
    53
  apply (unfold square_def)
berghofe@22270
    54
  apply (blast dest: predicate2D)
wenzelm@9811
    55
  done
nipkow@1278
    56
wenzelm@9811
    57
lemma square_rtrancl:
berghofe@22270
    58
    "square R S S T ==> square (R^**) S S (T^**)"
wenzelm@9811
    59
  apply (unfold square_def)
wenzelm@9811
    60
  apply (intro strip)
berghofe@22270
    61
  apply (erule rtrancl_induct')
wenzelm@9811
    62
   apply blast
berghofe@22270
    63
  apply (blast intro: rtrancl.rtrancl_into_rtrancl)
wenzelm@9811
    64
  done
wenzelm@9811
    65
wenzelm@9811
    66
lemma square_rtrancl_reflcl_commute:
berghofe@22270
    67
    "square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
wenzelm@9811
    68
  apply (unfold commute_def)
berghofe@22270
    69
  apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl])
wenzelm@9811
    70
  done
wenzelm@9811
    71
nipkow@1278
    72
wenzelm@9811
    73
subsubsection {* commute *}
wenzelm@9811
    74
wenzelm@9811
    75
lemma commute_sym: "commute R S ==> commute S R"
wenzelm@9811
    76
  apply (unfold commute_def)
wenzelm@9811
    77
  apply (blast intro: square_sym)
wenzelm@9811
    78
  done
wenzelm@9811
    79
berghofe@22270
    80
lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
wenzelm@9811
    81
  apply (unfold commute_def)
wenzelm@9811
    82
  apply (blast intro: square_rtrancl square_sym)
wenzelm@9811
    83
  done
wenzelm@9811
    84
wenzelm@9811
    85
lemma commute_Un:
haftmann@22422
    86
    "[| commute R T; commute S T |] ==> commute (sup R S) T"
wenzelm@9811
    87
  apply (unfold commute_def square_def)
wenzelm@9811
    88
  apply blast
wenzelm@9811
    89
  done
wenzelm@9811
    90
wenzelm@9811
    91
wenzelm@9811
    92
subsubsection {* diamond, confluence, and union *}
wenzelm@9811
    93
wenzelm@9811
    94
lemma diamond_Un:
haftmann@22422
    95
    "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
wenzelm@9811
    96
  apply (unfold diamond_def)
wenzelm@9811
    97
  apply (assumption | rule commute_Un commute_sym)+
wenzelm@9811
    98
  done
wenzelm@9811
    99
wenzelm@9811
   100
lemma diamond_confluent: "diamond R ==> confluent R"
wenzelm@9811
   101
  apply (unfold diamond_def)
wenzelm@9811
   102
  apply (erule commute_rtrancl)
wenzelm@9811
   103
  done
nipkow@1278
   104
wenzelm@9811
   105
lemma square_reflcl_confluent:
berghofe@22270
   106
    "square R R (R^==) (R^==) ==> confluent R"
wenzelm@9811
   107
  apply (unfold diamond_def)
berghofe@22270
   108
  apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
wenzelm@9811
   109
  done
wenzelm@9811
   110
wenzelm@9811
   111
lemma confluent_Un:
haftmann@22422
   112
    "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
berghofe@22270
   113
  apply (rule rtrancl_Un_rtrancl' [THEN subst])
wenzelm@9811
   114
  apply (blast dest: diamond_Un intro: diamond_confluent)
wenzelm@9811
   115
  done
nipkow@1278
   116
wenzelm@9811
   117
lemma diamond_to_confluence:
berghofe@22270
   118
    "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
wenzelm@9811
   119
  apply (force intro: diamond_confluent
berghofe@22270
   120
    dest: rtrancl_subset' [symmetric])
wenzelm@9811
   121
  done
wenzelm@9811
   122
wenzelm@9811
   123
wenzelm@9811
   124
subsection {* Church-Rosser *}
nipkow@1278
   125
wenzelm@9811
   126
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
wenzelm@9811
   127
  apply (unfold square_def commute_def diamond_def Church_Rosser_def)
wenzelm@9811
   128
  apply (tactic {* safe_tac HOL_cs *})
wenzelm@9811
   129
   apply (tactic {*
wenzelm@9811
   130
     blast_tac (HOL_cs addIs
haftmann@22422
   131
       [thm "sup_ge2" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
berghofe@22270
   132
        thm "rtrancl_converseI'", thm "conversepI",
haftmann@22422
   133
        thm "sup_ge1" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
berghofe@22270
   134
  apply (erule rtrancl_induct')
wenzelm@9811
   135
   apply blast
berghofe@22270
   136
  apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
wenzelm@9811
   137
  done
wenzelm@9811
   138
berghofe@13089
   139
berghofe@13089
   140
subsection {* Newman's lemma *}
berghofe@13089
   141
berghofe@13349
   142
text {* Proof by Stefan Berghofer *}
nipkow@13346
   143
nipkow@13343
   144
theorem newman:
berghofe@22270
   145
  assumes wf: "wfP (R\<inverse>\<inverse>)"
berghofe@22270
   146
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
berghofe@22270
   147
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@22270
   148
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
berghofe@22270
   149
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@13349
   150
  using wf
berghofe@13349
   151
proof induct
berghofe@13349
   152
  case (less x b c)
berghofe@22270
   153
  have xc: "R\<^sup>*\<^sup>* x c" .
berghofe@22270
   154
  have xb: "R\<^sup>*\<^sup>* x b" . thus ?case
berghofe@22270
   155
  proof (rule converse_rtranclE')
berghofe@13349
   156
    assume "x = b"
berghofe@22270
   157
    with xc have "R\<^sup>*\<^sup>* b c" by simp
nipkow@17589
   158
    thus ?thesis by iprover
berghofe@13349
   159
  next
berghofe@13349
   160
    fix y
berghofe@22270
   161
    assume xy: "R x y"
berghofe@22270
   162
    assume yb: "R\<^sup>*\<^sup>* y b"
berghofe@13349
   163
    from xc show ?thesis
berghofe@22270
   164
    proof (rule converse_rtranclE')
berghofe@13349
   165
      assume "x = c"
berghofe@22270
   166
      with xb have "R\<^sup>*\<^sup>* c b" by simp
nipkow@17589
   167
      thus ?thesis by iprover
berghofe@13089
   168
    next
berghofe@13349
   169
      fix y'
berghofe@22270
   170
      assume y'c: "R\<^sup>*\<^sup>* y' c"
berghofe@22270
   171
      assume xy': "R x y'"
berghofe@22270
   172
      with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
berghofe@22270
   173
      then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
berghofe@22270
   174
      from xy have "R\<inverse>\<inverse> y x" ..
berghofe@22270
   175
      from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
berghofe@22270
   176
      then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
berghofe@22270
   177
      from xy' have "R\<inverse>\<inverse> y' x" ..
berghofe@22270
   178
      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
berghofe@13349
   179
      moreover note y'c
berghofe@22270
   180
      ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
berghofe@22270
   181
      then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
berghofe@22270
   182
      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
nipkow@17589
   183
      with cw show ?thesis by iprover
berghofe@13089
   184
    qed
berghofe@13089
   185
  qed
berghofe@13089
   186
qed
berghofe@13089
   187
berghofe@13349
   188
text {*
berghofe@13349
   189
  \medskip Alternative version.  Partly automated by Tobias
berghofe@13349
   190
  Nipkow. Takes 2 minutes (2002).
nipkow@13346
   191
berghofe@13349
   192
  This is the maximal amount of automation possible at the moment.
berghofe@13349
   193
*}
nipkow@13346
   194
berghofe@13349
   195
theorem newman':
berghofe@22270
   196
  assumes wf: "wfP (R\<inverse>\<inverse>)"
berghofe@22270
   197
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
berghofe@22270
   198
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@22270
   199
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
berghofe@22270
   200
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
wenzelm@18241
   201
  using wf
nipkow@13346
   202
proof induct
nipkow@13346
   203
  case (less x b c)
berghofe@22270
   204
  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
berghofe@22270
   205
                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
berghofe@22270
   206
  have xc: "R\<^sup>*\<^sup>* x c" .
berghofe@22270
   207
  have xb: "R\<^sup>*\<^sup>* x b" .
nipkow@13346
   208
  thus ?case
berghofe@22270
   209
  proof (rule converse_rtranclE')
nipkow@13346
   210
    assume "x = b"
berghofe@22270
   211
    with xc have "R\<^sup>*\<^sup>* b c" by simp
nipkow@17589
   212
    thus ?thesis by iprover
nipkow@13346
   213
  next
nipkow@13346
   214
    fix y
berghofe@22270
   215
    assume xy: "R x y"
berghofe@22270
   216
    assume yb: "R\<^sup>*\<^sup>* y b"
nipkow@13346
   217
    from xc show ?thesis
berghofe@22270
   218
    proof (rule converse_rtranclE')
nipkow@13346
   219
      assume "x = c"
berghofe@22270
   220
      with xb have "R\<^sup>*\<^sup>* c b" by simp
nipkow@17589
   221
      thus ?thesis by iprover
nipkow@13346
   222
    next
nipkow@13346
   223
      fix y'
berghofe@22270
   224
      assume y'c: "R\<^sup>*\<^sup>* y' c"
berghofe@22270
   225
      assume xy': "R x y'"
berghofe@22270
   226
      with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
wenzelm@18241
   227
        by (blast dest: lc)
nipkow@13346
   228
      from yb u y'c show ?thesis
berghofe@22270
   229
        by (blast del: rtrancl.rtrancl_refl
berghofe@22270
   230
            intro: rtrancl_trans'
berghofe@22270
   231
            dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
nipkow@13346
   232
    qed
nipkow@13346
   233
  qed
nipkow@13346
   234
qed
nipkow@13346
   235
nipkow@10179
   236
end