(* Title: HOL/Proofs/Lambda/Commutation.thy
Author: Tobias Nipkow
Copyright 1995 TU Muenchen
*)
section ‹Abstract commutation
and confluence notions
›
theory Commutation
imports Main
begin
declare [[syntax_ambiguity_warning = false]]
subsection ‹Basic definitions
›
definition
square ::
"['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
"square R S T U =
(
∀x y. R x y --> (
∀z. S x z --> (
∃u. T y u
∧ U z u)))
"
definition
commute ::
"['a => 'a => bool, 'a => 'a => bool] => bool" where
"commute R S = square R S S R"
definition
diamond ::
"('a => 'a => bool) => bool" where
"diamond R = commute R R"
definition
Church_Rosser ::
"('a => 'a => bool) => bool" where
"Church_Rosser R =
(
∀x y. (sup R (R
-1-1))
🚫*
🚫* x y
⟶ (
∃z. R
🚫*
🚫* x z
∧ R
🚫*
🚫* y z))
"
abbreviation
confluent ::
"('a => 'a => bool) => bool" where
"confluent R == diamond (R\<^sup>*\<^sup>*)"
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 dest: predicate2D)
done
lemma square_reflcl:
"[| square R S T (R\<^sup>=\<^sup>=); S \ T |] ==> square (R\<^sup>=\<^sup>=) S T (R\<^sup>=\<^sup>=)"
apply (unfold square_def)
apply (blast dest: predicate2D)
done
lemma square_rtrancl:
"square R S S T ==> square (R\<^sup>*\<^sup>*) S S (T\<^sup>*\<^sup>*)"
apply (unfold square_def)
apply (intro strip)
apply (erule rtranclp_induct)
apply blast
apply (blast intro: rtranclp.rtrancl_into_rtrancl)
done
lemma square_rtrancl_reflcl_commute:
"square R S (S\<^sup>*\<^sup>*) (R\<^sup>=\<^sup>=) ==> commute (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*)"
apply (unfold commute_def)
apply (fastforce dest: square_reflcl square_sym [
THEN square_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\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*)"
apply (unfold commute_def)
apply (blast intro: square_rtrancl square_sym)
done
lemma commute_Un:
"[| commute R T; commute S T |] ==> commute (sup 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 (sup R S)"
apply (unfold diamond_def)
apply (blast intro: 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\<^sup>=\<^sup>=) (R\<^sup>=\<^sup>=) ==> confluent R"
apply (unfold diamond_def)
apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
done
lemma confluent_Un:
"[| confluent R; confluent S; commute (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*) |] ==> confluent (sup R S)"
apply (rule rtranclp_sup_rtranclp [
THEN subst])
apply (blast dest: diamond_Un intro: diamond_confluent)
done
lemma diamond_to_confluence:
"[| diamond R; T \ R; R \ T\<^sup>*\<^sup>* |] ==> confluent T"
apply (force intro: diamond_confluent
dest: rtranclp_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 (put_claset HOL_cs
🍋)
›)
apply (tactic
‹
blast_tac (put_claset HOL_cs
🍋 addIs
[@{
thm sup_ge2} RS @{
thm rtranclp_mono} RS @{
thm predicate2D} RS @{
thm rtranclp_trans},
@{
thm rtranclp_converseI}, @{
thm conversepI},
@{
thm sup_ge1} RS @{
thm rtranclp_mono} RS @{
thm predicate2D}]) 1
›)
apply (erule rtranclp_induct)
apply blast
apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
done
subsection ‹Newman
's lemma\
text ‹Proof by Stefan Berghofer
›
theorem newman:
assumes wf:
"wfP (R\\)"
and lc:
"\a b c. R a b \ R a c \
∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
"
shows "\b c. R\<^sup>*\<^sup>* a b \ R\<^sup>*\<^sup>* a c \
∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
"
using wf
proof induct
case (less x b c)
have xc:
"R\<^sup>*\<^sup>* x c" by fact
have xb:
"R\<^sup>*\<^sup>* x b" by fact
thus ?
case
proof (rule converse_rtranclpE)
assume "x = b"
with xc
have "R\<^sup>*\<^sup>* b c" by simp
thus ?thesis
by iprover
next
fix y
assume xy:
"R x y"
assume yb:
"R\<^sup>*\<^sup>* y b"
from xc
show ?thesis
proof (rule converse_rtranclpE)
assume "x = c"
with xb
have "R\<^sup>*\<^sup>* c b" by simp
thus ?thesis
by iprover
next
fix y
'
assume y
'c: "R\<^sup>*\<^sup>* y' c
"
assume xy
': "R x y'"
with xy
have "\u. R\<^sup>*\<^sup>* y u \ 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\\ y x" ..
from this
and yb yu
have "\d. R\<^sup>*\<^sup>* b d \ 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\\ y' x
" ..
moreover from y
'u and uv have "R\<^sup>*\<^sup>* y' v
" by (rule rtranclp_trans)
moreover note y
'c
ultimately have "\d. R\<^sup>*\<^sup>* v d \ 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 rtranclp_trans)
with cw
show ?thesis
by iprover
qed
qed
qed
text ‹
Alternative version. Partly automated
by Tobias
Nipkow. Takes 2 minutes (2002).
This
is the maximal amount of automation possible
using ‹blast
›.
›
theorem newman
':
assumes wf:
"wfP (R\\)"
and lc:
"\a b c. R a b \ R a c \
∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
"
shows "\b c. R\<^sup>*\<^sup>* a b \ R\<^sup>*\<^sup>* a c \
∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
"
using wf
proof induct
case (less x b c)
note IH =
‹∧y b c.
[R
-1-1 y x; R
🚫*
🚫* y b; R
🚫*
🚫* y c
]
==> ∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
›
have xc:
"R\<^sup>*\<^sup>* x c" by fact
have xb:
"R\<^sup>*\<^sup>* x b" by fact
thus ?
case
proof (rule converse_rtranclpE)
assume "x = b"
with xc
have "R\<^sup>*\<^sup>* b c" by simp
thus ?thesis
by iprover
next
fix y
assume xy:
"R x y"
assume yb:
"R\<^sup>*\<^sup>* y b"
from xc
show ?thesis
proof (rule converse_rtranclpE)
assume "x = c"
with xb
have "R\<^sup>*\<^sup>* c b" by simp
thus ?thesis
by iprover
next
fix y
'
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: rtranclp.rtrancl_refl
intro: rtranclp_trans
dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy
'])
qed
qed
qed
text ‹
Using the coherent logic prover, the
proof of the
induction step
is completely automatic.
›
lemma eq_imp_rtranclp:
"x = y \ r\<^sup>*\<^sup>* x y"
by simp
theorem newman
'':
assumes wf:
"wfP (R\\)"
and lc:
"\a b c. R a b \ R a c \
∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
"
shows "\b c. R\<^sup>*\<^sup>* a b \ R\<^sup>*\<^sup>* a c \
∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
"
using wf
proof induct
case (less x b c)
note IH =
‹∧y b c.
[R
-1-1 y x; R
🚫*
🚫* y b; R
🚫*
🚫* y c
]
==> ∃d. R
🚫*
🚫* b d
∧ R
🚫*
🚫* c d
›
show ?
case
by (coherent
‹R
🚫*
🚫* x c
› ‹R
🚫*
🚫* x b
›
refl [
where 'a='a] sym
eq_imp_rtranclp
r_into_rtranclp [of R]
rtranclp_trans
lc IH [OF conversepI]
converse_rtranclpE)
qed
end
