Theory First_Order_Clause.IsaFoR_Ground_Context

theory IsaFoR_Ground_Context
  imports 
    Generic_Context 
    IsaFoR_Ground_Term
begin

abbreviation hole_position where 
  "hole_position ≡ hole_pos"

type_synonym 'f ground_context = "('f, 'f ground_term) actxt"

abbreviation apply_ground_context (‹_⟨_⟩G› [1000, 0] 1000) where
  "C⟨s⟩G ≡ GFun⟨C;s⟩"

interpretation ground_context: "context" where
  hole = □ and 
  apply_context = apply_ground_context and 
  compose_context = actxt_compose
proof unfold_locales
  fix c :: "'f ground_context" and t t' 
  assume "c⟨t⟩G = c⟨t'⟩G" 

  then show "t = t'"
    by (induction c) auto
qed (simp_all add: intp_actxt_compose)

lemma gsubt_at_hole [simp]: "c⟨t⟩G !tG hole_position c = t"
  by (induction c) auto

lemma hole_position_in_positionsG [intro]: "hole_position c ∈ positionsG c⟨t⟩G"
  by (induction c) auto

fun context_at_positionG :: "'f ground_term ⇒ pos ⇒ 'f ground_context" (infixl ‹!c› 64) where
  "t !c [] = □" |
  "GFun f ts !c i # ps = More f (take i ts) (ts!i !c ps) (drop (Suc i) ts)"

text‹Behaves differently than const‹replace_gterm_at›!›
abbreviation replace_atG (‹_⟦_ := _⟧› [70, 0, 50] 70) where
  "replace_atG t p s ≡ (t !c p)⟨s⟩G"

lemma replace_atG_hole [simp]: "c⟨t⟩G⟦hole_position c := t'⟧ = c⟨t'⟩G"
  by (induction c) auto

lemma gsubt_at_id: 
  assumes "p ∈ positionsG t"  
  shows "t⟦p := t !tG p⟧ = t"
  using assms 
  by (induction t arbitrary: p) (auto simp: id_take_nth_drop[symmetric])

(* TODO: actually not needed here, use me to clean up nonground case *)
lemma parallel_replace_atG_in_positionsG:
  assumes "p1 ⊥ p2" "p1 ∈ positionsG t" 
  shows "p2 ∈ positionsG (t⟦p1 := t'⟧) ⟷ p2 ∈ positionsG t"
proof (induction rule: parallel_induct_first_in_positionsG[OF assms])
  case base: (1 p1 p2 i j q1 q2 t f ts)

  let ?p1 = "i # q1"
  let ?ti = "(ts ! i)⟦q1 := t'⟧"

  have "t⟦?p1 := t'⟧ = GFun f (ts[i := ?ti])"
    unfolding base upd_conv_take_nth_drop[OF base(5)] 
    by simp

  then show ?case 
    unfolding base
    using base
    by auto
next
  case step: (2 p1 p2 p k i j q1 q2 t f ts)

  then have "min (length ts) k = k" 
    by simp

  then show ?case
    using step
    by (auto simp: nth_append)
qed

(* TODO: actually not needed here, use me to clean up nonground case *)
lemma parallel_replace_atG_gsubt_at: 
  assumes "p1 ⊥ p2" "p1 ∈ positionsG t"
  shows "t⟦p1 := t'⟧ !tG p2 = t !tG p2"
proof (induction rule: parallel_induct_first_in_positionsG[OF assms])
  case base: (1 p1 p2 i j q1 q2 t f ts)

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

  let ?ti = "replace_atG (ts ! i) q1 t'"
  let ?tsi = "ts[i := ?ti]"

  have "t⟦?p1 := t'⟧ !tG ?p2 = GFun f ?tsi !tG ?p2"
    unfolding base upd_conv_take_nth_drop[OF base(5)] 
    by simp

  also have "... = ts ! j !tG q2"
    using base 
    by simp

  finally show ?case
    by (simp add: base.hyps)
next
  case step: (2 p1 p2 p k i j q1 q2 t f ts)
 
  then show ?case
    by (simp add: nth_append)
qed

lemma parallel_replace_atG:
  assumes "p1 ⊥ p2"  "p1 ∈ positionsG t" "p2 ∈ positionsG t"
  shows "t⟦p1 := s1⟧⟦p2 := s2⟧ = t⟦p2 := s2⟧⟦p1 := s1⟧"
proof (induction rule: parallel_induct_in_positionsG[OF assms])
  case base: (1 p1 p2 i j q1 q2 t f 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⟧ = (GFun f ?ts1)⟦?p2 := s2⟧" 
    unfolding base upd_conv_take_nth_drop[OF i] 
    by simp

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

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

  also have "... = (GFun f ?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

end