Theory Simulation

theory Simulation (*TODO: rename, das ist nur fuer AllgemeinesGesetz*)
imports Gesetz Handlung AllgemeinesGesetz
begin

section‹Simulation›
text‹Gegeben eine handelnde Person und eine Maxime,
wir wollen simulieren was für ein allgemeines Gesetz abgeleitet werden könnte.›


datatype ('person, 'welt, 'a, 'b) simulation_constants = SimConsts
    ‹'person› ― ‹handelnde Person›
    ‹('person, 'welt) maxime›
    ‹('welt, 'a, 'b) allgemeines_gesetz_ableiten›

    (*moeglich :: H.Handlung world -> Bool, -- brauch ich das oder geht das mit typen?*)


text‹...›
(*<*)

text‹Simulate one \<^typ>‹('person, 'welt) handlungsabsicht› once:›
fun simulate_handlungsabsicht
    :: ‹('person, 'welt, 'a, 'b) simulation_constants ⇒
        ('person, 'welt) handlungsabsicht ⇒ 'welt ⇒ (nat, 'a, 'b) gesetz
        ⇒ ('welt × (nat, 'a, 'b) gesetz)›
  where
    ‹simulate_handlungsabsicht (SimConsts person maxime aga) ha welt g =
    (let (sollensanordnung, g') = moarlisch_gesetz_ableiten person welt maxime ha aga g in
      let w' = (if sollensanordnung = Erlaubnis
                then
                  nachher (handeln person welt ha)
                else
                  welt
               ) in
      (w', g')
    )›

lemma ‹simulate_handlungsabsicht
       (SimConsts
          ()
          (Maxime (λ_ _. True))
          (λh s. Rechtsnorm (Tatbestand h) (Rechtsfolge ''count'')))
       (Handlungsabsicht (λp w. Some (w+1)))
       (32::int)
       (Gesetz {})= 
  (33,
   Gesetz
    {(§ (Suc 0), Rechtsnorm (Tatbestand (Handlung 32 33)) (Rechtsfolge ''count''))})›
  by eval

text‹Funktion begrenzt oft anwenden bis sich die Welt nicht mehr ändert.
Parameter
 ▪ Funktion
 ▪ Maximale Anzahl Iterationen (Simulationen)
 ▪ Initialwelt
 ▪ Initialgesetz
›
fun converge
    :: ‹('welt ⇒ 'gesetz ⇒ ('welt × 'gesetz)) ⇒ nat ⇒ 'welt ⇒ 'gesetz ⇒ ('welt × 'gesetz)›
  where
      ‹converge _ 0         w g = (w, g)›
    | ‹converge f (Suc its) w g =
        (let (w', g') = f w g in
          if w = w' then
            (w, g')
          else
            converge f its w' g')›

text‹Example: Count 32..42,
      where \<^term>‹32::int› is the initial world and we do \<^term>‹10::nat› iterations.›
lemma ‹converge (λw g. (w+1, w#g)) 10 (32::int) ([]) =
        (42, [41, 40, 39, 38, 37, 36, 35, 34, 33, 32])› by eval

text‹simulate one \<^typ>‹('person, 'welt) handlungsabsicht› a few times›
definition simulateOne
    :: ‹('person, 'welt, 'a, 'b) simulation_constants ⇒
        nat ⇒ ('person, 'welt) handlungsabsicht ⇒ 'welt ⇒ (nat, 'a, 'b) gesetz
        ⇒ (nat, 'a, 'b) gesetz›
    where
    ‹simulateOne simconsts i ha w g ≡
      let (welt, gesetz) = converge (simulate_handlungsabsicht simconsts ha) i w g in
            gesetz›
(*>*)
text‹...
Die Funktion \<^const>‹simulateOne› nimmt
eine Konfiguration \<^typ>‹('person, 'welt, 'a, 'b) simulation_constants›,
eine Anzahl an Iterationen die durchgeführt werden sollen,
eine Handlung,
eine Initialwelt,
ein Initialgesetz,
und gibt das daraus resultierende Gesetz nach so vielen Iterationen zurück.


Beispiel:
Wir nehmen die mir-ist-alles-egal Maxime.
Wir leiten ein allgemeines Gesetz ab indem wir einfach nur die Handlung wörtlich ins Gesetz
übernehmen.
Wir machen \<^term>‹10› Iterationen.
Die Welt ist nur eine Zahl und die initiale Welt sei \<^term>‹32›.
Die Handlung ist es diese Zahl um Eins zu erhöhen,
Das Ergebnis der Simulation ist dann, dass wir einfach von \<^term>‹32› bis \<^term>‹42› zählen.›
lemma ‹simulateOne
        (SimConsts () (Maxime (λ_ _. True)) (λh s. Rechtsnorm (Tatbestand h) (Rechtsfolge ''count'')))
        10 (Handlungsabsicht (λp n. Some (Suc n)))
        32
        (Gesetz {}) =
  Gesetz
  {(§ 10, Rechtsnorm (Tatbestand (Handlung 41 42)) (Rechtsfolge ''count'')),
   (§ 9, Rechtsnorm (Tatbestand (Handlung 40 41)) (Rechtsfolge ''count'')),
   (§ 8, Rechtsnorm (Tatbestand (Handlung 39 40)) (Rechtsfolge ''count'')),
   (§ 7, Rechtsnorm (Tatbestand (Handlung 38 39)) (Rechtsfolge ''count'')),
   (§ 6, Rechtsnorm (Tatbestand (Handlung 37 38)) (Rechtsfolge ''count'')),
   (§ 5, Rechtsnorm (Tatbestand (Handlung 36 37)) (Rechtsfolge ''count'')),
   (§ 4, Rechtsnorm (Tatbestand (Handlung 35 36)) (Rechtsfolge ''count'')),
   (§ 3, Rechtsnorm (Tatbestand (Handlung 34 35)) (Rechtsfolge ''count'')),
   (§ 2, Rechtsnorm (Tatbestand (Handlung 33 34)) (Rechtsfolge ''count'')),
   (§ 1, Rechtsnorm (Tatbestand (Handlung 32 33)) (Rechtsfolge ''count''))}›
  by eval


text‹Eine Iteration der Simulation liefert genau einen Paragraphen im Gesetz:›
lemma ‹∃tb rf. 
  simulateOne
    (SimConsts person maxime gesetz_ableiten)
    1 handlungsabsicht
    initialwelt
    (Gesetz {})
  = Gesetz {(§ 1, Rechtsnorm (Tatbestand tb) (Rechtsfolge rf))}›
  apply(simp add: simulateOne_def moarlisch_gesetz_ableiten_def)
  apply(case_tac ‹maxime›, simp)
  apply(simp add: moralisch_unfold max_paragraph_def)
  apply(intro conjI impI)
  by(metis rechtsfolge.exhaust rechtsnorm.exhaust tatbestand.exhaust)+
end