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