src/HOL/Proofs/Lambda/Commutation.thy
author wenzelm
Fri Feb 17 15:42:26 2012 +0100 (2012-02-17)
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 58372 bfd497f2f4c2
permissions -rw-r--r--
simplified configuration options for syntax ambiguity;
wenzelm@39157
     1
(*  Title:      HOL/Proofs/Lambda/Commutation.thy
clasohm@1476
     2
    Author:     Tobias Nipkow
nipkow@1278
     3
    Copyright   1995  TU Muenchen
nipkow@1278
     4
*)
nipkow@1278
     5
wenzelm@9811
     6
header {* Abstract commutation and confluence notions *}
wenzelm@9811
     7
haftmann@16417
     8
theory Commutation imports Main begin
wenzelm@9811
     9
wenzelm@46512
    10
declare [[syntax_ambiguity_warning = false]]
wenzelm@39126
    11
wenzelm@39126
    12
wenzelm@9811
    13
subsection {* Basic definitions *}
wenzelm@9811
    14
wenzelm@19086
    15
definition
berghofe@22270
    16
  square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
wenzelm@19086
    17
  "square R S T U =
berghofe@22270
    18
    (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
wenzelm@9811
    19
wenzelm@21404
    20
definition
berghofe@22270
    21
  commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
wenzelm@19086
    22
  "commute R S = square R S S R"
wenzelm@9811
    23
wenzelm@21404
    24
definition
berghofe@22270
    25
  diamond :: "('a => 'a => bool) => bool" where
wenzelm@19086
    26
  "diamond R = commute R R"
wenzelm@9811
    27
wenzelm@21404
    28
definition
berghofe@22270
    29
  Church_Rosser :: "('a => 'a => bool) => bool" where
wenzelm@19086
    30
  "Church_Rosser R =
haftmann@22422
    31
    (\<forall>x y. (sup R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
wenzelm@9811
    32
wenzelm@19363
    33
abbreviation
berghofe@22270
    34
  confluent :: "('a => 'a => bool) => bool" where
berghofe@22270
    35
  "confluent R == diamond (R^**)"
wenzelm@9811
    36
wenzelm@9811
    37
wenzelm@9811
    38
subsection {* Basic lemmas *}
wenzelm@9811
    39
wenzelm@25972
    40
subsubsection {* @{text "square"} *}
nipkow@1278
    41
wenzelm@9811
    42
lemma square_sym: "square R S T U ==> square S R U T"
wenzelm@9811
    43
  apply (unfold square_def)
wenzelm@9811
    44
  apply blast
wenzelm@9811
    45
  done
wenzelm@9811
    46
wenzelm@9811
    47
lemma square_subset:
berghofe@22270
    48
    "[| square R S T U; T \<le> T' |] ==> square R S T' U"
wenzelm@9811
    49
  apply (unfold square_def)
berghofe@22270
    50
  apply (blast dest: predicate2D)
wenzelm@9811
    51
  done
wenzelm@9811
    52
wenzelm@9811
    53
lemma square_reflcl:
berghofe@22270
    54
    "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
wenzelm@9811
    55
  apply (unfold square_def)
berghofe@22270
    56
  apply (blast dest: predicate2D)
wenzelm@9811
    57
  done
nipkow@1278
    58
wenzelm@9811
    59
lemma square_rtrancl:
berghofe@22270
    60
    "square R S S T ==> square (R^**) S S (T^**)"
wenzelm@9811
    61
  apply (unfold square_def)
wenzelm@9811
    62
  apply (intro strip)
berghofe@23750
    63
  apply (erule rtranclp_induct)
wenzelm@9811
    64
   apply blast
berghofe@23750
    65
  apply (blast intro: rtranclp.rtrancl_into_rtrancl)
wenzelm@9811
    66
  done
wenzelm@9811
    67
wenzelm@9811
    68
lemma square_rtrancl_reflcl_commute:
berghofe@22270
    69
    "square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
wenzelm@9811
    70
  apply (unfold commute_def)
nipkow@44890
    71
  apply (fastforce dest: square_reflcl square_sym [THEN square_rtrancl])
wenzelm@9811
    72
  done
wenzelm@9811
    73
nipkow@1278
    74
wenzelm@25972
    75
subsubsection {* @{text "commute"} *}
wenzelm@9811
    76
wenzelm@9811
    77
lemma commute_sym: "commute R S ==> commute S R"
wenzelm@9811
    78
  apply (unfold commute_def)
wenzelm@9811
    79
  apply (blast intro: square_sym)
wenzelm@9811
    80
  done
wenzelm@9811
    81
berghofe@22270
    82
lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
wenzelm@9811
    83
  apply (unfold commute_def)
wenzelm@9811
    84
  apply (blast intro: square_rtrancl square_sym)
wenzelm@9811
    85
  done
wenzelm@9811
    86
wenzelm@9811
    87
lemma commute_Un:
haftmann@22422
    88
    "[| commute R T; commute S T |] ==> commute (sup R S) T"
wenzelm@9811
    89
  apply (unfold commute_def square_def)
wenzelm@9811
    90
  apply blast
wenzelm@9811
    91
  done
wenzelm@9811
    92
wenzelm@9811
    93
wenzelm@25972
    94
subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *}
wenzelm@9811
    95
wenzelm@9811
    96
lemma diamond_Un:
haftmann@22422
    97
    "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
wenzelm@9811
    98
  apply (unfold diamond_def)
paulson@23815
    99
  apply (blast intro: commute_Un commute_sym) 
wenzelm@9811
   100
  done
wenzelm@9811
   101
wenzelm@9811
   102
lemma diamond_confluent: "diamond R ==> confluent R"
wenzelm@9811
   103
  apply (unfold diamond_def)
wenzelm@9811
   104
  apply (erule commute_rtrancl)
wenzelm@9811
   105
  done
nipkow@1278
   106
wenzelm@9811
   107
lemma square_reflcl_confluent:
berghofe@22270
   108
    "square R R (R^==) (R^==) ==> confluent R"
wenzelm@9811
   109
  apply (unfold diamond_def)
berghofe@22270
   110
  apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
wenzelm@9811
   111
  done
wenzelm@9811
   112
wenzelm@9811
   113
lemma confluent_Un:
haftmann@22422
   114
    "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
berghofe@23750
   115
  apply (rule rtranclp_sup_rtranclp [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:
berghofe@22270
   120
    "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
wenzelm@9811
   121
  apply (force intro: diamond_confluent
berghofe@23750
   122
    dest: rtranclp_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@42793
   130
  apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
wenzelm@9811
   131
   apply (tactic {*
wenzelm@42793
   132
     blast_tac (put_claset HOL_cs @{context} addIs
wenzelm@39159
   133
       [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
wenzelm@39159
   134
        @{thm rtranclp_converseI}, @{thm conversepI},
wenzelm@39159
   135
        @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
berghofe@23750
   136
  apply (erule rtranclp_induct)
wenzelm@9811
   137
   apply blast
berghofe@23750
   138
  apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_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@22270
   147
  assumes wf: "wfP (R\<inverse>\<inverse>)"
berghofe@22270
   148
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
berghofe@22270
   149
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@22270
   150
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
berghofe@22270
   151
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@13349
   152
  using wf
berghofe@13349
   153
proof induct
berghofe@13349
   154
  case (less x b c)
wenzelm@23464
   155
  have xc: "R\<^sup>*\<^sup>* x c" by fact
wenzelm@23464
   156
  have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
berghofe@23750
   157
  proof (rule converse_rtranclpE)
berghofe@13349
   158
    assume "x = b"
berghofe@22270
   159
    with xc have "R\<^sup>*\<^sup>* b c" by simp
nipkow@17589
   160
    thus ?thesis by iprover
berghofe@13349
   161
  next
berghofe@13349
   162
    fix y
berghofe@22270
   163
    assume xy: "R x y"
berghofe@22270
   164
    assume yb: "R\<^sup>*\<^sup>* y b"
berghofe@13349
   165
    from xc show ?thesis
berghofe@23750
   166
    proof (rule converse_rtranclpE)
berghofe@13349
   167
      assume "x = c"
berghofe@22270
   168
      with xb have "R\<^sup>*\<^sup>* c b" by simp
nipkow@17589
   169
      thus ?thesis by iprover
berghofe@13089
   170
    next
berghofe@13349
   171
      fix y'
berghofe@22270
   172
      assume y'c: "R\<^sup>*\<^sup>* y' c"
berghofe@22270
   173
      assume xy': "R x y'"
berghofe@22270
   174
      with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
berghofe@22270
   175
      then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
berghofe@22270
   176
      from xy have "R\<inverse>\<inverse> y x" ..
berghofe@22270
   177
      from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
berghofe@22270
   178
      then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
berghofe@22270
   179
      from xy' have "R\<inverse>\<inverse> y' x" ..
berghofe@23750
   180
      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans)
berghofe@13349
   181
      moreover note y'c
berghofe@22270
   182
      ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
berghofe@22270
   183
      then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
berghofe@23750
   184
      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_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@28455
   191
  Alternative version.  Partly automated by Tobias
berghofe@13349
   192
  Nipkow. Takes 2 minutes (2002).
nipkow@13346
   193
berghofe@28455
   194
  This is the maximal amount of automation possible using @{text blast}.
berghofe@13349
   195
*}
nipkow@13346
   196
berghofe@13349
   197
theorem newman':
berghofe@22270
   198
  assumes wf: "wfP (R\<inverse>\<inverse>)"
berghofe@22270
   199
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
berghofe@22270
   200
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@22270
   201
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
berghofe@22270
   202
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
wenzelm@18241
   203
  using wf
nipkow@13346
   204
proof induct
nipkow@13346
   205
  case (less x b c)
berghofe@22270
   206
  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
   207
                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
wenzelm@23464
   208
  have xc: "R\<^sup>*\<^sup>* x c" by fact
wenzelm@23464
   209
  have xb: "R\<^sup>*\<^sup>* x b" by fact
nipkow@13346
   210
  thus ?case
berghofe@23750
   211
  proof (rule converse_rtranclpE)
nipkow@13346
   212
    assume "x = b"
berghofe@22270
   213
    with xc have "R\<^sup>*\<^sup>* b c" by simp
nipkow@17589
   214
    thus ?thesis by iprover
nipkow@13346
   215
  next
nipkow@13346
   216
    fix y
berghofe@22270
   217
    assume xy: "R x y"
berghofe@22270
   218
    assume yb: "R\<^sup>*\<^sup>* y b"
nipkow@13346
   219
    from xc show ?thesis
berghofe@23750
   220
    proof (rule converse_rtranclpE)
nipkow@13346
   221
      assume "x = c"
berghofe@22270
   222
      with xb have "R\<^sup>*\<^sup>* c b" by simp
nipkow@17589
   223
      thus ?thesis by iprover
nipkow@13346
   224
    next
nipkow@13346
   225
      fix y'
berghofe@22270
   226
      assume y'c: "R\<^sup>*\<^sup>* y' c"
berghofe@22270
   227
      assume xy': "R x y'"
berghofe@22270
   228
      with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
wenzelm@18241
   229
        by (blast dest: lc)
nipkow@13346
   230
      from yb u y'c show ?thesis
berghofe@23750
   231
        by (blast del: rtranclp.rtrancl_refl
berghofe@23750
   232
            intro: rtranclp_trans
berghofe@22270
   233
            dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
nipkow@13346
   234
    qed
nipkow@13346
   235
  qed
nipkow@13346
   236
qed
nipkow@13346
   237
berghofe@28455
   238
text {*
berghofe@28455
   239
  Using the coherent logic prover, the proof of the induction step
berghofe@28455
   240
  is completely automatic.
berghofe@28455
   241
*}
berghofe@28455
   242
berghofe@28455
   243
lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
berghofe@28455
   244
  by simp
berghofe@28455
   245
berghofe@28455
   246
theorem newman'':
berghofe@28455
   247
  assumes wf: "wfP (R\<inverse>\<inverse>)"
berghofe@28455
   248
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
berghofe@28455
   249
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@28455
   250
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
berghofe@28455
   251
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
berghofe@28455
   252
  using wf
berghofe@28455
   253
proof induct
berghofe@28455
   254
  case (less x b c)
berghofe@28455
   255
  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
   256
                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
berghofe@28455
   257
  show ?case
berghofe@28455
   258
    by (coherent
berghofe@28455
   259
      `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
berghofe@28455
   260
      refl [where 'a='a] sym
berghofe@28455
   261
      eq_imp_rtranclp
berghofe@28455
   262
      r_into_rtranclp [of R]
berghofe@28455
   263
      rtranclp_trans
berghofe@28455
   264
      lc IH [OF conversepI]
berghofe@28455
   265
      converse_rtranclpE)
berghofe@28455
   266
qed
berghofe@28455
   267
nipkow@10179
   268
end