Theory TA_Impl_Misc

theory TA_Impl_Misc
  imports Main
begin

subsection ‹Invariants on folds›

lemma fold_acc_preserv:
  assumes "⋀ x acc. P acc ⟹ P (f x acc)" "P acc"
  shows "P (fold f xs acc)"
  using assms(2) by (induction xs arbitrary: acc) (auto intro: assms(1))

lemma fold_acc_preserv':
  assumes "⋀ x acc. x ∈ set xs ⟹ P acc ⟹ P (f x acc)" "P acc"
  shows "P (fold f xs acc)"
  using assms by (induction xs arbitrary: acc) auto

lemma fold_acc_ev_preserv':
  fixes x
  assumes
    "⋀ x acc. P acc ⟹ P (f x acc)" "⋀ x acc. Q acc ⟹ Q (f x acc)"
    "⋀ acc. Q acc ⟹ P (f x acc)" "x ∈ set xs" "Q acc"
  shows "P (fold f xs acc) ∧ Q (fold f xs acc)"
  using assms(4,5) apply (induction xs arbitrary: acc)
  using assms(1,2,3) by (auto intro: fold_acc_preserv)

lemma fold_acc_ev_preserv:
  fixes x
  assumes
    "⋀ x acc. P acc ⟹ Q acc ⟹ P (f x acc)" "⋀ x acc. Q acc ⟹ Q (f x acc)"
    "⋀ acc. Q acc ⟹ P (f x acc)" "x ∈ set xs" "Q acc"
  shows "P (fold f xs acc) ∧ Q (fold f xs acc)"
  apply (rule fold_acc_ev_preserv'[where P = "λ acc. P acc ∧ Q acc" and Q = Q, THEN conjunct1])
  by (auto intro: assms)

lemmas fold_ev_preserv = fold_acc_ev_preserv[where Q = "λ _. True", simplified]

lemma fold_evD':
  assumes "¬ P acc" "P (fold f xs acc)"
    shows "∃ x ys zs. xs = ys @ x # zs ∧ ¬ P (fold f ys acc) ∧ P (f x (fold f ys acc))"
  using assms
  apply (induction xs arbitrary: acc)
   apply (simp; fail)
  subgoal premises prems for x xs acc
    apply (cases "P (f x acc)")
     using prems(2-) apply fastforce
     apply (drule prems(1))
     using prems apply simp
     apply clarsimp
     subgoal for xa ys zs
       apply (rule exI[where x = xa])
       apply (rule exI[where x = "x # ys"])
       by fastforce
     done
   done

lemma fold_evD:
  assumes
    "P y (fold f xs acc)" "¬ P y acc" "⋀ acc x. ¬ P y acc ⟹ Q acc ⟹ P y (f x acc) ⟹ x = y"
    "Q acc" "⋀ acc x. Q acc ⟹ Q (f x acc)" "⋀ acc x. ¬ P y acc ⟹ Q acc ⟹ P y (f x acc) ⟹ R y"
  shows "∃ ys zs. xs = ys @ y # zs ∧ ¬ P y (fold f ys acc) ∧ P y (f y (fold f ys acc)) ∧ R y"
proof -
  from fold_evD'[OF assms(2,1)] obtain x ys zs where *:
    "xs = ys @ x # zs" "¬ P y (fold f ys acc)" "P y (f x (fold f ys acc))"
    by auto
  moreover from assms(4-) have "Q (fold f ys acc)" by (auto intro: fold_acc_preserv)
  ultimately show ?thesis using assms(3,6) by auto
qed

lemmas fold_evD'' = fold_evD[where R = "λ _. True", simplified]

end