Theory Zahlenwelt

theory Zahlenwelt
imports BeispielPerson ExecutableHelper Swap SchleierNichtwissen
begin

section‹Zahlenwelt Helper›
text‹In diesem Abschnitt definieren wir Hilfsfunktionen für kommende "Zahlenwelt" Beispiele.›

text‹Wir werden Beispiele betrachten, in denen wir Welten modellieren, in denen jeder Person eine
Zahl zugewiesen wird, Typ \<^typ>‹person ⇒ int›.
Diese Zahl kann zum Beispiel der Besitz oder Wohlstand einer Person sein, oder das Einkommen.
Dabei ist zu beachten,
dass Gesamtbesitz und Einkommen (über einen kurzen Zeitraum) recht unterschiedliche Sachen
modellieren, jedoch den gleichen Typen in unserem Modell haben werden.

Hier sind einige Hilfsfunktionen um mit dem Typ \<^typ>‹person ⇒ int› allgemein zu arbeiten.›

text‹Default: Standardmäßig hat jede Person \<^term>‹0::int›:›
definition DEFAULT :: ‹person ⇒ int› ("€") where
  ‹DEFAULT ≡ λp. 0›

beispiel ‹(DEFAULT(Alice:=8, Bob:=3, Eve:= 5)) Bob = 3› by eval

text‹Beispiel mit fancy Syntax:›
beispiel ‹(€(Alice:=8, Bob:=3, Eve:= 5)) Bob = 3› by eval

text‹Das Beispiel liest sich wie folgt.
Die Welt @{term_type [source=true] ‹(€(Alice:=8, Bob:=3, Eve:= 5)) :: person ⇒ int›} ist eine Funktion von
\<^typ>‹person› nach \<^typ>‹int›.
Wir rufen diese Funktion mit den Parameter \<^const>‹Bob› auf.
Das Ergebnis ist \<^term>‹3::int›.›

text‹Die Funktion @{term [source=true] ‹(€(Alice := 4, Carol := 4))›} lässt sich auch mit Hilfe folgender
Hilfsfunktionen als eine Menge von Tupeln darstellen.›
beispiel ‹show_fun (€(Alice := 4, Carol := 4)) = [(Alice, 4), (Bob, 0), (Carol, 4), (Eve, 0)]› by eval
beispiel ‹show_num_fun (€(Alice := 4, Carol := 4)) = [(Alice, 4), (Carol, 4)]› by eval

text‹Folgende Syntaxabkürzungen erlauben es uns eine einfachere Notation einzuführen,
um den Besitz einer Person zu erhöhen oder zu verringern.›
(* this can produce ambiguous parse trees. So I added those ⟦⟧ *)
abbreviation num_fun_add_syntax ("⟦_ '(_ += _')⟧") where
  ‹⟦f(p += n)⟧ ≡ (f(p := (f p) + n))›

abbreviation num_fun_minus_syntax ("⟦_ '(_ -= _')⟧") where
  ‹⟦f(p -= n)⟧ ≡ (f(p := (f p) - n))›

beispiel ‹⟦€(Alice:=8, Bob:=3, Eve:= 5)(Bob += 4)⟧ Bob = 7› by eval
beispiel ‹⟦€(Alice:=8, Bob:=3, Eve:= 5)(Bob -= 4)⟧ Bob = -1› by eval

text‹Erhöhen und verringern heben sich auf.›
beispiel fixes n:: ‹int› shows ‹⟦⟦f(p += n)⟧(p -= n)⟧ = f› by(simp)


text‹Folgende Funktion wählt diskriminierungsfrei
eine \<^typ>‹'person› eindeutig anhand Ihres Besitzes aus.›
definition opfer_eindeutig_nach_besitz_auswaehlen
  :: ‹int ⇒ ('person ⇒ int) ⇒ 'person list ⇒ 'person option› where
  ‹opfer_eindeutig_nach_besitz_auswaehlen b besitz ps = 
     (case filter (λp. besitz p = b) ps
        of [opfer] ⇒ Some opfer
         | _ ⇒ None)›

(*<*)
lemma case_filter_empty_some_helper:
  ‹(case filter P ps of [] ⇒ Some a | aa # x ⇒ Map.empty x) = Some x
  ⟷ (∀x∈set ps. ¬ P x) ∧ a = x›
  apply(simp add: list.case_eq_if)
  using empty_filter_conv by metis

lemma case_filter_empty_some_helper2:
  ‹(case if P a then a # filter P ps else filter P ps of
        [] ⇒ None | [opfer] ⇒ Some opfer | opfer # aa # x ⇒ Map.empty x) =
       Some x ⟷
  (P a ∧ x = a ∧ filter P ps = []) ∨ (¬P a ∧ filter P ps = [x])›
  apply(cases ‹P a›)
   apply(simp add: case_filter_empty_some_helper)
   apply(metis empty_filter_conv)
  apply(simp)
  apply(cases ‹filter P ps›)
   apply(simp)
  by(simp split: list.split)

lemma case_filter_empty_some_helper3:
  ‹(case filter P ps of [] ⇒ None | [opfer] ⇒ Some opfer
            | opfer # aa # x ⇒ Map.empty x) =
           Some opfer
    ⟷
    filter P ps = [opfer]›
  by(simp split: list.split)

lemma opfer_eindeutig_nach_besitz_auswaehlen_injective:
  ‹opfer_eindeutig_nach_besitz_auswaehlen opfer_nach_besitz besitz ps = Some opfer
  ⟹ inj_on besitz {p ∈ set ps. besitz p = opfer_nach_besitz}›
  apply(simp add: inj_on_def)
  apply(safe)
  apply(induction ‹ps›)
   apply(simp)
  apply(simp)
  apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_def)
  apply(safe)
    apply(simp_all)
    apply(simp add: case_filter_empty_some_helper; fail)
   apply(simp add: case_filter_empty_some_helper)
   apply fastforce
  apply(simp add: case_filter_empty_some_helper3)
  apply(simp add: case_filter_empty_some_helper2[of ‹(λp. besitz p = besitz _)›])
  by (metis (mono_tags) empty_filter_conv)
(*>*)

text‹Folgende Hilfsdefinition definiert eindeutig das Element in einer Einelementigen Menge,
wenn dieses existiert.›
definition the_single_elem :: ‹'a set ⇒ 'a option› where
  ‹the_single_elem s ≡ if card s = 1 then Some (Set.the_elem s) else None›

beispiel ‹the_single_elem {a} = Some a› by(simp add: the_single_elem_def)
beispiel ‹the_single_elem {1::nat,2} = None› by(simp add: the_single_elem_def)
beispiel ‹the_single_elem {} = None› by(simp add: the_single_elem_def)

text‹Hier sehen wir unser Shallow Embedding:
Unsere Definition \<^const>‹the_single_elem› lässt sich komplett auf bereits existierende Konzepte
in HOL reduzieren.›
lemma the_single_elem:
  ‹the_single_elem s = (if is_singleton s then Some (Set.the_elem s) else None)›
  apply(simp add: is_singleton_the_elem the_single_elem_def card_1_singleton_iff)
  by auto

(*<*)
lemma ‹the_single_elem {a} = Some a›
  by(simp add: the_single_elem_def)
lemma ‹a ≠ b ⟹ the_single_elem {a,b} = None›
  by(simp add: the_single_elem_def)


lemma the_single_elem_exhaust:
  ‹(the_single_elem S = None ⟹ P None) ⟹
        (⋀x. the_single_elem S = Some x ⟹ P (Some x)) ⟹ P (the_single_elem S)›
apply(cases ‹the_single_elem S›)
by(auto)
(*>*)


lemma opfer_nach_besitz_induct_step_set_simp: ‹besitz a ≠ opfer_nach_besitz ⟹
  {p. (p = a ∨ p ∈ set ps) ∧ besitz p = opfer_nach_besitz} =
    {p ∈ set ps. besitz p = opfer_nach_besitz}›
  by auto

lemma opfer_eindeutig_nach_besitz_auswaehlen_the_single_elem:
  ‹distinct ps ⟹ 
  opfer_eindeutig_nach_besitz_auswaehlen opfer_nach_besitz besitz ps =
          the_single_elem {p ∈ set ps. besitz p = opfer_nach_besitz}›
proof(simp add: the_single_elem, intro conjI impI)
  show ‹distinct ps ⟹
    is_singleton {p ∈ set ps. besitz p = opfer_nach_besitz} ⟹
    opfer_eindeutig_nach_besitz_auswaehlen opfer_nach_besitz besitz ps =
    Some (the_elem {p ∈ set ps. besitz p = opfer_nach_besitz})›
    apply(induction ‹ps›)
     apply (simp add: is_singleton_altdef; fail)
    apply(simp)
    apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_def)
    apply(simp add: is_singleton_the_elem)
    apply(simp add: case_filter_empty_some_helper case_filter_empty_some_helper3)
    apply(safe)
      apply (metis (mono_tags, lifting) mem_Collect_eq singleton_iff)
     apply (metis (mono_tags, lifting) mem_Collect_eq singleton_iff)
    apply(simp add: opfer_nach_besitz_induct_step_set_simp; fail)
    done
next
  show ‹distinct ps ⟹
    ¬ is_singleton {p ∈ set ps. besitz p = opfer_nach_besitz} ⟹
    opfer_eindeutig_nach_besitz_auswaehlen opfer_nach_besitz besitz ps = None›
    apply(induction ‹ps›)
     apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_def; fail)
    apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_def)
    apply(safe)
     apply(simp split: list.split)
     apply(simp add: filter_empty_conv is_singleton_def)
     apply blast
    by(simp add: opfer_nach_besitz_induct_step_set_simp)
qed

lemma opfer_eindeutig_nach_besitz_auswaehlen_the_single_elem_enumall:
  ‹opfer_eindeutig_nach_besitz_auswaehlen opfer_nach_besitz besitz enum_class.enum =
          the_single_elem {p. besitz p = opfer_nach_besitz}›
  apply(subst opfer_eindeutig_nach_besitz_auswaehlen_the_single_elem)
  using enum_class.enum_distinct apply(simp)
  apply(simp add: enum_class.enum_UNIV)
  done


(*<*)
lemma ‹p1 ∈ Ps ⟹ p2 ∈ Ps ⟹
  {pa ∈ Ps. swap p1 p2 besitz pa = b} = {p2} ⟷ {pa ∈ Ps. besitz pa = b} = {p1}›
  apply(simp add: singleton_set_to_all)
  by (metis swap_b swap_nothing swap_symmetric)

lemma the_elem_singleton_swap:
  ‹p1 ∈ Ps ⟹
    p2 ∈ Ps ⟹
    the_elem {pa ∈ Ps. swap p1 p2 besitz pa = b} = p2 ⟹
    is_singleton {pa ∈ Ps. swap p1 p2 besitz pa = b} ⟹
    is_singleton {pa ∈ Ps. besitz pa = b} ⟹ the_elem {pa ∈ Ps. besitz pa = b} = p1›
  apply(simp add: is_singleton_the_elem_as_set)
  apply(elim is_singletonE)
  apply(simp add: singleton_set_to_all)
  by (metis swap_b)

lemma the_elem_singleton_swap_none:
    ‹p1 ∈ set ps ⟹
    p2 ∈ set ps ⟹
    the_elem {pa ∈ set ps. swap p1 p2 besitz pa = p} ≠ p2 ⟹
    the_elem {pa ∈ set ps. swap p1 p2 besitz pa = p} ≠ p1 ⟹
    is_singleton {pa ∈ set ps. besitz pa = p} ⟹
    is_singleton {pa ∈ set ps. swap p1 p2 besitz pa = p} ⟹
    the_elem {pa ∈ set ps. swap p1 p2 besitz pa = p} = the_elem {pa ∈ set ps. besitz pa = p}›
  apply(rule arg_cong[of _ _ ‹the_elem›])
  apply(rule Collect_cong)
  apply(elim is_singletonE)
  apply(simp add: is_singleton_the_elem_as_set)
  apply(simp add: singleton_set_to_all)
  by (metis swap_nothing)
  

lemma set_swap_image_pullout:
  ‹p1 ∈ A ⟹
   p2 ∈ A ⟹
    {a ∈ A. swap p1 p2 besitz a = b} = swap p1 p2 id ` {a ∈ A. besitz a = b}›
  apply(simp add: image_def)
  apply(rule Collect_cong)
  apply(safe)
    apply(rule swap_cases)
      apply(rule_tac x=‹p2› in exI, simp add: swap_a swap_b; fail)
     apply(rule_tac x=‹p1› in exI, simp add: swap_a swap_b; fail)
    apply(rule_tac x=‹a› in exI, simp add: swap_a swap_b swap_nothing; fail)
   apply(rule swap_cases, simp_all add: swap_a swap_b swap_nothing)
  by (simp add: swap_fun_swap_id)

lemma is_singleton_swap:
  ‹p1 ∈ set ps ⟹
   p2 ∈ set ps ⟹
    is_singleton {pa ∈ set ps. swap p1 p2 besitz pa = p}
    ⟷ is_singleton {pa ∈ set ps. besitz pa = p}›
  apply(simp add: set_swap_image_pullout)
  apply(rule is_singleton_bij_image)
  by (simp add: involuntory_imp_bij swap_fun_swap_id)
 

lemma if_swap_person_help_same: ‹p1 = a ⟹
       p2 = a ⟹
       (λp. if p = a then p2 else if p = p2 then p1 else p) = id›
  by auto


(*TODO: das if will in ne definition*)
lemma opfer_eindeutig_nach_besitz_auswaehlen_swap:
    ‹p1 ∈ set ps ⟹
     p2 ∈ set ps ⟹
     distinct ps ⟹
  map_option
        (λp. if p = p1 then p2 else if p = p2 then p1 else p)
        (opfer_eindeutig_nach_besitz_auswaehlen p (swap p1 p2 besitz) ps)
  = opfer_eindeutig_nach_besitz_auswaehlen p besitz ps›
  apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_the_single_elem)
  apply(simp add: the_single_elem)
  apply(safe, simp_all add: swap_a swap_b swap_nothing is_singleton_swap)
    apply(rule sym)
    apply(rule the_elem_singleton_swap, simp_all)
    apply(simp add: is_singleton_swap; fail)
   apply(rule sym)
   apply(rule the_elem_singleton_swap, simp_all)
    apply(simp add: swap_symmetric; fail)
   apply(simp add: is_singleton_swap; fail)
  apply(rule the_elem_singleton_swap_none, simp_all)
  using is_singleton_swap by fast

lemma opfer_eindeutig_nach_besitz_auswaehlen_swap_alt:
  ‹p1 ∈ set ps ⟹
   p2 ∈ set ps ⟹
   distinct ps ⟹
   opfer_eindeutig_nach_besitz_auswaehlen p (swap p1 p2 besitz) ps =
     map_option (λp. if p = p1 then p2 else if p = p2 then p1 else p)
       (opfer_eindeutig_nach_besitz_auswaehlen p besitz ps)›
  using opfer_eindeutig_nach_besitz_auswaehlen_swap[of ‹p1› ‹ps› ‹p2› ‹p› ‹(swap p1 p2 besitz)›, simplified swap1]
  by simp

lemma opfer_eindeutig_nach_besitz_auswaehlen_swap_enumall:
‹opfer_eindeutig_nach_besitz_auswaehlen p (swap p1 p2 besitz) enum_class.enum =
  map_option (λp. if p = p1 then p2 else if p = p2 then p1 else p)
    (opfer_eindeutig_nach_besitz_auswaehlen p besitz enum_class.enum)›
  apply(rule opfer_eindeutig_nach_besitz_auswaehlen_swap_alt)
  using enum_class.in_enum enum_class.enum_distinct by auto

lemma opfer_eindeutig_nach_besitz_auswaehlen_swap_None:
  ‹opfer_eindeutig_nach_besitz_auswaehlen p (swap p1 p2 welt) enum_class.enum = None
    ⟷
   opfer_eindeutig_nach_besitz_auswaehlen p welt enum_class.enum = None›
  by(simp add: opfer_eindeutig_nach_besitz_auswaehlen_swap_enumall)

lemma the_single_elem_None_swap:
  ‹the_single_elem {p. x p = a} = None ⟹
       the_single_elem {p. swap p1 p2 x p = a} = None›
  apply(simp add: the_single_elem split: if_split_asm)
  apply(simp add: is_singleton_def)
  apply(safe)
  apply(simp add: singleton_set_to_all2)
  by (metis swap_a swap_b swap_nothing)

lemma the_single_elem_Some_Some_swap:
  ‹the_single_elem {p. x p = a} = Some s1 ⟹
      the_single_elem {p. swap s1 p2 x p = a} = Some s2 ⟹ p2 = s2›
  apply(simp add: the_single_elem is_singleton_the_elem split: if_split_asm)
  by (metis empty_iff insert_iff mem_Collect_eq swap_a swap_nothing)
lemma the_single_elem_Some_ex_swap:
  ‹the_single_elem {p. x p = a} = Some x2 ⟹ ∃y. the_single_elem {p. swap p1 p2 x p = a} = Some y›
  apply(case_tac ‹the_single_elem {p. swap p1 p2 x p = a}›)
   apply(simp)
  using the_single_elem_None_swap apply (metis option.distinct(1) swap2)
  by simp

lemma the_single_elem_Some_swap:
  ‹the_single_elem {p. x p = a} = Some s ⟹
      the_single_elem {p. swap s p2 x p = a} = Some p2›
  using the_single_elem_Some_ex_swap the_single_elem_Some_Some_swap by fastforce
(*>*)

fun stehlen :: ‹int ⇒ int ⇒ 'person::enum ⇒ ('person ⇒ int) ⇒ ('person ⇒ int) option› where
  ‹stehlen beute opfer_nach_besitz dieb besitz =
    (case opfer_eindeutig_nach_besitz_auswaehlen opfer_nach_besitz besitz Enum.enum
       of None ⇒ None
        | Some opfer ⇒ if opfer = dieb then None else Some ⟦⟦besitz(opfer -= beute)⟧(dieb += beute)⟧
    )›

lemma wohlgeformte_handlungsabsicht_stehlen:
  ‹wohlgeformte_handlungsabsicht swap welt (Handlungsabsicht (stehlen n p))›
    apply(simp add: wohlgeformte_handlungsabsicht.simps)
    apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_swap_enumall)
    apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_the_single_elem_enumall)
    apply(simp add: the_single_elem)
    apply(safe)
     apply (simp add: swap_def Fun.swap_def; fail)
  by (simp add: fun_upd_twist swap_def Fun.swap_def)


(*<*)
lemma stehlen_swap_None:
  ‹stehlen n opf p2 (swap p1 p2 welt) = None
    ⟷
   stehlen n opf p1 welt = None›
  apply(simp split: option.split)
  apply(simp add: opfer_eindeutig_nach_besitz_auswaehlen_swap_None)
  by(auto simp add: opfer_eindeutig_nach_besitz_auswaehlen_swap_enumall)

declare stehlen.simps[simp del]
(*>*)


definition aufsummieren :: ‹('person::enum ⇒ int) ⇒ int› where
  ‹aufsummieren besitz = sum_list (map besitz Enum.enum)›

lemma ‹aufsummieren (besitz :: person⇒int) = (∑p←[Alice,Bob,Carol,Eve]. besitz p)›
  by(simp add: aufsummieren_def enum_person_def)

lemma ‹aufsummieren (€(Alice := 4, Carol := 8)) = 12› by eval
lemma ‹aufsummieren (€(Alice := 4, Carol := 4)) = 8› by eval

lemma aufsummieren_swap:
  ‹aufsummieren (swap p1 p2 welt) = aufsummieren welt›
  apply(simp add: aufsummieren_def)
  apply(rule sum_list_swap)
  using enum_class.in_enum enum_class.enum_distinct by auto







lemma list_not_empty_iff_has_element: ‹as ≠ [] ⟷ (∃a. a ∈ set as)›
  by (simp add: ex_in_conv)

lemma enum_class_not_empty_list: ‹enum_class.enum ≠ []›
  using enum_class.in_enum list_not_empty_iff_has_element by blast

lemma alles_kaputt_machen_code_help:
  ‹(λ_. Min (range x) - 1) = (λ_. min_list (map x enum_class.enum) - 1)›
  apply(subst min_list_Min)
   apply(simp add: enum_class_not_empty_list; fail)
  apply(simp)
  apply(simp add: enum_UNIV)
  done




text‹\<^const>‹swap› funktioniert auch auf Mengen.›
lemma ‹(swap Alice Carol id) ` {Alice, Bob} = {Carol, Bob}› by eval


end