header {* Eine Implementierung von Mengen durch Intervall-Listen *}

(*<*)
theory Aufgabe5 = Main:
(*>*)

text {* Eine m\"ogliche Implementierung von Mengen nat\"urlicher Zahlen ist als
Liste von Intervallen, ein Intervall kann dabei einfach als ein Paar 
nat\"urlicher Zahlen aufgefa{\ss}t werden. Beispielsweise kann die Menge 
@{term "{#2, #3, #5, #7, #8, #9::nat}"}
dargestellt werden durch die Liste 
@{term "[(#2, #3), (#5, #5), (#7::nat,#9::nat)]"}. *}

subsection {* Definitionen *} 

text {* Wir f\"uhren also einen neuen Typ *}

types intervals = "(nat*nat) list" 

text {* ein. Diese Typ enth\"alt alle Listen von Paaren nat\"urlicher Zahlen, 
also auch solche, die nicht die Intervall-Listen-Darstellung einer Menge sind.

F\"uhren Sie daher eine Invariante *}

consts inv :: "intervals => bool"

text {* ein, also eine Bedingung, die genau 
diejenigen Intervall-Listen charakterisiert, die Mengen nat\"urlicher Zahlen
darstellen. Wegen der Eindeutigkeit sollen die Intervalle aufsteigend
geordnet sein, die untere Grenze des Intervalls soll kleiner oder gleich der
oberen Grenze sein und die Intervalle sollen so gro{\ss} wie m\"oglich sein
(d.h. zwei direkt nebeneinanderliegende Intervalle sollen zu einem 
zusammengefasst werden). Zur Definition bietet es sich an, eine eingebettete
Funktion *}

consts inv2 :: "nat => intervals => bool"

text {* zu verwenden, die als zus\"atzlichen Parameter eine untere Grenze
f\"ur die Intervall-Listen hat und die primitiv rekursiv definiert werden
kann. 

Definieren Sie au{\ss}erdem eine Abstraktionsfunktion  *} 

consts set_of :: "intervals => nat set"

text {*
die zu einer Intervall-Liste die Menge der nat\"urlichen Zahlen liefert, 
die durch die Liste repr\"asentiert wird. (Dabei kann man voraussetzen, 
dass die Liste die Invariante erf\"ullt.)

Definieren Sie primitiv rekursive Funktionen
*}

consts add :: "(nat*nat) => intervals => intervals"
consts rem :: "(nat*nat) => intervals => intervals"

text {* Zum Einf\"ugen bzw. L\"oschen eines Intervalls in eine Intervall-Liste.
Dabei sollen, soweit wie m\"oglich, Intervalle zusammengefasst werden, so 
da{\ss} das Resultat wieder die Invariante erf\"ullt. 
*}

subsection {* Beweis der Invarianten *}

declare Let_def [simp]
declare split_split [split]

text {* Beweisen Sie zun\"achst die Monotonie von @{term inv2}. *}

lemma inv2_monoton: "inv2 m ins \<Longrightarrow> n\<le>m \<Longrightarrow> inv2 n ins"
sorry

text {*
Zeigen Sie, da{\ss} die Funktion @{term add} die Invariante erh\"allt. 
*}

theorem inv_add: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (add (i,j) ins)"
sorry

text {*
Zeigen Sie, dass die Funktion @{term rem} die Invariante erh\"allt.
*}

theorem inv_rem: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (rem (i,j) ins)"
sorry

text {* Hinweis: Beweisen Sie in beiden F\"allen zuerst mit Induktion eine 
allgemeinere Aussage \"uber @{term inv2} (siehe Abschnitt 8.3.1 im Tutorial). 
*}


subsection {* Korrektheit der Implementierung *}

text {* Zeigen Sie die Korrektheit der Funktion @{term add}. *}

theorem set_of_add: 
  "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> set_of (add (i,j) ins) = set_of [(i,j)] \<union> set_of ins"
sorry

text {*
Zeigen Sie die Korrektheit der Funktion @{term rem}.
*}

theorem set_of_rem:
  "\<lbrakk> i \<le> j; inv ins \<rbrakk> \<Longrightarrow> set_of (rem (i,j) ins) = set_of ins - set_of [(i,j)]"
sorry

text {* Hinweis: Beweisen Sie zuerst mit Induktion eine allgemeinere Aussage.
\"uber @{term inv2}. Eventuell kann es hilfreich sein, auch noch einen 
Zusammenhang \"uber @{term inv2} und @{term set_of} als Lemma zu beweisen.
*}

subsection{* Allgemeine Hinweise: *}

text {* 
\begin{itemize}
\item Es stehen Ihnen die folgenden aus der Vorlesung bekannten Methoden zur 
Verf\"ugung:
@{text "induct_tac"}~$as$\\
@{text "simp"}\\
@{text "simp (no_asm_simp)"}\\
@{text "simp (no_asm)"}\\
@{text "simp add:"}~$r$\\
@{text "simp only:"}\\
@{text "rule"}~$r$\\
@{text "erule"}~$r$\\
@{text "erule_tac"}~$x$~@{text"=\""}$t$@{text "\" in"}~$r$\\
@{text "drule"}\\
@{text "drule_tac"}~$x$~@{text"=\""}$t$@{text "\" in"}~$r$\\
@{text "arith"}\\
@{text "clarify"}\\
@{text "blast"}\\
@{text "auto"}\\
@{text "auto simp add:"}~$r$\\
@{text "force"}\\
@{text "force simp add:"}~$r$\\
@{text "force intro:"}~$r$\\
@{text "subgoal_tac \""}g@{text "\""}

\item 
Zum Beweis der Gleichheit zweier Mengen eignet sich die Anwendung der Regel
@{text "set_ext:"}~@{thm set_ext[of A B,no_vars]}.

\item 
N\"utzliche Thoreme zum Vereinfachen von Gleichungen mit Mengen sind z. B. \\
@{text "Un_Diff:"}~@{thm Un_Diff [no_vars]} \\
@{text "Diff_triv:"}~@{thm Diff_triv [no_vars]}.

\item 
Freie Varialen in Theoremen k\"onnen in der Reihenfolge ihres Auftretens in 
einem Theorem instantiiert werden mit dem Attribut @{text of}, 
zum Beispiel @{text "r [of _ _ 0]"} instantiiert die dritte in @{text r} 
auftretende Variable mit dem Wert @{text 0}.

\item Das Attribut @{text "[rule_format]"} bringt ein Theorem in das Standard 
Regel-Format. Das ist hilfreich, wenn man ein Theorem, das man mit Induktion 
beweisen will, in der Objekt-Logik formulieren will, aber im Regel-Formal 
verwenden will.

\item
Das Attribut @{text "[simplified]"} vereinfacht ein Theorem mit dem Simplifier.
Das ist insbesondere hilfreich in Kombination mit Variablen-Instantiierung.
\end{itemize}
*}(*<*)
end
(*>*)