Theory Handlung

theory Handlung
imports Main BeispielTac
begin

section‹Handlung›
text‹In diesem Abschnitt werden wir Handlungen und Handlungsabsichten modellieren.›

text‹Wir beschreiben Handlungen als ein Änderung der Welt.
Das Modell einer Handlung ist rein auf die extern beobachtbare Änderung der Welt beschränkt.
Die handelnden Person ist dabei Nebensache.
Wir beschreiben nur vergangene bzw. hypothetische Handlungen und deren Auswirkungen.
›
datatype 'welt handlung = Handlung (vorher: ‹'welt›) (nachher: ‹'welt›)

text‹
Eine Handlung ist reduziert auf die beobachtbaren Auswirkungen der Handlung.
Die dahinterliegende Handlungsabsicht, bzw. Intention oder "Wollen" sind
in einer \<^typ>‹'welt handlung› nicht modelliert.
Dies liegt daran,
dass wir irgendwie die geistige Welt mit der physischen Welt verbinden müssen und wir daher
am Anfang nur messbare Tatsachen betrachten können.
Diese initiale Entscheidung,
eine Handlung rein auf ihre beobachtbaren und messbaren Auswirkungen zu reduzieren,
ist essentiell für diese Theorie.

Handlungen können Leute betreffen.
Handlungen können aus Sicht Anderer wahrgenommen werden.
Unser Modell einer Handlung enthält jedoch nur die Welt vorher und Welt nachher.
So können wir handelnde Person und beobachtende Person trennen.›

(*<*)
text‹The datatype-generated functions are really cool:›
beispiel ‹map_handlung Suc (Handlung 1 2) = Handlung 2 3› by eval
(*>*)


text‹Folgende Funktion beschreibt ob eine Handlung eine No-Op ist,
also eine Handlung welche die Welt nicht verändert.›
definition ist_noop :: ‹'welt handlung ⇒ bool› where
  ‹ist_noop h ≡ vorher h = nachher h›

(*<*)

lemma ist_noop_map_handlung:
  shows ‹ist_noop h ⟹ ist_noop (map_handlung f h)›
  by(cases ‹h›, rename_tac vor nach, simp add: ist_noop_def)
(*>*)


text ‹
Folgende Definition ist eine Handlung als Funktion gewrapped.
Diese abstrakte Art eine Handlung darzustellen erlaubt es nun,
die Absicht oder Intention hinter einer Handlung zu modellieren.
›
datatype ('person, 'welt) handlungsabsicht = Handlungsabsicht ‹'person ⇒ 'welt ⇒ 'welt option›

text‹Im Vergleich zu unserer \<^typ>‹'welt handlung› sehen wir bereits am Typen,
dass eine \<^typ>‹('person, 'welt) handlungsabsicht› nicht nur eine einfache Aussage über die
\<^typ>‹'welt› trifft, sondern auch die Absicht der handelnden \<^typ>‹'person› beinhaltet.

Die Idee ist, dass eine \<^typ>‹('person, 'welt) handlungsabsicht› eine generische Handlungsabsicht
modelliert. Beispielsweise \<^term>‹Handlungsabsicht (λich welt. brezen_kaufen welt ich)›.
›


text‹Eine \<^typ>‹('person, 'welt) handlungsabsicht› gibt eine \<^typ>‹'welt option› zurück,
anstatt einer \<^typ>‹'welt›.
Handlungsabsichten sind damit partielle Funktionen, was modelliert,
dass die Ausführung einer Handlungsabsicht scheitern kann.
Beispielsweise könnte ein Dieb versuchen ein Opfer zu bestehlen;
wenn sich allerdings kein passendes Opfer findet, dann darf die Handlung scheitern.
Oder es könnte der pathologische Sonderfall eintreten, dass ein Dieb sich selbst
bestehlen soll.
Auch hier darf die Handlung scheitern.
Von außen betrachtet ist eine solche gescheiterte Handlung nicht zu unterscheiden vom Nichtstun.
Allerdings ist es für die moralische Betrachtung dennoch wichtig zu unterscheiden,
ob die Handlungsabsicht ein gescheiterter Diebstahl war,
oder ob die Handlungsabsicht einfach Nichtstun war.
Dadurch dass Handlungsabsichten partiell sind, können wir unterscheiden ob die Handlung
wie geplant ausgeführt wurde oder gescheitert ist.
Denn moralisch sind Stehlen und Nichtstun sehr verschieden.›


text‹Folgende Funktion modelliert die Ausführung einer Handlungsabsicht.›
fun nachher_handeln
  :: ‹'person ⇒ 'welt ⇒ ('person, 'welt) handlungsabsicht ⇒ 'welt›
where
  ‹nachher_handeln handelnde_person welt (Handlungsabsicht h) = 
    (case h handelnde_person welt of Some welt' ⇒ welt'
                                  | None ⇒ welt)›

text‹Gegeben die \<^term_type>‹handelnde_person :: 'person›,
die \<^term_type>‹welt :: 'welt› in ihrem aktuellen Zustand,
und eine \<^term_type>‹ha :: ('person, 'welt) handlungsabsicht›, so liefert
\<^term_type>‹(nachher_handeln handelnde_person welt ha) :: 'welt› die potenziell veränderte Welt zurück,
nachdem die Handlungsabsicht ausgeführt wurde.

Die Funktion \<^const>‹nachher_handeln› besagt, dass eine gescheiterte Handlung
die Welt nicht verändert.
Ab diesem Punkt sind also die Handlungen "sich selbst bestehlen" und "Nichtstun"
von außen ununterscheidbar, da beide die Welt nicht verändern.›

text‹Dank der Hilfsdefinition \<^const>‹nachher_handeln› können wir nun "Handeln"
allgemein definieren.
Folgende Funktion überführt effektiv eine \<^typ>‹('person, 'welt) handlungsabsicht› in
eine \<^typ>‹'welt handlung›.›
definition handeln
  :: ‹'person ⇒ 'welt ⇒ ('person, 'welt) handlungsabsicht ⇒ 'welt handlung›
where
  ‹handeln handelnde_person welt ha ≡ Handlung welt (nachher_handeln handelnde_person welt ha)›


text‹Die Funktion \<^const>‹nachher_handeln› liefert die Welt nach der Handlung.
Die Funktion \<^const>‹handeln› liefert eine \<^typ>‹'welt handlung›,
welche die Welt vor und nach der Handlung darstellt.›


text‹
Beispiel, für eine Welt die nur aus einer Zahl besteht:
Wenn die Zahl kleiner als 9000 ist erhöhe ich sie, ansonsten schlägt die Handlung fehl.
›
definition ‹beispiel_handlungsabsicht ≡ Handlungsabsicht (λ_ n. if n < 9000 then Some (n+1) else None)›

beispiel ‹nachher_handeln ''Peter'' (42::nat) beispiel_handlungsabsicht = 43› by eval
beispiel ‹handeln ''Peter'' (42::nat) beispiel_handlungsabsicht = Handlung 42 43› by eval
beispiel ‹nachher_handeln ''Peter'' (9000::nat) beispiel_handlungsabsicht = 9000› by eval
beispiel ‹ist_noop (handeln ''Peter'' (9000::nat) beispiel_handlungsabsicht)› by eval

text ‹
Von Außen können wir Funktionen nur extensional betrachten, d.h. Eingabe und Ausgabe anschauen.
Die Absicht die sich in einer Funktion verstecken kann ist schwer zu erkennen.
Dies deckt sich ganz gut damit, dass Isabelle standardmäßig Funktionen nicht printet.
Eine \<^typ>‹('person, 'welt) handlungsabsicht› kann nicht geprinted werden!
›

text‹Da Funktionen nicht geprintet werden können, sieht \<^const>‹beispiel_handlungsabsicht› so aus:
\<^value>‹beispiel_handlungsabsicht::(nat, int) handlungsabsicht››


(*<*)
lemma vorher_handeln[simp]: ‹vorher (handeln p welt h) = welt›
  by(cases ‹h›, simp add: handeln_def)
lemma nachher_handeln_raw: ‹nachher (handeln p welt (Handlungsabsicht h)) = 
  (case h p welt of None ⇒ welt
                  | Some w ⇒ w)›
  by(simp add: handeln_def)

(*I don't want to expand this definition by default, but keep the handeln function around.
Otherwise, case distinctions for the option type pop up in all proof obligations.*)
declare nachher_handeln.simps[simp del]
(*>*)


text‹Um eine gescheiterte Handlung von einer Handlung welche die Welt nicht verändert
zu unterscheiden, sagen wir, dass eine Handlungsabsicht ausführbar ist,
wenn die ausgeführte Handlungsabsicht nicht gescheitert ist:›

fun ausfuehrbar :: ‹'person ⇒ 'welt ⇒ ('person, 'welt) handlungsabsicht ⇒ bool›
where
  ‹ausfuehrbar p welt (Handlungsabsicht h) = (h p welt ≠ None)›

(*<*)
lemma do_not_get_lazy_and_just_assume_everything_is_ausfuehrbar:
  "(∀ ha. ausfuehrbar p welt ha) ⟹ False"
proof -
  assume a: ‹∀ ha. ausfuehrbar p welt ha›
  hence ‹∀ h. ausfuehrbar p welt (Handlungsabsicht h)› by blast
  thus ?thesis
    apply(simp)
    by fastforce
qed

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

text‹Nicht ausführbare Handlungen resultieren in unserem Modell im Nichtstun:›
lemma nicht_ausfuehrbar_ist_noop:
  ‹¬ausfuehrbar p welt ha ⟹ ist_noop (handeln p welt ha)›
  apply(cases ‹ha›)
  by(simp add: ausfuehrbar.simps ist_noop_def handeln_def nachher_handeln.simps)

(*<*)
lemma ausfuehrbar_nachher_handeln:
  ‹ausfuehrbar p welt (Handlungsabsicht h) ⟹
    nachher_handeln p welt (Handlungsabsicht h) = the (h p welt)›
  apply(simp add: ausfuehrbar.simps nachher_handeln.simps split:option.split)
  by fastforce
lemma nicht_ausfuehrbar_nachher_handeln:
  ‹¬ausfuehrbar p welt ha ⟹
    nachher_handeln p welt ha = welt›
  by(cases ‹ha›, simp add: ausfuehrbar.simps nachher_handeln.simps split:option.split)
(*>*)


subsection‹Interpretation: Gesinnungsethik vs. Verantwortungethik \label{sec:gesinnungsverantwortungsethik}›
text‹
Nur basierend auf unserem Modell einer \<^const>‹Handlung› und \<^const>‹Handlungsabsicht› können
wir bereits erste Aussagen über moralische Bewertungen treffen.



Sei eine Ethik eine Funktion, welche einem beliebigen \<^typ>‹'α› eine
Bewertung Gut = \<^const>‹True›, Schlecht = \<^const>‹False› zuordnet.

  ▪ Eine Ethik hat demnach den Typ: \<^typ>‹'α ⇒ bool›.

┉

Laut 🌐‹https://de.wikipedia.org/wiki/Gesinnungsethik› ist eine Gesinnungsethik
"[..] eine der moralischen Theorien,
 die Handlungen nach der Handlungsabsicht [...]  bewertet,
 und zwar ungeachtet der nach erfolgter Handlung eingetretenen Handlungsfolgen."

  ▪ Demnach ist eine Gesinnungsethik: \<^typ>‹('person, 'welt) handlungsabsicht ⇒ bool›.

┈

Nach 🌐‹https://de.wikipedia.org/wiki/Verantwortungsethik› steht die Verantwortungsethik
dazu im strikten Gegensatz, da die Verantwortungsethik
"in der Bewertung des Handelns die Verantwortbarkeit der ∗‹tatsächlichen Ergebnisse› betont."

  ▪ Demnach ist eine Verantwortungsethik: \<^typ>‹'welt handlung ⇒ bool›.


┉

Da \<^const>‹handeln› eine Handlungsabsicht \<^typ>‹('person, 'welt) handlungsabsicht›
in eine konkrete Änderung der Welt \<^typ>‹'welt handlung› überführt,
können wie die beiden Ethiktypen miteinander in Verbindung setzen.
Wir sagen, eine Gesinnungsethik und eine Verantwortungsethik sind konsistent,
genau dann wenn für jede Handlungsabsicht, die
Gesinnungsethik die Handlungsabsicht genau so bewertet,
wie die Verantwortungsethik die Handlungsabsicht bewerten würde,
wenn die die Handlungsabsicht in jeder möglichen Welt und
als jede mögliche handelnde Person tatsächlich ausgeführt wird und die Folgen betrachtet werden:
›

definition gesinnungsethik_verantwortungsethik_konsistent
  :: ‹(('person, 'welt) handlungsabsicht ⇒ bool) ⇒ ('welt handlung ⇒ bool) ⇒ bool›
where
  ‹gesinnungsethik_verantwortungsethik_konsistent gesinnungsethik verantwortungsethik ≡
    ∀handlungsabsicht.
      gesinnungsethik handlungsabsicht ⟷
        (∀person welt. verantwortungsethik (handeln person welt handlungsabsicht))›


text‹Ich habe aktuell kein Beispiel für eine Gesinnungsethik
und eine Verantwortungsethik,
die tatsächlich konsistent sind.
Später (In \S\ref{sec:golregelutilkonsistent}) werden wir sehen, dass es eine Übersetzung gibt,
mit der die goldene Regel und der Utilitarismus konsistent sind.›

end