src/HOL/Lambda/Commutation.thy
author nipkow
Thu Jul 11 09:17:01 2002 +0200 (2002-07-11)
changeset 13343 3b2b18c58d80
parent 13331 47e9950a502d
child 13346 6918b6d5192b
permissions -rw-r--r--
*** empty log message ***
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
wenzelm@9811
     9
theory Commutation = Main:
wenzelm@9811
    10
wenzelm@9811
    11
subsection {* Basic definitions *}
wenzelm@9811
    12
wenzelm@9811
    13
constdefs
wenzelm@9811
    14
  square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
wenzelm@9811
    15
  "square R S T U ==
wenzelm@9811
    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@9811
    18
  commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
wenzelm@9811
    19
  "commute R S == square R S S R"
wenzelm@9811
    20
wenzelm@9811
    21
  diamond :: "('a \<times> 'a) set => bool"
wenzelm@9811
    22
  "diamond R == commute R R"
wenzelm@9811
    23
wenzelm@9811
    24
  Church_Rosser :: "('a \<times> 'a) set => bool"
wenzelm@9811
    25
  "Church_Rosser R ==
wenzelm@9811
    26
    \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
wenzelm@9811
    27
wenzelm@9811
    28
syntax
wenzelm@9811
    29
  confluent :: "('a \<times> 'a) set => bool"
wenzelm@9811
    30
translations
wenzelm@9811
    31
  "confluent R" == "diamond (R^*)"
wenzelm@9811
    32
wenzelm@9811
    33
wenzelm@9811
    34
subsection {* Basic lemmas *}
wenzelm@9811
    35
wenzelm@9811
    36
subsubsection {* square *}
nipkow@1278
    37
wenzelm@9811
    38
lemma square_sym: "square R S T U ==> square S R U T"
wenzelm@9811
    39
  apply (unfold square_def)
wenzelm@9811
    40
  apply blast
wenzelm@9811
    41
  done
wenzelm@9811
    42
wenzelm@9811
    43
lemma square_subset:
wenzelm@9811
    44
    "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
wenzelm@9811
    45
  apply (unfold square_def)
wenzelm@9811
    46
  apply blast
wenzelm@9811
    47
  done
wenzelm@9811
    48
wenzelm@9811
    49
lemma square_reflcl:
wenzelm@9811
    50
    "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
wenzelm@9811
    51
  apply (unfold square_def)
wenzelm@9811
    52
  apply blast
wenzelm@9811
    53
  done
nipkow@1278
    54
wenzelm@9811
    55
lemma square_rtrancl:
wenzelm@9811
    56
    "square R S S T ==> square (R^*) S S (T^*)"
wenzelm@9811
    57
  apply (unfold square_def)
wenzelm@9811
    58
  apply (intro strip)
wenzelm@9811
    59
  apply (erule rtrancl_induct)
wenzelm@9811
    60
   apply blast
wenzelm@9811
    61
  apply (blast intro: rtrancl_into_rtrancl)
wenzelm@9811
    62
  done
wenzelm@9811
    63
wenzelm@9811
    64
lemma square_rtrancl_reflcl_commute:
wenzelm@9811
    65
    "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
wenzelm@9811
    66
  apply (unfold commute_def)
wenzelm@9811
    67
  apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
wenzelm@9811
    68
    elim: r_into_rtrancl)
wenzelm@9811
    69
  done
wenzelm@9811
    70
nipkow@1278
    71
wenzelm@9811
    72
subsubsection {* commute *}
wenzelm@9811
    73
wenzelm@9811
    74
lemma commute_sym: "commute R S ==> commute S R"
wenzelm@9811
    75
  apply (unfold commute_def)
wenzelm@9811
    76
  apply (blast intro: square_sym)
wenzelm@9811
    77
  done
wenzelm@9811
    78
wenzelm@9811
    79
lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
wenzelm@9811
    80
  apply (unfold commute_def)
wenzelm@9811
    81
  apply (blast intro: square_rtrancl square_sym)
wenzelm@9811
    82
  done
wenzelm@9811
    83
wenzelm@9811
    84
lemma commute_Un:
wenzelm@9811
    85
    "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
wenzelm@9811
    86
  apply (unfold commute_def square_def)
wenzelm@9811
    87
  apply blast
wenzelm@9811
    88
  done
wenzelm@9811
    89
wenzelm@9811
    90
wenzelm@9811
    91
subsubsection {* diamond, confluence, and union *}
wenzelm@9811
    92
wenzelm@9811
    93
lemma diamond_Un:
wenzelm@9811
    94
    "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
wenzelm@9811
    95
  apply (unfold diamond_def)
wenzelm@9811
    96
  apply (assumption | rule commute_Un commute_sym)+
wenzelm@9811
    97
  done
wenzelm@9811
    98
wenzelm@9811
    99
lemma diamond_confluent: "diamond R ==> confluent R"
wenzelm@9811
   100
  apply (unfold diamond_def)
wenzelm@9811
   101
  apply (erule commute_rtrancl)
wenzelm@9811
   102
  done
nipkow@1278
   103
wenzelm@9811
   104
lemma square_reflcl_confluent:
wenzelm@9811
   105
    "square R R (R^=) (R^=) ==> confluent R"
wenzelm@9811
   106
  apply (unfold diamond_def)
wenzelm@9811
   107
  apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
wenzelm@9811
   108
    elim: square_subset)
wenzelm@9811
   109
  done
wenzelm@9811
   110
wenzelm@9811
   111
lemma confluent_Un:
wenzelm@9811
   112
    "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
wenzelm@9811
   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:
wenzelm@9811
   118
    "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
wenzelm@9811
   119
  apply (force intro: diamond_confluent
wenzelm@9811
   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
wenzelm@9811
   131
       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
wenzelm@9811
   132
       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
wenzelm@9811
   133
  apply (erule rtrancl_induct)
wenzelm@9811
   134
   apply blast
nipkow@10212
   135
  apply (blast del: rtrancl_refl intro: rtrancl_trans)
wenzelm@9811
   136
  done
wenzelm@9811
   137
berghofe@13089
   138
berghofe@13089
   139
subsection {* Newman's lemma *}
berghofe@13089
   140
nipkow@13343
   141
theorem newman:
berghofe@13089
   142
  assumes wf: "wf (R\<inverse>)"
berghofe@13089
   143
  and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
berghofe@13089
   144
    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
nipkow@13343
   145
  shows "(a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
nipkow@13343
   146
    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" (is "PROP ?conf b c")
nipkow@13343
   147
proof -
nipkow@13343
   148
  from wf show "\<And>b c. PROP ?conf b c"
nipkow@13343
   149
  proof induct
nipkow@13343
   150
    case (less x b c)
nipkow@13343
   151
    have xc: "(x, c) \<in> R\<^sup>*" .
nipkow@13343
   152
    have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
berghofe@13089
   153
    proof (rule converse_rtranclE)
nipkow@13343
   154
      assume "x = b"
nipkow@13343
   155
      with xc have "(b, c) \<in> R\<^sup>*" by simp
berghofe@13089
   156
      thus ?thesis by rules
berghofe@13089
   157
    next
nipkow@13343
   158
      fix y
nipkow@13343
   159
      assume xy: "(x, y) \<in> R"
nipkow@13343
   160
      assume yb: "(y, b) \<in> R\<^sup>*"
nipkow@13343
   161
      from xc show ?thesis
nipkow@13343
   162
      proof (rule converse_rtranclE)
nipkow@13343
   163
	assume "x = c"
nipkow@13343
   164
	with xb have "(c, b) \<in> R\<^sup>*" by simp
nipkow@13343
   165
	thus ?thesis by rules
nipkow@13343
   166
      next
nipkow@13343
   167
	fix y'
nipkow@13343
   168
	assume y'c: "(y', c) \<in> R\<^sup>*"
nipkow@13343
   169
	assume xy': "(x, y') \<in> R"
nipkow@13343
   170
	with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
nipkow@13343
   171
        then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
nipkow@13343
   172
	from xy[symmetric] yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*"
nipkow@13343
   173
	  by (rule less)
nipkow@13343
   174
	then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
nipkow@13343
   175
	note xy'[symmetric]
nipkow@13343
   176
	moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
nipkow@13343
   177
	moreover note y'c
nipkow@13343
   178
	ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
nipkow@13343
   179
	then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
nipkow@13343
   180
	from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
nipkow@13343
   181
	with cw show ?thesis by rules
nipkow@13343
   182
      qed
berghofe@13089
   183
    qed
berghofe@13089
   184
  qed
berghofe@13089
   185
qed
berghofe@13089
   186
nipkow@10179
   187
end