Theory SchleierNichtwissen

theory SchleierNichtwissen
imports BeispielPerson Handlung Maxime Swap
begin

section‹Schleier des Nichtwissens›
text‹In diesem Abschnitt werden wir,
basierend auf der Idee von Rawls Schleier des Nitchwissens,
definieren, was eine wohlgeformte Handlungsabsicht und eine wohlgeformte Maxime sind.›


text‹
Rawls' Schleier des Nichtwissens 🌐‹https://de.wikipedia.org/wiki/Schleier_des_Nichtwissens›
ist ein fiktives Modell, in der Personen
>>über die zukünftige Gesellschaftsordnung entscheiden können,
aber selbst nicht wissen,
an welcher Stelle dieser Ordnung sie sich später befinden werden,
also unter einem „Schleier des Nichtwissens“ stehen.<< Quote wikipedia


Wir bedienen uns bei der Idee dieses Modells um gültige Handlungsabsichten und Maximen
zu definieren.
Handlungsabsichten und Maximen sind nur gültig, wenn darin keine Personen hardgecoded werden.

Beispielsweise ist folgende Handlungsabsicht ungültig:
\<^term>‹λich welt. if ich = Alice then Do_A welt else Do_B welt›

Handlungsabsichten und Maximen müssen immer generisch geschrieben werden,
so dass die handelnden und betroffenen Personen niemals anhand ihres Namens ausgewählt werden.

unser Modell von Handlungsabsichten und Maximen stellt beispielsweise die
handelnde Person als Parameter bereit.
Folgendes ist also eine gültige Handlung:
\<^term>‹λich welt. ModifiziereWelt welt ich›

Auch ist es erlaubt, Personen in einer Handlungsabsicht oder Maxime nur anhand ihrer
Eigenschaften in der Welt auszuwählen.
Folgendes wäre eine wohlgeformte Handlung, wenn auch eine moralisch fragwürdige:
\<^term>‹λich welt. enteignen ` {opfer. besitz opfer > besitz ich}›

Um diese Idee von wohlgeformten Handlungsabsichten und Maximen zu formalisieren bedienen
wir uns der Idee des Schleiers des Nichtwissens.
Wir sagen, dass Handlungsabsichten wohlgeformt sind, wenn die Handlungsabsicht gleich bleibt,
wenn man sowohl die handelnde Person austauscht,
als auch alle weltlichen Eigenschaften dieser Person.
Anders ausgedrückt: Wohlgeformte Handlungsabsichten und Maximen sind solche,
bei denen bei der Definition noch nicht feststeht, auf we sie später zutreffen.
›

text‹Für jede Welt muss eine Welt-Personen Swap (wps) Funktion bereit gestellt werden,
die alle Weltlichen Eigenschaften von 2 Personen vertauscht:›
type_synonym ('person, 'welt) wp_swap = ‹'person ⇒ 'person ⇒ 'welt ⇒ 'welt›

text‹Ein jeder \<^typ>‹('person, 'welt) wp_swap› sollte mindestens folgendes erfüllen:›
definition wps_id :: ‹('person, 'welt) wp_swap ⇒ 'welt ⇒ bool›
where
  ‹wps_id wps welt ≡ ∀p1 p2. wps p2 p1 (wps p1 p2 welt) = welt›


text_raw‹
\begin{equation*}
\begin{tikzcd}[column sep=14em, row sep=huge]
\textit{welt}
  \arrow[red, d, "\textit{wps}\ \textit{p1}\ \textit{p2}" near start]
  \arrow[blue, r, "\textit{handeln}\ \textit{p1}"]
& \textit{welt'} \\
\textit{alternativ-welt}
  \arrow[red, r, "\textit{handeln}\ \textit{p2}"]
& \textit{alternativ-welt'}
  \arrow[red, u, "\textit{wps}\ \textit{p1}\ \textit{p2}" near start]
\end{tikzcd}
\end{equation*}
›

subsection‹Wohlgeformte Handlungsabsicht›
text‹Wir sagen, eine Handlungsabsicht ist wohlgeformt,
genau dann wenn sie obiges kommutatives Diagramm erfüllt,
d.h. wenn folgendes equivalent ist
  ▪ handeln in einer Welt.
  ▪ zwei Personen in einer Welt zu vertauschen, in der veränderten Welt zu handeln,
    und die beiden Personen wieder zurück tauschen.›

fun wohlgeformte_handlungsabsicht
  :: ‹('person, 'welt) wp_swap ⇒ 'welt ⇒ ('person, 'welt) handlungsabsicht ⇒ bool›
where
  ‹wohlgeformte_handlungsabsicht wps welt (Handlungsabsicht h) =
   (∀p1 p2. h p1 welt = map_option (wps p2 p1) (h p2 (wps p1 p2 welt)))›

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

lemma wohlgeformte_handlungsabsicht_ausfuehrbar:
  ‹wohlgeformte_handlungsabsicht wps welt ha ⟹
        ∀p1 p2. ausfuehrbar p1 welt ha ⟷ ausfuehrbar p2 (wps p1 p2 welt) ha›
  apply(cases ‹ha›, simp add: wohlgeformte_handlungsabsicht.simps)
  by (metis ausfuehrbar.simps option.map_disc_iff)


(*rueckrichtung gilt nicht*)
lemma wohlgeformte_handlungsabsicht_mit_wpsid:
  ‹wohlgeformte_handlungsabsicht wps welt ha ⟹
   wps_id wps welt ⟹
    ∀p1 p2. handeln p1 welt ha =
            map_handlung (wps p2 p1) (handeln p2 (wps p1 p2 welt) ha)›
  apply(cases ‹ha›, simp add: wohlgeformte_handlungsabsicht.simps)
  apply(simp add: handeln_def nachher_handeln.simps)
  apply(safe)
   apply(simp add: wps_id_def; fail)
  apply(erule_tac x=‹p1› in allE)
  apply(erule_tac x=‹p2› in allE)
  apply(simp)
  apply(simp split: option.split)
  apply(simp add: wps_id_def)
  done
(*>*)


(*TODO: gilt die rueckrichting?*)
text‹Folgende Folgerung erklärt die Definition vermutlich besser:›
lemma wohlgeformte_handlungsabsicht_wpsid_imp_handeln:
  ‹wohlgeformte_handlungsabsicht wps welt ha ⟹ wps_id wps welt ⟹
    (∀p1 p2. handeln p1 welt ha =
                Handlung welt
                        (wps p2 p1 (nachher_handeln p2 (wps p1 p2 welt) ha)))›
  apply(drule(1) wohlgeformte_handlungsabsicht_mit_wpsid)
  apply(cases ‹ha›, simp add: wohlgeformte_handlungsabsicht.simps handeln_def)
  done
(*TODO: das sollte ein Homomorphismus sein.*)

text‹Folgendes Lemma erlaubt es uns das kommutative Diagramm auch leicht anders zu zeichnen.›
lemma wohlgeformte_handlungsabsicht_wpsid_wpssym_komm:
  assumes wpsid: ‹∀welt. wps_id wps welt›
    and wps_sym: ‹∀welt. wps p1 p2 welt = wps p2 p1 welt›
  shows ‹wohlgeformte_handlungsabsicht wps (wps p1 p2 welt) ha ⟹
    handeln p1 (wps p1 p2 welt) ha =
            map_handlung (wps p1 p2) (handeln p2 welt ha)›
  apply(drule wohlgeformte_handlungsabsicht_mit_wpsid)
  subgoal using wpsid by simp
  apply(erule_tac x=‹p1› in allE)
  apply(erule_tac x=‹p2› in allE)
  apply(subgoal_tac ‹wps p1 p2 (wps p1 p2 welt) = welt›)
   prefer 2
   apply (metis wps_id_def wps_sym wpsid)
  apply(simp add: )
  apply(subgoal_tac ‹wps p2 p1 = wps p1 p2›)
   prefer 2 using wps_sym apply presburger
  by simp

  text_raw‹
\begin{equation*}
\begin{tikzcd}[column sep=14em, row sep=huge]
\textit{welt}
  \arrow[blue, d, "\textit{wps}\ \textit{p1}\ \textit{p2}" near start]
  \arrow[red, r, "\textit{handeln}\ \textit{p2}"]
& \textit{welt'} 
  \arrow[red, d, "\textit{wps}\ \textit{p1}\ \textit{p2}" near start]\\
\textit{alternativ-welt}
  \arrow[blue, r, "\textit{handeln}\ \textit{p1}"]
& \textit{alternativ-welt'}
\end{tikzcd}
\end{equation*}
›

(*<*)
lemma wfh_handeln_imp_wpsid:
  ‹(∀p1 p2. handeln p1 welt ha =
            map_handlung (wps p2 p1) (handeln p2 (wps p1 p2 welt) ha)) ⟹
  wps_id wps welt›
  by(cases ‹ha›, simp add: wps_id_def handeln_def)

lemma wohlgeformte_handlungsabsicht_wpsid_simp:
  ‹wohlgeformte_handlungsabsicht wps welt ha ∧ wps_id wps welt
  ⟷
      (∀p1 p2. ausfuehrbar p1 welt ha ⟷ ausfuehrbar p2 (wps p1 p2 welt) ha)
      ∧ (∀p1 p2. handeln p1 welt ha =
                 map_handlung (wps p2 p1) (handeln p2 (wps p1 p2 welt) ha))›
  apply(rule iffI)
  using wohlgeformte_handlungsabsicht_ausfuehrbar wohlgeformte_handlungsabsicht_mit_wpsid apply fast
  apply(rule conjI)
   prefer 2 using wfh_handeln_imp_wpsid apply fast
  apply(cases ‹ha›, simp add: wohlgeformte_handlungsabsicht.simps handeln_def nachher_handeln.simps)
  apply(intro allI, rename_tac h p1 p2)
  apply(case_tac ‹h p2 (wps p1 p2 welt)›)
   apply(simp)
   apply (metis ausfuehrbar.simps)
  apply(simp add: ausfuehrbar.simps)
  apply(clarsimp)
  apply(erule_tac x=‹p1› in allE)
  apply(erule_tac x=‹p1› in allE)
  apply(erule_tac x=‹p2› in allE)
  apply(erule_tac x=‹p2› in allE)
  apply(simp split: option.split_asm)
  done

lemma wohlgeformte_handlungsabsicht_ifI:
  ‹wohlgeformte_handlungsabsicht wps welt (Handlungsabsicht h1) ⟹
   wohlgeformte_handlungsabsicht wps welt (Handlungsabsicht h2) ⟹
   (⋀p1 p2. P p1 welt ⟷ P p2 (wps p1 p2 welt)) ⟹
   wohlgeformte_handlungsabsicht wps welt
      (Handlungsabsicht (λich welt. if P ich welt then h1 ich welt else h2 ich welt))›
  by(simp add: wohlgeformte_handlungsabsicht.simps)
(*>*)


text‹In einigen späteren Beispielen möchten wir zeigen, dass bestimmte Handlungsabsichten
nicht wohlgeformt sind.›
fun wohlgeformte_handlungsabsicht_gegenbeispiel
  :: ‹('person, 'welt) wp_swap ⇒ 'welt ⇒ ('person, 'welt) handlungsabsicht ⇒ 'person ⇒ 'person ⇒ bool›
where
  ‹wohlgeformte_handlungsabsicht_gegenbeispiel wps welt (Handlungsabsicht h) taeter opfer ⟷
  h taeter welt ≠ map_option (wps opfer taeter) (h opfer (wps taeter opfer welt))›

lemma
  ‹∃p1 p2. wohlgeformte_handlungsabsicht_gegenbeispiel wps welt ha p1 p2 ⟷
        ¬wohlgeformte_handlungsabsicht wps welt ha›
  apply(cases ‹ha›, simp add: wohlgeformte_handlungsabsicht.simps)
  by blast




(*<*)
text‹Assume we have a compound datatype, consisting of the parts selected by \<^term>‹sel›
and the parts selected by \<^term>‹sel_other›.
Together, they build the complete datatype.
But we can reason about \<^const>‹map_option› equivalence in isolation.›
lemma datatype_split_map_option_equal:
  ‹map_option sel w1 = map_option sel w2 ⟹
   (⋀ w. makeZ (sel w) (sel_other w) = w) ⟹
   map_option sel_other w1 = map_option sel_other w2 ⟹
  w1 = w2›
  by (metis (no_types, lifting) None_eq_map_option_iff option.exhaust_sel option.map_sel)

text‹Assume we have a compound complex world \<^typ>‹'zw›.
Assume we have a simpler sub-world \<^typ>‹'w›.
Assume we have a Handlungsabsicht in this simpler sub-world \<^term_type>‹ha :: 'person ⇒ 'w ⇒ 'w option›
which only modifies the sub-world.
Then we can lift \<^const>‹wohlgeformte_handlungsabsicht› from the sub-world to the compound world.

\<^term>‹makeZ› is basically the constructor which combines the simpler sub-world with other stuff
to the complicated compound world.

The \<^term_type>‹sel :: 'zw ⇒ 'w› selects the parts of the compound world which are modified.
The \<^term_type>‹sel_other :: 'zw ⇒ 'a› selects the parts of the compound world which are not modified.›
  lemma wfh_generalize_worldI:
  fixes wps :: ‹('person, 'w) wp_swap› ―‹swap in the simple world›
    and zwps :: ‹('person, 'zw) wp_swap› ―‹swap in the compound world›
    and welt :: ‹'w› ―‹the simple world›
    and zwelt :: ‹'zw› ―‹the compound world›
    and ha :: ‹'person ⇒ 'w ⇒ 'w option›
    and sel :: ‹'zw ⇒ 'w› ―‹selects the parts from the compound wold which are modified.›
    and makeZ :: ‹'w ⇒ 'other ⇒ 'zw› ―‹builds the compound world from the simple world and other stuff›
  assumes wf_ha: ‹wohlgeformte_handlungsabsicht wps welt (Handlungsabsicht ha)›
  and     sel_welt: ‹sel zwelt = welt›
  and     sel_wps: ‹⋀p1 p2 zw. wps p1 p2 (sel zw) = sel (zwps p1 p2 zw)›
  and     sel_ha: ‹⋀p zw. ha p (sel zw) = map_option sel (zha p zw)›
  and     make_whole: ‹⋀ w. makeZ (sel w) (sel_other w) = w›

  and not_touches_other:
      ‹⋀p welt welt'. zha p welt = Some welt' ⟹ sel_other welt' = sel_other welt›
  and iff_None: ‹⋀p1 p2 welt. zha p1 welt = None ⟷ zha p2 (zwps p1 p2 welt) = None›
  and makeZ_pullout:
    ‹⋀p1 p2 a b. makeZ (sel (zwps p2 p1 a)) (sel_other (zwps p2 p1 b)) = zwps p2 p1 (makeZ (sel a) (sel_other b))›
  and wpsid: ‹⋀ welt p1 p2. zwps p2 p1 (zwps p1 p2 welt) = welt›
  and wps_sym: ‹⋀welt p1 p2. zwps p1 p2 welt = zwps p2 p1 welt›

  shows
    ‹wohlgeformte_handlungsabsicht zwps zwelt (Handlungsabsicht zha)›
proof -         
  from wf_ha sel_welt sel_wps sel_ha have wohlgeformt_sel:
    ‹map_option sel (zha p1 zwelt) = map_option sel (map_option (zwps p2 p1) (zha p2 (zwps p1 p2 zwelt)))›
    for p1 p2
    apply(simp add: wohlgeformte_handlungsabsicht.simps)
    apply(clarsimp)
    apply(erule_tac x=‹p1› in allE)
    apply(erule_tac x=‹p2› in allE)
    apply(simp add: option.map_comp)
    apply(subgoal_tac ‹wps p2 p1 ∘ sel = sel ∘ zwps p2 p1›)
     prefer 2
     apply fastforce
    apply(simp)
    done

  have wohlgeformt_sel_on_wps_zwelt:
    ‹map_option sel (zha p2 (zwps p1 p2 zwelt)) =
      map_option sel (map_option (zwps p1 p2) (zha p1 (zwps p2 p1 (zwps p1 p2 zwelt))))›
    for p2 p1
    using wohlgeformt_sel[of ‹p1› ‹p2›]
    apply(simp add: wpsid)
    apply(cases ‹zha p1 zwelt›)
     apply(simp; fail)
    apply(cases ‹zha p2 (zwps p1 p2 zwelt)›)
     apply(simp; fail)
    apply(simp)
    by (metis wpsid sel_wps)

  from wps_sym have not_touches_other_wps:
    ‹zha p2 (zwps p1 p2 welt) = Some welt'
                          ⟹ sel_other welt' = sel_other (zwps p2 p1 welt)›
    for p1 p2 welt welt'
    using not_touches_other[of ‹p2› ‹(zwps p1 p2 welt)›] by simp

  have wpsid': ‹zwps p2 p1 (zwps p2 p1 w) = w› for w p1 p2
    using wps_sym wpsid by simp

  have sel_wps_propagate:
    ‹zha p2 (zwps p1 p2 zwelt) = Some welt'
      ⟹ sel welt' = sel (the (map_option (zwps p2 p1) (zha p1 zwelt)))›
    for welt' p1  p2
    using wohlgeformt_sel_on_wps_zwelt[of ‹p2› ‹p1›]
    apply(simp add: wpsid)
    apply(case_tac ‹zha p1 zwelt›)
     apply(simp; fail)
    apply(simp)
    using wps_sym by presburger

  have sel_other_makeZ:
    ‹zha p1 zwelt = Some welt' ⟹
       sel_other zwelt = sel_other (makeZ (sel welt') (sel_other zwelt))›
    for welt' p1
    apply -
    apply(drule not_touches_other[symmetric])
    using make_whole[of ‹welt'›] by simp

  have wohlgeformt_sel_other:
    ‹map_option sel_other (zha p1 zwelt) =
                 map_option sel_other (map_option (zwps p2 p1) (zha p2 (zwps p1 p2 zwelt)))›
    for p1 p2
  proof -
    let ‹?w›=‹zha p2 (zwps p1 p2 zwelt)›
    let ‹?ignoreMe›=‹case ?w of Some w ⇒ sel w›
  
    have ignoreMe: ‹?w ≠ None ⟹ makeZ ?ignoreMe (sel_other (the ?w)) = the ?w›
      apply (cases ‹?w›)
       apply(simp; fail)
      apply(simp)
      using make_whole by simp
  
    have shuffle_sel:
      ‹map_option (sel_other ∘ zwps p2 p1) ?w =
        map_option (sel_other ∘ zwps p2 p1 ∘ (λother. makeZ ?ignoreMe other) ∘ sel_other) ?w›
      for p1 p2
      apply(cases ‹?w›)
       apply(simp; fail)
      apply(simp)
      using ignoreMe by simp

    show ‹?thesis›
    apply(cases ‹zha p1 zwelt›)
     apply(simp)
     using iff_None apply blast
    apply(simp add: not_touches_other[of ‹p1›])
     apply(simp add: option.map_comp)
    apply(subst shuffle_sel)
    apply(case_tac ‹zha p2 (zwps p1 p2 zwelt)›)
     apply(simp)
     using iff_None apply force
    apply(simp)
    apply(frule not_touches_other_wps, simp)
    apply(simp add: sel_wps_propagate)
    apply(simp add: makeZ_pullout)
    apply(simp add: wpsid')
     using sel_other_makeZ by simp
 qed

  from datatype_split_map_option_equal[OF wohlgeformt_sel make_whole wohlgeformt_sel_other] make_whole have
    ‹(zha p1 zwelt) = (map_option (zwps p2 p1) (zha p2 (zwps p1 p2 zwelt)))›
    for p1 p2
    by simp
  then show ‹?thesis›
  by(simp add: wohlgeformte_handlungsabsicht.simps )
qed

(*TODO: can we derive wfh_generalize_world_ConstrI from wfh_generalize_worldI?*)
thm wfh_generalize_worldI[where makeZ=‹λw other. C w› and sel=‹λzw. (inv C) zw›
                                and zha=‹zha› and zwelt=‹C welt› and zwps=‹zwps›]
lemma ‹inj C ⟹ inv C (C welt) = welt› by(simp)

text‹Wenn sich eine einfache Welt \<^typ>‹'w› in eine komplexere Welt \<^typ>‹'zw› übersetzen lässt,
(wobei die Übersetzung hier \<^term>‹C::'w ⇒ 'zw› ist),
dann kann auch \<^const>‹wohlgeformte_handlungsabsicht› mit übersetzt werden.

This is basically @{thm wfh_generalize_worldI}, but instead of \<^term>‹sel›,
we have the opposite: Constructor \<^term>‹C›.›
lemma wfh_generalize_world_ConstrI:
  fixes wps :: ‹('person, 'w) wp_swap›
    and welt :: ‹'w›
    and ha :: ‹'person ⇒ 'w ⇒ 'w option›
    and C :: ‹'w ⇒ 'zw›
  shows
‹wohlgeformte_handlungsabsicht wps welt (Handlungsabsicht (ha)) ⟹
  zwelt = C welt ⟹
  (⋀p1 p2 w. zwps p1 p2 (C w) = C (wps p1 p2 w)) ⟹
  (⋀p w. zha p (C w) =  map_option C (ha p w)) ⟹
wohlgeformte_handlungsabsicht zwps zwelt (Handlungsabsicht (zha))›
  apply(simp)
  apply(simp add: wohlgeformte_handlungsabsicht.simps)
  apply(clarsimp)
  apply(erule_tac x=‹p1› in allE)
  apply(erule_tac x=‹p2› in allE)
  apply(simp)
  apply(simp add: option.map_comp)
  apply(simp add: comp_def)
  done
(*>*)


subsection‹Spezialfall: Maxime und Handlungsabsichten haben nette Eigenschaften›
text‹Dieses Kapitel darf gerne übersprungen werden,
da der Spezialfall nur in bestimmten Beweisen interessant wird.›

text‹Nach der gleichen Argumentation müssten Maxime und Handlungsabsicht so generisch sein,
dass sie in allen Welten zum gleichen Ergebnis kommen.
Dies gilt jedoch nicht immer.
Wenn dieser Sonderfall eintritt sagen wir, Maxime und Handlungsabsicht generalisieren.›
definition maxime_und_handlungsabsicht_generalisieren
  :: ‹('person, 'welt) wp_swap ⇒ 'welt ⇒ 
      ('person, 'welt) maxime ⇒ ('person, 'welt) handlungsabsicht ⇒ 'person ⇒ bool›
where
  ‹maxime_und_handlungsabsicht_generalisieren wps welt m ha p =
    (∀p1 p2. (ausfuehrbar p welt ha ∧ ausfuehrbar p (wps p1 p2 welt) ha)
              ⟶ okay m p (handeln p welt ha) ⟷ okay m p (handeln p (wps p1 p2 welt) ha))›
text‹Die Vorbedingungen in obiger Definition,
nämlich dass die Handlungsabsicht \<^const>‹ausfuehrbar› ist,
ist nötig, um z.B. Handlungsabsichten wie das Stehlen zu ermöglichen;
jedoch gibt es beim Stehlen genau den pathologischen Grenzfall von-sich-selbst Stehlen,
welcher in einer No-Op endet und das Ergebnis damit nicht moralisch falsch ist.
Durch die Einschränkung auf \<^const>‹ausfuehrbar› Fälle lassen sich solche pathologischen Grenzfälle
ausklammern.›

text‹Für eine gegebene Maxime schließt die Forderung
\<^const>‹maxime_und_handlungsabsicht_generalisieren› leider einige Handlungen aus.
Beispiel:
In einer Welt besitzt \<^const>‹Alice› 2 und \<^const>‹Eve› hat 1 Schulden.
Die Maxime ist, dass Individuen gerne keinen Besitz verlieren.
Die Handlung sei ein globaler reset, bei dem jeden ein Besitz von 0 zugeordnet wird.
Leider generalisiert diese Handlung nicht, da \<^const>‹Eve› die Handlung gut findet,
\<^const>‹Alice› allerdings nicht.
›
beispiel
   ‹¬ maxime_und_handlungsabsicht_generalisieren
      swap
      ((λx. 0)(Alice := (2::int), Eve := - 1))
      (Maxime (λich h. (vorher h) ich ≤ (nachher h) ich))
      (Handlungsabsicht (λich w. Some (λ_. 0)))
      Eve›
  apply(simp add: maxime_und_handlungsabsicht_generalisieren_def )
  apply(simp add: ist_noop_def fun_eq_iff handeln_def nachher_handeln.simps)
  by(code_simp)

(*<*)
lemma maxime_und_handlungsabsicht_generalisieren_MaximeConj:
  ‹maxime_und_handlungsabsicht_generalisieren wps welt m1 ha p
    ∧ maxime_und_handlungsabsicht_generalisieren wps welt m2 ha p
  ⟹maxime_und_handlungsabsicht_generalisieren wps welt (MaximeConj m1 m2) ha p›
  apply(simp add: maxime_und_handlungsabsicht_generalisieren_def okay_MaximeConj)
  apply(clarsimp)
  done

(*there is an ∧ in there, not an ∨*)
lemma maxime_und_handlungsabsicht_generalisieren_MaximeDisj_Conj:
  ‹maxime_und_handlungsabsicht_generalisieren wps welt m1 ha p
    ∧ maxime_und_handlungsabsicht_generalisieren wps welt m2 ha p
    ⟹ maxime_und_handlungsabsicht_generalisieren wps welt (MaximeDisj m1 m2) ha p›
  apply(simp add: maxime_und_handlungsabsicht_generalisieren_def okay_MaximeDisj)
  apply(clarsimp)
  done
(*>*)
  
  


text‹Die Maxime und \<^typ>‹('person, 'welt) wp_swap› können einige Eigenschaften erfüllen.

Wir kürzen das ab mit \<^term>‹wpsm :: ('person, 'welt) wp_swap›: Welt Person Swap Maxime.›

text‹Die Person für die Maxime ausgewertet wird und swappen der Personen in der Welt
kann equivalent sein:›
definition wpsm_kommutiert
  :: ‹('person, 'welt) maxime ⇒ ('person, 'welt) wp_swap ⇒ 'welt ⇒ bool›
where
  ‹wpsm_kommutiert m wps welt ≡
  ∀ p1 p2 ha.
    okay m p2 (handeln p1 (wps p1 p2 welt) ha)
    ⟷
    okay m p1 (Handlung welt (wps p1 p2 (nachher_handeln p1 (wps p2 p1 welt) ha)))›

(*<*)
lemma wpsm_kommutiert_handlung_raw:
  ‹wpsm_kommutiert m wps welt =
  (∀ p1 p2 ha.
    okay m p2 (Handlung (wps p1 p2 welt) (nachher_handeln p1 (wps p1 p2 welt) ha))
    ⟷
    okay m p1 (Handlung welt (wps p1 p2 (nachher_handeln p1 (wps p2 p1 welt) ha))))›
  apply(simp add: wpsm_kommutiert_def)
  apply(rule iffI)
   apply(intro allI)
   apply(erule_tac x=‹p1› in allE)
   apply(erule_tac x=‹p2› in allE)
   apply(erule_tac x=‹ha› in allE)
   apply(simp add: nachher_handeln.simps handeln_def; fail)
  apply(intro allI)
  apply(case_tac ‹ha›)
  apply(simp add: handeln_def)
  done


lemma wpsm_kommutiert_unfold_handlungsabsicht:
  ‹wpsm_kommutiert m wps welt =
  (∀ p1 p2 ha.
    okay m p2 (handeln p1 (wps p1 p2 welt) ha)
    ⟷
    okay m p1 (handeln p1 welt (Handlungsabsicht (λp w. Some (wps p1 p2 (nachher_handeln p (wps p2 p1 w) ha)))))
  )›
  apply(simp add: wpsm_kommutiert_handlung_raw)
  by (simp add: handeln_def nachher_handeln.simps)
(*>*)

text‹Wenn sowohl eine \<^const>‹wohlgeformte_handlungsabsicht› vorliegt,
als auch \<^const>‹wpsm_kommutiert›,
dann erhalten wir ein sehr intuitives Ergebnis,
welches besagt, dass ich handelnde Person und Person für die die Maxime gelten soll
vertauschen kann.›
lemma wfh_wpsm_kommutiert_simp:
  assumes wpsid: ‹wps_id wps welt›
  shows ‹wohlgeformte_handlungsabsicht wps welt ha ⟹
  wpsm_kommutiert m wps welt ⟹
    okay m p2 (handeln p1 (wps p1 p2 welt) ha)
    ⟷
    okay m p1 (handeln p2 welt ha)›
  apply(cases ‹ha›, simp)
  apply(simp add: wpsm_kommutiert_def)
  apply(drule wohlgeformte_handlungsabsicht_wpsid_imp_handeln[OF _ wpsid])
  by simp

text‹Die Rückrichtung gilt auch,
aber da wir das für alle Handlungsabsichten in der Annahme brauchen,
ist das eher weniger hilfreich.›
lemma wfh_kommutiert_wpsm:
  assumes wpsid: ‹wps_id wps welt›
  shows 
  ‹∀ha. wohlgeformte_handlungsabsicht wps welt ha ∧
       (∀p1 p2. okay m p2 (handeln p1 (wps p1 p2 welt) ha)
           ⟷
           okay m p1 (handeln p2 welt ha)) ⟹
    wpsm_kommutiert m wps welt›
  apply(simp add: wpsm_kommutiert_def)
  apply(intro allI, rename_tac p1 p2 ha)
  apply(erule_tac x=‹ha› in allE)
  apply(case_tac ‹ha›, simp)
  apply(erule conjE)
  apply(drule wohlgeformte_handlungsabsicht_wpsid_imp_handeln[OF _ wpsid])
  by simp

(*<*)
lemma wpsm_kommutiert_map_handlung:
  assumes wpsid: ‹wps_id wps welt›
    and wps_sym: ‹wps p1 p2 welt = wps p2 p1 welt›
  shows ‹wpsm_kommutiert m wps (wps p1 p2 welt) ⟹
    okay m p1 (map_handlung (wps p1 p2) (handeln p1 welt ha))
    ⟷
    okay m p2 (handeln p1 welt ha)›
  apply(cases ‹ha›, simp)
  apply(simp add: wpsm_kommutiert_def)
  apply(erule_tac x=‹p1› in allE)
  apply(erule_tac x=‹p2› in allE)
  apply(simp add: handeln_def wpsid[simplified wps_id_def])
  by (metis wps_id_def wps_sym wpsid)
(*>*)


subsection‹Wohlgeformte Maxime›
text‹Nach dem gleichen Konzept nach dem wir die \<^const>‹wohlgeformte_handlungsabsicht›
definiert haben,
definieren wir, was es bedeutet für eine Maxime wohlgeformt zu sein.›

(*Eigentlich sollte das fuer alle Handlungen gelten, aber wenn ich ausfuehrbaren code will
habe ich ein Problem, dass Handlungen nicht enumerable sind.*)
definition wohlgeformte_maxime_auf
  :: ‹'welt handlung ⇒ ('person, 'welt) wp_swap ⇒ ('person, 'welt) maxime ⇒ bool›
where
  ‹wohlgeformte_maxime_auf h wps m ≡
    ∀p1 p2. okay m p1 h ⟷ okay m p2 (map_handlung (wps p1 p2) h)›

text‹Eigentlich sollte eine Maxime wohlgeformte sein für alle Handlungen.
Jedoch definieren wir hier eine restriktive Version \<^const>‹wohlgeformte_maxime_auf› welche
nur auf einer Handlung wohlgeformt ist.
Der Grund ist leider ein Implementierungsdetail.
Da wir ausführbaren Code wollen und Handlungen normalerweise nicht vollständig
aufzählbar sind, werden wir auch den kategorischen Imperativ auf eine endliche Menge
von Handlungsabsichten beschränken.
Die eigentlich schönere (jedoch schwer zu beweisende) Forderung lautet:›

definition wohlgeformte_maxime
  :: ‹('person, 'welt) wp_swap ⇒ ('person, 'welt) maxime ⇒ bool›
where
  ‹wohlgeformte_maxime wps m ≡
    ∀h. wohlgeformte_maxime_auf h wps m›


text‹Beispiel:›
beispiel ‹wohlgeformte_maxime swap (Maxime (λich h. (vorher h) ich ≤ (nachher h) ich))›
  apply(simp add: wohlgeformte_maxime_def wohlgeformte_maxime_auf_def)
  apply(intro allI, case_tac ‹h›, simp)
  by (metis swap_a swap_symmetric)
  

(*
aus wpsm_kommutiert koennen wir FAST wohlgeformte_maxime_auf ableiten.
Leider muss pX=p2.
lemma
  assumes wpsid: ‹wps_id wps welt›
    and wps_sym: ‹∀p1 p2. wps p1 p2 = wps p2 p1›
  shows ‹(∀p1 p2::'person. wpsm_kommutiert m wps (wps p1 p2 welt)) ⟹
    wohlgeformte_maxime_auf (handeln (pX::'person) welt ha) wps m›
  apply(simp add: wohlgeformte_maxime_auf_def)
  apply(clarsimp)
  apply(erule_tac x=p2 in allE)
  apply(erule_tac x=p1 in allE)
  apply(subgoal_tac "wps p2 p1 welt = wps p1 p2 welt")
  prefer 2 subgoal using wps_sym by simp
  apply(drule(1) wpsm_kommutiert_map_handlung[OF wpsid, where ha=ha])
  apply(case_tac "pX=p2")
   apply(simp add: wps_sym; fail)
  apply(simp)
  oops
*)

(*<*)
subsection‹Generische Lemmata›

lemma ist_noop_map_handlung_wpsid:
  assumes strong_wps_id:
        ‹∀p1 p2 welt. wps p1 p2 (wps p1 p2 welt) = welt›
  shows ‹ist_noop (map_handlung (wps p1 p2) h) ⟷ ist_noop h›
  apply(cases ‹h›, rename_tac vor nach, simp add: ist_noop_def)
  using strong_wps_id by metis

lemma ist_noop_wps:
  assumes wfh: ‹wohlgeformte_handlungsabsicht wps welt ha›
  and wps_id: ‹wps_id wps welt›
  and strong_wps_id: ‹∀p1 p2 welt. wps p1 p2 (wps p1 p2 welt) = welt›
  shows ‹ist_noop (handeln p2 (wps ich p2 welt) ha) ⟷ ist_noop (handeln ich welt ha)›
proof -
  from wps_id have weak_wps_sym: ‹∀p1 p2. wps p1 p2 welt = wps p2 p1 welt› by (metis strong_wps_id wps_id_def)
  from wohlgeformte_handlungsabsicht_wpsid_imp_handeln[OF wfh wps_id]
  have ‹ist_noop (handeln ich welt ha)
        = ist_noop (Handlung welt (wps p2 ich (nachher_handeln p2 (wps ich p2 welt) ha)))›
    by simp
  also have ‹… = ist_noop (Handlung (wps ich p2 welt) (nachher_handeln p2 (wps ich p2 welt) ha))›
    apply(simp add: ist_noop_def)
    using strong_wps_id weak_wps_sym by metis
  finally have ‹ist_noop (handeln ich welt ha)
    = ist_noop (Handlung (wps ich p2 welt) (nachher_handeln p2 (wps ich p2 welt) ha))› .
  thus ‹?thesis›
    by(simp add: handeln_def wps_id[simplified wps_id_def])
qed


(*>*)

end