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