src/HOL/Lambda/Commutation.thy
 changeset 22270 4ccb7e6be929 parent 21669 c68717c16013 child 22422 ee19cdb07528
```     1.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Feb 07 17:39:49 2007 +0100
1.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Feb 07 17:41:11 2007 +0100
1.3 @@ -11,26 +11,26 @@
1.4  subsection {* Basic definitions *}
1.5
1.6  definition
1.7 -  square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
1.8 +  square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
1.9    "square R S T U =
1.10 -    (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
1.11 +    (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
1.12
1.13  definition
1.14 -  commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
1.15 +  commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
1.16    "commute R S = square R S S R"
1.17
1.18  definition
1.19 -  diamond :: "('a \<times> 'a) set => bool" where
1.20 +  diamond :: "('a => 'a => bool) => bool" where
1.21    "diamond R = commute R R"
1.22
1.23  definition
1.24 -  Church_Rosser :: "('a \<times> 'a) set => bool" where
1.25 +  Church_Rosser :: "('a => 'a => bool) => bool" where
1.26    "Church_Rosser R =
1.27 -    (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
1.28 +    (\<forall>x y. (join R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
1.29
1.30  abbreviation
1.31 -  confluent :: "('a \<times> 'a) set => bool" where
1.32 -  "confluent R == diamond (R^*)"
1.33 +  confluent :: "('a => 'a => bool) => bool" where
1.34 +  "confluent R == diamond (R^**)"
1.35
1.36
1.37  subsection {* Basic lemmas *}
1.38 @@ -43,31 +43,30 @@
1.39    done
1.40
1.41  lemma square_subset:
1.42 -    "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
1.43 +    "[| square R S T U; T \<le> T' |] ==> square R S T' U"
1.44    apply (unfold square_def)
1.45 -  apply blast
1.46 +  apply (blast dest: predicate2D)
1.47    done
1.48
1.49  lemma square_reflcl:
1.50 -    "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
1.51 +    "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
1.52    apply (unfold square_def)
1.53 -  apply blast
1.54 +  apply (blast dest: predicate2D)
1.55    done
1.56
1.57  lemma square_rtrancl:
1.58 -    "square R S S T ==> square (R^*) S S (T^*)"
1.59 +    "square R S S T ==> square (R^**) S S (T^**)"
1.60    apply (unfold square_def)
1.61    apply (intro strip)
1.62 -  apply (erule rtrancl_induct)
1.63 +  apply (erule rtrancl_induct')
1.64     apply blast
1.65 -  apply (blast intro: rtrancl_into_rtrancl)
1.66 +  apply (blast intro: rtrancl.rtrancl_into_rtrancl)
1.67    done
1.68
1.69  lemma square_rtrancl_reflcl_commute:
1.70 -    "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
1.71 +    "square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
1.72    apply (unfold commute_def)
1.73 -  apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
1.74 -    elim: r_into_rtrancl)
1.75 +  apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl])
1.76    done
1.77
1.78
1.79 @@ -78,13 +77,13 @@
1.80    apply (blast intro: square_sym)
1.81    done
1.82
1.83 -lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
1.84 +lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
1.85    apply (unfold commute_def)
1.86    apply (blast intro: square_rtrancl square_sym)
1.87    done
1.88
1.89  lemma commute_Un:
1.90 -    "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
1.91 +    "[| commute R T; commute S T |] ==> commute (join R S) T"
1.92    apply (unfold commute_def square_def)
1.93    apply blast
1.94    done
1.95 @@ -93,7 +92,7 @@
1.96  subsubsection {* diamond, confluence, and union *}
1.97
1.98  lemma diamond_Un:
1.99 -    "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
1.100 +    "[| diamond R; diamond S; commute R S |] ==> diamond (join R S)"
1.101    apply (unfold diamond_def)
1.102    apply (assumption | rule commute_Un commute_sym)+
1.103    done
1.104 @@ -104,22 +103,21 @@
1.105    done
1.106
1.107  lemma square_reflcl_confluent:
1.108 -    "square R R (R^=) (R^=) ==> confluent R"
1.109 +    "square R R (R^==) (R^==) ==> confluent R"
1.110    apply (unfold diamond_def)
1.111 -  apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
1.112 -    elim: square_subset)
1.113 +  apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
1.114    done
1.115
1.116  lemma confluent_Un:
1.117 -    "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
1.118 -  apply (rule rtrancl_Un_rtrancl [THEN subst])
1.119 +    "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (join R S)"
1.120 +  apply (rule rtrancl_Un_rtrancl' [THEN subst])
1.121    apply (blast dest: diamond_Un intro: diamond_confluent)
1.122    done
1.123
1.124  lemma diamond_to_confluence:
1.125 -    "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
1.126 +    "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
1.127    apply (force intro: diamond_confluent
1.128 -    dest: rtrancl_subset [symmetric])
1.129 +    dest: rtrancl_subset' [symmetric])
1.130    done
1.131
1.132
1.133 @@ -130,12 +128,12 @@
1.134    apply (tactic {* safe_tac HOL_cs *})
1.135     apply (tactic {*
1.137 -       [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
1.138 -        thm "rtrancl_converseI", thm "converseI",
1.139 -        thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
1.140 -  apply (erule rtrancl_induct)
1.141 +       [thm "join_right_le" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
1.142 +        thm "rtrancl_converseI'", thm "conversepI",
1.143 +        thm "join_left_le" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
1.144 +  apply (erule rtrancl_induct')
1.145     apply blast
1.146 -  apply (blast del: rtrancl_refl intro: rtrancl_trans)
1.147 +  apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
1.148    done
1.149
1.150
1.151 @@ -144,44 +142,44 @@
1.152  text {* Proof by Stefan Berghofer *}
1.153
1.154  theorem newman:
1.155 -  assumes wf: "wf (R\<inverse>)"
1.156 -  and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
1.157 -    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.158 -  shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
1.159 -    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.160 +  assumes wf: "wfP (R\<inverse>\<inverse>)"
1.161 +  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
1.162 +    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
1.163 +  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
1.164 +    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
1.165    using wf
1.166  proof induct
1.167    case (less x b c)
1.168 -  have xc: "(x, c) \<in> R\<^sup>*" .
1.169 -  have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
1.170 -  proof (rule converse_rtranclE)
1.171 +  have xc: "R\<^sup>*\<^sup>* x c" .
1.172 +  have xb: "R\<^sup>*\<^sup>* x b" . thus ?case
1.173 +  proof (rule converse_rtranclE')
1.174      assume "x = b"
1.175 -    with xc have "(b, c) \<in> R\<^sup>*" by simp
1.176 +    with xc have "R\<^sup>*\<^sup>* b c" by simp
1.177      thus ?thesis by iprover
1.178    next
1.179      fix y
1.180 -    assume xy: "(x, y) \<in> R"
1.181 -    assume yb: "(y, b) \<in> R\<^sup>*"
1.182 +    assume xy: "R x y"
1.183 +    assume yb: "R\<^sup>*\<^sup>* y b"
1.184      from xc show ?thesis
1.185 -    proof (rule converse_rtranclE)
1.186 +    proof (rule converse_rtranclE')
1.187        assume "x = c"
1.188 -      with xb have "(c, b) \<in> R\<^sup>*" by simp
1.189 +      with xb have "R\<^sup>*\<^sup>* c b" by simp
1.190        thus ?thesis by iprover
1.191      next
1.192        fix y'
1.193 -      assume y'c: "(y', c) \<in> R\<^sup>*"
1.194 -      assume xy': "(x, y') \<in> R"
1.195 -      with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
1.196 -      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
1.197 -      from xy have "(y, x) \<in> R\<inverse>" ..
1.198 -      from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
1.199 -      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
1.200 -      from xy' have "(y', x) \<in> R\<inverse>" ..
1.201 -      moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
1.202 +      assume y'c: "R\<^sup>*\<^sup>* y' c"
1.203 +      assume xy': "R x y'"
1.204 +      with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
1.205 +      then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
1.206 +      from xy have "R\<inverse>\<inverse> y x" ..
1.207 +      from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
1.208 +      then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
1.209 +      from xy' have "R\<inverse>\<inverse> y' x" ..
1.210 +      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
1.211        moreover note y'c
1.212 -      ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
1.213 -      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
1.214 -      from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
1.215 +      ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
1.216 +      then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
1.217 +      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
1.218        with cw show ?thesis by iprover
1.219      qed
1.220    qed
1.221 @@ -195,42 +193,42 @@
1.222  *}
1.223
1.224  theorem newman':
1.225 -  assumes wf: "wf (R\<inverse>)"
1.226 -  and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
1.227 -    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.228 -  shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
1.229 -    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.230 +  assumes wf: "wfP (R\<inverse>\<inverse>)"
1.231 +  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
1.232 +    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
1.233 +  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
1.234 +    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
1.235    using wf
1.236  proof induct
1.237    case (less x b c)
1.238 -  note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
1.239 -                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
1.240 -  have xc: "(x, c) \<in> R\<^sup>*" .
1.241 -  have xb: "(x, b) \<in> R\<^sup>*" .
1.242 +  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
1.243 +                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
1.244 +  have xc: "R\<^sup>*\<^sup>* x c" .
1.245 +  have xb: "R\<^sup>*\<^sup>* x b" .
1.246    thus ?case
1.247 -  proof (rule converse_rtranclE)
1.248 +  proof (rule converse_rtranclE')
1.249      assume "x = b"
1.250 -    with xc have "(b, c) \<in> R\<^sup>*" by simp
1.251 +    with xc have "R\<^sup>*\<^sup>* b c" by simp
1.252      thus ?thesis by iprover
1.253    next
1.254      fix y
1.255 -    assume xy: "(x, y) \<in> R"
1.256 -    assume yb: "(y, b) \<in> R\<^sup>*"
1.257 +    assume xy: "R x y"
1.258 +    assume yb: "R\<^sup>*\<^sup>* y b"
1.259      from xc show ?thesis
1.260 -    proof (rule converse_rtranclE)
1.261 +    proof (rule converse_rtranclE')
1.262        assume "x = c"
1.263 -      with xb have "(c, b) \<in> R\<^sup>*" by simp
1.264 +      with xb have "R\<^sup>*\<^sup>* c b" by simp
1.265        thus ?thesis by iprover
1.266      next
1.267        fix y'
1.268 -      assume y'c: "(y', c) \<in> R\<^sup>*"
1.269 -      assume xy': "(x, y') \<in> R"
1.270 -      with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
1.271 +      assume y'c: "R\<^sup>*\<^sup>* y' c"
1.272 +      assume xy': "R x y'"
1.273 +      with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
1.274          by (blast dest: lc)
1.275        from yb u y'c show ?thesis
1.276 -        by (blast del: rtrancl_refl
1.277 -            intro: rtrancl_trans
1.278 -            dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
1.279 +        by (blast del: rtrancl.rtrancl_refl
1.280 +            intro: rtrancl_trans'
1.281 +            dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
1.282      qed
1.283    qed
1.284  qed
```