Theory Swap

theory Swap
imports Helper "HOL-Combinatorics.Transposition" BeispielTac
begin

section‹Swap›
text‹In diesem Abschnitt werden wir eine swap Funktion bauen,
welche es erlaubt Eigenschaften von Personen auszutauschen.
Wenn wir beispielsweise eine Funktion haben welche Personen ihren Besitz zuordnet,
beispielsweise \<^term_type>‹besitz :: 'person ⇒ int›,
so soll die swap Funktion es erlauben, den Besitz von zwei Personen \<^term_type>‹p1::'person› und
\<^term_type>‹p2::'person› zu vertauschen.
So soll \<^term>‹swap (p1::'person) (p2::'person) (besitz :: 'person ⇒ int)›
die \<^term>‹besitz :: 'person ⇒ int› Funktion zurückgeben,
allerdings mit dem Besitz von \<^term>‹p1::'person› und \<^term>‹p2::'person› vertauscht.
›

(*
Initially, I introduced my own swap implementation as `swap a b f = f(a:=f b, b:= f a)`.
But then I found that Isabelle/HOL already provides this implementation.
*)

definition swap :: ‹'a ⇒ 'a ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b› where
  ‹swap a b f ≡ Fun.swap a b f›

beispiel ‹swap a b f = f(a:=f b, b:= f a)›
  by (simp add: Fun.swap_def swap_def)

lemma swap1[simp]: ‹swap a b (swap a b f) = f›
  by (simp add: swap_def swap_nilpotent)
lemma swap2[simp]: ‹swap b a (swap a b f) = f›
  by (simp add: swap_def swap_nilpotent transpose_commute)

beispiel ‹(swap p1 p2 swap) p1 p2 x = x› (*wow, types*)
  by(simp add: swap_def)
beispiel ‹(swap p2 p1 swap) p1 p2 x = x› (*wow, types*)
  by(simp add: swap_def)

lemma swap_id[simp]: ‹swap a a f = f›
  by(simp add: swap_def)

beispiel ‹f_swapped = (swap a b f) ⟹ f_swapped a = f b ∧ f_swapped b = f a›
  by(simp add: swap_def)

(*TODO rename*)
lemma swap_symmetric: ‹swap a b = swap b a›
  unfolding swap_def
  by (simp add: swap_commute)
lemma map_swap_none: ‹a ∉ set P ⟹ b ∉ set P ⟹ map (swap a b f) P = map f P›
  by (simp add: swap_def Fun.swap_def)

lemma map_swap_one: ‹a ∉ set P ⟹  map (swap a b f) P = map (f(b:=f a)) P›
  by(simp add: swap_def Fun.swap_def)

lemma swap_a: ‹swap a b f a = f b›
  by(simp add: swap_def)
lemma swap_b: ‹swap a b f b = f a›
  by(simp add: swap_def)

lemma sum_swap_none: ‹a ∉ P ⟹ b ∉ P ⟹ sum (swap a b f) P = sum f P›
  apply(rule sum.cong, simp)
  apply(simp add: swap_def Fun.swap_def)
  by fastforce
lemma swap_nothing: ‹a ≠ p1 ⟹ a ≠ p2 ⟹ swap p1 p2 f a = f a›
  by(simp add: swap_def)

lemma swap_id_comp: ‹swap a a = id›
  by(simp add: fun_eq_iff)
lemma swap_fun_comp_id:
  ‹swap p1 p2 (f ∘ swap p1 p2 (f ∘ kons)) = f ∘ (f ∘ kons)›
  apply(simp add: comp_def fun_eq_iff)
  apply(simp add: swap_def)
  done
lemma swap_fun_map_comp_id:
  ‹swap p1 p2 (map (swap p1 p2) ∘ swap p1 p2 (map (swap p1 p2) ∘ kons)) = kons›
  apply(simp add: comp_def fun_eq_iff)
  apply(simp add: swap_def swap_id_comp)
  by (simp add: map_idI)

lemma swap_forall: ‹(∀p. P (swap p1 p2 a p) (swap p1 p2 b p)) ⟷ (∀p. P (a p) (b p))›
  apply(simp add: swap_def)
  by (metis transpose_involutory)

(*
whenever a prove can be solved by (metis swap_a swap_b swap_nothing)
maybe by(rule swap_cases, simp_all add: swap_a swap_b swap_nothing)
can be faster
*)
lemma swap_cases:
  ‹(p = p1 ⟹ P (f p2)) ⟹ (p = p2 ⟹ P (f p1)) ⟹ (p ≠ p1 ⟹ p ≠ p2 ⟹ P (f p))⟹ P (swap p1 p2 f p)›
apply(case_tac ‹p=p1›, simp add: swap_a)
apply(case_tac ‹p=p2›, simp add: swap_b)
apply(simp add: swap_nothing)
done

lemma swap_in_set_of_functions:
  ‹swap p2 p1 x ∈ A ⟷ x ∈ swap p1 p2 ` A›
  using image_iff by fastforce

lemma swap_image: ‹p1 ∈ A ⟹ p2 ∈ A ⟹ swap p1 p2 f ` A = f ` A›
  apply(simp add: image_def)
  apply(rule Collect_cong)
  by (metis swap_a swap_b swap_nothing)

lemma swap_id_eq_simp: ‹swap p1 p2 id a = swap p1 p2 id b ⟷ a = b›
  by (metis id_apply swap_a swap_nothing swap_symmetric)

lemma swap_id_in_set:
  ‹swap p2 p1 id x ∈ swap p1 p2 id ` A ⟷ x ∈ A›
  apply(simp add: image_iff)
  by (simp add: swap_id_eq_simp swap_symmetric) 

thm sum.remove
lemma sum_swap_a: ‹finite P ⟹ a ∉ P ⟹ b ∈ P ⟹ sum (swap a b f) P = f a + sum f (P - {b})›
  apply(subst sum.remove[of ‹P› ‹b›])
  by(simp_all add: swap_b sum_swap_none)

lemma sum_list_swap: ‹p1 ∈ set P ⟹ p2 ∈ set P ⟹ distinct P ⟹
        sum_list (map (swap p1 p2 f) P) = sum_list (map (f::'a⇒int) P)›
  apply(simp add: sum_list_map_eq_sum_count_int)
  apply(simp add: count_list_distinct)
  thm sum.cong
  apply(induction ‹P› arbitrary: ‹p1› ‹p2›)
   apply(simp)
  apply(simp)
  apply(elim disjE)
     apply(simp_all)
    apply(simp add: swap_a sum_swap_a sum.remove[symmetric]; fail)
   apply(simp add: swap_symmetric swap_a sum_swap_a sum.remove[symmetric]; fail)
  apply(rule swap_nothing)
  by auto

  
lemma min_list_swap_int:
  fixes f::‹'person ⇒ int›
  shows ‹p1 ∈ set ps ⟹ p2 ∈ set ps ⟹ min_list (map (swap p1 p2 f) ps) = min_list (map f ps)›
  apply(cases ‹ps = []›)
   apply(simp; fail)
  apply(simp add: min_list_Min)
  apply(cases ‹p1 = p2›)
   apply(simp; fail)
  apply(rule arg_cong[where f=‹Min›])
  apply(simp add: swap_image)
  done

lemma min_list_swap_int_enum:
  fixes f::‹'person::enum ⇒ int›
  shows ‹min_list (map (swap p1 p2 f) enum_class.enum) = min_list (map f enum_class.enum)›
  apply(subst min_list_swap_int)
  by(simp_all add: enum_class.enum_UNIV)

lemma remove1_swap:
  ‹remove1 (swap p1 p2 a) (map (swap p1 p2) ks)
    = map (swap p1 p2) (remove1 a ks)›
  apply(induction ‹ks›)
   apply(simp)
  apply(simp)
  by (metis swap2)

lemma remove1_swap2:
  ‹map (swap p1 p2) (remove1 (swap p1 p2 a) (map (swap p1 p2) ks))
    =  remove1 a ks›
  apply(induction ‹ks›)
   apply(simp)
  apply(simp add: comp_def)
  by (metis (mono_tags, lifting) swap2)

lemma swap_if_move_inner:
  ‹swap p2 p1 (λp. if P p then A p else B p)
    = (λp. if P (swap p2 p1 id p) then A (swap p2 p1 id p) else B (swap p2 p1 id p))›
  by(simp add: swap_def fun_eq_iff)



lemma swap_fun_swap_id: ‹swap p1 p2 konsens (swap p1 p2 id p) = konsens p›
  apply(cases ‹p=p1›)
   apply(simp add: swap_a swap_b)
  apply(cases ‹p=p2›)
   apply(simp add: swap_a swap_b)
  by(simp add: swap_nothing)


(*TODO: baut swap eine Permutation und gibt es darauf lemmata?
TODO: HOL-Combinatorics.Permutations
*)
lemma ‹distinct [p1,p2,p3,p4] ⟹ swap p1 p2 (swap p3 p4 welt) = swap p3 p4 (swap p1 p2 welt)›
  by(auto simp add: swap_def Fun.swap_def)

lemma swap_comm: ‹p1 ≠ p3 ⟹ p1 ≠ p4 ⟹ p2 ≠ p3 ⟹ p2 ≠ p4 ⟹
  swap p1 p2 (swap p3 p4 welt) = swap p3 p4 (swap p1 p2 welt)›
  by(auto simp add: swap_def Fun.swap_def)

lemma swap_unrelated_im_kreis:
  ‹p ≠ p1 ⟹ p ≠ p2 ⟹
    swap p2 p (swap p1 p2 (swap p p1 (swap p1 p2 welt))) = welt›
  by(simp add: swap_def Fun.swap_def)

end