src/HOL/Lambda/Commutation.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28455 a79701b14a30
child 36862 952b2b102a0a
permissions -rw-r--r--
added lemmas
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@25972
    38
subsubsection {* @{text "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@23750
    61
  apply (erule rtranclp_induct)
wenzelm@9811
    62
   apply blast
berghofe@23750
    63
  apply (blast intro: rtranclp.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@25972
    73
subsubsection {* @{text "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@25972
    92
subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "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)
paulson@23815
    97
  apply (blast intro: 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@23750
   113
  apply (rule rtranclp_sup_rtranclp [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@23750
   120
    dest: rtranclp_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
berghofe@23750
   131
       [thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans",
berghofe@23750
   132
        thm "rtranclp_converseI", thm "conversepI",
berghofe@23750
   133
        thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *})
berghofe@23750
   134
  apply (erule rtranclp_induct)
wenzelm@9811
   135
   apply blast
berghofe@23750
   136
  apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_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)
wenzelm@23464
   153
  have xc: "R\<^sup>*\<^sup>* x c" by fact
wenzelm@23464
   154
  have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
berghofe@23750
   155
  proof (rule converse_rtranclpE)
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@23750
   164
    proof (rule converse_rtranclpE)
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@23750
   178
      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_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@23750
   182
      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_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@28455
   189
  Alternative version.  Partly automated by Tobias
berghofe@13349
   190
  Nipkow. Takes 2 minutes (2002).
nipkow@13346
   191
berghofe@28455
   192
  This is the maximal amount of automation possible using @{text blast}.
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`
wenzelm@23464
   206
  have xc: "R\<^sup>*\<^sup>* x c" by fact
wenzelm@23464
   207
  have xb: "R\<^sup>*\<^sup>* x b" by fact
nipkow@13346
   208
  thus ?case
berghofe@23750
   209
  proof (rule converse_rtranclpE)
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@23750
   218
    proof (rule converse_rtranclpE)
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@23750
   229
        by (blast del: rtranclp.rtrancl_refl
berghofe@23750
   230
            intro: rtranclp_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
berghofe@28455
   236
text {*
berghofe@28455
   237
  Using the coherent logic prover, the proof of the induction step
berghofe@28455
   238
  is completely automatic.
berghofe@28455
   239
*}
berghofe@28455
   240
berghofe@28455
   241
lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
berghofe@28455
   242
  by simp
berghofe@28455
   243
berghofe@28455
   244
theorem newman'':
berghofe@28455
   245
  assumes wf: "wfP (R\<inverse>\<inverse>)"
berghofe@28455
   246
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
berghofe@28455
   247
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@28455
   248
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
berghofe@28455
   249
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@28455
   250
  using wf
berghofe@28455
   251
proof induct
berghofe@28455
   252
  case (less x b c)
berghofe@28455
   253
  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
berghofe@28455
   254
                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
berghofe@28455
   255
  show ?case
berghofe@28455
   256
    by (coherent
berghofe@28455
   257
      `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
berghofe@28455
   258
      refl [where 'a='a] sym
berghofe@28455
   259
      eq_imp_rtranclp
berghofe@28455
   260
      r_into_rtranclp [of R]
berghofe@28455
   261
      rtranclp_trans
berghofe@28455
   262
      lc IH [OF conversepI]
berghofe@28455
   263
      converse_rtranclpE)
berghofe@28455
   264
qed
berghofe@28455
   265
nipkow@10179
   266
end