Theory BeispielPerson

theory BeispielPerson
imports Main
begin

section‹Beispiel Person›
text‹Wir führen eine Beispielbevölkerung für Beispiele ein.
Sie besteht aus vier Personen.›

datatype person = Alice | Bob | Carol | Eve

text‹In Isabelle/HOL steht die Konstante \<^term>‹UNIV::'a set› vom Typ \<^typ>‹'a set› für die Menge aller \<^typ>‹'a›,
also das Universum über \<^typ>‹'a›.
Das Universum \<^term>‹UNIV::person set› vom Typ \<^typ>‹person set› unserer Bevölkerung ist sehr endlich:›
lemma UNIV_person: ‹UNIV = {Alice, Bob, Carol, Eve}›
  by(auto intro:person.exhaust UNIV_eq_I)

text‹Wir werden unterscheiden:
  ▪ \<^typ>‹'person›: generischer Typ, erlaubt es jedes Modell einer Person und Bevölkerung zu haben.
  ▪ \<^typ>‹person›: Unser minimaler Beispielstyp, bestehend aus \<^const>‹Alice›, \<^const>‹Bob›, ...
›

(*<*)
text‹
Technisch müssen wir \<^class>‹enum› implementieren, damit wir über alle Personen iterieren können.
Ansonsten würden nur Beweise funktionieren, aber keine ausführbaren Beispiele.
›
instantiation person :: ‹enum›
begin
  definition ‹enum_person ≡ [Alice, Bob, Carol, Eve]›
  definition ‹enum_all_person P ⟷ P Alice ∧ P Bob ∧ P Carol ∧ P Eve›
  definition ‹enum_ex_person P ⟷ P Alice ∨ P Bob ∨ P Carol ∨ P Eve›

instance proof
  qed (simp_all add: enum_person_def enum_all_person_def enum_ex_person_def UNIV_person)
end

text‹Also makes maps partially executable.›
lemma ‹dom [Alice ↦ (3::nat), Carol ↦ 6] = {Alice, Carol}› by eval


lemma obtain_fresh_person:
  ‹∃p::person. p ≠ p1 ∧ p ≠ p2›
  apply(cases ‹p1›, case_tac [!] ‹p2›)
  by(auto)

(*TODO: use https://www.isa-afp.org/entries/Generic_Deriving.html to get a linorder?
value "sorted_list_of_set {Alice, Carol}"
*)
(*>*)
end