--- a/src/HOL/Lambda/Commutation.thy Wed Feb 07 17:39:49 2007 +0100
+++ b/src/HOL/Lambda/Commutation.thy Wed Feb 07 17:41:11 2007 +0100
@@ -11,26 +11,26 @@
subsection {* Basic definitions *}
definition
- square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
+ square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
"square R S T U =
- (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
+ (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
definition
- commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
+ commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
"commute R S = square R S S R"
definition
- diamond :: "('a \<times> 'a) set => bool" where
+ diamond :: "('a => 'a => bool) => bool" where
"diamond R = commute R R"
definition
- Church_Rosser :: "('a \<times> 'a) set => bool" where
+ Church_Rosser :: "('a => 'a => bool) => bool" where
"Church_Rosser R =
- (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
+ (\<forall>x y. (join R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
abbreviation
- confluent :: "('a \<times> 'a) set => bool" where
- "confluent R == diamond (R^*)"
+ confluent :: "('a => 'a => bool) => bool" where
+ "confluent R == diamond (R^**)"
subsection {* Basic lemmas *}
@@ -43,31 +43,30 @@
done
lemma square_subset:
- "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
+ "[| square R S T U; T \<le> T' |] ==> square R S T' U"
apply (unfold square_def)
- apply blast
+ apply (blast dest: predicate2D)
done
lemma square_reflcl:
- "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
+ "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
apply (unfold square_def)
- apply blast
+ apply (blast dest: predicate2D)
done
lemma square_rtrancl:
- "square R S S T ==> square (R^*) S S (T^*)"
+ "square R S S T ==> square (R^**) S S (T^**)"
apply (unfold square_def)
apply (intro strip)
- apply (erule rtrancl_induct)
+ apply (erule rtrancl_induct')
apply blast
- apply (blast intro: rtrancl_into_rtrancl)
+ apply (blast intro: rtrancl.rtrancl_into_rtrancl)
done
lemma square_rtrancl_reflcl_commute:
- "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
+ "square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
apply (unfold commute_def)
- apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
- elim: r_into_rtrancl)
+ apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl])
done
@@ -78,13 +77,13 @@
apply (blast intro: square_sym)
done
-lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
+lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
apply (unfold commute_def)
apply (blast intro: square_rtrancl square_sym)
done
lemma commute_Un:
- "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
+ "[| commute R T; commute S T |] ==> commute (join R S) T"
apply (unfold commute_def square_def)
apply blast
done
@@ -93,7 +92,7 @@
subsubsection {* diamond, confluence, and union *}
lemma diamond_Un:
- "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
+ "[| diamond R; diamond S; commute R S |] ==> diamond (join R S)"
apply (unfold diamond_def)
apply (assumption | rule commute_Un commute_sym)+
done
@@ -104,22 +103,21 @@
done
lemma square_reflcl_confluent:
- "square R R (R^=) (R^=) ==> confluent R"
+ "square R R (R^==) (R^==) ==> confluent R"
apply (unfold diamond_def)
- apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
- elim: square_subset)
+ apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
done
lemma confluent_Un:
- "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
- apply (rule rtrancl_Un_rtrancl [THEN subst])
+ "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (join R S)"
+ apply (rule rtrancl_Un_rtrancl' [THEN subst])
apply (blast dest: diamond_Un intro: diamond_confluent)
done
lemma diamond_to_confluence:
- "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
+ "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
apply (force intro: diamond_confluent
- dest: rtrancl_subset [symmetric])
+ dest: rtrancl_subset' [symmetric])
done
@@ -130,12 +128,12 @@
apply (tactic {* safe_tac HOL_cs *})
apply (tactic {*
blast_tac (HOL_cs addIs
- [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
- thm "rtrancl_converseI", thm "converseI",
- thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
- apply (erule rtrancl_induct)
+ [thm "join_right_le" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
+ thm "rtrancl_converseI'", thm "conversepI",
+ thm "join_left_le" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
+ apply (erule rtrancl_induct')
apply blast
- apply (blast del: rtrancl_refl intro: rtrancl_trans)
+ apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
done
@@ -144,44 +142,44 @@
text {* Proof by Stefan Berghofer *}
theorem newman:
- assumes wf: "wf (R\<inverse>)"
- and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
- \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
- shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
- \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
+ assumes wf: "wfP (R\<inverse>\<inverse>)"
+ and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
+ \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
+ shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
+ \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
using wf
proof induct
case (less x b c)
- have xc: "(x, c) \<in> R\<^sup>*" .
- have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
- proof (rule converse_rtranclE)
+ have xc: "R\<^sup>*\<^sup>* x c" .
+ have xb: "R\<^sup>*\<^sup>* x b" . thus ?case
+ proof (rule converse_rtranclE')
assume "x = b"
- with xc have "(b, c) \<in> R\<^sup>*" by simp
+ with xc have "R\<^sup>*\<^sup>* b c" by simp
thus ?thesis by iprover
next
fix y
- assume xy: "(x, y) \<in> R"
- assume yb: "(y, b) \<in> R\<^sup>*"
+ assume xy: "R x y"
+ assume yb: "R\<^sup>*\<^sup>* y b"
from xc show ?thesis
- proof (rule converse_rtranclE)
+ proof (rule converse_rtranclE')
assume "x = c"
- with xb have "(c, b) \<in> R\<^sup>*" by simp
+ with xb have "R\<^sup>*\<^sup>* c b" by simp
thus ?thesis by iprover
next
fix y'
- assume y'c: "(y', c) \<in> R\<^sup>*"
- assume xy': "(x, y') \<in> R"
- with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
- then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
- from xy have "(y, x) \<in> R\<inverse>" ..
- from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
- then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
- from xy' have "(y', x) \<in> R\<inverse>" ..
- moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
+ assume y'c: "R\<^sup>*\<^sup>* y' c"
+ assume xy': "R x y'"
+ with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
+ then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
+ from xy have "R\<inverse>\<inverse> y x" ..
+ from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
+ then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
+ from xy' have "R\<inverse>\<inverse> y' x" ..
+ moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
moreover note y'c
- ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
- then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
- from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
+ ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
+ then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
+ from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
with cw show ?thesis by iprover
qed
qed
@@ -195,42 +193,42 @@
*}
theorem newman':
- assumes wf: "wf (R\<inverse>)"
- and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
- \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
- shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
- \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
+ assumes wf: "wfP (R\<inverse>\<inverse>)"
+ and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
+ \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
+ shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
+ \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
using wf
proof induct
case (less x b c)
- note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
- \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
- have xc: "(x, c) \<in> R\<^sup>*" .
- have xb: "(x, b) \<in> R\<^sup>*" .
+ note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
+ \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
+ have xc: "R\<^sup>*\<^sup>* x c" .
+ have xb: "R\<^sup>*\<^sup>* x b" .
thus ?case
- proof (rule converse_rtranclE)
+ proof (rule converse_rtranclE')
assume "x = b"
- with xc have "(b, c) \<in> R\<^sup>*" by simp
+ with xc have "R\<^sup>*\<^sup>* b c" by simp
thus ?thesis by iprover
next
fix y
- assume xy: "(x, y) \<in> R"
- assume yb: "(y, b) \<in> R\<^sup>*"
+ assume xy: "R x y"
+ assume yb: "R\<^sup>*\<^sup>* y b"
from xc show ?thesis
- proof (rule converse_rtranclE)
+ proof (rule converse_rtranclE')
assume "x = c"
- with xb have "(c, b) \<in> R\<^sup>*" by simp
+ with xb have "R\<^sup>*\<^sup>* c b" by simp
thus ?thesis by iprover
next
fix y'
- assume y'c: "(y', c) \<in> R\<^sup>*"
- assume xy': "(x, y') \<in> R"
- with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
+ assume y'c: "R\<^sup>*\<^sup>* y' c"
+ assume xy': "R x y'"
+ with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
by (blast dest: lc)
from yb u y'c show ?thesis
- by (blast del: rtrancl_refl
- intro: rtrancl_trans
- dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
+ by (blast del: rtrancl.rtrancl_refl
+ intro: rtrancl_trans'
+ dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
qed
qed
qed