Theory Fofu_Abs_Base

theory Fofu_Abs_Base
imports 
  Complex_Main 
  "HOL-Library.Rewrite"
  Automatic_Refinement.Misc
  Refine_Imperative_HOL.Sepref_Misc
  "Program-Conflict-Analysis.LTS"
begin  

  (* TODO: Move *)
  lemma swap_in_iff_inv: "prod.swap p ∈ S ⟷ p ∈ S¯"
    apply (cases p) by auto
  
      
(* TODO: Move *)  
lemma length_filter_disj_or_conv:
  assumes "⋀x. x∈set xs ⟶ ¬(P x ∧ Q x)"
  shows "length [x ← xs. P x ∨ Q x] = length (filter P xs) + length (filter Q xs)"  
  using assms
  by (induction xs) auto  

(* TODO: Move. Extract an element from a summation, combined with congruence. *)  
lemma sum_arb:
  assumes A_fin: "finite A"
      and x_mem: "x ∈ A" 
      and x_dif: "∀y∈A. y ≠ x ⟶ g y = h y"
    shows "(∑a∈A. g a) = (∑a∈A - {x}. h a) + g x"
proof -
  have "A = (A - {x}) ∪ {x}" using x_mem by auto
  moreover note sum.union_disjoint[of "A - {x}" "{x}" g]
  moreover note sum.cong[of "A - {x}" "A - {x}" g h]
  ultimately show ?thesis using A_fin x_dif by auto
qed
  
    
    
    
lemma trcl_cons_conv: 
  "(u,a#xs,v)∈trcl R ⟷ (∃uh. (u,a,uh)∈R ∧ (uh,xs,v)∈trcl R)"
  by (auto dest!: trcl_uncons)
  
lemma trcl_conc_conv: 
  "(u,xs@ys,v)∈trcl R ⟷ (∃uh. (u,xs,uh)∈trcl R ∧ (uh,ys,v)∈trcl R)"    
  by (auto dest!: trcl_unconcat intro: trcl_concat)
  
lemmas trcl_conv = trcl_cons_conv trcl_conc_conv
  ― ‹Adding these to simpset will split all cons and append operations in paths›

      
      
  
end