Theory Gesetze

theory Gesetze
imports Gesetz AllgemeinesGesetz Aenderung
begin

section‹Gesetze›
text‹Wir implementieren Strategien um \<^typ>‹('welt, 'a, 'b) allgemeines_gesetz_ableiten›
zu implementieren.›

subsection‹Case Law Absolut›

text‹
Gesetz beschreibt: wenn (vorher, nachher) dann Erlaubt/Verboten,
                    wobei vorher/nachher die Welt beschreiben.
Paragraphen sind einfache natürliche Zahlen.›
type_synonym 'welt case_law = ‹(nat, ('welt × 'welt), sollensanordnung) gesetz›

text‹
Überträgt einen Tatbestand wörtlich ins Gesetz.
Nicht sehr allgemein.›
definition case_law_ableiten_absolut
    :: ‹('welt, ('welt × 'welt), sollensanordnung) allgemeines_gesetz_ableiten›
  where
    ‹case_law_ableiten_absolut handlung sollensanordnung =
        Rechtsnorm
            (Tatbestand (vorher handlung, nachher handlung))
            (Rechtsfolge sollensanordnung)›

definition printable_case_law_ableiten_absolut
  :: ‹('welt ⇒'printable_world) ⇒
     ('welt, ('printable_world × 'printable_world), sollensanordnung) allgemeines_gesetz_ableiten›
  where
  ‹printable_case_law_ableiten_absolut print_world h ≡
      case_law_ableiten_absolut (map_handlung print_world h)›

subsection‹Case Law Relativ›

text‹Case Law etwas besser, wir zeigen nur die Änderungen der Welt.›
fun case_law_ableiten_relativ
    :: ‹('welt handlung ⇒ (('person, 'etwas) aenderung) list)
        ⇒ ('welt, (('person, 'etwas) aenderung) list, sollensanordnung)
              allgemeines_gesetz_ableiten›
  where
    ‹case_law_ableiten_relativ delta handlung erlaubt =
      Rechtsnorm (Tatbestand (delta handlung)) (Rechtsfolge erlaubt)›

end