Theory Maxime

theory Maxime
imports Handlung BeispielPerson ExecutableHelper Xor
begin

section‹Maxime›
text‹In diesem Abschnitt werden wir das Konzept einer Maxime modellieren.›

text‹
Nach 🌐‹https://de.wikipedia.org/wiki/Maxime› ist eine Maxime ein
persönlicher Grundsatz des Wollens und Handelns.
Nach Kant ist eine Maxime ein "subjektives Prinzip des Wollens".

Modell einer ∗‹Maxime›:
Eine Maxime in diesem Modell beschreibt ob eine Handlung in einer gegebenen Welt gut ist.

Faktisch bruachen wir um eine Maxime zu modellieren
  ▪ \<^typ>‹'person›: die handelnde Person, i.e., ∗‹ich›.
  ▪ \<^typ>‹'welt handlung›: die zu betrachtende Handlung.
  ▪ \<^typ>‹bool›: Das Ergebnis der Betrachtung. \<^const>‹True› = Gut; \<^const>‹False› = Schlecht.

Wir brauchen sowohl die \<^typ>‹'welt handlung› als auch die \<^typ>‹'person› aus deren Sicht die Maxime
definiert ist,
da es einen großen Unterschied machen kann ob ich selber handel,
ob ich Betroffener einer fremden Handlung bin, oder nur Außenstehender.
›
datatype ('person, 'welt) maxime = Maxime ‹'person ⇒ 'welt handlung ⇒ bool›
                                 (*          ich    -> Auswirkung      -> gut/schlecht  *)

text‹Auswertung einer Maxime:›
fun okay :: ‹('person, 'welt) maxime ⇒ 'person ⇒ 'welt handlung ⇒ bool› where
  ‹okay (Maxime m) p h = m p h›


text‹Beispiel›
definition maxime_mir_ist_alles_recht :: ‹('person, 'welt) maxime› where
  ‹maxime_mir_ist_alles_recht ≡ Maxime (λ_ _. True)›

subsection‹Maxime in Sinne Kants?›
text‹Kants kategorischer Imperativ ist eine deontologische Ethik,
d.h.,
"Es wird eben nicht bewertet, was die Handlung bewirkt, sondern wie die Absicht beschaffen ist."
🌐‹https://de.wikipedia.org/wiki/Kategorischer_Imperativ›.

Wenn wir Kants kategorischen Imperativ bauen wollen, dürfen wir also nicht die Folgen einer
Handlung betrachten, sondern nur die Absicht dahinter.
Doch unsere \<^const>‹Maxime› betrachtet eine \<^typ>‹'welt handlung›, also eine konkrete Handlung,
die nur durch ihre Folgen gegeben ist.
Die Maxime betrachtet keine Handlungsabsicht \<^typ>‹('person, 'welt) handlungsabsicht›.

>>Zweifellos hat Immanuel Kant eine Art von Gesinnungsethik vertreten<<
🌐‹https://de.wikipedia.org/wiki/Gesinnungsethik#Gesinnungsethik_bei_Kant›.
Wie wir bereits im Abschnitt \ref{sec:gesinnungsverantwortungsethik} gesehen haben,
sollte eine Maxime demnach eine \<^typ>‹('person, 'welt) handlungsabsicht› und
keine \<^typ>‹'welt handlung› betrachten.
Dennoch haben wir uns für unsere ∗‹extensionale› Interpretation für
eine \<^typ>‹('person, 'welt) handlungsabsicht› entschieden.
Und auch wenn wir das Zitat der
🌐‹https://de.wikipedia.org/w/index.php?title=Gesinnungsethik&oldid=218409490#Gesinnungsethik_bei_Kant›
weiterlesen, sehen wir, dass unser Modell zumindest nicht komplett inkonsistent ist:
>>Zweifellos hat Immanuel Kant eine Art von Gesinnungsethik vertreten,
die allerdings nicht im Gegensatz zu einer Verantwortungsethik,
sondern allenfalls zu einer bloßen „Erfolgsethik“ steht.<<

Kant unterscheidet unter Anderem
"zwischen >>apriorischen<< und >>empirischen<< Urteilen" @{cite russellphi}.
Wenn wir uns den Typ \<^typ>‹'welt handlung› als Beobachtung der Welt \<^const>‹vorher› und \<^const>‹nachher› anschauen,
dann könnte man sagen, unser Moralbegriff der \<^const>‹Maxime› sei empirisch.
Für Kant gilt jedoch:
"Alle Moralbegriffe [...] haben ∗‹a priori› ihren Sitz und Ursprung ausschließlich in der Vernunft" @{cite russellphi}.
Hier widerspricht unser Modell wieder Kant, da unser Modell empirisch ist und nicht apriorisch.


Dies mag nun als Fehler in unserem Modell verstanden werden.
Doch irgendwo müssen wir praktisch werden.
Nur von Handlungsabsichten zu reden, ohne dass die beabsichtigten Folgen betrachtet werden
ist mir einfach zu abstrakt und nicht greifbar.


Alles ist jedoch nicht verloren, denn "Alle rein mathematischen Sätze sind [...] apriorisch" @{cite russellphi}.
Und auch Russel schlussfolgert:
"Um ein ausreichendes Kriterium zu gewinnen, müßten wir Kants rein formalen Standpunkt aufgeben
und die Wirkung der Handlungen in Betracht ziehen" @{cite russellphi}.

Auch Kants kategorischer Imperativ und die Goldene Regel sind grundverschieden:
🌐‹https://web.archive.org/web/20220123174117/https://www.goethegymnasium-hildesheim.de/index.php/faecher/faecher/gesellschaftswissenschaften/philosophie›
Dennoch, betrachten wir den kategorischen Imperativ als eine Verallgemeinerung
der goldenen Regel.
›


subsection‹Die Goldene Regel›
text‹Die Goldene Regel nach 🌐‹https://de.wikipedia.org/wiki/Goldene_Regel› sagt:

  „Behandle andere so, wie du von ihnen behandelt werden willst.“

  „Was du nicht willst, dass man dir tu, das füg auch keinem andern zu.“


So wie wir behandelt werden wollen ist modelliert durch eine \<^typ>‹('person, 'welt) maxime›.

Die goldene Regel testet ob eine Handlung, bzw. Handlungsabsicht moralisch ist.
Um eine Handlung gegen eine Maxime zu testen fragen wir uns:
  ▪ Was wenn jeder so handeln würde?
  ▪ Was wenn jeder nach dieser Maxime handeln würde?

Beispielsweise mag "stehlen" und "bestohlen werden" die gleiche Handlung sein,
jedoch wird sie von Täter und Opfer grundverschieden wahrgenommen.
›
definition bevoelkerung :: ‹'person set› where ‹bevoelkerung ≡ UNIV›

definition wenn_jeder_so_handelt
    :: ‹'welt ⇒ ('person, 'welt) handlungsabsicht ⇒ ('welt handlung) set›
  where
    ‹wenn_jeder_so_handelt welt handlungsabsicht ≡
      (λhandelnde_person. handeln handelnde_person welt handlungsabsicht) ` bevoelkerung›

fun was_wenn_jeder_so_handelt_aus_sicht_von
    :: ‹'welt ⇒ ('person, 'welt) maxime ⇒ ('person, 'welt) handlungsabsicht ⇒ 'person ⇒ bool›
  where
    ‹was_wenn_jeder_so_handelt_aus_sicht_von welt m handlungsabsicht betroffene_person =
        (∀ h ∈ wenn_jeder_so_handelt welt handlungsabsicht. okay m betroffene_person h)›


text‹Für eine gegebene Welt und eine gegebene Maxime nennen wir eine Handlungsabsicht
genau dann moralisch, wenn die Handlung auch die eigene Maxime erfüllt,
wenn die Handlung von anderen durchgeführt würde.›
definition moralisch ::
  ‹'welt ⇒ ('person, 'welt) maxime ⇒ ('person, 'welt) handlungsabsicht ⇒ bool› where
‹moralisch welt handlungsabsicht maxime ≡
  ∀p ∈ bevoelkerung. was_wenn_jeder_so_handelt_aus_sicht_von welt handlungsabsicht maxime p›

text‹
Faktisch bedeutet diese Definition, wir bilden das Kreuzprodukt \<^term>‹bevoelkerung × bevoelkerung›,
wobei jeder einmal als handelnde Person auftritt und einmal als betroffene Person.
›
lemma moralisch_unfold:
  ‹moralisch welt (Maxime m) handlungsabsicht ⟷
        (∀p1∈bevoelkerung. ∀p2∈bevoelkerung. m p1 (handeln p2 welt handlungsabsicht))›
  by(simp add: moralisch_def wenn_jeder_so_handelt_def)
lemma ‹moralisch welt (Maxime m) handlungsabsicht ⟷
        (∀(p1,p2)∈bevoelkerung×bevoelkerung. m p1 (handeln p2 welt handlungsabsicht))›
  unfolding moralisch_unfold by simp

lemma moralisch_simp:
  ‹moralisch welt m handlungsabsicht ⟷
        (∀p1 p2. okay m p1 (handeln p2 welt handlungsabsicht))›
  unfolding moralisch_unfold
  by (cases ‹m›, simp add: bevoelkerung_def moralisch_unfold)

text‹
Wir können die goldene Regel auch umformulieren,
nicht als Imperativ, sondern als Beobachtung eines Wunschzustandes:
Wenn eine Handlung für eine Person okay ist, dann muss sie auch Okay sein,
wenn jemand anderes diese Handlung ausführt.

Formal:
\<^term>‹okay m ich (handeln ich welt handlungsabsicht) ⟹ ∀p2. okay m ich (handeln p2 welt handlungsabsicht)›

Genau dies können wir aus unserer Definition von \<^const>‹moralisch› ableiten:›

lemma goldene_regel:
  ‹moralisch welt m handlungsabsicht ⟹
   okay m ich (handeln ich welt handlungsabsicht) ⟹
   ∀p2. okay m ich (handeln p2 welt handlungsabsicht)›
  by (simp add: moralisch_simp)

text‹Für das obige lemma brauchen wir die Annahme
\<^term>‹m ich (handeln ich welt handlungsabsicht)› gar nicht.

Wenn für eine gegebene \<^term>‹Maxime m› eine Handlungsabsicht moralisch ist,
dann ist es auch okay, wenn ich von der Handlungsabsicht betroffen bin,
egal wer sie ausführt.›
corollary
  ‹moralisch welt m handlungsabsicht ⟹
   ∀p2. okay m ich (handeln p2 welt handlungsabsicht)›
  by (simp add: moralisch_simp)

text‹Die umgekehrte Richtung gilt nicht, weil diese Formulierung nur die Handlungen betrachtet,
die okay sind.›


text‹Entweder ist etwas moralisch,
oder es gibt zwei Personen, für die eine Handlungsabsicht nicht \<^const>‹okay› ist.›
lemma moralisch_oder_nicht_okay:
  "moralisch welt m ha ⊕ (∃p1 p2. ¬ okay m p2 (handeln p1 welt ha))"
  by (auto simp add: xor2 moralisch_simp)

(*<*)
text‹Versuch eine executable version zu bauen.
Wir müssen die Bevölkerung enumerieren.›
definition moralisch_exhaust where
  ‹moralisch_exhaust bevoelk welt maxime handlungsabsicht ≡
    (case maxime of (Maxime m) ⇒ 
      list_all (λ(p,x). m p (handeln x welt handlungsabsicht)) (List.product bevoelk bevoelk))›

lemma moralisch_exhaust_univ: ‹set b = (UNIV::'person set) ⟹
        moralisch welt maxime ha = moralisch_exhaust b welt maxime ha›
  apply(case_tac ‹maxime›, rename_tac m, simp)
  unfolding moralisch_unfold moralisch_exhaust_def bevoelkerung_def
  apply(simp)
  by(simp add: list_all_iff)

subsection ‹Making it executable›
  (*TODO: for reasons I do not understand,
    moralisch_exhaust [Alice, Bob, Carol, Eve] (not enum) needs [code_unfold]
    but
    moralisch_exhaust (enum) needs [code]
    ? ? ?*)
  lemma moralisch_exhaust [code]: ‹moralisch = moralisch_exhaust enum_class.enum›
    apply(simp add: fun_eq_iff)
    apply(rule allI)+
    apply(rule moralisch_exhaust_univ)
    using enum_UNIV by simp
  
  declare moralisch_def[code del] ― ‹Only use executable \<^const>‹moralisch_exhaust››
(*>*)

text‹Hier schlägt das Programmiererherz höher:
Wenn \<^typ>‹'person› aufzählbar ist haben wir ausführbaren Code: @{thm moralisch_exhaust}
wobei \<^const>‹moralisch_exhaust› implementiert ist als @{thm moralisch_exhaust_def}.
›

subsection‹Maximen Debugging›
text‹Der folgende Datentyp modelliert ein Beispiel in welcher Konstellation eine gegebene
Maxime verletzt ist:›

record ('person, 'welt) dbg_verletzte_maxime =
  dbg_opfer :: ‹'person› ―‹verletzt für; das Opfer›
  dbg_taeter :: ‹'person› ―‹handelnde Person; der Täter›
  dbg_handlung :: ‹'welt handlung› ―‹Die verletzende Handlung›

text‹Alle Feldnamen bekommen das Präfix "dbg" für Debug um den Namensraum nicht zu verunreinigen.›
    

text‹Die folgende Funktion liefert alle Gegebenheiten welche eine Maxime verletzen:›
fun debug_maxime
  :: ‹('welt ⇒ 'printable_world) ⇒ 'welt ⇒
      ('person, 'welt) maxime ⇒ ('person, 'welt) handlungsabsicht
      ⇒ (('person, 'printable_world) dbg_verletzte_maxime) set›
where
  ‹debug_maxime print_world welt m handlungsabsicht =
    {⦇
      dbg_opfer = p1,
      dbg_taeter = p2,
      dbg_handlung = map_handlung print_world (handeln p2 welt handlungsabsicht)
     ⦈
      | p1 p2. ¬okay m p1 (handeln p2 welt handlungsabsicht)}›


text‹Es gibt genau dann keine Beispiele für Verletzungen, wenn die Maxime erfüllt ist:›
lemma ‹debug_maxime print_world welt maxime handlungsabsicht = {}
        ⟷ moralisch welt maxime handlungsabsicht›
  apply(case_tac ‹maxime›, rename_tac m, simp)
  by(simp add: moralisch_unfold bevoelkerung_def)

(*<*)
definition debug_maxime_exhaust where
  ‹debug_maxime_exhaust bevoelk print_world welt maxime ha ≡
    (case maxime of (Maxime m) ⇒ 
      map (λ(p1,p2). ⦇ dbg_opfer=p1, dbg_taeter=p2, dbg_handlung=map_handlung print_world (handeln p2 welt ha)⦈)
        (filter (λ(p1,p2). ¬m p1 (handeln p2 welt ha)) (List.product bevoelk bevoelk)))›

lemma debug_maxime_exhaust [code]:
  ‹debug_maxime print_world welt maxime ha
    = set (debug_maxime_exhaust enum_class.enum print_world welt maxime ha)›
  apply(case_tac ‹maxime›, rename_tac m, simp)
  apply(simp add: debug_maxime_exhaust_def enum_UNIV)
  by(simp add: image_Collect)
(*>*)

subsection ‹Beispiel›
(*TODO: bekomme ich das irgendwie in einen eignenen namespace?*)
(*this causes
  fun moralisch _ _ _ = raise Fail "Kant.moralisch";
when we don't use moralisch_exhaust.
So when code fails with "Kant.moralisch", make sure the 'person implements enum.*)

text‹Beispiel:
Die Welt sei nur eine Zahl und die zu betrachtende Handlungsabsicht sei,
dass wir diese Zahl erhöhen.
Die Mir-ist-alles-Recht Maxime ist hier erfüllt:›
beispiel ‹moralisch
            (42::nat)
             maxime_mir_ist_alles_recht
            (Handlungsabsicht (λ(person::person) welt. Some (welt + 1)))› by eval

text‹Beispiel:
Die Welt ist modelliert als eine Abbildung von Person auf Besitz.
Die Maxime sagt, dass Leute immer mehr oder gleich viel wollen, aber nie etwas verlieren wollen.
In einer Welt in der keiner etwas hat, erfüllt die Handlung jemanden 3 zu geben die Maxime.
›
beispiel ‹moralisch
            [Alice ↦ (0::nat), Bob ↦ 0, Carol ↦ 0, Eve ↦ 0]
            (Maxime (λperson handlung.
                (the ((vorher handlung) person)) ≤ (the ((nachher handlung) person))))
            (Handlungsabsicht (λperson welt. Some (welt(person ↦ 3))))›
  by eval
beispiel ‹debug_maxime show_map
            [Alice ↦ (0::nat), Bob ↦ 0, Carol ↦ 0, Eve ↦ 0]
            (Maxime (λperson handlung.
                (the ((vorher handlung) person)) ≤ (the ((nachher handlung) person))))
            (Handlungsabsicht (λperson welt. Some(welt(person ↦ 3))))
  = {}›
  by eval


text‹Wenn nun \<^const>‹Bob› allerdings bereits 4 hat, würde die obige Handlung ein Verlust
für ihn bedeuten und die Maxime ist nicht erfüllt.›
beispiel ‹¬ moralisch
            [Alice ↦ (0::nat), Bob ↦ 4, Carol ↦ 0, Eve ↦ 0]
            (Maxime (λperson handlung.
                (the ((vorher handlung) person)) ≤ (the ((nachher handlung) person))))
            (Handlungsabsicht (λperson welt. Some (welt(person ↦ 3))))›
  by eval
beispiel ‹debug_maxime show_map
            [Alice ↦ (0::nat), Bob ↦ 4, Carol ↦ 0, Eve ↦ 0]
            (Maxime (λperson handlung.
                (the ((vorher handlung) person)) ≤ (the ((nachher handlung) person))))
            (Handlungsabsicht (λperson welt. Some (welt(person ↦ 3))))
  = {⦇
      dbg_opfer = Bob,
      dbg_taeter = Bob,
      dbg_handlung = Handlung [(Alice, 0), (Bob, 4), (Carol, 0), (Eve, 0)]
                              [(Alice, 0), (Bob, 3), (Carol, 0), (Eve, 0)]
     ⦈}›
  by eval



subsection‹Maximen Kombinieren›
text‹Konjunktion (Und) zweier Maximen.›
fun MaximeConj
  :: ‹('person, 'welt) maxime ⇒ ('person, 'welt) maxime ⇒ ('person, 'welt) maxime›
  where
‹MaximeConj (Maxime m1) (Maxime m2) = Maxime (λp h. m1 p h ∧ m2 p h)›

text‹Die erwarteten Regeln auf einer Konjunktion gelten.›
lemma okay_MaximeConj: ‹okay (MaximeConj m1 m2) p h ⟷ okay m1 p h ∧ okay m2 p h›
  by(cases ‹m1›, cases ‹m2›, simp)

lemma moralisch_MaximeConj:
  ‹moralisch welt (MaximeConj m1 m2) ha ⟷ moralisch welt m1 ha ∧ moralisch welt m2 ha›
  apply(simp add: moralisch_simp okay_MaximeConj)
  by blast

lemma moralisch_MaximeConj_False:
  ‹moralisch welt (MaximeConj m1 (Maxime (λ_ _. True))) ha ⟷ moralisch welt m1 ha›
  by(simp add: moralisch_simp okay_MaximeConj)

lemma moralisch_MaximeConj_True:
  ‹¬ moralisch welt (MaximeConj m1 (Maxime (λ_ _. False))) ha›
  by(simp add: moralisch_simp okay_MaximeConj)

(*<*)
declare MaximeConj.simps[simp del]
(*>*)

text‹Disjunktion (Oder) zweier Maximen.›
fun MaximeDisj
  :: ‹('person, 'welt) maxime ⇒ ('person, 'welt) maxime ⇒ ('person, 'welt) maxime›
  where
‹MaximeDisj (Maxime m1) (Maxime m2) = Maxime (λp h. m1 p h ∨ m2 p h)›

lemma okay_MaximeDisj: ‹okay (MaximeDisj m1 m2) p h ⟷ okay m1 p h ∨ okay m2 p h›
  by(cases ‹m1›, cases ‹m2›, simp)


text‹Leider ist \<^const>‹MaximeDisj› weniger schön,
weil es kein genau-dann-wenn mit der Disjunktion (\<^term>‹m1 ∨ m2›) gibt.›

lemma moralisch_MaximeDisjI:
  ‹moralisch welt m1 ha ∨ moralisch welt m2 ha ⟹ moralisch welt (MaximeDisj m1 m2) ha›
  apply(simp add: moralisch_simp okay_MaximeDisj)
  by auto
text‹Die Rückrichtung gilt leider nicht.
\<^term>‹MaximeDisj m1 m2› is effektiv schwächer, da sich jede Person unabhängig entscheiden darf,
ob sie \<^term>‹m1› oder \<^term>‹m2› folgt.
Im Gegensatz dazu sagt \<^term>‹moralisch welt m1 ha ∨ moralisch welt m2 ha›, dass für
∗‹alle› Personen entweder \<^term>‹m1› oder \<^term>‹m2› gelten muss.›

lemma moralisch_MaximeDisj1:
  ‹moralisch welt m1 ha ⟹ moralisch welt (MaximeDisj m1 m2) ha›
  by(simp add: moralisch_MaximeDisjI)
lemma moralisch_MaximeDisj2:
  ‹moralisch welt m2 ha ⟹ moralisch welt (MaximeDisj m1 m2) ha›
  by(simp add: moralisch_MaximeDisjI)

lemma moralisch_MaximeDisj_False:
  ‹moralisch welt (MaximeDisj m1 (Maxime (λ_ _. False))) ha ⟷ moralisch welt m1 ha›
  by(simp add: moralisch_simp okay_MaximeDisj)

lemma moralisch_MaximeDisj_True:
  ‹moralisch welt (MaximeDisj m1 (Maxime (λ_ _. True))) ha›
  by(simp add: moralisch_simp okay_MaximeDisj)

(*<*)
declare MaximeDisj.simps[simp del]
(*>*)

text‹Negation.›
fun MaximeNot :: ‹('person, 'welt) maxime ⇒ ('person, 'welt) maxime›
  where
‹MaximeNot (Maxime m) = Maxime (λp h. ¬ m p h)›

lemma okay_MaximeNot: ‹okay (MaximeNot m) p h ⟷ ¬ okay m p h›
  by(cases ‹m›, simp)

lemma okay_DeMorgan:
‹okay (MaximeNot (MaximeConj m1 m2)) p h
  ⟷  okay (MaximeDisj (MaximeNot m1) (MaximeNot m2)) p h›
  by (simp add: okay_MaximeConj okay_MaximeDisj okay_MaximeNot)

lemma moralisch_DeMorgan:
‹moralisch welt (MaximeNot (MaximeConj m1 m2)) ha
  ⟷  moralisch welt (MaximeDisj (MaximeNot m1) (MaximeNot m2)) ha›
  by (simp add: moralisch_simp okay_DeMorgan)
  
(*<*)
declare MaximeNot.simps[simp del]
(*>*)
end