Proofs and Induction

header {* The famous Dreadbury Mansion example *}

theory Agatha
imports Main

typedecl Person

  Agatha :: Person
  Charles :: Person
  butler :: Person
  livesInMansion :: "Person \<Rightarrow> bool"
  killed  :: "Person \<Rightarrow> Person \<Rightarrow> bool"
  hates :: "Person \<Rightarrow> Person \<Rightarrow> bool"
  richer :: "Person \<Rightarrow> Person \<Rightarrow> bool"

definition facts :: "bool" where
  "facts \<equiv> 
    (*Someone who lives in Dreadbury Mansion killed Aunt Agatha.*)
    (\<exists> x . livesInMansion x \<and> killed x Agatha)
    (*Agatha, the butler, and Charles live in Dreadbury Mansion, and are the only people who live
    \<and> (livesInMansion Agatha \<and> livesInMansion butler \<and> livesInMansion Charles
                \<and> (\<forall> x . x \<noteq> Agatha \<and> x \<noteq> butler \<and> x \<noteq> Charles \<longrightarrow> \<not> livesInMansion x))
    (*A killer always hates his victim, and is never richer than his victim.*)
    \<and> (\<forall> x y . killed x y \<longrightarrow> (hates x y \<and> \<not> richer x y))
    (*Charles hates no one that Aunt Agatha hates.*)
    \<and> (\<forall> x . hates Agatha x \<longrightarrow> \<not> hates Charles x)
    (*Agatha hates everyone except the butler.*)
    \<and> (\<forall> x . x \<noteq> butler \<longrightarrow> hates Agatha x)
    (*The butler hates everyone not richer than Aunt Agatha.*)
    \<and> (\<forall> x . (\<not> richer x Agatha) \<longrightarrow> hates butler x)
    (*The butler hates everyone Aunt Agatha hates.*)
    \<and> (\<forall> x . hates Agatha x \<longrightarrow> hates butler x)
    (*No one hates everyone.*)
    \<and> (\<forall> x . \<not> (\<forall> y . hates x y))
    (*Agatha is not the butler.*)
    \<and> Agatha \<noteq> butler"