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