Theory Aenderung

theory Aenderung
imports Main ExecutableHelper BeispielPerson Handlung Zahlenwelt "HOL-Library.Multiset"
begin

section‹Änderungen in Welten›
text‹In diesem Abschnitt werden wir Änderungen in Welten,
und darauf basierend, Abmachungen modellieren.›

text‹Bei einer Änderung keine eine Person entweder etwas verlieren oder gewinnen.
Dieses einfache Modell ist natürlich auf unsere Zahlenwelten angepasst,
in der normalerweise Typ \<^typ>‹'etwas› ein \<^typ>‹int› ist.›
datatype ('person, 'etwas) aenderung = Verliert ‹'person› ‹'etwas› | Gewinnt ‹'person› ‹'etwas›

text‹Beispiel: \<^term>‹[Gewinnt Alice 3, Verliert Bob 3]::(person, int) aenderung list›.›

text‹Von einer \<^typ>‹('person, 'etwas) aenderung› betroffene Person bzw. Personen.›
definition betroffen :: ‹('person, 'etwas) aenderung ⇒ 'person›
  where
‹betroffen a ≡ case a of Verliert p _ ⇒ p | Gewinnt p _ ⇒ p›

definition betroffene :: ‹('person, 'etwas) aenderung list ⇒ 'person list›
  where
‹betroffene as ≡ map betroffen as›

(*<*)
lemma betroffene_case_aenderung:
  ‹betroffene = map (case_aenderung (λp _. p) (λp _. p))›
  by(simp add: fun_eq_iff betroffene_def betroffen_def)
(*>*)


beispiel ‹betroffene [Verliert Alice (2::int), Gewinnt Bob 3, Gewinnt Carol 2, Verliert Eve 1]
  = [Alice, Bob, Carol, Eve]› by eval
beispiel ‹betroffene [Verliert Alice (5::nat), Gewinnt Bob 3, Verliert Eve 7]
  = [Alice, Bob, Eve]› by eval
beispiel ‹betroffene [Verliert Alice (5::nat), Gewinnt Alice 3]
  = [Alice, Alice]› by eval

(*<*)
text‹Das Delta um von \<^term>‹i2› nach \<^term>‹i2› zu kommen.›
definition delta_num
  :: ‹'person ⇒ 'etwas::{ord,minus} ⇒ 'etwas ⇒ (('person, 'etwas) aenderung) option›
  where
    ‹delta_num p i1 i2 = (
           if i1 > i2 then Some (Verliert p (i1 - i2))
      else if i1 < i2 then Some (Gewinnt p (i2 - i1))
      else None
  )›

lemma ‹delta_num p i1 i2 = Some (Gewinnt p (i::int)) ⟹ i > 0›
  by(auto simp add: delta_num_def split_ifs)
lemma ‹delta_num p i1 i2 = Some (Verliert p (i::int)) ⟹ i > 0›
  by(auto simp add: delta_num_def split_ifs)
lemma ‹delta_num p1 i1 i2 = Some (Gewinnt p2 (i::int)) ⟹ p1 = p2›
  by(auto simp add: delta_num_def split_ifs)
lemma ‹delta_num p1 i1 i2 = Some (Verliert p2 (i::int)) ⟹ p1 = p2›
  by(auto simp add: delta_num_def split_ifs)


beispiel ‹delta_num Alice (2::int) 6 = Some (Gewinnt Alice 4)› by eval
beispiel ‹delta_num Alice (-2::int) 6 = Some (Gewinnt Alice 8)› by eval


lemma delta_num_same: ‹delta_num p (a::'a::ordered_ab_group_add) a = None›
  by(simp add: delta_num_def)

text‹The absolute delta between \<^term>‹i1› and \<^term>‹i2›.
This basically merges the two terms.›
definition sum_delta_num
  :: ‹'person ⇒ 'etwas::{ord,zero,plus,uminus,minus} ⇒ 'etwas ⇒ (('person, 'etwas) aenderung) option›
  where
    ‹sum_delta_num p i1 i2 = (
      let s = i1 + i2 in
           if s < 0 then Some (Verliert p (-s))
      else if s > 0 then Some (Gewinnt p s)
      else None
  )›

beispiel ‹sum_delta_num Alice (2::int) 6 = Some (Gewinnt Alice 8)› by eval
beispiel ‹sum_delta_num Alice (-2::int) 6 = Some (Gewinnt Alice 4)› by eval

lemma sum_delta_num_delta_num:
  fixes i1::‹'a::ordered_ab_group_add›
  shows ‹sum_delta_num p i1 i2 = delta_num p 0 (i1+i2)›
  by(simp add: sum_delta_num_def delta_num_def Let_def)

lemma  delta_num_sum_delta_num:
  fixes i1::‹'a::ordered_ab_group_add›
  shows ‹delta_num p i1 i2 = sum_delta_num p (-i1) i2›
  by(simp add: sum_delta_num_def delta_num_def Let_def)

(*>*)

subsection‹Deltas›
text‹Deltas, d.h. Unterschiede zwischen Welten.
Ein Delta ist eine Liste von Änderungen.
Wir definieren das ⬚‹type_synonym› delta als die Funktion,
welche solch eine Liste berechnet,
gegeben die Handlung welche die Veränderung hervorruft.›
(*Man könnte eine class Delta world einführen, mit einer delta-Funtion
  :: welt -> welt -> [Aenderung person etwas]
Diese Klasse würde dann Welten mit Personen und Etwas in Relation setzen.
Dafür bräuchte es MultiParamTypeClasses. Eine simple Funktion ist da einfacher.*)
type_synonym ('welt, 'person, 'etwas) delta =
    ‹'welt handlung ⇒ (('person, 'etwas) aenderung) list›

(*<*)
definition aenderung_val :: ‹('person, ('etwas::uminus)) aenderung ⇒ 'etwas›
  where
‹aenderung_val a ≡ case a of Verliert _ n ⇒ -n | Gewinnt _ n ⇒ n›

beispiel ‹aenderung_val (Verliert Alice (2::int)) = -2› by eval
beispiel ‹aenderung_val (Gewinnt Alice (2::int)) = 2› by eval

lemma betroffen_simps[simp]:
  ‹betroffen (Gewinnt a ab) = a›
  ‹betroffen (Verliert a ab) = a›
  by(simp add: betroffen_def)+
lemma aenderung_val_simps[simp]:
  ‹aenderung_val (Gewinnt a ab) = ab›
  ‹aenderung_val (Verliert a ab) = -ab›
  by(simp add: aenderung_val_def)+

fun delta_num_map
  :: ‹(('person::enum ⇀ ('etwas::{zero,minus,ord})), 'person, 'etwas) delta›
  where
  ‹delta_num_map (Handlung vor nach) =
      List.map_filter
        (λp. case (the_default (vor p) 0, the_default (nach p) 0)
               of (a,b) ⇒ delta_num p a b)
        (Enum.enum::'person list)›

beispiel‹delta_num_map
  (Handlung [Alice ↦ 5::int, Bob ↦ 10, Eve ↦ 1]
            [Alice ↦ 3, Bob ↦ 13, Carol ↦ 2])
  = [Verliert Alice 2, Gewinnt Bob 3, Gewinnt Carol 2, Verliert Eve 1]› by eval

fun delta_num_fun
  :: ‹(('person::enum ⇒ ('etwas::{minus,ord})), 'person, 'etwas) delta›
  where
  ‹delta_num_fun (Handlung vor nach) =
      List.map_filter (λp. delta_num p (vor p) (nach p)) Enum.enum›

beispiel ‹delta_num_fun
    (Handlung
        ((λp. 0::int)(Alice:=8, Bob:=12, Eve:=7))
        ((λp. 0::int)(Alice:=3, Bob:=15, Eve:=0)))
  = [Verliert Alice 5, Gewinnt Bob 3, Verliert Eve 7]› by eval

lemma delta_num_map: ‹delta_num_map (Handlung m1 m2) =
        delta_num_fun (Handlung (λp. the_default (m1 p) 0) (λp. the_default (m2 p) 0))›
  by(simp)


(*TODO: das if will in die swap.thy?*)
term ‹map_aenderung›
definition aenderung_swap
  :: ‹'person ⇒ 'person ⇒ ('person, 'etwas) aenderung ⇒ ('person, 'etwas) aenderung›
where
  ‹aenderung_swap p1 p2 a ≡ map_aenderung (λp. if p = p1 then p2 else if p = p2 then p1 else p) id a›

beispiel‹aenderung_swap Alice Bob (Gewinnt Alice (3::nat)) = Gewinnt Bob 3› by eval
beispiel‹aenderung_swap Alice Bob (Gewinnt Bob (3::nat)) = Gewinnt Alice 3› by eval
beispiel‹aenderung_swap Alice Bob (Gewinnt Carol (3::nat)) = Gewinnt Carol 3› by eval


lemma aenderung_swap_id: ‹aenderung_swap p1 p2 (aenderung_swap p1 p2 a) = a›
  apply(simp add: aenderung_swap_def)
  apply(cases ‹a›)
  by simp_all

lemma aenderung_swap_sym: ‹aenderung_swap p1 p2 = aenderung_swap p2 p1›
  apply(simp add: fun_eq_iff aenderung_swap_def, intro allI, rename_tac a)
  apply(case_tac ‹a›)
  by simp_all

lemma map_map_aenderung_swap:
  ‹map (map (aenderung_swap p1 p2)) ∘ (map (map (aenderung_swap p1 p2)) ∘ kons) = kons›
  by(simp add: fun_eq_iff aenderung_swap_id comp_def)

lemma swap_map_map_aenderung_swap:
  ‹swap p2 p1 (map (map (aenderung_swap p2 p1)) ∘ swap p1 p2 (map (map (aenderung_swap p1 p2)) ∘ kons))
  = kons›
  apply(subst aenderung_swap_sym)
  apply(subst swap_symmetric)
  apply(subst swap_fun_comp_id)
  apply(simp add: map_map_aenderung_swap)
  done
(*>*)


text‹Eine Liste von Änderungen lässt sich ausführen.›
fun aenderung_ausfuehren
  :: ‹('person, 'etwas::{plus,minus}) aenderung list ⇒ ('person ⇒ 'etwas) ⇒ ('person ⇒ 'etwas)›
where
  ‹aenderung_ausfuehren [] bes = bes›
| ‹aenderung_ausfuehren (Verliert p n # deltas) bes = aenderung_ausfuehren deltas ⟦bes(p -= n)⟧›
| ‹aenderung_ausfuehren (Gewinnt p n # deltas) bes = aenderung_ausfuehren deltas ⟦bes(p += n)⟧›

text‹Die lokale Variable \<^term_type>‹bes :: ('person ⇒ 'etwas)› stellt dabei den
aktuellen Besitz dar.
Die Ausgabe der Funktion ist der modifizierte Besitz, nachdem die Änderung ausgeführt wurde.›

beispiel
‹aenderung_ausfuehren
  [Verliert Alice (2::int), Gewinnt Bob 3, Gewinnt Carol 2, Verliert Eve 1]
  (€(Alice:=8, Bob:=3, Eve:= 5))
  =
  (€(Alice:=6, Bob:=6, Carol:=2, Eve:= 4))›
  by eval

beispiel
‹aenderung_ausfuehren
  [Verliert Alice (2::int), Verliert Alice 6]
  (€(Alice:=8, Bob:=3, Eve:= 5))
  =
  (€(Bob:=3, Eve:= 5))›
  by eval
text‹Im vorherigen Beispiel verliert \<^const>‹Alice› alles.
Da sie nun den \<^const>‹DEFAULT›-Wert von \<^term>‹0::int› besitzt, wird ihre Besitz nicht angezeigt.›

(*<*)
(*TODO: upstream und vereinfachen!*)
lemma swap_aenderung_ausfuehren:
  ‹swap p1 p2 (Aenderung.aenderung_ausfuehren a bes)
      = Aenderung.aenderung_ausfuehren (map (aenderung_swap p1 p2) a) (swap p1 p2 bes)›
  apply(induction ‹a› arbitrary: ‹bes›)
   apply(simp)
  apply(simp)
  apply(case_tac ‹a1›)
  subgoal
    apply(simp)
    apply(simp add: aenderung_swap_def, safe)
      apply (simp_all add: fun_upd_twist swap_def Fun.swap_def)
    done
  apply(simp)
    apply(simp add: aenderung_swap_def, safe)
    apply (simp_all add: fun_upd_twist swap_def Fun.swap_def)
  done
(*>*)

subsection‹Abmachungen›
text‹Eine \<^typ>‹('person, 'etwas) aenderung list› wie
z.B. \<^term>‹[Gewinnt Alice (3::int), Verliert Bob 3]› ließe sich gut verwenden,
um eine Abmachung zwischen \<^const>‹Alice› und \<^const>‹Bob› zu modellieren.
Allerdings ist diese Darstellung unpraktisch zu benutzen.
Beispielsweise sind

  ▪ \<^term>‹[Gewinnt Alice (3::int), Verliert Bob 3]›
  ▪ \<^term>‹[Verliert Bob 3, Gewinnt Alice (3::int)]›
  ▪ \<^term>‹[Gewinnt Alice (1::int), Gewinnt Alice 1, Gewinnt Alice 1, Verliert Bob 3, Verliert Carol 0]›

extensional betrachtet alle equivalent.
Es ist praktischer, eine Darstellung zu wählen,
in der syntaktische und semantische Äquivalenz zusammenfallen.
Das bedeutet, eine Abmachung muss eindeutig dargestellt werden.
Ein Kandidat dafür wäre eine Map vom Typ \<^typ>‹'person ⇀ 'etwas›, da diese eindeutig einer
\<^typ>‹'person› ein \<^typ>‹'etwas› zuordnet.
Dies funktioniert allerdings nur, wenn @{typ [source=true] ‹'etwas::{uminus,plus}›} mit Plus und Minus
dargestellt werden kann, um \<^const>‹Gewinnt› und \<^const>‹Verliert› darzustellen.
Allerdings ist auch diese Darstellung nicht eindeutig,
da z.B. \<^term>‹[Alice ↦ 0] = Map.empty› semantisch gilt,
solange \<^term>‹0› ein neutrales Element ist.
Deshalb stellen wir eine Abmachung als eine
totale Funktion vom Typ @{typ [source=true] ‹'person ⇒ ('etwas::{uminus, plus, zero})›} dar.
Der Term \<^term>‹(λ_. 0)(Alice := 3, Bob := -3)› bedeutet \<^const>‹Alice› bekommt 3, \<^const>‹Bob› verliert 3.
›
type_synonym  ('person, 'etwas) abmachung = ‹'person ⇒ 'etwas›


text‹Folgende Funktion konvertiert eine Liste von Änderungen in ein Abmachung.
Persönlich finde ich es schöner eine Liste von Änderungen aufzuschreiben,
mathematisch ist eine Abmachung allerdings überlegen.
Folgende Funktion sorgt dafür, dass wir Abmachungen dennoch als
Liste von Änderungen aufschreiben können, dann allerdings mit der Abmachung weiterrechnen.›
fun to_abmachung
  :: ‹('person, 'etwas::{ord,zero,plus,minus,uminus}) aenderung list ⇒ ('person, 'etwas) abmachung›
where
  ‹to_abmachung [] = (λp. 0)›
| ‹to_abmachung (delta # deltas) = 
   ⟦(to_abmachung deltas)(betroffen delta += aenderung_val delta)⟧›


beispiel ‹[to_abmachung [Gewinnt Alice (3::int)], to_abmachung [Gewinnt Alice 3, Verliert Bob 3]]
        = [(λp.0)(Alice := 3), (λp.0)(Alice := 3, Bob := -3)]› by eval


(*<*)
lemma to_abmachung_simp_call:
  ‹to_abmachung (delta # deltas) p =
    (if p = betroffen delta
     then (to_abmachung deltas p) + (aenderung_val delta)
     else (to_abmachung deltas p))›
  by(simp)

lemma to_abmachung_fold_induct_helper:
  fixes as :: ‹('person, 'etwas::ordered_ab_group_add) aenderung list›
  shows ‹fold (λa acc. ⟦acc(betroffen a += aenderung_val a)⟧) as abmachung =
    (λp. to_abmachung as p + abmachung p)›
  apply(induction ‹as› arbitrary:‹abmachung›)
  by(simp add: fun_eq_iff)+
lemma to_abmachung_fold:
  fixes as :: ‹('person, 'etwas::ordered_ab_group_add) aenderung list›
  shows ‹to_abmachung as = fold (λa acc. ⟦acc(betroffen a += aenderung_val a)⟧) as (λ_. 0)›
  apply(subst to_abmachung_fold_induct_helper[where abmachung=‹λ_. 0›])
  by simp

lemma to_abmachung_List_map_filter_simp_call:
  fixes f :: ‹'person::enum ⇒ ('person, 'etwas::ordered_ab_group_add) aenderung option›
  assumes valid_f: ‹⋀p a. f p = Some a ⟹ betroffen a = p›
  shows
  ‹p ∈ set as ⟹ distinct as ⟹
   to_abmachung (List.map_filter f as) p =
    (case f p of Some a ⇒ to_abmachung [a] p | None ⇒ 0)›
proof(induction ‹as›)
  case Nil
  then show ‹?case› by simp
next
  case (Cons a as)
  have filter_not_in_set:
    ‹p ∉ set ps ⟹ to_abmachung (List.map_filter f ps) p = 0› for p ps
    apply(induction ‹ps›)
    apply(simp add: List.map_filter_simps)
    apply(simp add: List.map_filter_simps split:option.split)
    apply(clarsimp, rename_tac a ps a2)
    apply(subgoal_tac ‹betroffen a2 = a›)
     apply simp
    by(auto dest: valid_f)

  from Cons show ‹?case›
    apply(simp add: List.map_filter_simps)
    apply(safe)
     apply(case_tac ‹f p›)
      apply(simp add: filter_not_in_set; fail)
     apply(simp add: filter_not_in_set)
    using filter_not_in_set apply blast
    apply(simp)
     apply(case_tac ‹f a›)
      apply(simp add: filter_not_in_set; fail)
    apply(simp add: filter_not_in_set)
    by(auto dest: valid_f)
qed

lemma to_abmachung_List_map_filter_enum_simp_call:
fixes f :: ‹'person::enum ⇒ ('person, 'etwas::ordered_ab_group_add) aenderung option›
  assumes valid_f: ‹⋀p a. f p = Some a ⟹ betroffen a = p›
  shows
  ‹to_abmachung (List.map_filter f Enum.enum) p =
    (case f p of Some a ⇒ to_abmachung [a] p | None ⇒ 0)›
  apply(rule to_abmachung_List_map_filter_simp_call)
  using valid_f apply(simp)
   apply(simp add: enum_class.enum_UNIV)
  apply(simp add: enum_class.enum_distinct)
  done

fun abmachung_to_aenderung_list
  :: ‹'person list ⇒ ('person, 'etwas::{ord,zero,plus,minus,uminus}) abmachung ⇒ ('person, 'etwas) aenderung list›
where
  ‹abmachung_to_aenderung_list [] _ = []›
| ‹abmachung_to_aenderung_list (p#ps) a =
    (if a p = 0
     then abmachung_to_aenderung_list ps a
     else (if a p > 0 then Gewinnt p (a p) else Verliert p (- (a p))) # abmachung_to_aenderung_list ps a
    )›

definition abmachung_to_aenderung
  :: ‹('person::enum, 'etwas::{ord,zero,plus,minus,uminus}) abmachung ⇒ ('person, 'etwas) aenderung list›
where
  ‹abmachung_to_aenderung ≡ abmachung_to_aenderung_list Enum.enum›

beispiel ‹abmachung_to_aenderung ((λp.0)(Alice := (3::int), Bob := -3))
            = [Gewinnt Alice 3, Verliert Bob 3]› by eval


definition aenderung_to_abmachung
  :: ‹('person, 'etwas) aenderung list ⇒ ('person::enum, 'etwas::{ord,zero,plus,minus,uminus}) abmachung›
where
  ‹aenderung_to_abmachung ≡ to_abmachung›

lemma fixes as :: ‹('person::enum, int) aenderung list›
  shows ‹abmachung_to_aenderung (aenderung_to_abmachung as) = as›
  (* nitpick as = [Verliert person⇩1 (- 1)] *)
  oops (*gilt nicht, weil aenderungen nicht eindeutig*)


lemma abmachung_to_aenderung_list_to_abmachung_not_in_ps:
  ‹p ∉ set ps ⟹  to_abmachung (abmachung_to_aenderung_list ps a) p = 0›
  by(induction ‹ps›) simp+

lemma abmachung_to_aenderung_list_not_in_ps:
  ‹p ∉ set ps ⟹
       abmachung_to_aenderung_list ps (a(p := v)) = abmachung_to_aenderung_list ps a›
  apply(induction ‹ps›)
   apply(simp)
  apply(simp)
  by fastforce


definition abmachung_dom :: ‹('person, 'etwas::zero) abmachung ⇒ 'person set› where
  ‹abmachung_dom m = {a. m a ≠ 0}›

lemma abmachung_dom_swap:
  ‹abmachung_dom (swap p1 p2 a) = (swap p1 p2 id) ` (abmachung_dom a)›
  apply(simp add: abmachung_dom_def)
  apply(simp add: image_def)
  apply(rule Collect_cong)
  apply(simp add: swap_def Fun.swap_def)
  by fast

lemma to_abmachung_abmachung_to_aenderung_list_induct_helper:
  fixes a :: ‹('person::enum, 'etwas::ordered_ab_group_add) abmachung›
  shows ‹abmachung_dom a ⊆ set ps ⟹ distinct ps ⟹ to_abmachung (abmachung_to_aenderung_list ps a) = a›
  apply(induction ‹ps› arbitrary: ‹a›)
   apply(simp add: abmachung_dom_def)
   apply fastforce
  apply(rename_tac p ps a)
  apply(simp)
  apply(simp add: abmachung_to_aenderung_list_to_abmachung_not_in_ps)
  apply(case_tac ‹p ∉ abmachung_dom a›)
   apply(subgoal_tac ‹abmachung_dom a ⊆ set ps›)
    apply(simp add: abmachung_dom_def; fail)
   apply(simp add: abmachung_dom_def)
   apply blast
  apply(subgoal_tac ‹abmachung_dom (a(p := 0)) ⊆ set ps›)
   prefer 2
   apply(simp add: abmachung_dom_def)
   apply blast
  apply(subgoal_tac ‹to_abmachung (abmachung_to_aenderung_list ps a) = (a(p := 0))›) (*instantiate IH*)
   prefer 2
   apply(simp)
   apply (metis abmachung_to_aenderung_list_not_in_ps)
  apply(simp)
  by fastforce

lemma aenderung_to_abmachung_abmachung_to_aenderung:
  fixes a :: ‹('person::enum, 'etwas::ordered_ab_group_add) abmachung›
  shows ‹aenderung_to_abmachung (abmachung_to_aenderung a) = a›
  apply(simp add: abmachung_to_aenderung_def aenderung_to_abmachung_def)
  apply(rule to_abmachung_abmachung_to_aenderung_list_induct_helper)
   apply(simp add: enum_class.enum_UNIV)
  apply(simp add: enum_class.enum_distinct)
  done
(*>*)



text‹Personen, welche von einer Abmachung betroffen sind.›
definition abmachungs_betroffene :: ‹('person::enum, 'etwas::zero) abmachung ⇒ 'person list›
where
  ‹abmachungs_betroffene a ≡ [p. p ← Enum.enum, a p ≠ 0]›

beispiel ‹abmachungs_betroffene (to_abmachung [Gewinnt Bob (3::int), Verliert Alice 3])
  = [Alice, Bob]› by eval


(*<*)
lemma abmachungs_betroffene_simp: ‹abmachungs_betroffene a = filter (λp. a p ≠ 0) Enum.enum›
proof -
  have ‹concat (map (λp. if a p ≠ 0 then [p] else []) as) = filter (λp. a p ≠ 0) as› for as
    by(induction ‹as›) auto
  thus ‹?thesis›
    by(simp add: abmachungs_betroffene_def)
qed

lemma abmachungs_betroffene_distinct: ‹distinct (abmachungs_betroffene a)›
  apply(simp add: abmachungs_betroffene_simp)
  using enum_class.enum_distinct distinct_filter by blast

lemma abmachungs_betroffene_is_dom: ‹set (abmachungs_betroffene a) = abmachung_dom a›
  by(simp add: abmachung_dom_def abmachungs_betroffene_simp enum_class.enum_UNIV)

lemma set_abmachungs_betroffene_swap:
  ‹set (abmachungs_betroffene (swap p1 p2 a)) = (swap p1 p2 id) ` set (abmachungs_betroffene a)›
  apply(simp add: abmachungs_betroffene_simp enum_class.enum_UNIV)
  apply(simp add: image_def)
  apply(rule Collect_cong)
  apply(simp add: swap_def Fun.swap_def)
  by fast
(*>*)

text‹Eine Abmachung lässt sich ausführen.
Dabei wird effektiv die gegebene \<^term>‹besitz::('person ⇒ 'etwas)› Funktion upgedated.›
definition abmachung_ausfuehren
  :: ‹('person, 'etwas::{plus,minus}) abmachung ⇒ ('person ⇒ 'etwas) ⇒ ('person ⇒ 'etwas)›
where
  ‹abmachung_ausfuehren a besitz ≡ λp. a p + (besitz p)›

beispiel
  ‹abmachung_ausfuehren
    (to_abmachung [Gewinnt Alice 3, Verliert Bob 3])
    (€(Alice:=8, Bob:=3, Eve:= 5))
  = (€(Alice:=11, Bob:=0, Eve:= 5))›
  by(code_simp)


(*<*)
lemma abmachung_ausfuehren_swap:
  ‹abmachung_ausfuehren (swap p1 p2 a) (swap p1 p2 welt)
    = swap p2 p1 (abmachung_ausfuehren a welt)›
  by(auto simp add: abmachung_ausfuehren_def swap_def Fun.swap_def)

lemma aenderung_ausfuehren_abmachung_to_aenderung_induction_helper:
  fixes welt :: ‹'person::enum ⇒ 'etwas::ordered_ab_group_add›
  shows ‹abmachung_dom abmachung ⊆ set ps ⟹ distinct ps ⟹ 
          aenderung_ausfuehren (abmachung_to_aenderung_list ps abmachung) welt p =
            welt p + (abmachung p)›
  apply(induction ‹ps› arbitrary: ‹abmachung› ‹welt›)
   apply(simp add: abmachung_dom_def; fail)
  apply(simp)
  apply(rename_tac pa ps abmachung welt)
  apply(subgoal_tac ‹abmachung_dom (abmachung(pa := 0)) ⊆ set ps›)
   prefer 2
  subgoal
    apply(simp add: abmachung_dom_def)
    by blast
(*thank you sledgehammer isar proofs*)
proof -
  fix pa :: ‹'person› and psa :: ‹'person list› and abmachunga :: ‹'person ⇒ 'etwas› and welta :: ‹'person ⇒ 'etwas›
  assume a1: ‹pa ∉ set psa ∧ distinct psa›
  assume a2: ‹abmachung_dom (abmachunga(pa := 0)) ⊆ set psa›
  assume ‹⋀abmachung welt. abmachung_dom abmachung ⊆ set psa ⟹ aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachung) welt p = (welt p::'etwas) + abmachung p›
  then have f3: ‹⋀f. f p + (abmachunga(pa := 0)) p = aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachunga) f p›
    using a2 a1 by (metis (full_types) abmachung_to_aenderung_list_not_in_ps)
  then have ‹pa = p ⟶ (0 < abmachunga pa ⟶ abmachunga pa ≠ 0 ⟶ aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachunga) ⟦welta (pa += abmachunga pa)⟧ p = welta p + abmachunga p) ∧ (¬ 0 < abmachunga pa ⟶ (abmachunga pa = 0 ⟶ aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachunga) welta p = welta p + abmachunga p) ∧ (abmachunga pa ≠ 0 ⟶ aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachunga) ⟦welta (pa += abmachunga pa)⟧ p = welta p + abmachunga p))›
    by force
  then show ‹(0 < abmachunga pa ⟶ abmachunga pa ≠ 0 ⟶ aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachunga) ⟦welta (pa += abmachunga pa)⟧ p = welta p + abmachunga p) ∧ (¬ 0 < abmachunga pa ⟶ (abmachunga pa = 0 ⟶ aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachunga) welta p = welta p + abmachunga p) ∧ (abmachunga pa ≠ 0 ⟶ aenderung_ausfuehren (abmachung_to_aenderung_list psa abmachunga) ⟦welta (pa += abmachunga pa)⟧ p = welta p + abmachunga p))›
    using f3 by (metis fun_upd_other)
qed


lemma aenderung_ausfuehren_abmachung_to_aenderung:
  fixes welt :: ‹'person::enum ⇒ 'etwas::ordered_ab_group_add›
  shows ‹aenderung_ausfuehren (abmachung_to_aenderung abmachung) welt p = welt p + (abmachung p)›
  apply(simp add: abmachung_to_aenderung_def)
  apply(rule aenderung_ausfuehren_abmachung_to_aenderung_induction_helper)
   apply(simp add: enum_class.enum_UNIV)
  apply(simp add: enum_class.enum_distinct)
  done

(*>*)


text‹Es ist equivalent eine Abmachung oder die entsprechende Änderungsliste auszuführen.›
(*TODO: does this make a good [code] rule? I cannot measure performance changes.*)
lemma abmachung_ausfuehren_aenderung:
  fixes abmachung :: ‹('person::enum, 'etwas::ordered_ab_group_add) abmachung›
  shows ‹abmachung_ausfuehren abmachung = aenderung_ausfuehren (abmachung_to_aenderung abmachung)›
  by(simp add: abmachung_ausfuehren_def fun_eq_iff aenderung_ausfuehren_abmachung_to_aenderung)


subsection‹Konsens›
text‹Laut 🌐‹https://de.wikipedia.org/wiki/Konsens#Konsens_im_Rechtssystem› lässt sich Konsens
wie folgt definieren:
"die Übereinstimmung der Willenserklärungen beider Vertragspartner über die Punkte des Vertrages".
Wir können also \<^term>‹to_abmachung [Gewinnt Alice 3, Verliert Bob 3]› verwenden,
um Konsens zu modellieren.
Dabei müssen alle Betroffenen die gleiche Vorstellung der Abmachung haben.
Beispielsweise lässt sich der gesamte Konsens in einer Welt darstellen als
\<^typ>‹'person ⇒ ('person, 'etwas) abmachung list›, wobei jeder Person genau die Abmachungen
zugeordnet werden, deren sie zustimmt.
Die Abmachungen sind in einer Liste und keiner Menge, da eine Person eventuell bereit ist,
Abmachungen mehrfach auszuführen.
›

type_synonym ('person, 'etwas) globaler_konsens = ‹'person ⇒ ('person, 'etwas) abmachung list›

text‹
Folgendes Beispiel liest sich wie folgt:

\<^term>‹(λ_. [])(
    Alice := [to_abmachung [Gewinnt Alice 3], to_abmachung [Gewinnt Alice 3, Verliert Bob 3]],
    Bob := [to_abmachung [Gewinnt Alice 3, Verliert Bob 3]]) :: (person, int) globaler_konsens›

\<^const>‹Alice› stimmt folgendem zu:
  ▪ \<^const>‹Alice› bekommt 3.
  ▪ \<^const>‹Alice› bekommt 3 und \<^const>‹Bob› muss 3 abgeben.

\<^const>‹Bob› stimmt folgendem zu:
  ▪ \<^const>‹Alice› bekommt 3 und \<^const>‹Bob› muss 3 abgeben.

Wir könnten also sagen, dass Konsens zwischen \<^const>‹Alice› und \<^const>‹Bob› herrscht,
dass 3 Besitz von \<^const>‹Bob› auf \<^const>‹Alice› übergehen.
Zusätzlich wäre es in diesem Beispiel auch okay für \<^const>‹Alice›,
wenn sie 3 Besitz erhalten würde, ohne dass \<^const>‹Bob› 3 Besitz verliert.
›

(*<*)
definition konsensswap
:: ‹'person ⇒ 'person ⇒ ('person, 'etwas) globaler_konsens
    ⇒ ('person, 'etwas) globaler_konsens›
  where
‹konsensswap p1 p2 kons ≡ swap p1 p2 ((map (swap p1 p2)) ∘ kons)›

lemma konsensswap_id[simp]: ‹konsensswap p1 p2 (konsensswap p1 p2 kons) = kons›
  apply(simp add: konsensswap_def)
  apply(subst swap_fun_map_comp_id)
  by simp

lemma konsensswap_sym: ‹konsensswap p1 p2 = konsensswap p2 p1›
  by(simp add: fun_eq_iff konsensswap_def swap_symmetric)

lemma konsensswap_apply:
  ‹konsensswap p1 p2 kons p =  map (swap p1 p2) (swap p1 p2 kons p)›
  apply(simp add: konsensswap_def comp_def)
  by(rule swap_cases, simp_all add: swap_a swap_b swap_nothing)

lemma konsensswap_same[simp]:
  ‹konsensswap p p konsens = konsens›
  by(simp add: konsensswap_def swap_id_comp)

lemma konsensswap_swap_id:
  ‹konsensswap p1 p2 konsens (swap p1 p2 id p) = map (swap p1 p2) (konsens p)›
  apply(simp add: konsensswap_apply)
  by (simp add: swap_fun_swap_id)
(*>*)


text‹Folgendes Prädikat prüft, ob für eine gegebene Abmachung Konsens herrscht.›
definition enthaelt_konsens
  :: ‹('person::enum, 'etwas::zero) abmachung ⇒ ('person, 'etwas) globaler_konsens ⇒ bool›
where
  ‹enthaelt_konsens abmachung konsens ≡ ∀betroffene_person ∈ set (abmachungs_betroffene abmachung).
      abmachung ∈ set (konsens betroffene_person)›

(*<*)
lemma swap_konsensswap_swap:
  ‹swap p2 p1 ` set (konsensswap p1 p2 konsens (swap p1 p2 id p)) =
  (set (konsens p))›
  apply(simp add: konsensswap_apply)
  apply(simp add: swap_fun_swap_id)
  by (simp add: image_comp)

lemma enthaelt_konsens_swap:
  ‹enthaelt_konsens (swap p1 p2 a) (konsensswap p1 p2 konsens) = enthaelt_konsens a konsens› 
  apply(simp add: enthaelt_konsens_def abmachungs_betroffene_is_dom)
  apply(simp add: abmachung_dom_swap)
  apply(rule ball_cong)
   apply(simp; fail)
  by(simp add: swap_in_set_of_functions swap_konsensswap_swap)
(*>*)


text‹Eine (ausgeführte) Abmachung einlösen, bzw. entfernen.›
definition konsens_entfernen
 :: ‹('person::enum, 'etwas::zero) abmachung ⇒ ('person ⇒ ('person, 'etwas) abmachung list)
   ⇒ ('person ⇒ ('person, 'etwas) abmachung list)›
 where
‹konsens_entfernen abmachung kons =
      fold (λp k. k(p := remove1 abmachung (k p))) (abmachungs_betroffene abmachung) kons›


beispiel
  ‹konsens_entfernen
    (to_abmachung [Gewinnt Alice (3::int), Verliert Bob 3])
    ((λ_. [])(
      Alice := [to_abmachung [Gewinnt Alice 3], to_abmachung [Gewinnt Alice 3, Verliert Bob 3]],
      Bob := [to_abmachung [Gewinnt Alice 3, Verliert Bob 3]])
    )
  = (λ_. [])(
    Alice := [to_abmachung [Gewinnt Alice 3]],
    Bob := [])›
  by eval


(*<*)
lemma konsens_entfernen_fold_induct_helper_helper:
  ‹a ∉ set as ⟹ fold (λa k. k(a := f (k a))) as kons a = kons a›
  by(induction ‹as› arbitrary: ‹kons›) simp+
lemma konsens_entfernen_fold_induct_helper:
  ‹x ∈ set as ⟹ distinct as ⟹
         fold (λa k. k(a := f (k a))) as kons x = f (kons x)›
  apply(induction ‹as› arbitrary: ‹kons›)
   apply(simp; fail)
  apply(simp)
  apply(erule disjE)
   apply(simp)
  apply(simp add: konsens_entfernen_fold_induct_helper_helper; fail)
   apply(simp)
  apply blast
  done
(*>*)



text‹Alternative Definition:›
lemma konsens_entfernen_simp:
  ‹konsens_entfernen a kons
    = (λp. if p ∈ set (abmachungs_betroffene a) then remove1 a (kons p) else (kons p))›
  apply(simp add: konsens_entfernen_def fun_eq_iff)
  apply(intro allI conjI impI)
   apply(subst konsens_entfernen_fold_induct_helper, simp_all)
   apply(simp add: abmachungs_betroffene_distinct)
  apply(simp add: konsens_entfernen_fold_induct_helper_helper)
  done


(*<*)  
lemma remove1_konsensswap:
  ‹remove1 (swap p1 p2 a) (konsensswap p1 p2 kons p)
    = map (swap p1 p2) (remove1 a (swap p1 p2 kons p))›
  by(simp add: konsensswap_apply remove1_swap)

lemma konsens_entfernen_konsensswap:
  ‹konsensswap p2 p1 (konsens_entfernen (swap p1 p2 a) (konsensswap p1 p2 kons))
    = konsens_entfernen a kons›
  apply(simp add: konsens_entfernen_simp fun_eq_iff)
  apply(safe)
   apply(simp add: set_abmachungs_betroffene_swap)
   apply(simp add: konsensswap_apply)
   apply(simp add: swap_if_move_inner)
   apply(simp add: swap_id_in_set)
   apply(subst(2) remove1_swap2[of ‹p1› ‹p2›, symmetric])
   apply(auto simp add: konsensswap_apply swap_def Fun.swap_def)[1] (*wants helper*)

  apply(simp add: set_abmachungs_betroffene_swap)
  apply(simp add: konsensswap_apply)
  apply(simp add: swap_if_move_inner)
  apply(simp add: swap_id_in_set)
  apply(simp add: konsensswap_apply swap_def comp_def)
  by (simp add: transpose_commute)

lemma to_abmachung_delta_num_fun_simp_call:
  (*stronger than the usual ordered_ab_group_add*)
  fixes vor::‹('person::enum ⇒ 'etwas::linordered_ab_group_add)›
  shows ‹to_abmachung (delta_num_fun (Handlung vor nach)) p = nach p - vor p›
  apply(simp)
  apply(subst to_abmachung_List_map_filter_enum_simp_call)
  subgoal by(auto simp add: delta_num_def split: if_split_asm)
  by(simp add: delta_num_def)
(*>*)

text‹Folgendes Prädikat prüft ob eine Abmachung korrekt aus dem Konsens entfernt wurde.
Dies sollte normalerweise direkt nachdem eine Abmachung eingelöst wurde geschehen.›
definition konsens_wurde_entfernt
  :: ‹('person::enum, 'etwas::zero) abmachung ⇒
      ('person, 'etwas) globaler_konsens ⇒ ('person, 'etwas) globaler_konsens ⇒ bool›
where
  ‹konsens_wurde_entfernt abmachung konsens_vor konsens_nach ≡
    ∀betroffene_person ∈ set (abmachungs_betroffene abmachung).
       mset (konsens_vor betroffene_person) = mset (abmachung#(konsens_nach betroffene_person))›

text‹Wir müssen hier Multisets (\<^const>‹mset›) verwenden,
da eine Abmachung sowohl mehrfach vorkommen kann aber nur einmal eingelöst wird
und die Reihenfolge in welcher die Abmachungen angeordnet sind egal ist.›
(*TODO: will ich multiset von Anfang an verwenden?*)


text‹Folgendes gilt nicht \<^term>‹konsens_wurde_entfernt a konsens (konsens_entfernen a konsens)›,
da \<^const>‹konsens_entfernen› nur einen existierenden Konsens entfernt.
Sollte der gegebene Konsens nicht existieren passiert nichts!
›
beispiel
‹konsens = (λ_. []) ⟹ a = to_abmachung [Gewinnt Alice (3::int), Verliert Bob 3]
  ⟹ ¬ konsens_wurde_entfernt a konsens (konsens_entfernen a konsens)›
  by(simp, eval)

text‹Wenn wir allerdings Konsens haben, dann verhalten sich \<^const>‹konsens_wurde_entfernt› und
\<^const>‹konsens_entfernen› doch wie erwartet.›
lemma konsens_wurde_entfernt_konsens_entfernen:
  ‹enthaelt_konsens a konsens ⟹ konsens_wurde_entfernt a konsens (konsens_entfernen a konsens)›
  apply(simp add: konsens_wurde_entfernt_def)
  apply(simp add: konsens_entfernen_simp)
  by (simp add: enthaelt_konsens_def)

(*<*)

(*makes the simplifier loop*)
lemma
  ‹add_mset (swap p1 p2 a) (image_mset (swap p1 p2) M) =
     image_mset (swap p1 p2) (add_mset a M)›
  by simp

lemma konsens_wurde_entfernt_swap:
  ‹konsens_wurde_entfernt (swap p1 p2 a) (konsensswap p1 p2 konsens_vor) (konsensswap p1 p2 konsens_nach)
    = konsens_wurde_entfernt a konsens_vor konsens_nach› 
  apply(simp add: konsens_wurde_entfernt_def abmachungs_betroffene_is_dom)
  apply(simp add: abmachung_dom_swap)
  apply(rule ball_cong)
   apply(simp; fail)
  apply(simp add: konsensswap_swap_id)
  (*TODO: wow, ugly*)
  by (metis (no_types, opaque_lifting) comp_apply image_mset_add_mset multiset.map_comp multiset.map_ident_strong swap1)
(*>*)

text‹Gegeben eine Handlung berechnet folgende Funktion die Abmachung,
aus der diese Handlung resultiert haben könnte.›
definition reverse_engineer_abmachung
  :: ‹('person::enum ⇒ 'etwas::linordered_ab_group_add) handlung ⇒ ('person, 'etwas) abmachung›
where
  ‹reverse_engineer_abmachung h ≡
    fold (λp acc. acc(p := (nachher h p) - (vorher h p))) Enum.enum (λ_. 0)›

text‹Sollte die Abmachung vom Typ \<^typ>‹(person, int) abmachung› sein, ist dies eindeutig.›
lemma reverse_engineer_abmachung_delta_num_fun:
  ‹reverse_engineer_abmachung h = to_abmachung (delta_num_fun h)›
  apply(simp add: fun_eq_iff reverse_engineer_abmachung_def)
  apply(cases ‹h›, simp del: delta_num_fun.simps)
  apply(subst to_abmachung_delta_num_fun_simp_call)
  apply(subst fold_enum_fun_update_call)
  by simp

(*<*)
lemma reverse_engineer_abmachung_same:
  ‹reverse_engineer_abmachung (Handlung v v) = (λ_. 0)›
  by(simp add: reverse_engineer_abmachung_def fun_eq_iff fold_enum_fun_update_call)

lemma reverse_engineer_abmachung_swap:
  ‹reverse_engineer_abmachung (Handlung (swap p1 p2 vor) (swap p1 p2 nach)) =
        swap p1 p2 (reverse_engineer_abmachung (Handlung vor nach))›
  by(simp add: fun_eq_iff reverse_engineer_abmachung_def fold_enum_fun_update swap_def)
(*>*)

lemma reverse_engineer_abmachung:
  ‹reverse_engineer_abmachung (Handlung welt welt') = a ⟷ abmachung_ausfuehren a welt = welt'›
  apply(simp add: abmachung_ausfuehren_def fun_eq_iff)
  apply(simp add: reverse_engineer_abmachung_def fold_enum_fun_update_call)
  by (metis add_diff_cancel diff_add_cancel)

end