(* 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¯¯))⇧^{*}⇧^{*}x y ⟶ (∃z. R⇧^{*}⇧^{*}x z ∧ R⇧^{*}⇧^{*}y z))" abbreviation confluent :: "('a => 'a => bool) => bool" where "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 dest: predicate2D) done lemma square_reflcl: "[| square R S T (R⇧^{=}⇧^{=}); S ≤ T |] ==> square (R⇧^{=}⇧^{=}) S T (R⇧^{=}⇧^{=})" apply (unfold square_def) apply (blast dest: predicate2D) done lemma square_rtrancl: "square R S S T ==> square (R⇧^{*}⇧^{*}) S S (T⇧^{*}⇧^{*})" 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⇧^{*}⇧^{*}) (R⇧^{=}⇧^{=}) ==> commute (R⇧^{*}⇧^{*}) (S⇧^{*}⇧^{*})" 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⇧^{*}⇧^{*}) (S⇧^{*}⇧^{*})" 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⇧^{=}⇧^{=}) (R⇧^{=}⇧^{=}) ==> 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⇧^{*}⇧^{*}) (S⇧^{*}⇧^{*}) |] ==> 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⇧^{*}⇧^{*}|] ==> 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 @{context})›) apply (tactic ‹ blast_tac (put_claset HOL_cs @{context} 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⇧^{*}⇧^{*}a b ⟹ R⇧^{*}⇧^{*}a c ⟹ ∃d. R⇧^{*}⇧^{*}b d ∧ R⇧^{*}⇧^{*}c d" using wf proof induct case (less x b c) have xc: "R⇧^{*}⇧^{*}x c" by fact have xb: "R⇧^{*}⇧^{*}x b" by fact thus ?case proof (rule converse_rtranclpE) assume "x = b" with xc have "R⇧^{*}⇧^{*}b c" by simp thus ?thesis by iprover next fix y assume xy: "R x y" assume yb: "R⇧^{*}⇧^{*}y b" from xc show ?thesis proof (rule converse_rtranclpE) assume "x = c" with xb have "R⇧^{*}⇧^{*}c b" by simp thus ?thesis by iprover next fix y' assume y'c: "R⇧^{*}⇧^{*}y' c" assume xy': "R x y'" with xy have "∃u. R⇧^{*}⇧^{*}y u ∧ R⇧^{*}⇧^{*}y' u" by (rule lc) then obtain u where yu: "R⇧^{*}⇧^{*}y u" and y'u: "R⇧^{*}⇧^{*}y' u" by iprover from xy have "R¯¯ y x" .. from this and yb yu have "∃d. R⇧^{*}⇧^{*}b d ∧ R⇧^{*}⇧^{*}u d" by (rule less) then obtain v where bv: "R⇧^{*}⇧^{*}b v" and uv: "R⇧^{*}⇧^{*}u v" by iprover from xy' have "R¯¯ y' x" .. moreover from y'u and uv have "R⇧^{*}⇧^{*}y' v" by (rule rtranclp_trans) moreover note y'c ultimately have "∃d. R⇧^{*}⇧^{*}v d ∧ R⇧^{*}⇧^{*}c d" by (rule less) then obtain w where vw: "R⇧^{*}⇧^{*}v w" and cw: "R⇧^{*}⇧^{*}c w" by iprover from bv vw have "R⇧^{*}⇧^{*}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⇧^{*}⇧^{*}a b ⟹ R⇧^{*}⇧^{*}a c ⟹ ∃d. R⇧^{*}⇧^{*}b d ∧ R⇧^{*}⇧^{*}c d" using wf proof induct case (less x b c) note IH = ‹⋀y b c. ⟦R¯¯ y x; R⇧^{*}⇧^{*}y b; R⇧^{*}⇧^{*}y c⟧ ⟹ ∃d. R⇧^{*}⇧^{*}b d ∧ R⇧^{*}⇧^{*}c d› have xc: "R⇧^{*}⇧^{*}x c" by fact have xb: "R⇧^{*}⇧^{*}x b" by fact thus ?case proof (rule converse_rtranclpE) assume "x = b" with xc have "R⇧^{*}⇧^{*}b c" by simp thus ?thesis by iprover next fix y assume xy: "R x y" assume yb: "R⇧^{*}⇧^{*}y b" from xc show ?thesis proof (rule converse_rtranclpE) assume "x = c" with xb have "R⇧^{*}⇧^{*}c b" by simp thus ?thesis by iprover next fix y' assume y'c: "R⇧^{*}⇧^{*}y' c" assume xy': "R x y'" with xy obtain u where u: "R⇧^{*}⇧^{*}y u" "R⇧^{*}⇧^{*}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⇧^{*}⇧^{*}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⇧^{*}⇧^{*}a b ⟹ R⇧^{*}⇧^{*}a c ⟹ ∃d. R⇧^{*}⇧^{*}b d ∧ R⇧^{*}⇧^{*}c d" using wf proof induct case (less x b c) note IH = ‹⋀y b c. ⟦R¯¯ 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