Theory Parallel_Rewrite

theory Parallel_Rewrite
  imports 
    Parallel_Induct 
    Generic_Term_Context
    Ground_Term_Rewrite_System
begin

locale parallel_rewrite =
  term_interpretation where Fun = Fun and is_var = "λ_. False" +
  smaller_subcontext where size = sizec +
  replace_at_subterm where Fun = Fun and is_var = "λ_. False" +
  ground_term_rewrite_system
  for Fun :: "'f ⇒ 'e ⇒ 't list ⇒ 't" and sizec :: "'c ⇒ nat"
begin

lemma parallel_induct_in_positions [case_names parallel p1_in_t p2_in_t base step]: 
  assumes
    parallel: "p1 ⊥ p2" and
    p1_in_t: "p1 ∈ positions t" and
    p2_in_t: "p2 ∈ positions t" and
    base: 
      "⋀p1 p2 i j q1 q2 t f e ts.
        p1 = i # q1 ⟹ 
        p2 = j # q2 ⟹
        i ≠ j ⟹
        t = Fun f e ts ⟹
        j < length ts ⟹
        i < length ts ⟹
        P p1 p2 t" and
    step: 
      "⋀p1 p2 p k i j q1 q2 t f e ts.
        p1 = k # p @ i # q1 ⟹
        p2 = k # p @ j # q2 ⟹
        i ≠ j ⟹
        t = Fun f e ts ⟹ 
        k < length ts ⟹
        p1 ∈ positions t ⟹
        p2 ∈ positions t ⟹
        P (p @ i # q1) (p @ j # q2) (ts ! k) ⟹
        P p1 p2 t"
    shows "P p1 p2 t"
  using p1_in_t p2_in_t
proof (induction arbitrary: t rule: parallel_induct[OF parallel])
  case base': (1 p1 p2 i j q1 q2 t)

  obtain f e ts where t: "t = Fun f e ts" 
    using term_destruct[of t]
    by blast

  moreover have "i < length ts" 
    using base'(4) t
    unfolding base'(1)
    by simp

  moreover have "j < length ts"
    using base'(5) t
    unfolding base'(2)
    by simp

  ultimately show ?case
    using base' base
    by metis
next
  case step': (2 p1 p2 p k i j q1 q2 t)

  obtain f e ts where t: "t = Fun f e ts"
    using term_destruct
    by metis

  then have k: "k < length ts"
    using step'(5)
    unfolding step'(1)
    by simp

  show ?case
  proof (rule step[OF step'(1, 2, 3) t k step'(5, 6)])

    let ?p1 = "p @ i # q1"
    let ?p2 = "p @ j # q2" 

    have "?p1 ∈ positions (ts ! k)"  "?p2 ∈ positions (ts ! k)"
      using step'(5, 6)
      unfolding step'(1, 2)
      by (simp_all add: t)

    then show "P ?p1 ?p2 (ts ! k)"
      using step'.IH
      by blast
  qed
qed

lemma parallel_replace_at:
  assumes "p1 ⊥ p2"  "p1 ∈ positions t" "p2 ∈ positions t"
  shows "t⟦p1 := s1⟧⟦p2 := s2⟧ = t⟦p2 := s2⟧⟦p1 := s1⟧"
proof (induction rule: parallel_induct_in_positions[OF assms])
  case base: (1 p1 p2 i j q1 q2 t f e ts)

  let ?p1 = "i # q1"
  let ?p2 = "j # q2"
  let ?s1 = "(ts ! i)⟦q1 := s1⟧"
  let ?s2 = "(ts ! j)⟦q2 := s2⟧"
  let ?ts1 = "ts[i := ?s1]"
  let ?ts2 = "ts[j := ?s2]"

  note i_neq_j = base(3)

  note i = base(6)
  note j = base(5)

  have j': "j < length ?ts1" and i': "i < length ?ts2" 
    using i j
    by simp_all

  have "t⟦?p1 := s1⟧⟦?p2 := s2⟧ = (Fun f e ?ts1)⟦?p2 := s2⟧" 
    unfolding base upd_conv_take_nth_drop[OF i]
    by simp

  also have "... = Fun f e (?ts1[j := ?s2])"
    unfolding upd_conv_take_nth_drop[OF j']
    using i_neq_j
    by simp

  also have "... = Fun f e (?ts2[i := ?s1])"
    using list_update_swap[OF i_neq_j]
    by metis

  also have "... = (Fun f e ?ts2)⟦?p1 := s1⟧"
    unfolding upd_conv_take_nth_drop[OF i'] 
    using i_neq_j
    by simp

  also have "... = t⟦?p2 := s2⟧⟦?p1 := s1⟧" 
    unfolding upd_conv_take_nth_drop[OF j] base
    by simp

  finally show ?case
    unfolding base
    by satx
next
  case step: 2

  then show ?case
    by (simp add: nth_append)
qed

lemma parallel_rewrite_in_context:
  assumes 
    parallel: "p1 ⊥ p2" and
    p1_in_t: "p1 ∈ positions t" and
    p2_in_t: "p2 ∈ positions t" and
    l2: "l2 = t !t p2" and
    l2_r2: "(l2, r2) ∈ R" 
  shows "(t⟦p1 := v⟧, t⟦p1 := v⟧⟦p2 := r2⟧) ∈ rewrite_in_context R" (is "(?t1,?t2) ∈ _")
proof (unfold rewrite_in_context_def mem_Collect_eq, intro exI conjI)
  let ?c = "t⟦p1 := v⟧ !c p2"

  show "(?t1, ?t2) = (?c⟨l2⟩, ?c⟨r2⟩)"
    unfolding l2 parallel_replace_at[OF parallel p1_in_t p2_in_t] context_at_subterm_at[OF p2_in_t] ..  
qed (rule l2_r2)

end

end