Theory Parallel_Rewriting
subsection ‹The Parallel Rewrite Relation›
theory Parallel_Rewriting
imports
Trs
Multihole_Context
begin
text ‹The parallel rewrite relation as inductive definition›
inductive_set par_rstep :: "('f,'v)trs ⇒ ('f,'v)trs" for R :: "('f,'v)trs"
where root_step[intro]: "(s,t) ∈ R ⟹ (s ⋅ σ,t ⋅ σ) ∈ par_rstep R"
| par_step_fun[intro]: "⟦⋀ i. i < length ts ⟹ (ss ! i,ts ! i) ∈ par_rstep R⟧ ⟹ length ss = length ts
⟹ (Fun f ss, Fun f ts) ∈ par_rstep R"
| par_step_var[intro]: "(Var x, Var x) ∈ par_rstep R"
lemma par_rstep_refl[intro]: "(t,t) ∈ par_rstep R"
by (induct t, auto)
lemma all_ctxt_closed_par_rstep[intro]: "all_ctxt_closed F (par_rstep R)"
unfolding all_ctxt_closed_def
by auto
lemma args_par_rstep_pow_imp_par_rstep_pow:
"length xs = length ys ⟹ ∀i<length xs. (xs ! i, ys ! i) ∈ par_rstep R ^^ n ⟹
(Fun f xs, Fun f ys) ∈ par_rstep R ^^ n"
proof(induct n arbitrary:ys)
case 0
then have "∀i<length xs. (xs ! i = ys ! i)" by simp
with 0 show ?case using relpow_0_I list_eq_iff_nth_eq by metis
next
case (Suc n)
let ?c = "λ z i. (xs ! i, z) ∈ par_rstep R ^^ n ∧ (z, ys ! i) ∈ par_rstep R"
{ fix i assume "i < length xs"
from relpow_Suc_E[OF Suc(3)[rule_format, OF this]]
have "∃ z. (?c z i)" by metis
}
with choice have "∃ zf. ∀ i < length xs. (?c (zf i) i)" by meson
then obtain zf where a:"∀ i < length xs. (?c (zf i) i)" by auto
let ?zs = "map zf [0..<length xs]"
have len:"length xs = length ?zs" by simp
from a map_nth have "∀i<length xs. (xs ! i, ?zs ! i) ∈ par_rstep R ^^ n" by auto
from Suc(1)[OF len this] have n:"(Fun f xs, Fun f ?zs) ∈ par_rstep R ^^ n" by auto
from a map_nth have "∀i<length xs. (?zs ! i, ys ! i) ∈ par_rstep R" by auto
with par_step_fun len Suc(2) have "(Fun f ?zs, Fun f ys) ∈ par_rstep R" by auto
with n show ?case by auto
qed
lemma ctxt_closed_par_rstep[intro]: "ctxt.closed (par_rstep R)"
proof (rule one_imp_ctxt_closed)
fix f bef s t aft
assume st: "(s,t) ∈ par_rstep R"
let ?ss = "bef @ s # aft"
let ?ts = "bef @ t # aft"
show "(Fun f ?ss, Fun f ?ts) ∈ par_rstep R"
proof (rule par_step_fun)
fix i
assume "i < length ?ts"
show "(?ss ! i, ?ts ! i) ∈ par_rstep R"
using par_rstep_refl[of "?ts ! i" R] st by (cases "i = length bef", auto simp: nth_append)
qed simp
qed
lemma subst_closed_par_rstep: "(s,t) ∈ par_rstep R ⟹ (s ⋅ σ, t ⋅ σ) ∈ par_rstep R"
proof (induct rule: par_rstep.induct)
case (root_step s t τ)
show ?case
using par_rstep.root_step[OF root_step, of "τ ∘⇩s σ"] by auto
next
case (par_step_var x)
show ?case by auto
next
case (par_step_fun ss ts f)
show ?case unfolding eval_term.simps
by (rule par_rstep.par_step_fun, insert par_step_fun(2-3), auto)
qed
lemma R_par_rstep: "R ⊆ par_rstep R"
using root_step[of _ _ R Var] by auto
lemma par_rstep_rsteps: "par_rstep R ⊆ (rstep R)⇧*"
proof
fix s t
assume "(s,t) ∈ par_rstep R"
then show "(s,t) ∈ (rstep R)⇧*"
proof (induct rule: par_rstep.induct)
case (root_step s t sigma)
then show ?case by auto
next
case (par_step_var x)
then show ?case by auto
next
case (par_step_fun ts ss f)
from all_ctxt_closedD[of UNIV, OF all_ctxt_closed_rsteps _ par_step_fun(3) par_step_fun(2)]
show ?case unfolding par_step_fun(3) by simp
qed
qed
lemma rstep_par_rstep: "rstep R ⊆ par_rstep R"
by (rule rstep_subset[OF ctxt_closed_par_rstep subst.closedI R_par_rstep],
insert subst_closed_par_rstep, auto)
lemma par_rsteps_rsteps: "(par_rstep R)⇧* = (rstep R)⇧*" (is "?P = ?R")
proof
from rtrancl_mono[OF par_rstep_rsteps[of R]] show "?P ⊆ ?R" by simp
from rtrancl_mono[OF rstep_par_rstep] show "?R ⊆ ?P" .
qed
lemma par_rsteps_union: "(par_rstep A ∪ par_rstep B)⇧* =
(rstep (A ∪ B))⇧*"
proof
show "(par_rstep A ∪ par_rstep B)⇧* ⊆ (rstep (A ∪ B))⇧*"
by (metis par_rsteps_rsteps rstep_union rtrancl_Un_rtrancl set_eq_subset)
show "(rstep (A ∪ B))⇧* ⊆ (par_rstep A ∪ par_rstep B)⇧*" unfolding rstep_union
by (meson rstep_par_rstep rtrancl_mono sup_mono)
qed
lemma par_rstep_inverse: "par_rstep (R^-1) = (par_rstep R)^-1"
proof -
{
fix s t :: "('a,'b)term" and R
assume "(s,t) ∈ par_rstep (R^-1)"
hence "(t,s) ∈ par_rstep R"
by (induct s t, auto)
}
from this[of _ _ R] this[of _ _ "R^-1"]
show ?thesis by auto
qed
lemma par_rstep_conversion: "(rstep R)⇧↔⇧* = (par_rstep R)⇧↔⇧*"
unfolding conversion_def
by (metis par_rsteps_rsteps rtrancl_Un_rtrancl rtrancl_converse)
lemma par_rstep_mono: assumes "R ⊆ S"
shows "par_rstep R ⊆ par_rstep S"
proof
fix s t
show "(s, t) ∈ par_rstep R ⟹ (s, t) ∈ par_rstep S"
by (induct s t rule: par_rstep.induct, insert assms, auto)
qed
lemma wf_trs_par_rstep: assumes wf: "⋀ l r. (l,r) ∈ R ⟹ is_Fun l"
and step: "(Var x, t) ∈ par_rstep R"
shows "t = Var x"
using step
proof (cases rule: par_rstep.cases)
case (root_step l r σ)
from root_step(1) wf[OF root_step(3)] show ?thesis by (cases l, auto)
qed auto
text ‹main lemma which tells us, that either a parallel rewrite step of ‹l ⋅ σ› is inside ‹l›, or
we can do the step completely inside ‹σ››
lemma par_rstep_linear_subst: assumes lin: "linear_term l"
and step: "(l ⋅ σ, t) ∈ par_rstep R"
shows "(∃ τ. t = l ⋅ τ ∧ (∀ x ∈ vars_term l. (σ x, τ x) ∈ par_rstep R) ∨
(∃ C l'' l' r'. l = C⟨l''⟩ ∧ is_Fun l'' ∧ (l',r') ∈ R ∧ (l'' ⋅ σ = l' ⋅ τ) ∧ ((C ⋅⇩c σ) ⟨ r' ⋅ τ ⟩, t) ∈ par_rstep R))"
using lin step
proof (induction l arbitrary: t)
case (Var x t)
let ?tau = "λ y. t"
show ?case
by (rule exI[of _ ?tau], rule disjI1, insert Var(2), auto)
next
case (Fun f ss)
let ?ss = "map (λ s. s ⋅ σ) ss"
let ?R = "par_rstep R"
from Fun(3)
show ?case
proof (cases rule: par_rstep.cases)
case (root_step l r τ)
show ?thesis
proof (rule exI, rule disjI2, intro exI conjI)
show "(l,r) ∈ R" by (rule root_step(3))
show "Fun f ss = □⟨Fun f ss⟩" by simp
show "(Fun f ss) ⋅ σ = l ⋅ τ" by (rule root_step(1))
show "((□ ⋅⇩c σ)⟨ r ⋅ τ ⟩, t) ∈ ?R" unfolding root_step(2) using par_rstep_refl by simp
qed simp
next
case (par_step_var x)
then show ?thesis by simp
next
case (par_step_fun ts ss1 g)
then have id: "ss1 = ?ss" "g = f" and len: "length ts = length ss" by auto
let ?p1 = "λ τ i. ts ! i = ss ! i ⋅ τ ∧ (∀ x ∈ vars_term (ss ! i). (σ x, τ x) ∈ ?R)"
let ?p2 = "λ τ i. (∃ C l'' l' r'. ss ! i = C⟨ l''⟩ ∧ is_Fun l'' ∧ (l',r') ∈ R ∧ l'' ⋅ σ = l' ⋅ τ ∧ ((C ⋅⇩c σ)⟨ r' ⋅ τ ⟩, (ts ! i)) ∈ ?R)"
let ?p = "λ τ i. ?p1 τ i ∨ ?p2 τ i"
{
fix i
assume i: "i < length ss"
with par_step_fun(4) id have i2: "i < length ts" by auto
from par_step_fun(3)[OF i2] have step: "(ss ! i ⋅ σ, ts ! i) ∈ par_rstep R" unfolding id nth_map[OF i] .
from i have mem: "ss ! i ∈ set ss" by auto
from Fun.prems(1) mem have "linear_term (ss ! i)" by auto
from Fun.IH[OF mem this step] have "∃ τ. ?p τ i" .
}
then have "∀ i. ∃ tau. i < length ss ⟶ ?p tau i" by blast
from choice[OF this] obtain taus where taus: "⋀ i. i < length ss ⟹ ?p (taus i) i" by blast
show ?thesis
proof (cases "∃ i. i < length ss ∧ ?p2 (taus i) i")
case True
then obtain i where i: "i < length ss" and p2: "?p2 (taus i) i" by blast+
from par_step_fun(2)[unfolded id] have t: "t = Fun f ts" .
from i have i': "i < length ts" unfolding len .
from p2 obtain C l'' l' r' where ssi: "ss ! i = C ⟨l''⟩" and "is_Fun l''" "(l',r') ∈ R" "l'' ⋅ σ = l' ⋅ taus i"
and tsi: "((C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩, ts ! i) ∈ ?R" by blast
from id_take_nth_drop[OF i, unfolded ssi] obtain bef aft where ss: "ss = bef @ C ⟨ l'' ⟩ # aft"
and bef: "bef = take i ss"
and aft: "aft = drop (Suc i) ss" by blast
let ?C = "More f bef C aft"
let ?r = "(C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩"
let ?sig = "map (λ s. s ⋅ σ)"
let ?bra = "?sig bef @ ?r # ?sig aft"
have C: "(?C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩ = Fun f ?bra" by simp
show ?thesis unfolding ss
proof (rule exI[of _ "taus i"], rule disjI2, rule exI[of _ ?C], intro exI conjI)
show "is_Fun l''" by fact
show "(l',r') ∈ R" by fact
show "l'' ⋅ σ = l' ⋅ taus i" by fact
show "((?C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩, t) ∈ ?R" unfolding C t
proof (rule par_rstep.par_step_fun)
show "length ?bra = length ts"
unfolding len unfolding ss by simp
next
fix j
assume j: "j < length ts"
show "(?bra ! j, ts ! j) ∈ ?R"
proof (cases "j = i")
case True
then have "?bra ! j = ?r" using bef i by (simp add: nth_append)
then show ?thesis using tsi True by simp
next
case False
from bef i have "min (length ss) i = i" by simp
then have "?bra ! j = (?sig bef @ (C ⟨ l'' ⟩ ⋅ σ) # ?sig aft) ! j" using False bef i by (simp add: nth_append)
also have "... = ?sig ss ! j" unfolding ss by simp
also have "... = ss1 ! j" unfolding id ..
finally show ?thesis
using par_step_fun(3)[OF j] by auto
qed
qed
qed simp
next
case False
with taus have taus: "⋀ i. i < length ss ⟹ ?p1 (taus i) i" by blast
from Fun(2) have "is_partition (map vars_term ss)" by simp
from subst_merge[OF this, of taus] obtain τ where tau: "⋀ i x. i < length ss ⟹ x ∈ vars_term (ss ! i) ⟹ τ x = taus i x" by auto
let ?tau = τ
{
fix i
assume i: "i < length ss"
then have mem: "ss ! i ∈ set ss" by auto
from taus[OF i] have p1: "?p1 (taus i) i" .
have id: "ss ! i ⋅ (taus i) = ss ! i ⋅ τ"
by (rule term_subst_eq, rule tau[OF i, symmetric])
have "?p1 ?tau i"
proof (rule conjI[OF _ ballI])
fix x
assume x: "x ∈ vars_term (ss ! i)"
with p1 have step: "(σ x, taus i x) ∈ par_rstep R" by auto
with tau[OF i x]
show "(σ x, ?tau x) ∈ par_rstep R" by simp
qed (insert p1[unfolded id], auto)
} note p1 = this
have p1: "⋀ i. i < length ss ⟹ ?p1 τ i" by (rule p1)
let ?ss = "map (λ s. s ⋅ τ) ss"
show ?thesis unfolding par_step_fun(2) id
proof (rule exI[of _ τ], rule disjI1, rule conjI[OF _ ballI])
have "ts = map (λ i. ts ! i) [0 ..< (length ts)]" by (rule map_nth[symmetric])
also have "... = map (λ i. ?ss ! i) [0 ..< length ?ss]" unfolding len using p1 by auto
also have "... = ?ss" by (rule map_nth)
finally have ts: "ts = ?ss" .
show "Fun f ts = Fun f ss ⋅ τ" unfolding ts by auto
next
fix x
assume "x ∈ vars_term (Fun f ss)"
then obtain s where s: "s ∈ set ss" and x: "x ∈ vars_term s" by auto
from s[unfolded set_conv_nth] obtain i where i: "i < length ss" and s: "s = ss ! i" by auto
from p1[OF i] x[unfolded s]
show "(σ x, τ x) ∈ par_rstep R" by blast
qed
qed
qed
qed
lemma par_rstep_id:
"(s, t) ∈ R ⟹ (s, t) ∈ par_rstep R"
using par_rstep.root_step [of s t R Var] by simp
subsection ‹Parallel Rewriting using Multihole Contexts›