theory week04B_demo
imports Main
begin

\<comment> \<open>---------------------------------------------------\<close>

text\<open>Defining sets:\<close>

(* try: declare [[show_sorts]] *)
term "{1, 2, 3}"

term "{x. x mod 2 = 0}"

term "{1..3}"

term "2 \<in> {1, 2, 3}"

value "(2 :: nat) \<in> {1, 2, 3}"

value "(2 :: nat) \<in> {1..3}"

value "(2 :: nat) \<in> {x. x mod 2 = 0}"

term "{1..4} - {1..3}"

value "{1..4} - {1..3} :: nat set"

value "{1..4} \<supseteq> {1..(3::nat)}"

value "{1..4} - {1..3} :: nat set"

value "{1..4} \<union> {1..3} :: nat set"

term "insert 4 {1..3}"

value "insert 4 {1..3} :: nat set"

term "(\<lambda>x. x + 1) ` {0..2}"

value "Suc ` {0..2}"


\<comment> \<open>---------------------------------------------------\<close>

text\<open>A manual proof in set theory:\<close>

thm equalityI subsetI UnI1 UnI2 UnE

lemma "(A \<union> B) = (B \<union> A)"
  sorry

(* try: find_theorems intro, find_theorems elim *)
lemma "(A \<inter> B) = (B \<inter> A)"
  sorry

text \<open>As an exercise, try the following one\<close>
lemma "(A \<union> B \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
  sorry

text\<open>Most simple proofs in set theory are automatic:\<close>

lemma "{a, b} \<inter> {b, c} = (if a=c then {a, b} else {b})"
  sorry

lemma "{a,b} \<inter> {b,c} = {b} \<union> (if a = c then {a} else {})"
  by simp

lemma "{a,b} \<inter> {b,c} = {b} \<union> {a} \<inter> {c}"
  by blast

lemma "-(A \<union> B) = (-A \<inter> -B)"
  by blast

lemma "{x. P x \<and> Q x} = {x. P x} \<inter> {x. Q x}"
  by blast

(* Useful rules for bounded quantifiers *)
thm ballI bspec bexI bexE
  ballE

\<comment> \<open>--------------------------------------------\<close>

text \<open>Introducing new types\<close>

\<comment> \<open>a new "undefined" type:\<close>
typedecl names
consts blah :: names


\<comment> \<open>simple abbreviation:\<close>
type_synonym 'a myrel = "'a \<Rightarrow> 'a \<Rightarrow> bool"

definition eq :: "'a myrel" where
  "eq x y \<equiv> (x = y)"

term "eq"

\<comment> \<open>type definition: pairs\<close>

typedef three = "{0::nat,1,2}"
  apply (rule_tac x=1 in exI)
  apply blast
  done

print_theorems
 
definition Prd :: "('a \<Rightarrow> 'b \<Rightarrow> bool) set" where
  "Prd \<equiv> {f. \<exists>a b. f = (\<lambda>x y. x=a \<and> y=b)}"

typedef ('a, 'b) prd = "Prd ::('a \<Rightarrow> 'b \<Rightarrow> bool) set"
  by (auto simp: Prd_def)
  (* To understand this proof, try:
  apply (simp add: Prd_def)
  \<comment> \<open>just need to exhibit *one* pair, any\<close>
  apply (rule_tac x="\<lambda>x y. x=blah1 \<and> y=blah2" in exI)
  apply (rule_tac x=blah1 in exI)
  apply (rule_tac x=blah2 in exI)
  apply (rule refl)
  done
  *)

print_theorems

definition pair :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) prd" where
  "pair a b \<equiv> Abs_prd (\<lambda>x y. x = a \<and> y = b)"

term Eps
definition fs :: "('a,'b) prd \<Rightarrow> 'a" where
  "fs x \<equiv> SOME a. \<exists>b. x = pair a b"

definition sn :: "('a,'b) prd \<Rightarrow> 'b" where
  "sn x \<equiv> SOME b. \<exists>a. x = pair a b"

lemma in_prd: "(\<lambda>x y. x = c \<and> y = d) \<in> Prd"
  apply (unfold Prd_def)
  apply blast
  done


lemma pair_inject:
  "pair a b = pair a' b' \<Longrightarrow> a=a' \<and> b=b'"
  (* TODO *)
  sorry

lemma pair_eq[simp]:
  "(pair a b = pair a' b') = (a=a' \<and> b=b')"
  by (blast dest: pair_inject)

lemma fs[simp]:
  "fs (pair a b) = a"
  apply (unfold fs_def)
  apply (blast dest: pair_inject)
  done

lemma sn[simp]:
  "sn (pair a b) = b"
  apply (unfold sn_def)
  apply (blast dest: pair_inject)
  done


\<comment> \<open>--------------------------------------------\<close>

section\<open>Inductive definitions\<close>

subsection\<open>Inductive definition of finite sets\<close>

inductive_set Fin :: "'a set set" where
  emptyI:  "{} \<in> Fin" |
  insertI: "A \<in> Fin \<Longrightarrow> insert a A \<in> Fin"

print_theorems

subsection\<open>Inductive definition of the even numbers\<close>

inductive_set Ev :: "nat set" where
  ZeroI: "0 \<in> Ev" |
  Add2I: "n \<in> Ev \<Longrightarrow> Suc(Suc n) \<in> Ev"

print_theorems
(* the predicate form of Ev *)
term Evp

text\<open>Using the introduction rules:\<close>
lemma "Suc(Suc(Suc(Suc 0))) \<in> Ev"
  (* try also: apply(clarsimp simp:Ev.intros) *)
  (* try also: apply(clarsimp intro!:Ev.intros) *)
  sorry

text\<open>Using the case elimination rules:\<close>
lemma "n \<in> Ev \<Longrightarrow> n = 0 \<or> (\<exists>n' \<in> Ev. n = Suc (Suc n'))"
  thm Ev.cases
  apply (blast elim: Ev.cases)
  done

text\<open>A simple inductive proof:\<close>
lemma "n \<in> Ev \<Longrightarrow> n+n \<in> Ev"
  thm Ev.induct
  sorry

text\<open>You can also use the rules for Ev as conditional simplification
rules. This can shorten proofs considerably.  \emph{Warning}:
conditional rules can lead to nontermination of the simplifier.  The
rules for Ev are OK because the premises are always `smaller' than the
conclusion. The list of rules for Ev is contained in Ev.intros.\<close>
thm Ev.intros
declare Ev.intros[simp]

text\<open>A shorter proof:\<close>

lemma "n \<in> Ev \<Longrightarrow> n+n \<in> Ev"
  apply (erule Ev.induct)
  apply simp_all
  done

text\<open>Nice example, but overkill: don't need assumption
@{prop "n \<in>Ev"} because @{prop"n+n \<in> Ev"} is true for all @{text n}.\<close>

lemma "n+n \<in> Ev"
  (* come back and try this after week05B *)
  sorry

text\<open>However, here we really need the assumptions:\<close>

lemma "\<lbrakk> m \<in> Ev; n \<in> Ev \<rbrakk> \<Longrightarrow> m+n \<in> Ev"
  apply (erule Ev.induct)
  apply auto
  done

text\<open>An inductive proof of @{prop "1 \<notin> Ev"}:\<close>
thm Ev.induct
lemma "n \<in> Ev \<Longrightarrow> n \<noteq> 1"
  apply (erule Ev.induct)
  apply simp+
  done

text\<open>The general case:\<close>
lemma "n \<in> Ev \<Longrightarrow> \<not>(\<exists>k. n = 2*k+1)"
  apply (erule Ev.induct)
   apply simp
  apply clarsimp
  apply arith
  done


subsection\<open>Proofs about finite sets\<close>

text\<open>Above we declared @{text Ev.intros} as simplification rules.
Now we declare @{text Fin.intros} as introduction rules (via attribute
``intro''). Then fast and blast use them automatically.\<close>

declare Fin.intros [intro]
thm Fin.intros
lemma "\<lbrakk> A \<in> Fin; B \<in> Fin \<rbrakk> \<Longrightarrow> A \<union> B \<in> Fin"
  apply (erule Fin.induct)
   apply simp
  apply auto
  done

lemma "\<lbrakk> A \<in> Fin; B \<subseteq> A \<rbrakk> \<Longrightarrow> B \<in> Fin"
  apply(erule Fin.induct)
  txt\<open>The base case looks funny: why is the premise not @{prop "B \<subseteq> {}"}?
      Because @{prop "B \<subseteq> A"} was not part of the conclusion we prove.
      Relief: pull @{prop "B \<subseteq> A"} into the conclusion with the help of @{text"\<longrightarrow>"}.
  \<close>
  oops

lemma "A \<in> Fin \<Longrightarrow> B \<subseteq> A \<longrightarrow> B \<in> Fin"
  apply(erule Fin.induct)
   apply auto[1]
  apply (clarsimp del: subsetI)
  txt\<open>We need to strengthen the theorem: quantify @{text B}.\<close>
  oops

lemma "A \<in> Fin \<Longrightarrow> \<forall>B. B \<subseteq> A \<longrightarrow> B \<in> Fin"
  apply(erule Fin.induct)
   apply simp
   apply (rule Fin.emptyI)
  apply (rule allI)
  apply (rule impI)
  apply simp thm subset_insert_iff insert_Diff
  apply (simp add:subset_insert_iff)
  apply (simp add:subset_insert_iff split:if_split_asm)
  apply (drule_tac A = B in insert_Diff)
  apply (erule subst)
  apply blast
  done

\<comment> \<open>---------------------------------------------------\<close>

section "Inductive Predicates"

text \<open>The whole thing also works for predicates directly:\<close>

inductive even :: "nat \<Rightarrow> bool" where
  0: "even 0" |
  2: "even n \<Longrightarrow> even (Suc (Suc n))"

print_theorems

lemma even_imp_Ev: "even x \<Longrightarrow> x \<in> Ev"
  (* come back and try this after week05B *)
  sorry

lemma Ev_imp_even: "x \<in> Ev \<Longrightarrow> even x"
  (* come back and try this after week05B *)
  sorry

lemma "even = Evp"
  unfolding Evp_Ev_eq
  (* prove this using the two sorried lemmas *)
  thm even_imp_Ev Ev_imp_even
  (* try: find_theorems intro *)
  sorry

end