Theory First_Order_Clause.IsaFoR_Ground_Term

theory IsaFoR_Ground_Term
  imports 
    "Regular_Tree_Relations.Ground_Terms"
    Parallel_Induct
begin

type_synonym 'f ground_term = "'f gterm"

no_notation Term_Context.position_par (infixl ‹⊥› 67)

(* TODO: Generalize consts for abstract contexts *)
abbreviation positionsG where
  "positionsG ≡ gposs"

notation gsubt_at (infixl ‹!tG› 64)

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

  then obtain f ts where "t = GFun f ts" "i < length ts"
    by (cases t, auto)

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

  then obtain f ts where t: "t = GFun f ts" and k: "k < length ts" 
    by (cases t, auto)

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

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

    from step' have "?p1 ∈ positionsG (ts ! k)"
      unfolding t
      by simp

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

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

  then obtain f ts where "t = GFun f ts" "j < length ts"
    by (cases t, auto)

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

  then obtain f ts where t: "t = GFun f ts" and k: "k < length ts" 
    by (cases t, auto)

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

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

    from step' have "?p2 ∈ positionsG (ts ! k)"
      unfolding t
      by simp

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

lemma parallel_induct_in_positionsG [case_names parallel p1_in_t p2_in_t base step]: 
  assumes
    parallel: "p1 ⊥ p2" and
    p1_in_t: "p1 ∈ positionsG t" and
    p2_in_t: "p2 ∈ positionsG t" and
    base: 
      "⋀p1 p2 i j q1 q2 t f ts.
        p1 = i # q1 ⟹ 
        p2 = j # q2 ⟹
        i ≠ j ⟹
        t = GFun f ts ⟹
        j < length ts ⟹
        i < length ts ⟹
        P p1 p2 t" and
    step: 
      "⋀p1 p2 p k i j q1 q2 t f ts.
        p1 = k # p @ i # q1 ⟹
        p2 = k # p @ j # q2 ⟹
        i ≠ j ⟹
        t = GFun f ts ⟹ 
        k < length ts ⟹
        p1 ∈ positionsG t ⟹
        p2 ∈ positionsG 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)

  then obtain f ts where "t = GFun f ts" "j < length ts" "i < length ts"
    by (cases t, auto)

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

  then obtain f ts where t: "t = GFun f ts" and k: "k < length ts" 
    by (cases t, auto)

  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" 

    from step' have "?p1 ∈ positionsG (ts ! k)" "?p2 ∈ positionsG (ts ! k)"
      unfolding t
      by simp_all

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

end