Theory BeispielZahlenwelt2

theory BeispielZahlenwelt2
imports Zahlenwelt BeispielPerson Aenderung KategorischerImperativ
begin

section‹Beispiel: Zahlenwelt2›
text‹In diesem Abschnitt werden wir ein weiteres Beispiel sehen.›

text‹Dieses Beispiel ist ähnlich zum Beispiel Zahlenwelt in Abschnitt \ref{sec:bspzahlenwelt}.
Allerdings führen wir einige Erweiterungen ein:
  ▪ Jeder Person wird weiterhin ihr Besitz zugeordnet.
  ▪ Neben dem Besitz gibt es auch ein Modell von Konsens.
    Dabei soll Konsens die Liste aller bereits getroffenen Abmachungen darstellen,
    bzw modellieren, zu was die Leute bereit wären.
    So lässt sich beispielsweise Schenken (Besitzübergang mit Konsens)
    von Stehlen (Besitzübergang ohne Konsens) unterscheiden.
  ▪ Es gibt eine spezielle Entität, nämlich den Staat.
    Diese Entität ist nicht in der Menge der natürlichen Personen enthalten.
    Dies erlaubt es z.B. den Staat in Handlungsabsichten hardzucoden und
    gleichzeitig eine wohlgeformte Handlungsabsicht zu haben.
    TODO: machen
  ▪ Als weitere spezielle Entität wird die Umwelt eingeführt.
›

record zahlenwelt =
  besitz :: ‹person ⇒ int›
  konsens :: ‹(person, int) globaler_konsens›
  staatsbesitz :: ‹int› ―‹Der Staat ist keine natürliche Person und damit besonders.›
  umwelt :: ‹int›

definition initialwelt :: ‹zahlenwelt›
  where
‹initialwelt ≡ ⦇
  besitz = (€(Alice := 5, Bob := 10, Carol := -3)),
  konsens = (λ_. [])(
    Alice := [to_abmachung [Gewinnt Alice 3], to_abmachung [Gewinnt Alice 3, Verliert Bob 3]],
    Bob := [to_abmachung [Gewinnt Alice 3, Verliert Bob 3]]),
  staatsbesitz = 9000,
  umwelt = 600
 ⦈›



text‹Mein persönlicher Besitz:›
fun meins :: ‹person ⇒ zahlenwelt ⇒ int› where
  ‹meins p welt = (besitz welt) p›

beispiel ‹meins Carol initialwelt = -3› by eval

(*<*)
definition zahlenwps :: ‹person ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt› where
  ‹zahlenwps p1 p2 welt = 
      welt⦇ besitz := swap p1 p2 (besitz welt),
            konsens := konsensswap p1 p2 (konsens welt) ⦈›


beispiel ‹zahlenwps Alice Bob initialwelt
= ⦇
  besitz = (€(Alice := 10, Bob := 5, Carol := -3)),
  konsens = (λ_. [])(
    Alice := [to_abmachung [Gewinnt Bob 3, Verliert Alice 3]],
    Bob := [to_abmachung [Gewinnt Bob 3], to_abmachung [Gewinnt Bob 3, Verliert Alice 3]]),
  staatsbesitz = 9000,
  umwelt = 600
 ⦈› by eval


beispiel ‹zahlenwps Alice Carol initialwelt
= ⦇
  besitz = (€(Alice := -3, Bob := 10, Carol := 5)),
  konsens = (λ_. [])(
    Bob := [to_abmachung [Gewinnt Carol 3, Verliert Bob 3]],
    Carol := [to_abmachung [Gewinnt Carol 3], to_abmachung [Gewinnt Carol 3, Verliert Bob 3]]),
  staatsbesitz = 9000,
  umwelt = 600
 ⦈› by eval

(*<*)
lemma zahlenwps_id: ‹zahlenwps p1 p2 (zahlenwps p1 p2 welt) = welt›
  by(simp add: zahlenwps_def)

lemma zahlenwps_sym: ‹zahlenwps p1 p2 = zahlenwps p2 p1›
  apply(simp add: fun_eq_iff zahlenwps_def)
  by (simp add: swap_symmetric konsensswap_sym)

lemma zahlenwps_same: ‹zahlenwps p p w = w›
  by(cases ‹w›, simp add: zahlenwps_def)

lemma besitz_zahlenwps[simp]: ‹besitz (zahlenwps p1 p2 welt) = swap p1 p2 (besitz welt)›
  by(simp add: zahlenwps_def)

lemma besitz_zahlenwps_apply: ‹besitz (zahlenwps p1 p2 welt) p2 = besitz welt p1›
  by (simp add: swap_b)

lemma besitz_zahlenwps_nothing: ‹pX ≠ p1 ⟹
       pX ≠ p2 ⟹
       besitz (zahlenwps p1 p2 welt) pX = besitz welt pX›
  by (simp add: swap_nothing)
(*>*)


definition enthaelt_konsens :: ‹(person, int) abmachung ⇒ zahlenwelt ⇒ bool›
where
  ‹enthaelt_konsens abmachung welt ≡ Aenderung.enthaelt_konsens abmachung (konsens welt)›

lemma enthaelt_konsens_swap:
  ‹enthaelt_konsens (swap p1 p2 a) (zahlenwps p1 p2 welt) = enthaelt_konsens a welt› 
  by(simp add: enthaelt_konsens_def zahlenwps_def Aenderung.enthaelt_konsens_swap)
(*>*)


text‹Wenn \<^const>‹reverse_engineer_abmachung› hier nicht genau die gleiche Abmachung
berechnet wie später eingelöst, dann wird das ganze exploitable.
Da eine \<^typ>‹('person, 'etwas) abmachung› aber eine eindeutige Darstellung sein sollte,
müsst das so funktionieren.›
definition einvernehmlich :: ‹zahlenwelt handlung ⇒ bool›
where
  ‹einvernehmlich h ≡
    let abmachung = reverse_engineer_abmachung (map_handlung besitz h)
    in enthaelt_konsens abmachung (vorher h)
        ∧ konsens_wurde_entfernt abmachung (konsens (vorher h)) (konsens (nachher h))›
(*TODO: hier will konsens_wurde_entfernt dazu? Neuer name! Einvernehmlich?*)


(*<*)
lemma einvernehmlich_swap:
  ‹einvernehmlich (map_handlung (zahlenwps p1 p2) h) = einvernehmlich h›
  apply(cases ‹h›, rename_tac vor nach, simp)
  apply(simp add: einvernehmlich_def)
  apply(case_tac ‹vor›, case_tac ‹nach›, simp add: zahlenwps_def)
  apply(simp add: reverse_engineer_abmachung_swap)
  apply(simp add: Aenderung.enthaelt_konsens_swap BeispielZahlenwelt2.enthaelt_konsens_def)
  apply(simp add: konsens_wurde_entfernt_swap)
  by metis (*wtf?*)

lemma einvernehmlich_swap_nachher_handeln:
  ‹einvernehmlich (Handlung (zahlenwps p1 p2 welt) (nachher_handeln p1 (zahlenwps p1 p2 welt) ha)) =
    einvernehmlich (Handlung welt (zahlenwps p1 p2 (nachher_handeln p1 (zahlenwps p2 p1 welt) ha)))›
  apply (metis (no_types, opaque_lifting) handlung.map einvernehmlich_swap zahlenwps_id zahlenwps_sym)
  done

lemma einvernehmlich_noop: ‹einvernehmlich (Handlung welt welt)›
  apply(simp add: einvernehmlich_def reverse_engineer_abmachung_same)
  by(code_simp)

lemma nicht_ausfuehrbar_einvernehmlich:
  ‹¬ ausfuehrbar p welt ha ⟹ einvernehmlich (handeln p welt ha)›
  apply(simp add: handeln_def nicht_ausfuehrbar_nachher_handeln einvernehmlich_noop)
  done
(*>*)


text‹Eine Handlung die keine Änderung bewirkt hat keine Betroffenen und damit immer Konsens.›
lemma ‹einvernehmlich (handeln p welt (Handlungsabsicht (λp w. Some w)))›
  apply(simp add: einvernehmlich_def Let_def)
  apply(simp add: handeln_def nachher_handeln.simps reverse_engineer_abmachung_same)
  apply(code_simp)
  done
  
beispiel
  ‹einvernehmlich (handeln Alice initialwelt
    (Handlungsabsicht (λp w. Some
       (w⦇ besitz := ⟦⟦(besitz w)(Alice += 3)⟧(Bob -= 3)⟧,
           konsens := konsens_entfernen (to_abmachung [Gewinnt Alice (3::int), Verliert Bob 3]) (konsens w) ⦈))))›
  by eval
beispiel ‹¬ einvernehmlich (handeln Alice initialwelt
          (Handlungsabsicht (λp w. Some (w⦇ besitz := ⟦⟦(besitz w)(Alice += 3)⟧(Bob -= 3)⟧ ⦈))))›
  by eval
beispiel ‹¬ einvernehmlich (handeln Alice initialwelt
          (Handlungsabsicht (λp w. Some (w⦇ besitz := ⟦⟦(besitz w)(Alice += 4)⟧(Bob -= 4)⟧ ⦈))))›
  by eval



definition abmachung_ausfuehren
  :: ‹(person, int) abmachung ⇒ zahlenwelt ⇒ zahlenwelt›
where
  ‹abmachung_ausfuehren abmachung welt ≡
    welt⦇ besitz := Aenderung.abmachung_ausfuehren abmachung (besitz welt) ⦈›

beispiel ‹abmachung_ausfuehren (to_abmachung [Gewinnt Alice 3]) initialwelt
  = initialwelt⦇ besitz := ⟦(besitz initialwelt)(Alice += 3)⟧⦈›
  by eval


text‹Um eine \<^typ>‹(person, int) abmachung› einzulösen wird diese erst ausgeführt
und danach aus dem globalen Konsens entfernt, damit die Abmachung
nicht mehrfach eingelöst werden kann.›
definition abmachung_einloesen :: ‹(person, int) abmachung ⇒ zahlenwelt ⇒ zahlenwelt option› where
  ‹abmachung_einloesen delta welt ≡ 
  if enthaelt_konsens delta welt
  then Some ((abmachung_ausfuehren delta welt)⦇ konsens := konsens_entfernen delta (konsens welt)⦈)
  else None›


beispiel ‹abmachung_einloesen (to_abmachung [Gewinnt Alice 3, Verliert Bob 3]) initialwelt
 = Some
  ⦇
    besitz = (€(Alice := 8, Bob := 7, Carol := -3)),
    konsens = (λ_. [])(
      Alice := [to_abmachung [Gewinnt Alice 3]],
      Bob := []),
    staatsbesitz = 9000,
    umwelt = 600
   ⦈›
  by eval

beispiel ‹abmachung_einloesen (to_abmachung [Gewinnt Alice 3]) initialwelt
 = Some
  ⦇
    besitz = (€(Alice := 8, Bob := 10, Carol := -3)),
    konsens = (λ_. [])(
      Alice := [to_abmachung [Gewinnt Alice 3, Verliert Bob 3]],
      Bob := [to_abmachung [Gewinnt Alice 3, Verliert Bob 3]]),
    staatsbesitz = 9000,
    umwelt = 600
   ⦈›
  by eval

beispiel ‹abmachung_einloesen (to_abmachung [Verliert Bob 3]) initialwelt = None›
  by eval

(*<*)
lemma abmachung_einloesen_some_entahelt_konsens:
  ‹abmachung_einloesen a welt = Some welt' ⟹ enthaelt_konsens a welt›
  by(simp add: abmachung_einloesen_def split: if_split_asm)

lemma abmachung_einloesen_reverse_engineer:
  ‹abmachung_einloesen a welt = Some welt'
    ⟹ reverse_engineer_abmachung (Handlung (besitz welt) (besitz welt')) = a›
  apply(simp add: abmachung_einloesen_def split: if_split_asm)
  apply(simp add: abmachung_ausfuehren_def)
  apply(simp add: reverse_engineer_abmachung)
  by force

lemma zahlenwelt_abmachung_ausfuehren_swap:
  ‹(BeispielZahlenwelt2.abmachung_ausfuehren (swap p1 p2 a) (zahlenwps p1 p2 welt)) =
       zahlenwps p2 p1 (BeispielZahlenwelt2.abmachung_ausfuehren a welt)›
    apply(simp add: BeispielZahlenwelt2.abmachung_ausfuehren_def)
  by(simp add: zahlenwps_def abmachung_ausfuehren_swap konsensswap_sym)

lemma abmachung_einloesen_zahlenwps_pullout:
  ‹abmachung_einloesen (swap p1 p2 a) (zahlenwps p1 p2 welt)
    = map_option (zahlenwps p2 p1) (abmachung_einloesen a welt)›
  apply(simp add: abmachung_einloesen_def enthaelt_konsens_swap)
  apply(clarsimp)
  apply(simp add: zahlenwelt_abmachung_ausfuehren_swap)
  apply(simp add: zahlenwps_def konsens_entfernen_konsensswap)
  by (metis konsens_entfernen_konsensswap konsensswap_id)
(*>*)


text‹Die Handlungsabsicht \<^const>‹abmachung_einloesen› stellt keine
\<^const>‹wohlgeformte_handlungsabsicht› dar, da in der Abmachung Personen
hardcedoded sind.
›
beispiel ‹¬ wohlgeformte_handlungsabsicht zahlenwps initialwelt
         (Handlungsabsicht (λp w. abmachung_einloesen (to_abmachung [Gewinnt Alice 3]) w))›
  by eval


text‹Wir können aber schnell eine wohlgeformte Handlungsabsicht daraus bauen,
indem wir nicht die Abmachung an sich in die Handlungsabsicht hardcoden,
sondern indem wir eine bestehende Abmachung in der Welt referenzieren.›
definition existierende_abmachung_einloesen :: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
  ‹existierende_abmachung_einloesen p welt ≡ 
  case (konsens welt) p
  of [] ⇒ None
  |  d#_ ⇒ abmachung_einloesen d welt›

lemma ‹wohlgeformte_handlungsabsicht zahlenwps initialwelt
         (Handlungsabsicht existierende_abmachung_einloesen)›
  by eval

(*<*)

lemma existierende_abmachung_einloesen_map_zahlenwps:
  ‹map_option (zahlenwps p2 p1) (existierende_abmachung_einloesen p2 (zahlenwps p1 p2 welt)) =
    existierende_abmachung_einloesen p1 welt›
  apply(simp add: existierende_abmachung_einloesen_def)
  apply(simp add: zahlenwps_def swap_b konsensswap_def)
  apply(case_tac ‹konsens welt p1›)
   apply(simp; fail)
  apply(simp)
  using abmachung_einloesen_zahlenwps_pullout
  by (metis swap2 swap_symmetric zahlenwps_id)

lemma existierende_abmachung_einloesen_zahlenwps_pullout:
  ‹existierende_abmachung_einloesen p (zahlenwps p1 p2 welt)
    = map_option (zahlenwps p2 p1) (existierende_abmachung_einloesen (swap p1 p2 id p) welt)›
  apply(cases ‹p = p1›)
  apply(simp add: swap_a)
  apply (metis existierende_abmachung_einloesen_map_zahlenwps zahlenwps_id)
  apply(cases ‹p = p2›)
  apply(simp add: swap_b)
   apply (metis existierende_abmachung_einloesen_map_zahlenwps zahlenwps_id zahlenwps_sym)
  apply(simp add: swap_nothing)

  apply(simp add: existierende_abmachung_einloesen_def)
  apply(simp add: zahlenwps_def konsensswap_def swap_nothing)
  apply(case_tac ‹konsens welt p›)
   apply(simp; fail)
  apply(simp)
  using abmachung_einloesen_zahlenwps_pullout by simp
(*>*)

text‹In jeder Welt ist damit die Handlungsabsicht wohlgeformt.›
lemma wohlgeformte_handlungsabsicht_existierende_abmachung_einloesen:
  ‹wohlgeformte_handlungsabsicht zahlenwps welt
         (Handlungsabsicht existierende_abmachung_einloesen)›
  apply(simp add: wohlgeformte_handlungsabsicht.simps)
  apply(cases ‹welt›, simp)
  using existierende_abmachung_einloesen_map_zahlenwps by simp



text‹Es ist nur möglich eine \<^const>‹existierende_abmachung_einloesen›,
wenn alle Betroffenen auch zustimmen.
Es is beispielsweise nicht möglich, dass \<^const>‹Alice› eine Handlung
ausführt, die \<^const>‹Carol› betrifft, ohne deren Zustimmung.›
beispiel ‹¬ ausfuehrbar Alice
  ⦇
    besitz = (€(Alice := 5, Bob := 10, Carol := -3)),
    konsens = (λ_. [])(
      Alice := [to_abmachung [Verliert Carol 3]]
      ),
    staatsbesitz = 9000,
    umwelt = 600
  ⦈
  (Handlungsabsicht existierende_abmachung_einloesen)›
  by eval
text‹Nur wenn \<^const>‹Carol› zustimmt wird die Handlung möglich.›
beispiel ‹ausfuehrbar Alice
  ⦇
    besitz = (€(Alice := 5, Bob := 10, Carol := -3)),
    konsens = (λ_. [])(
      Alice := [to_abmachung [Verliert Carol 3]],
      Carol := [to_abmachung [Verliert Carol 3]]
      ),
    staatsbesitz = 9000,
    umwelt = 600
  ⦈
  (Handlungsabsicht existierende_abmachung_einloesen)›
  by eval

(*bissal doof:*)
text‹Da \<^const>‹Alice› nicht betroffen is, bleibt \<^term>‹[Verliert Carol 3]› bei \<^const>‹Alice› übrig.›
beispiel ‹nachher_handeln Alice
  ⦇
    besitz = (€(Alice := 5, Bob := 10, Carol := -3)),
    konsens = (λ_. [])(
      Alice := [to_abmachung [Verliert Carol 3]],
      Carol := [to_abmachung [Verliert Carol 3]]
      ),
    staatsbesitz = 9000,
    umwelt = 600
  ⦈
  (Handlungsabsicht existierende_abmachung_einloesen)
= ⦇
    besitz = (€(Alice := 5, Bob := 10, Carol := -6)),
    konsens = (λ_. [])(
      Alice := [to_abmachung [Verliert Carol 3]],
      Carol := []
      ),
    staatsbesitz = 9000,
    umwelt = 600
  ⦈›
  by eval


text‹Für\<^const>‹existierende_abmachung_einloesen› gilt immer \<^const>‹einvernehmlich›.
Das \<^const>‹reverse_engineer_abmachung› macht also das Richtige.›
lemma einvernehmlich_existierende_abmachung_einloesen:
  ‹einvernehmlich (handeln p welt (Handlungsabsicht existierende_abmachung_einloesen))›
  apply(simp add: einvernehmlich_def handeln_def nachher_handeln.simps)
  apply(cases ‹existierende_abmachung_einloesen p welt›)
  apply(simp)
  using einvernehmlich_def einvernehmlich_noop apply fastforce
  apply(simp)
  apply(rename_tac welt')
  apply(simp add: existierende_abmachung_einloesen_def split:list.split_asm)
  apply(frule abmachung_einloesen_some_entahelt_konsens)
  apply(simp add: abmachung_einloesen_reverse_engineer)
  using BeispielZahlenwelt2.enthaelt_konsens_def abmachung_einloesen_def
    konsens_wurde_entfernt_konsens_entfernen by fastforce

fun stehlen :: ‹int ⇒ int ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt option› where
  ‹stehlen beute opfer_nach_besitz dieb welt =
        map_option (λb. welt⦇besitz := b⦈) (Zahlenwelt.stehlen beute opfer_nach_besitz dieb (besitz welt))›

beispiel‹stehlen 3 10 Alice initialwelt =
Some ⦇
  besitz = (€(Alice := 8, Bob := 7, Carol := -3)),
  konsens = (λ_. [])(
    Alice := [to_abmachung [Gewinnt Alice 3], to_abmachung [Gewinnt Alice 3, Verliert Bob 3]],
    Bob := [to_abmachung [Gewinnt Alice 3, Verliert Bob 3]]),
  staatsbesitz = 9000,
  umwelt = 600
 ⦈› by eval

text‹\<^const>‹stehlen› und \<^const>‹existierende_abmachung_einloesen› können ununterscheidbar sein,
was den \<^const>‹besitz› betrifft.
Der Hauptunterschied ist, ob \<^const>‹konsens› eingelöst wurde oder nicht.›
beispiel
 ‹besitz (the (stehlen 3 10 Alice initialwelt)) =
  besitz (the (existierende_abmachung_einloesen Bob initialwelt))›
 ‹konsens (the (stehlen 3 10 Alice initialwelt)) ≠
  konsens (the (existierende_abmachung_einloesen Bob initialwelt))›
  by code_simp+

(*<*)
lemma besitz_sel_update: ‹map_option besitz (map_option (λb. w⦇besitz := b⦈) b) = b›
  apply(cases ‹b›)
   apply(simp; fail)
  apply(simp)
  done

lemma wohlgeformte_handlungsabsicht_stehlen:
  ‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht (stehlen n p))›
  apply(rule wfh_generalize_worldI[OF wohlgeformte_handlungsabsicht_stehlen,
        where sel=‹besitz›
        and makeZ=‹λb other. case other of (k, s, u) ⇒ zahlenwelt.make b k s u›
        and sel_other=‹λw. (konsens w, staatsbesitz w, umwelt w)›
        , of ‹welt› ‹besitz welt› _ ‹n› ‹p›])
          apply(simp; fail)
         apply(simp add: zahlenwps_def; fail)
        apply(simp add: besitz_sel_update; fail)
       apply(case_tac ‹w›, simp add: zahlenwelt.defs; fail)
      apply(simp, force)
     apply(simp add: stehlen_swap_None; fail)
    apply(simp add: zahlenwelt.defs zahlenwps_def; fail)
   apply(simp add: zahlenwps_id zahlenwps_sym; fail)
  apply(simp add: zahlenwps_sym; fail)
  done
(* I case above proof fails, here is a version without wfh_generalize_worldI.
(*This is mostly a copy of wohlgeformte_handlungsabsicht_stehlen and this sucks.*)
  apply(case_tac ‹welt›, simp add: wohlgeformte_handlungsabsicht.simps Zahlenwelt.stehlen.simps)
  apply(simp add: zahlenwps_def)
  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: zahlenwps_def swap_def Fun.swap_def konsensswap_sym; fail)
  apply (simp add: zahlenwps_def swap_def Fun.swap_def konsensswap_sym fun_upd_twist)
  done
*)
(*>*)

text‹Ressourcen können nicht aus dem Nichts erschaffen werden.
Diese Handlungsabsicht entnimmt der Natur und weist einer Person zu.›
fun abbauen :: ‹nat ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt option› where
  ‹abbauen i p welt = Some (welt⦇ besitz := ⟦(besitz welt)(p += int i)⟧, umwelt := (umwelt welt) - int i ⦈)›

(*<*)
lemma wohlgeformte_handlungsabsicht_abbauen:
  ‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht (abbauen n))›
  apply(case_tac ‹welt›, simp add: wohlgeformte_handlungsabsicht.simps)
  apply(simp add: zahlenwps_def swap_def Fun.swap_def)
  by (simp add: konsensswap_sym)
(*>*)


text‹Diese Handlungsabsicht weist allen Personen ein Besitz von 0 zu.
Dies vernichtet allen Besitz.
Personen mit Schulden (negativem Besitz) könnten jedoch profitieren.›
fun reset :: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
  ‹reset ich welt = Some (welt⦇ besitz := λ _. 0⦈)›

(*<*)
lemma wohlgeformte_handlungsabsicht_reset:
  ‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht reset)›
  apply(simp add: wohlgeformte_handlungsabsicht.simps handeln_def nachher_handeln.simps)
  apply(simp add: zahlenwps_def konsensswap_sym)
  apply(simp add: swap_def fun_eq_iff)
  done
(*>*)

text‹Die Handlungsabsicht die alles kaputt macht.
Die Handlungsabsicht sucht sich den minimalen Besitz aller Personen und
weist allen Personen Eins weniger zu.
Damit haben alle Personen definitiv weniger als zuvor.›
fun alles_kaputt_machen :: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
  ‹alles_kaputt_machen ich welt = Some (welt⦇ besitz := λ _. Min ((besitz welt) ` UNIV) - 1 ⦈)›

lemma alles_kaputt_machen_code[code]:
  ‹alles_kaputt_machen ich welt =
   Some (welt⦇ besitz := (λ_. min_list (map (besitz welt) enum_class.enum) -1)⦈)›
  apply(cases ‹welt›, simp add: alles_kaputt_machen_code_help)
  done


(*<*)
declare alles_kaputt_machen.simps[simp del]

lemma wohlgeformte_handlungsabsicht_alles_kaputt_machen:
  ‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht alles_kaputt_machen)›
  apply(simp add: wohlgeformte_handlungsabsicht.simps)
  apply(simp add: alles_kaputt_machen_code)
  apply(simp add: zahlenwps_def konsensswap_sym)
  apply(case_tac ‹welt›, simp add: fun_eq_iff)
  apply(simp add: min_list_swap_int_enum)
  by (simp add: swap_def)
(*>*)



text‹Die unmögliche Handlungsabsicht, welche immer scheitert.›
fun unmoeglich :: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
  ‹unmoeglich _ _ = None›



text‹Die Beispielhandlungsabsichten, die wir betrachten wollen.›
definition ‹handlungsabsichten ≡ [
  Handlungsabsicht (abbauen 5),
  Handlungsabsicht (stehlen 3 10),
  Handlungsabsicht existierende_abmachung_einloesen,
  Handlungsabsicht reset,
  Handlungsabsicht alles_kaputt_machen,
  Handlungsabsicht unmoeglich
]›

lemma wfh_handlungsabsichten:
  ‹ha ∈ set handlungsabsichten ⟹ wohlgeformte_handlungsabsicht zahlenwps welt ha›
  apply(simp add: handlungsabsichten_def)
  apply(safe)
       apply(simp add: wohlgeformte_handlungsabsicht_abbauen; fail)
      apply(simp add: wohlgeformte_handlungsabsicht_stehlen; fail)
     apply(simp add: wohlgeformte_handlungsabsicht_existierende_abmachung_einloesen; fail)
    apply(simp add: wohlgeformte_handlungsabsicht_reset; fail)
  apply(simp add: wohlgeformte_handlungsabsicht_alles_kaputt_machen; fail)
  by (simp add: wohlgeformte_handlungsabsicht.simps)




fun individueller_fortschritt :: ‹person ⇒ zahlenwelt handlung ⇒ bool› where
  ‹individueller_fortschritt p (Handlung vor nach) ⟷ (meins p vor) ≤ (meins p nach)›

definition maxime_altruistischer_fortschritt :: ‹(person, zahlenwelt) maxime› where
  ‹maxime_altruistischer_fortschritt ≡
      Maxime (λich h. ∀pX. individueller_fortschritt pX h)›

(*existierende_abmachung_einloesen macht, dass die Maxime nicht erfuellt.*)
beispiel ‹erzeuge_beispiel
  zahlenwps initialwelt
  handlungsabsichten
  maxime_altruistischer_fortschritt
= Some
  ⦇
   bsp_erfuellte_maxime = False,
   bsp_erlaubte_handlungen = [
      Handlungsabsicht (abbauen 5),
      Handlungsabsicht unmoeglich],
   bsp_verbotene_handlungen = [
      Handlungsabsicht (stehlen 3 10),
      Handlungsabsicht reset,
      Handlungsabsicht alles_kaputt_machen],
   bsp_uneindeutige_handlungen = [
      Handlungsabsicht existierende_abmachung_einloesen]
  ⦈› by beispiel_tac


definition maxime_hatte_konsens :: ‹(person, zahlenwelt) maxime› where
  ‹maxime_hatte_konsens ≡ Maxime (λich h. einvernehmlich h)›


beispiel ‹∀h ∈ set (alle_moeglichen_handlungen initialwelt (Handlungsabsicht existierende_abmachung_einloesen)).
 wohlgeformte_maxime_auf
    h zahlenwps 
    maxime_hatte_konsens› by eval

lemma ‹wohlgeformte_maxime zahlenwps maxime_hatte_konsens›
  by(simp add: wohlgeformte_maxime_def wohlgeformte_maxime_auf_def
               maxime_hatte_konsens_def einvernehmlich_swap)

beispiel ‹erzeuge_beispiel
  zahlenwps initialwelt
  [Handlungsabsicht existierende_abmachung_einloesen]
  maxime_hatte_konsens
= Some
  ⦇
   bsp_erfuellte_maxime = True,
   bsp_erlaubte_handlungen = [Handlungsabsicht existierende_abmachung_einloesen],
   bsp_verbotene_handlungen = [],
   bsp_uneindeutige_handlungen = []⦈›
  by beispiel_tac

beispiel ‹erzeuge_beispiel
  zahlenwps initialwelt
  [Handlungsabsicht (abbauen 5),
   Handlungsabsicht (stehlen 3 10),
   Handlungsabsicht reset,
   Handlungsabsicht alles_kaputt_machen,
   Handlungsabsicht unmoeglich]
  maxime_altruistischer_fortschritt
= Some
  ⦇
   bsp_erfuellte_maxime = True,
   bsp_erlaubte_handlungen = [
      Handlungsabsicht (abbauen 5),
      Handlungsabsicht unmoeglich],
   bsp_verbotene_handlungen = [
      Handlungsabsicht (stehlen 3 10),
      Handlungsabsicht reset,
      Handlungsabsicht alles_kaputt_machen],
   bsp_uneindeutige_handlungen = []⦈›
  by beispiel_tac


beispiel ‹erzeuge_beispiel
  zahlenwps initialwelt
  handlungsabsichten
  (MaximeDisj maxime_altruistischer_fortschritt maxime_hatte_konsens)
= Some
  ⦇
   bsp_erfuellte_maxime = True,
   bsp_erlaubte_handlungen = [
      Handlungsabsicht (abbauen 5),
      Handlungsabsicht existierende_abmachung_einloesen,
      Handlungsabsicht unmoeglich],
   bsp_verbotene_handlungen = [
      Handlungsabsicht (stehlen 3 10),
      Handlungsabsicht reset,
      Handlungsabsicht alles_kaputt_machen],
   bsp_uneindeutige_handlungen = []⦈›
  by beispiel_tac

  




lemma ‹maxime_und_handlungsabsicht_generalisieren zahlenwps welt
     maxime_hatte_konsens (Handlungsabsicht existierende_abmachung_einloesen) p›
  apply(simp add: maxime_und_handlungsabsicht_generalisieren_def maxime_hatte_konsens_def)
  apply(clarsimp)
  apply(simp add: einvernehmlich_existierende_abmachung_einloesen)
  done
  
lemma mhg_katimp_maxime_hatte_konsens:
  ‹∀p. maxime_und_handlungsabsicht_generalisieren zahlenwps welt maxime_hatte_konsens ha p ⟹
    wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
    kategorischer_imperativ_auf ha welt maxime_hatte_konsens›
  apply(simp add: maxime_hatte_konsens_def)
  apply(erule globale_maxime_katimp)
      subgoal by(simp add: handeln_def einvernehmlich_noop ist_noop_def)
     subgoal by(simp add: wpsm_kommutiert_handlung_raw einvernehmlich_swap_nachher_handeln) 
    subgoal using zahlenwps_sym by fastforce
   subgoal by(simp add: zahlenwps_id)
  by simp


lemma wpsm_kommutiert_altruistischer_fortschritt:
  ‹wpsm_kommutiert maxime_altruistischer_fortschritt zahlenwps welt›
  apply(simp add: maxime_altruistischer_fortschritt_def wpsm_kommutiert_def handeln_def nachher_handeln.simps)
  apply(safe)
   apply(case_tac ‹pX = p1›)
    apply(erule_tac x=‹p2› in allE)
    apply (simp add: swap_a swap_b zahlenwps_sym; fail)
   apply(case_tac ‹pX = p2›)
    apply(erule_tac x=‹p1› in allE)
    apply (simp add: swap_a swap_b zahlenwps_sym; fail)
   apply(erule_tac x=‹pX› in allE)
   apply(simp add: besitz_zahlenwps_nothing zahlenwps_sym swap_nothing; fail)
  by (metis swap_a swap_b swap_nothing zahlenwps_sym)

lemma mhg_katimp_maxime_altruistischer_fortschritt:
  ‹∀p. maxime_und_handlungsabsicht_generalisieren zahlenwps welt maxime_altruistischer_fortschritt ha p ⟹
    wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
    kategorischer_imperativ_auf ha welt maxime_altruistischer_fortschritt›
  apply(simp add: maxime_altruistischer_fortschritt_def)
  apply(erule globale_maxime_katimp)
      subgoal by(simp add: handeln_def einvernehmlich_noop ist_noop_def)
     subgoal using wpsm_kommutiert_altruistischer_fortschritt by(simp add: maxime_altruistischer_fortschritt_def) 
    subgoal using zahlenwps_sym by fastforce
   subgoal by(simp add: zahlenwps_id)
  by simp

text‹Folgendes Theorem zeigt, dass das \<^const>‹MaximeDisj› Konstrukt in jeder Welt funktioniert.›
theorem
  ‹ex_erfuellbare_instanz maxime_altruistischer_fortschritt welt ha ∧
    (∀p. maxime_und_handlungsabsicht_generalisieren
          zahlenwps welt maxime_altruistischer_fortschritt ha p)
   ∨
   ex_erfuellbare_instanz maxime_hatte_konsens welt ha ∧
    (∀p. maxime_und_handlungsabsicht_generalisieren
          zahlenwps welt maxime_hatte_konsens ha p) ⟹
    wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
    kategorischer_imperativ_auf ha welt
      (MaximeDisj maxime_altruistischer_fortschritt maxime_hatte_konsens)›
  apply(rule kategorischer_imperativ_auf_MaximeDisjI2)
  apply(elim disjE)
   using mhg_katimp_maxime_altruistischer_fortschritt apply simp
  using mhg_katimp_maxime_hatte_konsens apply simp
  done

text‹Wir könnten zusätzlich noch eine Maxime einführen,
welche besagt, dass die Umwelt nicht zerstört werden darf.›
definition maxime_keine_umweltzerstoerung :: ‹(person, zahlenwelt) maxime› where
  ‹maxime_keine_umweltzerstoerung ≡
      Maxime (λ_ h. umwelt (vorher h) ≤ umwelt (nachher h))›

text‹Folgendes Beispiel ist wie die vorherigen Beispiel.
Zusätzlich fügen wir jedoch noch \<^const>‹maxime_keine_umweltzerstoerung› via \<^const>‹MaximeConj› hinzu.›
beispiel‹erzeuge_beispiel
  zahlenwps initialwelt
  handlungsabsichten
  (MaximeConj (MaximeDisj maxime_altruistischer_fortschritt maxime_hatte_konsens)
              maxime_keine_umweltzerstoerung)
= Some
  ⦇
   bsp_erfuellte_maxime = True,
   bsp_erlaubte_handlungen = [
      Handlungsabsicht existierende_abmachung_einloesen,
      Handlungsabsicht unmoeglich],
   bsp_verbotene_handlungen = [
      Handlungsabsicht (abbauen 5),
      Handlungsabsicht (stehlen 3 10),
      Handlungsabsicht reset,
      Handlungsabsicht alles_kaputt_machen],
   bsp_uneindeutige_handlungen = []⦈›
  by beispiel_tac
text‹Das Ergebnis ist fast wie in vorherigen Beispielen.
Allerdings ist \<^const>‹abbauen› nun Teil der verbotenen Handlungsabsichten,
da dabei Umwelt abgebaut wird.›

end