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.136       blast_tac (HOL_cs addIs
   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