Theory First_Order_Clause.Parallel_Induct

theory Parallel_Induct
  imports First_Order_Terms.Position
begin

lemma parallel_induct [case_names parallel base step]: 
  assumes
    parallel: "p⇩1 ⊥ p⇩2" and
    base: "⋀p⇩1 p⇩2 i j q⇩1 q⇩2. p⇩1 = i # q⇩1 ⟹ p⇩2 = j # q⇩2 ⟹ i ≠ j ⟹ P p⇩1 p⇩2" and
    step: 
      "⋀p⇩1 p⇩2 p k i j q⇩1 q⇩2.
        p⇩1 = k # p @ i # q⇩1 ⟹
        p⇩2 = k # p @ j # q⇩2 ⟹
        i ≠ j ⟹
        P (p @ i # q⇩1) (p @ j # q⇩2) ⟹
        P p⇩1 p⇩2"
    shows "P p⇩1 p⇩2"
proof -

  from parallel_remove_prefix[OF parallel]
  obtain p i j q⇩1 q⇩2 where 
    p⇩1: "p⇩1 = p @ i # q⇩1" and 
    p⇩2: "p⇩2 = p @ j # q⇩2" and
    i_neq_j: "i ≠ j" 
    by blast

  show ?thesis unfolding p⇩1 p⇩2
    using base step i_neq_j
    by (induction p) auto
qed

end