theory Demo8 imports Main begin

-- ---------------------------------------

text{*A manual proof in set theory:*}

thm equalityI subsetI
thm UnI1 UnI2 UnE

lemma "A \<union> B = B \<union> A" 
apply(rule equalityI)
 apply(rule subsetI)
 apply(erule UnE)
  apply(rule UnI2)
  apply(assumption)
 apply(rule UnI1)
 apply(assumption)
 apply(rule subsetI)
apply(erule UnE)
 apply(rule UnI2)
 apply(assumption)
apply(rule UnI1)
apply(assumption)
done


text{* Most simple proofs in set theory are automatic: *}

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


-- ------------------------------------------------------------------------

subsection{*Inductive definition of finite sets*}

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

print_theorems

subsection{*Inductive definition of the even numbers*}

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

print_theorems


text{* Using the introduction rules: *}
lemma "Suc(Suc(Suc(Suc 0))) \<in> Ev"
apply(rule Add2I)
apply(rule Add2I)
apply(rule ZeroI)
done

text{* Using the case elimination rules: *}
lemma "n \<in> Ev \<Longrightarrow> n = 0 \<or> (\<exists>n' \<in> Ev. n = Suc (Suc n'))"
apply (erule Ev.cases)
 apply blast
apply blast
done

text{*A simple inductive proof: *}
lemma "n \<in> Ev \<Longrightarrow> n+n \<in> Ev"
apply(erule Ev.induct)
 apply(simp)
 apply(rule ZeroI)
apply(simp)
apply(rule Add2I)
apply(rule Add2I)
apply(assumption)
done

text{* 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.intrs.  *}

declare Ev.intros[simp]

text{* A shorter proof: *}

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

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

However, here we really need the assumptions: *}

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

text{* An inductive proof of @{prop"1 \<notin> Ev"}: *}

lemma "n \<in> Ev \<Longrightarrow> n \<noteq> 1"
apply(erule Ev.induct)
apply(auto)
done

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

subsection{* Proofs about finite sets *}

text{* Above we declared @{text Ev.intrs} as simplification rules.
Now we declare @{text Fin.intrs} as introduction rules (via attribute
``intro''). Then fast and blast use them automatically.*}

declare Fin.intros [intro]

lemma "\<lbrakk> A \<in> Fin; B \<in> Fin \<rbrakk> \<Longrightarrow> A \<union> B \<in> Fin";
apply(erule Fin.induct)
apply(auto)
done

lemma "\<lbrakk> A \<in> Fin \<rbrakk> \<Longrightarrow> B \<subseteq> A \<longrightarrow> B \<in> Fin"
apply(erule Fin.induct)

txt{* 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>"}.
*}
oops

lemma "A \<in> Fin \<Longrightarrow> B \<subseteq> A \<longrightarrow> B \<in> Fin"
apply(erule Fin.induct)
apply(auto)
txt{* We need to strengthen the theorem: quantify @{text B}. *}
oops

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

-- ---------------------------------------------------

section "Inductive Predicates"

text {* The whole thing also works for predicates directly: *}

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

print_theorems

end