Theory KategorischerImperativ
theory KategorischerImperativ
imports Maxime SchleierNichtwissen
begin
section‹Kategorischer Imperativ›
text‹In diesem Abschnitt werden wir den kategorischen Imperativ modellieren.›
text‹
Wir haben mit der goldenen Regel bereits definiert,
wann für eine gegebene Welt und eine gegebene Maxime, eine Handlungsabsicht moralisch ist:
▪ \<^term_type>‹moralisch ::
'welt ⇒ ('person, 'welt) maxime ⇒ ('person, 'welt) handlungsabsicht ⇒ bool›
Effektiv testet die goldene Regel eine Handlungsabsicht.
Nach meinem Verständnis generalisiert Kant mit dem Kategorischen Imperativ diese Regel,
indem die Maxime nicht mehr als gegeben angenommen wird,
sondern die Maxime selbst getestet wird.
Sei die Welt weiterhin gegeben,
dann müsste der kategorische Imperativ folgende Typsignatur haben:
▪ \<^typ>‹'welt ⇒ ('person, 'welt) maxime ⇒ bool›
Eine Implementierung muss dann über alle möglichen Handlungsabsichten allquantifizieren.
Grob gesagt: Die goldene Regel urteilt über eine Handlungsabsicht gegeben eine Maxime,
der kategorische Imperativ urteilt über die Maxime an sich.
Ich behaupte, der kategorischer Imperativ lässt sich wie folgt umformulieren:
▪ Handle nur nach derjenigen Maxime, durch die du zugleich wollen kannst,
dass sie ein allgemeines Gesetz werde.
▪ Handle nur nach derjenigen Maxime, durch die du zugleich wollen kannst,
dass sie jeder befolgt, im Sinne der goldenen Regel.
▪ Handle nur nach derjenigen Maxime, durch die du zugleich wollen kannst,
dass sie (Handlung und Maxime) moralisch ist.
▪ Wenn es jemanden gibt der nach einer Maxime handeln will,
dann muss diese Handlung nach der Maxime moralisch sein.
▪ Für jede Handlungsabsicht muss gelten:
Wenn jemand nach einer Handlungsabsicht handeln würde (getestet durch die Maxime),
dann muss diese Handlung moralisch sein (getestet durch die Maxime).
Daraus ergibt sich diese Formalisierung:
Für eine bestimmte Handlungsabsicht:
Wenn es eine Person gibt für die diese Handlungsabsicht moralisch ist,
dann muss diese Handlungsabsicht auch für alle moralisch (im Sinne der goldenen Regel) sein.
›
definition kategorischer_imperativ_auf
:: ‹('person, 'welt) handlungsabsicht ⇒ 'welt ⇒ ('person, 'welt) maxime ⇒ bool›
where
‹kategorischer_imperativ_auf ha welt m ≡
(∃ich. ausfuehrbar ich welt ha ∧ okay m ich (handeln ich welt ha)) ⟶ moralisch welt m ha›
text‹
Wir beschränken uns auf die \<^const>‹ausfuehrbar›en Handlungsabsichten um pathologische
Grenzfälle (welche keinen Rückschluss auf moralische Gesinnung lassen) auszuschließen.
Für alle möglichen (wohlgeformten) Handlungsabsichten muss dies nun gelten:
›
definition kategorischer_imperativ
:: ‹('person, 'welt) wp_swap ⇒ 'welt ⇒ ('person, 'welt) maxime ⇒ bool›
where
‹kategorischer_imperativ wps welt m ≡
∀ha. wohlgeformte_handlungsabsicht wps welt ha ⟶
kategorischer_imperativ_auf ha welt m›
text‹Damit hat \<^term_type>‹kategorischer_imperativ wps :: 'welt ⇒ ('person, 'welt) maxime ⇒ bool›
die gewünschte Typsignatur.
Wir haben die interne Hilfsdefinition \<^const>‹kategorischer_imperativ_auf› eingeführt
um den kategorischen Imperativ nur für eine Teilmenge aller Handlungen besser
diskutieren zu können.
Leider fehlen mir nicht-triviale Beispiele von Maximen welche den kategorischen Imperativ uneingeschränkt
auf allen Handlungsabsichten erfüllen.
›
text‹Die Vorbedingung \<^term>‹ausfuehrbar ich welt ha› in \<^const>‹kategorischer_imperativ_auf›
wirkt etwas holprig.
Wir brauchen sie aber, um pathologische Grenzfälle auszuschließen.
Beispielsweise ist von-sich-selbst stehlen eine (nicht ausführbare) No-Op.
No-ops sind normalerweise nicht böse.
Stehlen ist schon böse.
Dieser Grenzfall in dem Stehlen zur no-op wird versteckt also den Charakter der
Handlungsabsicht und muss daher ausgeschlossen werden.
Da Handlungen partiell sind, ist von-sich-selbst-stehlen auch also nicht ausführbar modelliert,
da Stehlen bedeutet "jemand anderen etwas wegnehmen" und im Grenzfall "von sich selbst stehlen"
nicht definiert ist.
›
text‹In der Definition \<^const>‹kategorischer_imperativ› ist \<^const>‹wohlgeformte_handlungsabsicht›
ein technisch notwendiges Implementierungsdetail um nicht-wohlgeformte Handlungen
auszuschließen.›
text‹Minimal andere Formulierung:›
lemma
‹kategorischer_imperativ wps welt m ⟷
(∀ha.
(∃p.
wohlgeformte_handlungsabsicht wps welt ha ∧
ausfuehrbar p welt ha ∧
okay m p (handeln p welt ha))
⟶ moralisch welt m ha)›
unfolding kategorischer_imperativ_def kategorischer_imperativ_auf_def
apply(simp)
by blast
text‹Der Existenzquantor lässt sich auch in einen Allquantor umschreiben:›
lemma
‹kategorischer_imperativ wps welt m ⟷
(∀ha ich.
wohlgeformte_handlungsabsicht wps welt ha ∧ ausfuehrbar ich welt ha ∧
okay m ich (handeln ich welt ha) ⟶ moralisch welt m ha)›
apply(simp add: kategorischer_imperativ_def kategorischer_imperativ_auf_def)
by blast
text‹Vergleich zu \<^const>‹moralisch›.
Wenn eine Handlung moralisch ist, dann impliziert diese Handlung die Kernforderung des
\<^const>‹kategorischer_imperativ›.
Wenn die Handlungsabsicht für mich okay ist, ist sie auch für alle anderen okay.›
lemma ‹moralisch welt m ha ⟹
kategorischer_imperativ_auf ha welt m›
by(simp add: moralisch_simp kategorischer_imperativ_auf_def)
text‹Die andere Richtung gilt nicht,
z.B. ist die Maxime die immer False zurückgibt ein Gegenbeispiel.›
beispiel
‹m = Maxime (λ_ _. False) ⟹
kategorischer_imperativ_auf ha welt m ⟶ moralisch welt m ha
⟹ False›
by(simp add: kategorischer_imperativ_auf_def moralisch_simp)
lemma kategorischer_imperativ_auf_simp:
‹kategorischer_imperativ_auf ha welt m ⟷
(∀ p1 p2 ich.
ausfuehrbar ich welt ha ∧ okay m ich (handeln ich welt ha)
⟶ okay m p1 (handeln p2 welt ha))›
by(simp add: kategorischer_imperativ_auf_def moralisch_simp)
text‹Der \<^const>‹kategorischer_imperativ› lässt sich auch wie folgt umformulieren.
Für jede Handlungsabsicht:
wenn ich so handeln würde muss es auch okay sein, wenn zwei beliebige
Personen so handeln, wobei einer Täter und einer Opfer ist.›
lemma kategorischer_imperativ_simp:
‹kategorischer_imperativ wps welt m ⟷
(∀ha p1 p2 ich.
wohlgeformte_handlungsabsicht wps welt ha ∧ ausfuehrbar ich welt ha ∧
okay m ich (handeln ich welt ha)
⟶ okay m p1 (handeln p2 welt ha))›
apply(simp add: kategorischer_imperativ_def kategorischer_imperativ_auf_simp)
by blast
text‹Introduction rules›
lemma kategorischer_imperativI:
‹(⋀ha ich p1 p2. wohlgeformte_handlungsabsicht wps welt ha ⟹
ausfuehrbar ich welt ha ⟹
okay m ich (handeln ich welt ha) ⟹ okay m p1 (handeln p2 welt ha)
)
⟹ kategorischer_imperativ wps welt m›
by(auto simp add: kategorischer_imperativ_simp)
lemma kategorischer_imperativ_aufI:
‹(⋀ich p1 p2. ausfuehrbar ich welt ha
⟹ okay m ich (handeln ich welt ha) ⟹ okay m p1 (handeln p2 welt ha))
⟹ kategorischer_imperativ_auf ha welt m›
by(auto simp add: kategorischer_imperativ_auf_def moralisch_simp)
text‹Um den \<^const>‹kategorischer_imperativ_auf› einer Handlungsabsicht zu zeigen muss
die Handlungsabsicht moralisch sein,
oder es darf keine Person geben, die diese Handlung auch tatsächlich
unter gegebener Maxime ausführen würde:›
lemma kategorischer_imperativ_auf2:
‹kategorischer_imperativ_auf ha welt m ⟷
moralisch welt m ha ∨ ¬(∃ p. ausfuehrbar p welt ha ∧ okay m p (handeln p welt ha))›
by(auto simp add: kategorischer_imperativ_auf_def moralisch_simp)
corollary
‹kategorischer_imperativ_auf ha welt m ⟷
moralisch welt m ha ∨ (∀ p. ausfuehrbar p welt ha ⟶ ¬ okay m p (handeln p welt ha))›
by (simp add: kategorischer_imperativ_auf2)
text‹Man könnte auch sagen,
damit eine Handlungsabsicht den kategorischen Imperativ erfüllt,
muss die Handlungsabsicht entweder für alle moralisch sein,
oder die Handlungsabsicht (soweit ausführbar) ist für alle nicht okay.›
lemma katimp_eq_entweder_moralisch_oder_nicht_okay:
assumes ‹∃p. ausfuehrbar p welt ha›
shows
‹kategorischer_imperativ_auf ha welt m ⟷
(moralisch welt m ha ⊕ (∀p. ausfuehrbar p welt ha ⟶ ¬ okay m p (handeln p welt ha)))›
apply(simp add: xor_def)
apply(simp add: kategorischer_imperativ_auf2)
apply(case_tac "moralisch welt m ha")
apply(simp)
apply (simp add: assms moralisch_simp; fail)
apply(simp; fail)
done
text‹Also entweder ist die Absicht ∗‹für alle› okay, oder sie ist ∗‹für alle› nicht okay.›
lemma
‹∀p. ausfuehrbar p welt ha ⟹
kategorischer_imperativ_auf ha welt m
⟷
(moralisch welt m ha ⊕ (∀p. ¬ okay m p (handeln p welt ha)))›
apply(simp add: xor_def)
apply(simp add: kategorischer_imperativ_auf2)
apply(case_tac "moralisch welt m ha")
apply(simp add: moralisch_simp)
apply(simp)
done
lemma
‹(moralisch welt m ha ⊕ (∀p. ¬ okay m p (handeln p welt ha)))
⟹ kategorischer_imperativ_auf ha welt m›
apply(simp add: xor_def)
apply(simp add: kategorischer_imperativ_auf2)
apply(case_tac "moralisch welt m ha")
apply(simp)+
done
text‹Für Beispiele wird es einfacher zu zeigen, dass eine Maxime nicht den
kategorischen Imperativ erfüllt, wenn wir direkt ein Beispiel angeben.›
definition ‹kategorischer_imperativ_gegenbeispiel wps welt m ha ich p1 p2 ≡
wohlgeformte_handlungsabsicht wps welt ha ∧
ausfuehrbar ich welt ha ∧ okay m ich (handeln ich welt ha) ∧
¬ okay m p1 (handeln p2 welt ha)›
lemma ‹kategorischer_imperativ_gegenbeispiel wps welt m ha ich p1 p2 ⟹
¬ kategorischer_imperativ wps welt m›
apply(simp add: kategorischer_imperativ_simp kategorischer_imperativ_gegenbeispiel_def)
apply(rule_tac x=‹ha› in exI, simp)
by blast
subsection‹Triviale Maximen die den Kategorischen Imperativ immer Erfüllen›
text‹
Die Maxime die keine Handlung erlaubt (weil immer False) erfüllt den kategorischen
Imperativ:›
beispiel ‹kategorischer_imperativ wps welt (Maxime (λich h. False))›
by(simp add: kategorischer_imperativ_simp)
text‹Allerdings kann mit so einer Maxime nie etwas moralisch sein.›
beispiel ‹¬ moralisch welt (Maxime (λich h. False)) h›
by(simp add: moralisch_simp)
text‹Die Maxime die jede Handlung erlaubt (weil immer True) erfüllt den kategorischen
Imperativ:›
beispiel ‹kategorischer_imperativ wps welt (Maxime (λich h. True))›
by(simp add: kategorischer_imperativ_simp)
text‹Allerdings ist mit so einer Maxime alles moralisch.›
beispiel ‹moralisch welt (Maxime (λich h. True)) h›
by(simp add: moralisch_simp)
subsection‹Zusammenhang Goldene Regel›
text‹
Mit der goldenen Regel konnten wir wie folgt moralische Entscheidungen treffen:
@{thm goldene_regel}
In Worten:
Wenn eine Handlungsabsicht moralisch ist (nach goldener Regel)
und es okay ist für mich diese Handlung auszuführen,
dann ist es auch für mich okay, wenn jeder andere diese Handlung mit mir als Opfer ausführt.
Der kategorische Imperativ hebt diese eine Abstraktionsebene höher.
Wenn eine Maxime den kategorischen Imperativ erfüllt
und es okay ist für mich eine Handlung nach dieser Maxime auszuführen (wie in der goldenen Regel),
dann ist diese Handlungsabsicht allgemein moralisch.
Die goldene Regel konnte nur folgern, dass eine Handlungsabsicht auch okay ist wenn ich das
Opfer wäre, der kategorisch Imperativ schließt, dass eine Handlungsabsicht allgemein moralisch
sein muss, wobei beliebige Personen (nicht nur ich) Täter und Opfer sein können.
›
lemma
‹kategorischer_imperativ_auf ha welt m ⟹
(∀ p ich.
ausfuehrbar ich welt ha ∧ okay m ich (handeln ich welt ha)
⟶ okay m p (handeln ich welt ha))›
apply(simp add: kategorischer_imperativ_auf_simp)
by blast
lemma
assumes ausgangszustand_ist_gut: ‹∀p. okay m p (Handlung welt welt)›
shows
‹kategorischer_imperativ_auf ha welt m ⟹
(∀ p ich.
okay m ich (handeln ich welt ha)
⟶ okay m p (handeln ich welt ha))›
apply(simp add: kategorischer_imperativ_auf_simp)
apply(clarsimp)
apply (metis ausgangszustand_ist_gut handeln_def nicht_ausfuehrbar_nachher_handeln)
done
lemma ‹kategorischer_imperativ wps welt m ⟹
wohlgeformte_handlungsabsicht wps welt ha ⟹
ausfuehrbar ich welt ha ⟹
okay m ich (handeln ich welt ha) ⟹ moralisch welt m ha›
by(auto simp add: kategorischer_imperativ_simp moralisch_simp)
text‹
In Worten:
Wenn eine Maxime den kategorischen Imperativ erfüllt
und es für eine beliebige (wohlgeformte) Handlung auszuführen für mich okay ist diese auszuführen,
dann ist diese Handlung moralisch..
›
subsection‹Maximen die den Kategorischen Imperativ immer Erfüllen›
text‹Wenn eine Maxime jede Handlungsabsicht als moralisch bewertet,
erfüllt diese Maxime den kategorischen Imperativ.
Da diese Maxime jede Handlung erlaubt, ist es dennoch eine wohl ungeeignete Maxime.›
lemma ‹∀ha. moralisch welt maxime ha ⟹ kategorischer_imperativ wps welt maxime›
apply(cases ‹maxime›, rename_tac m)
by(simp add: kategorischer_imperativ_simp moralisch_simp)
text‹Eine Maxime die das ich und die Handlung ignoriert erfüllt den kategorischen Imperativ.›
lemma blinde_maxime_katimp:
‹kategorischer_imperativ wps welt (Maxime (λich h. m))›
apply(rule kategorischer_imperativI)
by(simp)
text‹Sollte eine Handlungsabsicht nicht ausführbar,
sein erfüllt sie immer den kategorischen Imperativ.›
lemma nicht_ausfuehrbar_katimp:
‹∀p. ¬ ausfuehrbar p welt ha ⟹ kategorischer_imperativ_auf ha welt m›
apply(rule kategorischer_imperativ_aufI)
by simp
text‹Eine Maxime welche das \<^term>‹ich::'person› ignoriert,
also nur die Handlung global betrachtet, erfüllt den kategorischen Imperativ
(mit einigen weiteren Annahmen).›
theorem globale_maxime_katimp:
fixes P :: ‹'welt handlung ⇒ bool›
assumes mhg: ‹∀p. maxime_und_handlungsabsicht_generalisieren wps welt (Maxime (λich::'person. P)) ha p›
and maxime_erlaubt_untaetigkeit: ‹∀p. ist_noop (handeln p welt ha) ⟶ okay (Maxime (λich::'person. P)) p (handeln p welt ha)›
and kom: ‹wpsm_kommutiert (Maxime (λich::'person. P)) wps welt›
and wps_sym:
‹∀p1 p2 welt. wps p1 p2 welt = wps p2 p1 welt›
and wps_id:
‹∀p1 p2 welt. wps p1 p2 (wps p1 p2 welt) = welt›
and wfh: ‹wohlgeformte_handlungsabsicht wps welt ha›
shows ‹kategorischer_imperativ_auf ha welt (Maxime (λich::'person. P))›
proof(rule kategorischer_imperativ_aufI, simp)
fix ich p2 :: ‹'person›
assume ausfuehrbarich: ‹ausfuehrbar ich welt ha›
and okayich: ‹P (handeln ich welt ha)›
from wps_id wps_sym have wpsid_swapped: ‹wps_id wps welt›
by(simp add: wps_id_def)
obtain h where h: ‹ha = Handlungsabsicht h›
by(cases ‹ha›, blast)
show ‹P (handeln p2 welt ha)›
proof(cases ‹¬ ausfuehrbar p2 welt ha›)
case True
assume ‹¬ ausfuehrbar p2 welt ha›
hence ‹ist_noop (handeln p2 welt ha)› using nicht_ausfuehrbar_ist_noop by fast
with maxime_erlaubt_untaetigkeit show ‹P (handeln p2 welt ha)› by simp
next
case False
assume ‹¬ ¬ ausfuehrbar p2 welt ha›
with wohlgeformte_handlungsabsicht_ausfuehrbar[OF wfh]
have mhg_pre: ‹ausfuehrbar ich (wps p2 ich welt) (Handlungsabsicht h)› using h by blast
from ausfuehrbarich mhg_pre[simplified h] mhg[simplified maxime_und_handlungsabsicht_generalisieren_def h] okayich[simplified h]
have
‹P (handeln ich (wps p2 ich welt) ha)›
by(auto simp add: h)
with wps_sym have
‹P (handeln ich (wps ich p2 welt) ha)›
by(simp)
with wfh_wpsm_kommutiert_simp[OF wpsid_swapped wfh kom] show ‹P (handeln p2 welt ha)›
by(simp add: h)
qed
qed
subsection‹Ausführbarer Beispielgenerator›
text‹Gegeben sei eine Welt, sowie eine Maxime, und eine Liste von Handlungsabsichten.
Wir wollen nun wissen ob die Maxime und Handlungsabsichten wohlgeformt sind,
und wenn ja, ob die Maxime auf diesen Handlungsabsichten den kategorischen Imperativ erfüllt,
und wie die Handlungen bewertet werden.›
text‹List comprehension syntax is sometime hard. Here is an example.›
value‹[(x,y). x ← xs, y ← ys, x ≠ y]›
definition alle_moeglichen_handlungen
:: ‹'welt ⇒ ('person::enum, 'welt) handlungsabsicht ⇒ 'welt handlung list›
where
‹alle_moeglichen_handlungen welt ha ≡ [handeln p welt ha. p ← (Enum.enum::'person list)]›
lemma set_alle_moeglichen_handlungen:
‹set (alle_moeglichen_handlungen welt ha) = {handeln p welt ha | p. True}›
apply(simp add: alle_moeglichen_handlungen_def)
apply(simp add: enum_class.enum_UNIV)
by blast
record ('person, 'welt) beipiel =
bsp_erfuellte_maxime :: ‹bool›
bsp_erlaubte_handlungen :: ‹('person, 'welt) handlungsabsicht list›
bsp_verbotene_handlungen :: ‹('person, 'welt) handlungsabsicht list›
bsp_uneindeutige_handlungen :: ‹('person, 'welt) handlungsabsicht list›
definition erzeuge_beispiel
:: ‹('person::enum, 'welt) wp_swap ⇒ 'welt ⇒
('person, 'welt) handlungsabsicht list ⇒ ('person, 'welt) maxime
⇒ ('person, 'welt) beipiel option›
where
‹erzeuge_beispiel wps welt has m ≡
if (∃h∈ (⋃ha ∈ set has. set (alle_moeglichen_handlungen welt ha)). ¬wohlgeformte_maxime_auf h wps m)
∨ (∃ha∈set has. ¬ wohlgeformte_handlungsabsicht wps welt ha)
then None
else Some
⦇
bsp_erfuellte_maxime = if ∀ha∈set has. kategorischer_imperativ_auf ha welt m then True else False,
bsp_erlaubte_handlungen = [ha←has. kategorischer_imperativ_auf ha welt m ∧ moralisch welt m ha],
bsp_verbotene_handlungen = [ha←has. kategorischer_imperativ_auf ha welt m ∧ ¬ moralisch welt m ha],
bsp_uneindeutige_handlungen = [ha←has. ¬ kategorischer_imperativ_auf ha welt m]
⦈›
text‹I think the following definition leads to more efficient evaluation.
And it allows reasoning about one \<^typ>‹('person, 'welt) handlungsabsicht› in isolation.›
definition erzeuge_beispiel_alt1
:: ‹('person::enum, 'welt) wp_swap ⇒ 'welt ⇒
('person, 'welt) handlungsabsicht ⇒ ('person, 'welt) maxime
⇒ ('person, 'welt) beipiel option›
where
‹erzeuge_beispiel_alt1 wps welt ha m ≡
if (∃h∈set (alle_moeglichen_handlungen welt ha). ¬wohlgeformte_maxime_auf h wps m)
∨ ¬ wohlgeformte_handlungsabsicht wps welt ha
then None
else Some
(if kategorischer_imperativ_auf ha welt m
then
⦇
bsp_erfuellte_maxime = True,
bsp_erlaubte_handlungen = if moralisch welt m ha then [ha] else [],
bsp_verbotene_handlungen = if ¬ moralisch welt m ha then [ha] else [],
bsp_uneindeutige_handlungen = []
⦈
else
⦇
bsp_erfuellte_maxime = False,
bsp_erlaubte_handlungen = [],
bsp_verbotene_handlungen = [],
bsp_uneindeutige_handlungen = [ha]
⦈
)›
fun beispiel_merge
:: ‹('person, 'welt) beipiel ⇒ ('person, 'welt) beipiel ⇒ ('person, 'welt) beipiel›
where
‹beispiel_merge
⦇ bsp_erfuellte_maxime=t1,
bsp_erlaubte_handlungen=e1, bsp_verbotene_handlungen=v1, bsp_uneindeutige_handlungen=u1 ⦈
⦇ bsp_erfuellte_maxime=t2,
bsp_erlaubte_handlungen=e2, bsp_verbotene_handlungen=v2, bsp_uneindeutige_handlungen=u2 ⦈
= ⦇ bsp_erfuellte_maxime = t1 ∧ t2,
bsp_erlaubte_handlungen= e1 @ e2,
bsp_verbotene_handlungen= v1 @ v2,
bsp_uneindeutige_handlungen= u1 @ u2
⦈›
lemma beispiel_merge_distrib:
‹beispiel_merge (beispiel_merge a b) c = beispiel_merge a (beispiel_merge b c)›
apply(case_tac ‹a›, case_tac ‹b›, case_tac ‹c›)
apply(simp)
done
text‹Combines \<^typ>‹'a option›, but if one of them is \<^const>‹None›,
the whole result is \<^const>‹None›. This is different from library's \<^const>‹combine_options›.›
definition merge_options :: ‹('a ⇒ 'a ⇒ 'a) ⇒ 'a option ⇒ 'a option ⇒ 'a option› where
‹merge_options f x y ≡
(case x of None ⇒ None | Some x ⇒ (case y of None ⇒ None | Some y ⇒ Some (f x y)))›
lemma merge_options_simps:
‹merge_options f None b = None›
‹merge_options f a None = None›
apply(simp add: merge_options_def)+
apply(cases ‹a›, simp_all)
done
lemma merge_options_distrib:
‹merge_options beispiel_merge (merge_options beispiel_merge a b) c
= merge_options beispiel_merge a (merge_options beispiel_merge b c)›
by(simp add: merge_options_def beispiel_merge_distrib split: option.split)
definition erzeuge_beispiel_alt_start :: ‹('person, 'welt) beipiel option› where
‹erzeuge_beispiel_alt_start ≡ Some
⦇ bsp_erfuellte_maxime=True,
bsp_erlaubte_handlungen=[], bsp_verbotene_handlungen=[], bsp_uneindeutige_handlungen=[] ⦈›
definition erzeuge_beispiel_alt
:: ‹('person::enum, 'welt) wp_swap ⇒ 'welt ⇒
('person, 'welt) handlungsabsicht list ⇒ ('person, 'welt) maxime
⇒ ('person, 'welt) beipiel option›
where
‹erzeuge_beispiel_alt wps welt has m
≡ fold
(λha acc. merge_options beispiel_merge acc (erzeuge_beispiel_alt1 wps welt ha m))
has
erzeuge_beispiel_alt_start
›
lemma erzeuge_beispiel_alt_start_neutral:
‹merge_options beispiel_merge erzeuge_beispiel_alt_start bsp = bsp›
apply(cases ‹bsp›)
apply(simp add: merge_options_def split:option.split)
apply(rename_tac bsp2, case_tac ‹bsp2›)
apply(simp add: merge_options_def erzeuge_beispiel_alt_start_def)
done
lemma erzeuge_beispiel1_alt:
‹erzeuge_beispiel_alt1 wps welt ha m = erzeuge_beispiel wps welt [ha] m›
by(simp add: erzeuge_beispiel_def erzeuge_beispiel_alt1_def)
lemma erzeuge_beispiel_cons:
‹erzeuge_beispiel wps welt (ha # has) m
= merge_options beispiel_merge (erzeuge_beispiel wps welt [ha] m) (erzeuge_beispiel wps welt has m)›
unfolding erzeuge_beispiel_def
apply(simp only: merge_options_simps split: if_split)
apply(intro conjI impI)
apply(simp_all only:, simp_all)
apply(blast | simp add: merge_options_def)+
done
lemma fold_merge_options_pullout:
‹fold (λha acc. merge_options beispiel_merge acc (f ha)) has
(merge_options beispiel_merge start start2)
= merge_options beispiel_merge start
(fold (λha acc. merge_options beispiel_merge acc (f ha)) has start2)›
apply(induction ‹has› arbitrary: ‹start› ‹start2›)
apply(simp; fail)
apply(simp add: merge_options_distrib)
done
lemma erzeuge_beispiel_alt_induct_helper:
‹merge_options beispiel_merge start (erzeuge_beispiel wps welt has m)
= fold (λha acc. merge_options beispiel_merge acc (erzeuge_beispiel_alt1 wps welt ha m)) has start›
apply(induction ‹has› arbitrary: ‹start›)
apply(simp add: erzeuge_beispiel_def merge_options_def split: option.split)
apply(clarsimp, rename_tac bsp)
apply(case_tac ‹bsp›, simp; fail)
apply(rename_tac ha has start)
apply(simp)
apply(subst erzeuge_beispiel_cons)
apply(simp)
apply(simp add: erzeuge_beispiel1_alt)
apply(simp add: fold_merge_options_pullout)
done
lemma erzeuge_beispiel_alt_helper:
‹erzeuge_beispiel wps welt has m
= fold
(λha acc. merge_options beispiel_merge acc(erzeuge_beispiel_alt1 wps welt ha m))
has
erzeuge_beispiel_alt_start›
apply(subst erzeuge_beispiel_alt_induct_helper[symmetric])
apply(simp add: erzeuge_beispiel_alt_start_neutral)
done
text‹The following looks like a perfect code equation.
But for some reasons, the document builds faster when not making this a ▩‹[code]›.›
lemma erzeuge_beispiel_alt:
‹erzeuge_beispiel = erzeuge_beispiel_alt›
by(simp add: fun_eq_iff erzeuge_beispiel_alt_def erzeuge_beispiel_alt_helper)