Theory Gesetz

theory Gesetz
imports ExecutableHelper
begin

section‹Gesetz›
text‹Definiert einen Datentyp um Gesetzestext zu modellieren.›

datatype 'a tatbestand = Tatbestand ‹'a›

datatype 'a rechtsfolge = Rechtsfolge ‹'a›

datatype ('a, 'b) rechtsnorm = Rechtsnorm ‹'a tatbestand› ‹'b rechtsfolge›

datatype 'p prg = Paragraph ‹'p› ("§")

datatype ('p, 'a, 'b) gesetz = Gesetz ‹('p prg × ('a, 'b) rechtsnorm) set›

(*
instance (Show a, Show b) => Show (Rechtsnorm a b) where
  show (Rechtsnorm tb folge) = "Wenn " ++ show tb ++ ", dann " ++ show folge
instance Show p => Show (Paragraph p) where
  show (Paragraph p) = "§" ++ show p

instance (Show p, Show a, Show b) => Show (Gesetz p a b) where
  show (Gesetz g) = S.foldl (\s p-> s ++ show_paragraph p ++ "\n") "" g
    where show_paragraph (p, rechtsnorm) = show p ++ ": " ++ show rechtsnorm

*)

text‹Beispiel, von 🌐‹https://de.wikipedia.org/wiki/Rechtsfolge›:›
value ‹Gesetz {
  (§ ''823 BGB'',
   Rechtsnorm
     (Tatbestand ''Wer vorsaetzlich oder fahrlaessig das Leben, den Koerper, die Gesundheit, (...),
                   das Eigentum oder (...) eines anderen widerrechtlich verletzt,'')
     (Rechtsfolge ''ist dem anderen zum Ersatz des daraus entstehenden Schadens verpflichtet.'')
  ),
  (§ ''985 BGB'',
   Rechtsnorm
     (Tatbestand ''Der Eigentuemer einer Sache kann von dem Besitzer'')
     (Rechtsfolge ''die Herausgabe der Sache verlangen'')
  ),
  (§ ''303 StGB'',
   Rechtsnorm
     (Tatbestand ''Wer rechtswidrig eine fremde Sache beschaedigt oder zerstoert,'')
     (Rechtsfolge ''wird mit Freiheitsstrafe bis zu zwei Jahren oder mit Geldstrafe bestraft.'')
  )
  }›


(*<*)
definition max_paragraph :: ‹nat prg set ⇒ nat› where
  [code del]: ‹max_paragraph ps ≡ if card ps = 0 then 0 else Max {p. (§ p)∈ps}›

lemma prg_set_deconstruct: ‹{p. § p ∈ ps} = (λx. case x of § p ⇒ p) ` ps›
  apply(rule set_of_constructor)
   apply(simp add: bij_def)
   apply (meson injI prg.exhaust prg.inject surj_def)
  by (metis prg.case prg.exhaust surj_def surj_f_inv_f)

lemma [code_unfold]:
  ‹max_paragraph ps = (if card ps = 0 then 0 else Max ((λpa. case pa of § p ⇒ p) ` ps))›
  by(simp add: max_paragraph_def prg_set_deconstruct)

lemma ‹max_paragraph {} = 0› by eval
lemma ‹max_paragraph {§ 1, § 7, § 2} = 7› by eval
(*>*)

fun neuer_paragraph :: ‹(nat, 'a, 'b) gesetz ⇒ nat prg› where
 ‹neuer_paragraph (Gesetz G) = § ((max_paragraph (fst ` G)) + 1)›

text‹Fügt eine Rechtsnorm als neuen Paragraphen hinzu:›
fun hinzufuegen :: ‹('a,'b) rechtsnorm ⇒ (nat,'a,'b) gesetz ⇒ (nat,'a,'b) gesetz› where
  ‹hinzufuegen rn (Gesetz G) =
    (if rn ∈ (snd ` G) then Gesetz G else Gesetz (insert (neuer_paragraph (Gesetz G), rn) G))›


text‹Modelliert ob eine Handlung ausgeführt werden muss, darf, kann, nicht muss:›
datatype sollensanordnung = Gebot | Verbot | Erlaubnis | Freistellung


text‹Beispiel:›
lemma ‹hinzufuegen
        (Rechtsnorm (Tatbestand ''tb2'') (Rechtsfolge Verbot))
        (Gesetz {(§ 1, (Rechtsnorm (Tatbestand ''tb1'') (Rechtsfolge Erlaubnis)))}) =
 Gesetz
  {(§ 2, Rechtsnorm (Tatbestand ''tb2'') (Rechtsfolge Verbot)),
   (§ 1, Rechtsnorm (Tatbestand ''tb1'') (Rechtsfolge Erlaubnis))}› by eval

end