Theory Steuern
theory Steuern
imports Main HOL.Real Percentage ExecutableHelper
begin
section‹Einkommensteuergesetzgebung›
text‹In diesem Abschnitt werden wir eine versuchen die Grundlagen der
Einkommenssteuergesetzgebung zu modellieren.›
text‹Helper›
definition floor :: ‹real ⇒ nat› where
‹floor x ≡ nat ⌊x⌋›
lemma floorD: ‹a ≤ b ⟹ floor a ≤ floor b›
apply(simp add: floor_def)
by linarith
lemma floor_minusD:
fixes a :: ‹nat› and a' :: ‹real›
shows ‹a ≤ b ⟹ a - a' ≤ b - b' ⟹ a - floor a' ≤ b - floor b'›
apply(simp add: floor_def)
by linarith
text‹Folgendes Modell basiert auf einer stark vereinfachten Version des deutschen Steuerrechts.
Wenn ich Wikipedia richtig verstanden habe, habe ich sogar aus Versehen einen Teil des
österreichischen Steuersystem gebaut mit deutschen Konstanten.
›
text‹Folgende @{command locale} nimmt an, dass wir eine Funktion
\<^term_type>‹steuer :: nat ⇒ nat› haben, welche basierend auf dem Einkommen
die zu zahlende Steuer berechnet.
Die \<^term>‹steuer› Funktion arbeitet auf natürlichen Zahlen.
Wir nehmen an, dass einfach immer auf ganze Geldbeträge gerundet wird.
Wie im deutschen System.
Die @{command locale} einhält einige Definition, gegeben die \<^term>‹steuer› Funktion.
Eine konkrete \<^term>‹steuer› Funktion wird noch nicht gegeben.
›
locale steuer_defs =
fixes steuer :: ‹nat ⇒ nat›
begin
definition brutto :: ‹nat ⇒ nat› where
‹brutto einkommen ≡ einkommen›
definition netto :: ‹nat ⇒ nat› where
‹netto einkommen ≡ einkommen - (steuer einkommen)›
definition steuersatz :: ‹nat ⇒ percentage› where
‹steuersatz einkommen ≡ percentage ((steuer einkommen) / einkommen)›
end
text‹Beispiel. Die \<^term>‹steuer› Funktion sagt, man muss 25 Prozent Steuern zahlen:›
definition beispiel_25prozent_steuer :: ‹nat ⇒ nat› where
‹beispiel_25prozent_steuer e ≡ nat ⌊real e * (percentage 0.25)⌋›
beispiel
‹beispiel_25prozent_steuer 100 = 25›
‹steuer_defs.brutto 100 = 100›
‹steuer_defs.netto beispiel_25prozent_steuer 100 = 75›
‹steuer_defs.steuersatz beispiel_25prozent_steuer 100 = percentage 0.25›
by(simp add: steuer_defs.brutto_def beispiel_25prozent_steuer_def
steuer_defs.netto_def percentage_code steuer_defs.steuersatz_def)+
text‹
Folgende @{command locale} erweitert die \<^locale>‹steuer_defs› @{command locale} und stellt
einige Anforderungen die eine gültige \<^term>‹steuer› Funktion erfüllen muss.
▪ Wer mehr Einkommen hat, muss auch mehr Steuern zahlen.
▪ Leistung muss sich lohnen:
Wer mehr Einkommen hat muss auch nach Abzug der Steuer mehr übrig haben.
▪ Existenzminimum: Es gibt ein Existenzminimum, welches nicht besteuert werden darf.
›
locale steuersystem = steuer_defs +
assumes wer_hat_der_gibt:
‹einkommen_a ≥ einkommen_b ⟹ steuer einkommen_a ≥ steuer einkommen_b›
and leistung_lohnt_sich:
‹einkommen_a ≥ einkommen_b ⟹ netto einkommen_a ≥ netto einkommen_b›
and existenzminimum:
‹einkommen ≤ 9888 ⟹ steuer einkommen = 0›
begin
end
text‹Eigentlich hätte ich gerne noch eine weitere Anforderung.
🌐‹https://de.wikipedia.org/wiki/Steuerprogression› sagt
"Steuerprogression bedeutet das Ansteigen des Steuersatzes in Abhängigkeit vom zu
versteuernden Einkommen oder Vermögen."
Formal betrachtet würde das bedeuten
\<^term>‹einkommen_a ≥ einkommen_b
⟹ steuer_defs.steuersatz einkommen_a ≥ steuer_defs.steuersatz einkommen_b›
Leider haben wir bereits jetzt in dem Modell eine Annahme getroffen,
die es uns quasi unmöglich macht, ein Steuersystem zu implementieren, welches die
Steuerprogression erfüllt.
Der Grund ist, dass wir die Steuerfunktion auf ganzen Zahlen definiert haben.
Aufgrund von Rundung können wir also immer Fälle haben, indem ein höheres
Einkommen einen leicht geringeren Steuersatz hat als ein geringeres Einkommen.
Beispielsweise bedeutet das für \<^const>‹beispiel_25prozent_steuer›, dass
jemand mit 100 EUR Einkommen genau 25 Prozent Steuer zahlt,
jemand mit 103 EUR Einkommen aber nur ca 24,3 Prozent Steuer zahlt.
›
beispiel
‹steuer_defs.steuersatz beispiel_25prozent_steuer 100 = percentage 0.25›
‹steuer_defs.steuersatz beispiel_25prozent_steuer 103 = percentage (25 / 103)›
‹percentage (25 / 103) < percentage 0.25›
‹(103::nat) > 100›
by(simp add: steuer_defs.brutto_def beispiel_25prozent_steuer_def
steuer_defs.netto_def percentage_code steuer_defs.steuersatz_def)+
text‹In der Praxis sollten diese kleinen Rundungsfehler kein Problem darstellen,
in diesem theoretischen Modell sorgen sie aber dafür,
dass unser Steuersystem (und wir modellieren eine vereinfachte Version des
deutschen Steuerystems) keine Steuerprogression erfüllt.›
fun zonensteuer :: ‹(nat × percentage) list ⇒ percentage ⇒ nat ⇒ real› where
‹zonensteuer ((zone, prozent)#zonen) spitzensteuer e =
((min zone e) * prozent) + (zonensteuer zonen spitzensteuer (e - zone))›
| ‹zonensteuer [] spitzensteuer e = e*spitzensteuer›
lemma zonensteuermono: ‹e1 ≤ e2
⟹ zonensteuer zs spitzensteuer e1 ≤ zonensteuer zs spitzensteuer e2›
apply(induction ‹zs› arbitrary: ‹e1› ‹e2›)
apply(simp add: mult_right_mono percentage_range; fail)
apply(rename_tac z zs e1 e2, case_tac ‹z›, rename_tac zone prozent)
apply(simp)
apply(rule Groups.add_mono_thms_linordered_semiring(1), rule conjI)
defer
apply(simp; fail)
by(simp add: mult_right_mono percentage_range)
text‹Kein Einkommen -> keine Steuer›
lemma zonensteuer_zero: ‹zonensteuer ls p 0 = 0›
by(induction ‹ls›) auto
text‹Steuer ist immer positiv.›
lemma zonensteuer_pos: ‹zonensteuer ls p e ≥ 0›
apply(induction ‹ls›)
apply(simp add: percentage_range)
by (metis zero_le zonensteuer_zero zonensteuermono)
text‹Steuer kann nicht höher sein als das Einkommen.›
lemma zonensteuer_limit: ‹zonensteuer ls spitzensteuer einkommen ≤ einkommen›
apply(induction ‹ls› arbitrary: ‹einkommen›)
apply(simp)
apply (simp add: real_of_percentage_mult; fail)
apply(rename_tac z zs einkommen, case_tac ‹z›, rename_tac zone prozent)
apply(simp)
apply(case_tac ‹zone ≤ einkommen›)
apply(simp)
apply(subst percentage_add_limit_helper, simp_all)
apply (metis of_nat_diff)
by (simp add: real_of_percentage_mult zonensteuer_zero)
lemma zonensteuer_leistung_lohnt_sich: ‹e1 ≤ e2
⟹ e1 - zonensteuer zs spitzensteuer e1 ≤ e2 - zonensteuer zs spitzensteuer e2›
proof(induction ‹zs› arbitrary: ‹e1› ‹e2›)
case Nil
then show ‹?case›
apply(simp)
using real_of_percentage_range by(metis
diff_ge_0_iff_ge mult.right_neutral mult_right_mono
of_nat_le_iff right_diff_distrib')
next
case (Cons z zs)
obtain zone prozent where z: ‹z = (zone, prozent)› by(cases ‹z›)
have ‹e1 - zone ≤ e2 - zone› using Cons.prems diff_le_mono by blast
from Cons.IH[OF this] have IH:
‹ (e1 - zone) - zonensteuer zs spitzensteuer (e1 - zone)
≤ (e2 - zone) - zonensteuer zs spitzensteuer (e2 - zone)› .
then have IH':
‹e1 - zonensteuer zs spitzensteuer (e1 - zone)
≤ e2 - zonensteuer zs spitzensteuer (e2 - zone)›
using Cons.prems by linarith
from Cons.prems percentage_nat_diff_mult_right_mono have e1e2diff:
‹e1 - e1 * prozent ≤ e2 - e2 * prozent› by simp
have
‹e1 - (min zone e1 * prozent + zonensteuer zs spitzensteuer (e1 - zone))
≤ e2 - (min zone e2 * prozent + zonensteuer zs spitzensteuer (e2 - zone))›
proof(cases ‹e1 ≤ zone›)
case True
assume ‹e1 ≤ zone›
have e1: ‹min (real zone) e1 = e1› using ‹e1 ≤ zone› by simp
from percentage_nat_diff_mult_right_mono have e1zonediff:
‹e1 - e1 * prozent ≤ zone - zone * prozent› using True by auto
show ‹?thesis›
proof(cases ‹e2 ≤ zone›)
case True
then show ‹?thesis›
apply(simp add: e1 ‹e1 ≤ zone›)
using e1e2diff by (simp)
next
case False
from False have ‹zone < e2› by simp
from this obtain mehr where mehr: ‹e2 = zone + mehr›
using less_imp_add_positive by blast
have zonensteuer_limit: ‹zonensteuer zs spitzensteuer mehr ≤ mehr›
using zonensteuer_limit by simp
from False show ‹?thesis›
apply(simp add: e1)
apply(simp add: ‹e1 ≤ zone›)
apply(simp add: mehr)
apply(simp add: zonensteuer_zero)
using e1zonediff zonensteuer_limit by linarith
qed
next
case False
have e1: ‹min zone e1 = zone› using False by auto
have e2: ‹min zone e2 = zone› using False Cons.prems by auto
from IH' e1 e2 show ‹?thesis› by (simp)
qed
then show ‹?case›
by(simp add: z)
qed
definition steuerzonen2022 :: ‹(nat × percentage) list› where
‹steuerzonen2022 ≡ [
(10347, percentage 0),
(4579, percentage 0.14),
(43670, percentage 0.2397),
(219229, percentage 0.42)
]›
fun steuerzonenAbs :: ‹(nat × percentage) list ⇒ (nat × percentage) list› where
‹steuerzonenAbs [] = []›
| ‹steuerzonenAbs ((zone, prozent)#zonen) =
(zone,prozent)#(map (λ(z,p). (zone+z, p)) (steuerzonenAbs zonen))›
text‹Die folgende Liste,
basierend auf 🌐‹https://de.wikipedia.org/wiki/Einkommensteuer_(Deutschland)#Tarif_2022›,
sagt in welchem Bereich welcher Prozentsatz an Steuern zu zahlen ist.
Beispielsweise sind die ersten \<^term>‹10347::nat› steuerfrei.
›
definition steuerbuckets2022 :: ‹(nat × percentage) list› where
‹steuerbuckets2022 ≡ [
(10347, percentage 0),
(14926, percentage 0.14),
(58596, percentage 0.2397),
(277825, percentage 0.42)
]›
text‹Für jedes Einkommen über 277825 gilt der Spitzensteuersatz von 45 Prozent.
Wir ignorieren die Progressionsfaktoren in Zone 2 und 3.›
lemma steuerbuckets2022: ‹steuerbuckets2022 = steuerzonenAbs steuerzonen2022›
by(simp add: steuerbuckets2022_def steuerzonen2022_def)
fun wfSteuerbuckets :: ‹(nat × percentage) list ⇒ bool› where
‹wfSteuerbuckets [] = True›
| ‹wfSteuerbuckets [bs] = True›
| ‹wfSteuerbuckets ((b1, p1)#(b2, p2)#bs) ⟷ b1 ≤ b2 ∧ wfSteuerbuckets ((b2,p2)#bs)›
text‹Folgende Funktion berechnet die zu zahlende Steuer, basierend auf einer Steuerbucketliste.›
fun bucketsteuerAbs :: ‹(nat × percentage) list ⇒ percentage ⇒ nat ⇒ real› where
‹bucketsteuerAbs ((bis, prozent)#mehr) spitzensteuer e =
((min bis e) * prozent)
+ (bucketsteuerAbs (map (λ(s,p). (s-bis,p)) mehr) spitzensteuer (e - bis))›
| ‹bucketsteuerAbs [] spitzensteuer e = e*spitzensteuer›
lemma wfSteuerbucketsConsD: ‹wfSteuerbuckets (z#zs) ⟹ wfSteuerbuckets zs›
apply(case_tac ‹z›, simp)
using wfSteuerbuckets.elims(3) by fastforce
lemma wfSteuerbucketsMapD:
‹wfSteuerbuckets (map (λ(z, y). (zone + z, y)) zs) ⟹ wfSteuerbuckets zs›
apply(induction ‹zs›)
apply(simp)
apply(rename_tac z zs, case_tac ‹z›)
apply(simp)
apply(case_tac ‹zs›)
apply(simp)
apply(simp)
by auto
lemma mapHelp1: ‹wfSteuerbuckets zs ⟹
(map ((λ(s, y). (s - x, y)) ∘ (λ(z, y). (x + z, y)))) zs = zs›
apply(induction ‹zs›)
apply(simp; fail)
apply(rename_tac z zs, case_tac ‹z›, rename_tac zone prozent)
apply(simp)
apply(simp add: wfSteuerbucketsConsD)
done
lemma bucketsteuerAbs_zonensteuer:
‹wfSteuerbuckets (steuerzonenAbs zs) ⟹
bucketsteuerAbs (steuerzonenAbs zs) spitzensteuer e
= zonensteuer zs spitzensteuer e›
apply(induction ‹zs› arbitrary:‹e›)
apply(simp; fail)
apply(rename_tac z zs e, case_tac ‹z›, rename_tac zone prozent)
apply(simp)
apply(subgoal_tac ‹wfSteuerbuckets (steuerzonenAbs zs)›)
apply(subst mapHelp1)
apply(simp; fail)
apply(simp; fail)
apply(simp)
apply(drule wfSteuerbucketsConsD)
using wfSteuerbucketsMapD by simp
text‹Die Einkommenssteuerberechnung, mit Spitzensteuersatz 45 Prozent und finalem Abrunden.›
definition einkommenssteuer :: ‹nat ⇒ nat› where
‹einkommenssteuer einkommen ≡
floor (bucketsteuerAbs steuerbuckets2022 (percentage 0.45) einkommen)›
text‹Beispiel. Alles unter dem Existenzminimum ist steuerfrei:›
beispiel ‹einkommenssteuer 10 = 0› by eval
beispiel ‹einkommenssteuer 10000 = 0› by eval
text‹Für ein Einkommen nur knapp über dem Existenzminimum fällt sehr wenig Steuer an:›
beispiel ‹einkommenssteuer 14000 = floor ((14000-10347)*0.14)› by eval
beispiel ‹einkommenssteuer 14000 = 511› by eval
text‹Bei einem Einkommen von 20000 EUR wird ein Teil bereits mit den höheren Steuersatz der
3. Zone besteuert:›
beispiel ‹einkommenssteuer 20000 = 1857› by eval
beispiel ‹einkommenssteuer 20000 =
floor ((14926-10347)*0.14 + (20000-14926)*0.2397)› by eval
text‹Höhere Einkommen führen zu einer höheren Steuer:›
beispiel ‹einkommenssteuer 40000 = 6651› by eval
beispiel ‹einkommenssteuer 60000 = 11698› by eval
lemma einkommenssteuer:
‹einkommenssteuer einkommen =
floor (zonensteuer steuerzonen2022 (percentage 0.45) einkommen)›
apply(simp add: einkommenssteuer_def)
apply(simp add: steuerbuckets2022)
apply(subst bucketsteuerAbs_zonensteuer)
apply(simp add: steuerzonen2022_def; fail)
apply(simp)
done
text‹Die \<^const>‹einkommenssteuer› Funktion erfüllt die Anforderungen an \<^locale>‹steuersystem›.›
interpretation steuersystem
where steuer = ‹einkommenssteuer›
proof
fix einkommen_a and einkommen_b
show ‹einkommen_a ≤ einkommen_b
⟹ einkommenssteuer einkommen_a ≤ einkommenssteuer einkommen_b›
apply(simp add: einkommenssteuer)
apply(rule floorD)
apply(rule zonensteuermono)
by(simp)
next
fix einkommen_a and einkommen_b
show ‹einkommen_b ≤ einkommen_a ⟹
steuer_defs.netto einkommenssteuer einkommen_b
≤ steuer_defs.netto einkommenssteuer einkommen_a›
apply(simp add: einkommenssteuer steuer_defs.netto_def)
thm floor_minusD
apply(rule floor_minusD, simp)
using zonensteuer_leistung_lohnt_sich by simp
next
fix einkommen
show ‹einkommen ≤ 9888 ⟹ einkommenssteuer einkommen = 0›
by(simp add: einkommenssteuer floor_def steuerzonen2022_def percentage_code)
qed
end