(* Title: HOL/Lambda/Commutation.thy ID: $Id: Commutation.thy,v 1.16 2005/09/22 21:56:35 nipkow Exp $ Author: Tobias Nipkow Copyright 1995 TU Muenchen *) header {* Abstract commutation and confluence notions *} theory Commutation imports Main begin subsection {* Basic definitions *} constdefs 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^*)" syntax confluent :: "('a × 'a) set => bool" translations "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* ∧ (c, d) ∈ R*" shows "!!b c. (a, b) ∈ R* ==> (a, c) ∈ R* ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*" using wf proof induct case (less x b c) have xc: "(x, c) ∈ R*" . have xb: "(x, b) ∈ R*" . thus ?case proof (rule converse_rtranclE) assume "x = b" with xc have "(b, c) ∈ R*" by simp thus ?thesis by iprover next fix y assume xy: "(x, y) ∈ R" assume yb: "(y, b) ∈ R*" from xc show ?thesis proof (rule converse_rtranclE) assume "x = c" with xb have "(c, b) ∈ R*" by simp thus ?thesis by iprover next fix y' assume y'c: "(y', c) ∈ R*" assume xy': "(x, y') ∈ R" with xy have "∃u. (y, u) ∈ R* ∧ (y', u) ∈ R*" by (rule lc) then obtain u where yu: "(y, u) ∈ R*" and y'u: "(y', u) ∈ R*" by iprover from xy have "(y, x) ∈ R¯" .. from this and yb yu have "∃d. (b, d) ∈ R* ∧ (u, d) ∈ R*" by (rule less) then obtain v where bv: "(b, v) ∈ R*" and uv: "(u, v) ∈ R*" by iprover from xy' have "(y', x) ∈ R¯" .. moreover from y'u and uv have "(y', v) ∈ R*" by (rule rtrancl_trans) moreover note y'c ultimately have "∃d. (v, d) ∈ R* ∧ (c, d) ∈ R*" by (rule less) then obtain w where vw: "(v, w) ∈ R*" and cw: "(c, w) ∈ R*" by iprover from bv vw have "(b, w) ∈ R*" 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* ∧ (c, d) ∈ R*" shows "!!b c. (a, b) ∈ R* ==> (a, c) ∈ R* ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*" using wf proof induct case (less x b c) have IH: "!!y b c. [|(y,x) ∈ R¯; (y,b) ∈ R*; (y,c) ∈ R*|] ==> ∃d. (b,d) ∈ R* ∧ (c,d) ∈ R*" by(rule less) have xc: "(x, c) ∈ R*" . have xb: "(x, b) ∈ R*" . thus ?case proof (rule converse_rtranclE) assume "x = b" with xc have "(b, c) ∈ R*" by simp thus ?thesis by iprover next fix y assume xy: "(x, y) ∈ R" assume yb: "(y, b) ∈ R*" from xc show ?thesis proof (rule converse_rtranclE) assume "x = c" with xb have "(c, b) ∈ R*" by simp thus ?thesis by iprover next fix y' assume y'c: "(y', c) ∈ R*" assume xy': "(x, y') ∈ R" with xy obtain u where u: "(y, u) ∈ R*" "(y', u) ∈ R*" 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
lemma square_sym:
square R S T U ==> square S R U T
lemma square_subset:
[| square R S T U; T ⊆ T' |] ==> square R S T' U
lemma square_reflcl:
[| square R S T (R=); S ⊆ T |] ==> square (R=) S T (R=)
lemma square_rtrancl:
square R S S T ==> square (R*) S S (T*)
lemma square_rtrancl_reflcl_commute:
square R S (S*) (R=) ==> commute (R*) (S*)
lemma commute_sym:
commute R S ==> commute S R
lemma commute_rtrancl:
commute R S ==> commute (R*) (S*)
lemma commute_Un:
[| commute R T; commute S T |] ==> commute (R ∪ S) T
lemma diamond_Un:
[| diamond R; diamond S; commute R S |] ==> diamond (R ∪ S)
lemma diamond_confluent:
diamond R ==> confluent R
lemma square_reflcl_confluent:
square R R (R=) (R=) ==> confluent R
lemma confluent_Un:
[| confluent R; confluent S; commute (R*) (S*) |] ==> confluent (R ∪ S)
lemma diamond_to_confluence:
[| diamond R; T ⊆ R; R ⊆ T* |] ==> confluent T
lemma Church_Rosser_confluent:
Church_Rosser R = confluent R
theorem newman:
[| wf (R^-1); !!a b c. [| (a, b) ∈ R; (a, c) ∈ R |] ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*; (a, b) ∈ R*; (a, c) ∈ R* |] ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*
theorem newman':
[| wf (R^-1); !!a b c. [| (a, b) ∈ R; (a, c) ∈ R |] ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*; (a, b) ∈ R*; (a, c) ∈ R* |] ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*