Theory BeispielZahlenweltGesetz

theory BeispielZahlenweltGesetz
imports BeispielZahlenwelt Simulation Gesetze AllgemeinesGesetz
begin

section‹Beispiel: BeispielZahlenwelt aber mit Gesetz (Experimental)›

  (*<*)
  fun delta_zahlenwelt :: ‹(zahlenwelt, person, int) delta› where
    ‹delta_zahlenwelt (Handlung (Zahlenwelt vor_besitz) (Zahlenwelt nach_besitz)) =
        Aenderung.delta_num_fun (Handlung vor_besitz nach_besitz)›
  (*>*)

subsection‹Setup›
  text‹Wir nehmen an unsere handelnde Person ist \<^const>‹Alice›.›
  
  definition ‹beispiel_case_law_absolut maxime handlungsabsicht ≡
    simulateOne
      (SimConsts
        Alice
        maxime
        (printable_case_law_ableiten_absolut show_zahlenwelt))
      5 handlungsabsicht initialwelt (Gesetz {})›
  definition ‹beispiel_case_law_relativ maxime handlungsabsicht ≡
    simulateOne
      (SimConsts
        Alice
        maxime
        (case_law_ableiten_relativ delta_zahlenwelt))
      10 handlungsabsicht initialwelt (Gesetz {})›


subsection‹Beispiele›
  text‹Alice kann beliebig oft 5 Wohlstand für sich selbst erschaffen.
  Das entstehende Gesetz ist nicht sehr gut, da es einfach jedes Mal einen
  Snapshot der Welt aufschreibt und nicht sehr generisch ist.›
  (*check: ist auch eine moralische Handlung*)
  lemma ‹beispiel_case_law_absolut maxime_zahlenfortschritt (Handlungsabsicht (erschaffen 5))
  =
  Gesetz
  {(§ 5,
    Rechtsnorm
     (Tatbestand ([(Alice, 25), (Bob, 10), (Carol, - 3)], [(Alice, 30), (Bob, 10), (Carol, - 3)]))
     (Rechtsfolge Erlaubnis)),
   (§ 4,
    Rechtsnorm
     (Tatbestand ([(Alice, 20), (Bob, 10), (Carol, - 3)], [(Alice, 25), (Bob, 10), (Carol, - 3)]))
     (Rechtsfolge Erlaubnis)),
   (§ 3,
    Rechtsnorm
     (Tatbestand ([(Alice, 15), (Bob, 10), (Carol, - 3)], [(Alice, 20), (Bob, 10), (Carol, - 3)]))
     (Rechtsfolge Erlaubnis)),
   (§ 2,
    Rechtsnorm
     (Tatbestand ([(Alice, 10), (Bob, 10), (Carol, - 3)], [(Alice, 15), (Bob, 10), (Carol, - 3)]))
     (Rechtsfolge Erlaubnis)),
   (§ 1,
    Rechtsnorm
     (Tatbestand ([(Alice, 5), (Bob, 10), (Carol, - 3)], [(Alice, 10), (Bob, 10), (Carol, - 3)]))
     (Rechtsfolge Erlaubnis))}
  › by eval
  
  
  text‹Die gleiche Handlung, wir schreiben aber nur die Änderung der Welt ins Gesetz:›
  lemma ‹beispiel_case_law_relativ maxime_zahlenfortschritt (Handlungsabsicht (erschaffen 5)) =
    Gesetz
    {(§ 1, Rechtsnorm (Tatbestand [Gewinnt Alice 5]) (Rechtsfolge Erlaubnis))}›
    by eval

  (*TODO: Beispiele mit der guten maxime!*)
  lemma ‹beispiel_case_law_relativ
    (Maxime (λ(ich::person) h. (∀pX. individueller_fortschritt pX h))) (Handlungsabsicht (erschaffen 5)) =
  Gesetz {(§ 1, Rechtsnorm (Tatbestand [Gewinnt Alice 5]) (Rechtsfolge Erlaubnis))}›
    by eval



  text‹Nun ist es \<^const>‹Alice› verboten Wohlstand für sich selbst zu erzeugen.›
  (*check: ist auch keine moralische Handlung*)
  lemma ‹beispiel_case_law_relativ
          (Maxime (λich. individueller_strikter_fortschritt ich))
          (Handlungsabsicht (erschaffen 5)) =
    Gesetz {(§ 1, Rechtsnorm (Tatbestand [Gewinnt Alice 5]) (Rechtsfolge Verbot))}›
    by eval



  (*check: ist auch eine moralische Handlung*)
  lemma ‹beispiel_case_law_relativ
          (Maxime (λich. globaler_strikter_fortschritt))
          (Handlungsabsicht (erschaffen 5)) =
    Gesetz {(§ 1, Rechtsnorm (Tatbestand [Gewinnt Alice 5]) (Rechtsfolge Erlaubnis))}›
    by eval

    

  (*check: ist auch keine moralische Handlung*)
  lemma ‹beispiel_case_law_relativ
          (Maxime (λich. globaler_strikter_fortschritt))
          (Handlungsabsicht (erschaffen 0)) =
    Gesetz {(§ 1, Rechtsnorm (Tatbestand []) (Rechtsfolge Verbot))}›
    by eval


  (*check: ist auch keine moralische Handlung*)
  lemma ‹beispiel_case_law_relativ
          maxime_zahlenfortschritt
          (Handlungsabsicht (erschaffen 0)) =
    Gesetz {(§ 1, Rechtsnorm (Tatbestand []) (Rechtsfolge Erlaubnis))}›
    by eval

  (*check: ist auch eine moralische Handlung*)
  lemma‹beispiel_case_law_relativ
            (Maxime (λich. globaler_fortschritt))
            (Handlungsabsicht (erschaffen 0))
    =
    Gesetz {(§ 1, Rechtsnorm (Tatbestand []) (Rechtsfolge Erlaubnis))}›
    by eval

  

  (*check: ist auch eine moralische Handlung*)
  lemma‹beispiel_case_law_relativ
          (Maxime (λich. globaler_fortschritt))
          (Handlungsabsicht (stehlen_nichtwf 5 Bob))
    =
    Gesetz
    {(§ 1, Rechtsnorm (Tatbestand [Gewinnt Alice 5, Verliert Bob 5]) (Rechtsfolge Erlaubnis))}›
    by eval




  text‹Stehlen ist verboten:›
  (*check: ist auch keine moralische Handlung*)
  lemma ‹beispiel_case_law_relativ maxime_zahlenfortschritt (Handlungsabsicht (stehlen_nichtwf 5 Bob)) =
    Gesetz
    {(§ 1, Rechtsnorm (Tatbestand [Gewinnt Alice 5, Verliert Bob 5]) (Rechtsfolge Verbot))}›
    by eval



  text‹Auch wenn \<^const>‹Alice› von sich selbst stehlen möchte ist dies verboten,
  obwohl hier keiner etwas verliert:›
  (*check: ist auch keine moralische Handlung*)
  lemma ‹beispiel_case_law_relativ maxime_zahlenfortschritt (Handlungsabsicht (stehlen_nichtwf 5 Alice)) =
    Gesetz {(§ 1, Rechtsnorm (Tatbestand []) (Rechtsfolge Verbot))}›
    by eval


  text‹Der Grund ist, dass \<^const>‹Alice› die abstrakte Handlung "Alice wird bestohlen" gar nicht gut
  fände, wenn sie jemand anderes ausführt:›
(*
  lemma ‹debug_maxime show_zahlenwelt initialwelt
          maxime_zahlenfortschritt (Handlungsabsicht (stehlen_nichtwf 5 Alice)) =
   {VerletzteMaxime (Opfer Alice) (Taeter Bob)
     (Handlung [(Alice, 5), (Bob, 10), (Carol, - 3)] [(Bob, 15), (Carol, - 3)]),
    VerletzteMaxime (Opfer Alice) (Taeter Carol)
     (Handlung [(Alice, 5), (Bob, 10), (Carol, - 3)] [(Bob, 10), (Carol, 2)]),
    VerletzteMaxime (Opfer Alice) (Taeter Eve)
     (Handlung [(Alice, 5), (Bob, 10), (Carol, - 3)] [(Bob, 10), (Carol, - 3), (Eve, 5)])
   }›
    by eval
*)  
  text‹Leider ist das hier abgeleitete Gesetz sehr fragwürdig:
  \<^term>‹Rechtsnorm (Tatbestand []) (Rechtsfolge Verbot)›
  
  Es besagt, dass Nichtstun verboten ist.›

  text‹Indem wir die beiden Handlungen Nichtstun und Selbstbestehlen betrachten,
  können wir sogar ein widersprüchliches Gesetz ableiten:›
  lemma ‹simulateOne
      (SimConsts
        Alice
        maxime_zahlenfortschritt
        (case_law_ableiten_relativ delta_zahlenwelt))
      20 (Handlungsabsicht (stehlen_nichtwf 5 Alice)) initialwelt
      (beispiel_case_law_relativ maxime_zahlenfortschritt (Handlungsabsicht (erschaffen 0)))
    =
    Gesetz
  {(§ 2, Rechtsnorm (Tatbestand []) (Rechtsfolge Verbot)),
   (§ 1, Rechtsnorm (Tatbestand []) (Rechtsfolge Erlaubnis))}›
    by eval

  text‹Meine persönliche Conclusion: Wir müssen irgendwie die Absicht mit ins Gesetz schreiben.›



  text‹Es ist \<^const>‹Alice› verboten, etwas zu verschenken:›
  (*Check*)
  lemma‹beispiel_case_law_relativ maxime_zahlenfortschritt (Handlungsabsicht (schenken 5 Bob))
    =
    Gesetz
      {(§ 1,
        Rechtsnorm (Tatbestand [Verliert Alice 5, Gewinnt Bob 5]) (Rechtsfolge Verbot))}›
    by eval
  text‹Der Grund ist, dass \<^const>‹Alice› dabei etwas verliert und
  die \<^const>‹maxime_zahlenfortschritt› dies nicht Erlaubt.
  Es fehlt eine Möglichkeit zu modellieren, dass \<^const>‹Alice› damit einverstanden ist,
  etwas abzugeben.
  Doch wir haben bereits in @{thm stehlen_ist_schenken} gesehen,
  dass \<^const>‹stehlen› und \<^const>‹schenken› nicht unterscheidbar sind.›

(*TODO: gesetz ableiten aendern, so dass allgemeines gesetz ableiten eine
handlungsabsicht anstatt einer handlung nimmt.
Evtl in neue Datei, damit sich dieses Beipsiel noch gut liesst.*)


  text‹Folgende ungültige Maxime würde es erlauben, dass \<^const>‹Alice› Leute bestehlen darf:›
  lemma‹beispiel_case_law_relativ
            (Maxime (λich. individueller_fortschritt Alice))
            (Handlungsabsicht (stehlen_nichtwf 5 Bob))
    =
    Gesetz
    {(§ 1, Rechtsnorm (Tatbestand [Gewinnt Alice 5, Verliert Bob 5]) (Rechtsfolge Erlaubnis))}›
    by eval
end