(* Title: HOL/Lambda/Commutation.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TU Muenchen
*)
header {* Abstract commutation and confluence notions *}
theory Commutation imports Main begin
subsection {* Basic definitions *}
definition
square :: "[('a \ 'a) set, ('a \ 'a) set, ('a \ 'a) set, ('a \ 'a) set] => bool"
"square R S T U =
(\x y. (x, y) \ R --> (\z. (x, z) \ S --> (\u. (y, u) \ T \ (z, u) \ U)))"
commute :: "[('a \ 'a) set, ('a \ 'a) set] => bool"
"commute R S = square R S S R"
diamond :: "('a \ 'a) set => bool"
"diamond R = commute R R"
Church_Rosser :: "('a \ 'a) set => bool"
"Church_Rosser R =
(\x y. (x, y) \ (R \ R^-1)^* --> (\z. (x, z) \ R^* \ (y, z) \ R^*))"
abbreviation (output)
confluent :: "('a \ 'a) set => bool"
"confluent R = diamond (R^*)"
subsection {* Basic lemmas *}
subsubsection {* square *}
lemma square_sym: "square R S T U ==> square S R U T"
apply (unfold square_def)
apply blast
done
lemma square_subset:
"[| square R S T U; T \ T' |] ==> square R S T' U"
apply (unfold square_def)
apply blast
done
lemma square_reflcl:
"[| square R S T (R^=); S \ T |] ==> square (R^=) S T (R^=)"
apply (unfold square_def)
apply blast
done
lemma square_rtrancl:
"square R S S T ==> square (R^*) S S (T^*)"
apply (unfold square_def)
apply (intro strip)
apply (erule rtrancl_induct)
apply blast
apply (blast intro: rtrancl_into_rtrancl)
done
lemma square_rtrancl_reflcl_commute:
"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)
done
subsubsection {* commute *}
lemma commute_sym: "commute R S ==> commute S R"
apply (unfold commute_def)
apply (blast intro: square_sym)
done
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 \ S) T"
apply (unfold commute_def square_def)
apply blast
done
subsubsection {* diamond, confluence, and union *}
lemma diamond_Un:
"[| diamond R; diamond S; commute R S |] ==> diamond (R \ S)"
apply (unfold diamond_def)
apply (assumption | rule commute_Un commute_sym)+
done
lemma diamond_confluent: "diamond R ==> confluent R"
apply (unfold diamond_def)
apply (erule commute_rtrancl)
done
lemma square_reflcl_confluent:
"square R R (R^=) (R^=) ==> confluent R"
apply (unfold diamond_def)
apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
elim: square_subset)
done
lemma confluent_Un:
"[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (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 \ R; R \ T^* |] ==> confluent T"
apply (force intro: diamond_confluent
dest: rtrancl_subset [symmetric])
done
subsection {* Church-Rosser *}
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
apply (unfold square_def commute_def diamond_def Church_Rosser_def)
apply (tactic {* safe_tac HOL_cs *})
apply (tactic {*
blast_tac (HOL_cs addIs
[Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
apply (erule rtrancl_induct)
apply blast
apply (blast del: rtrancl_refl intro: rtrancl_trans)
done
subsection {* Newman's lemma *}
text {* Proof by Stefan Berghofer *}
theorem newman:
assumes wf: "wf (R\)"
and lc: "\a b c. (a, b) \ R \ (a, c) \ R \
\d. (b, d) \ R\<^sup>* \ (c, d) \ R\<^sup>*"
shows "\b c. (a, b) \ R\<^sup>* \ (a, c) \ R\<^sup>* \
\d. (b, d) \ R\<^sup>* \ (c, d) \ R\<^sup>*"
using wf
proof induct
case (less x b c)
have xc: "(x, c) \ R\<^sup>*" .
have xb: "(x, b) \ R\<^sup>*" . thus ?case
proof (rule converse_rtranclE)
assume "x = b"
with xc have "(b, c) \ R\<^sup>*" by simp
thus ?thesis by iprover
next
fix y
assume xy: "(x, y) \ R"
assume yb: "(y, b) \ R\<^sup>*"
from xc show ?thesis
proof (rule converse_rtranclE)
assume "x = c"
with xb have "(c, b) \ R\<^sup>*" by simp
thus ?thesis by iprover
next
fix y'
assume y'c: "(y', c) \ R\<^sup>*"
assume xy': "(x, y') \ R"
with xy have "\u. (y, u) \ R\<^sup>* \ (y', u) \ R\<^sup>*" by (rule lc)
then obtain u where yu: "(y, u) \ R\<^sup>*" and y'u: "(y', u) \ R\<^sup>*" by iprover
from xy have "(y, x) \ R\" ..
from this and yb yu have "\d. (b, d) \ R\<^sup>* \ (u, d) \ R\<^sup>*" by (rule less)
then obtain v where bv: "(b, v) \ R\<^sup>*" and uv: "(u, v) \ R\<^sup>*" by iprover
from xy' have "(y', x) \ R\" ..
moreover from y'u and uv have "(y', v) \ R\<^sup>*" by (rule rtrancl_trans)
moreover note y'c
ultimately have "\d. (v, d) \ R\<^sup>* \ (c, d) \ R\<^sup>*" by (rule less)
then obtain w where vw: "(v, w) \ R\<^sup>*" and cw: "(c, w) \ R\<^sup>*" by iprover
from bv vw have "(b, w) \ R\<^sup>*" by (rule rtrancl_trans)
with cw show ?thesis by iprover
qed
qed
qed
text {*
\medskip Alternative version. Partly automated by Tobias
Nipkow. Takes 2 minutes (2002).
This is the maximal amount of automation possible at the moment.
*}
theorem newman':
assumes wf: "wf (R\)"
and lc: "\a b c. (a, b) \ R \ (a, c) \ R \
\d. (b, d) \ R\<^sup>* \ (c, d) \ R\<^sup>*"
shows "\b c. (a, b) \ R\<^sup>* \ (a, c) \ R\<^sup>* \
\d. (b, d) \ R\<^sup>* \ (c, d) \ R\<^sup>*"
using wf
proof induct
case (less x b c)
note IH = `\y b c. \(y,x) \ R\; (y,b) \ R\<^sup>*; (y,c) \ R\<^sup>*\
\ \d. (b,d) \ R\<^sup>* \ (c,d) \ R\<^sup>*`
have xc: "(x, c) \ R\<^sup>*" .
have xb: "(x, b) \ R\<^sup>*" .
thus ?case
proof (rule converse_rtranclE)
assume "x = b"
with xc have "(b, c) \ R\<^sup>*" by simp
thus ?thesis by iprover
next
fix y
assume xy: "(x, y) \ R"
assume yb: "(y, b) \ R\<^sup>*"
from xc show ?thesis
proof (rule converse_rtranclE)
assume "x = c"
with xb have "(c, b) \ R\<^sup>*" by simp
thus ?thesis by iprover
next
fix y'
assume y'c: "(y', c) \ R\<^sup>*"
assume xy': "(x, y') \ R"
with xy obtain u where u: "(y, u) \ R\<^sup>*" "(y', u) \ R\<^sup>*"
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]])
qed
qed
qed
end