theory Demo9
imports Main
begin

subsection{*Inductive definition of the even numbers*}

inductive_set Ev :: "nat set" where
ZeroI[intro!]: "0 : Ev" |
Add2I[intro!]: "n : Ev ==> Suc(Suc n) : Ev"

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

text{*A simple inductive proof: *}
lemma "n:Ev ==> n+n : Ev"
thm Ev.induct
(*apply (rule_tac P = "%n. n + n : Ev" in  Ev.induct)*)
apply(erule Ev.induct)
 apply(simp)
 apply(rule Ev.ZeroI)
apply(simp)
apply(rule Ev.Add2I)
apply(rule Ev.Add2I)
apply(assumption)
done

text{* A shorter proof: *}

lemma "n:Ev ==> n+n : Ev"
apply(erule Ev.induct)
apply(auto)
done

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

lemma "n+n : Ev"
apply (induct_tac "n");
apply (auto);
done;

text{* Here we really need the assumptions: *}

lemma "[| m:Ev; n:Ev |] ==> m+n : Ev"
apply(erule Ev.induct)
apply(auto)
done

text{* You can also use the rules for Ev as conditional simplification
rules. This can shorten proofs considerably.  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.  *}

thm Ev.intros

declare Ev.intros[simp]


lemma "n+n : Ev"
apply (induct_tac "n");
apply (simp_all);
done;


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

lemma one_not_Ev: "n : Ev ==> n ~= 1"
apply(erule Ev.induct)
apply simp_all
done

text{* The general case: *}
lemma "n : Ev ==> ~(EX k. n = 2*k+1)"
apply(erule Ev.induct)
 apply(simp)
apply arith
done

subsection{* Proofs about finite sets *}

inductive_set Fin :: "'a set set" where
EmptyFin[intro!]: "{} : Fin" |
InsertFin[intro!]: "A : Fin ==> insert a A : Fin"

lemma "[| A : Fin; B <= A |] ==> B : Fin"
apply(erule Fin.induct)

txt{* The base case looks funny: why is the premise not "B <= {}"?
Because "B <= A" was not part of the conclusion we prove.
Solution: move "B <= A" into the conclusion with the use of "-->".
*}
oops

lemma "A : Fin ==> B <= A --> B : Fin"
apply(erule Fin.induct)
apply(auto)
txt{* The same old problem: we need to quantify B *}
oops

lemma "A : Fin ==> ALL B. B <= A --> B : Fin"
apply(erule Fin.induct)
 thm subset_empty
 apply(simp add: subset_empty)
 apply(rule Fin.EmptyFin)
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

text{* Inductive Relations *}

inductive Finite :: "'a set \<Rightarrow> bool" where
EmptyFinite[intro!]: "Finite {}" |
InsertFinite[intro!]: "Finite A ==> Finite (insert a A)"

lemma "[| Finite A; Finite B |] ==> Finite (A Un B)";
apply(erule Finite.induct)
apply simp
apply simp
apply auto
done

lemma ex_Max [rule_format]:
"Finite A \<Longrightarrow> A \<noteq> {} \<longrightarrow> (\<exists>(x::nat)\<in>A. (\<forall>y\<in>A. x >= y))"
apply (erule Finite.induct) 
apply simp
apply (case_tac "A = {}")
apply clarsimp
apply clarify
apply simp
apply (case_tac "a <= x")
apply (rule disjI2)
apply (rule_tac x = "x" in bexI)
apply simp
apply assumption 
apply (rule disjI1)
apply clarify
apply (erule_tac x = y in ballE)
apply arith
apply simp
done

lemma Ev_or_next_Ev: "x : Ev \<or> Suc x : Ev"
apply (induct_tac x)
apply simp
apply (erule disjE)
apply (drule Add2I, simp)
by simp

lemma Ev_nonempty: "Ev \<noteq> {}"
apply blast
done

theorem inf_ev: "\<not> Finite Ev";
apply (rule notI)
apply (frule ex_Max);
apply (rule Ev_nonempty)
apply clarify
apply (drule Add2I)
apply (erule_tac x = "Suc(Suc x)" in ballE)
apply simp
apply simp
done

text{* Mutual Inductive Relations *}

inductive 
Even :: "nat \<Rightarrow> bool" and
Odd :: "nat \<Rightarrow> bool" where
ZeroEven [intro!]: "Even 0" |
OddOne [intro!]: "Odd (Suc 0)" |
OddSucEven [intro!]: "Odd n \<Longrightarrow> Even (Suc n)" |
EvenSucOdd [intro!]: "Even n \<Longrightarrow> Odd (Suc n)"

thm Even_Odd.induct
text{* To prove a fact about Even, you need to think of what the corrsponding
fact for Odd is. *}

lemma EvenEv: "(Even n \<longrightarrow> n \<in> Ev) \<and> (Odd m \<longrightarrow> Suc m \<in> Ev)"
apply (rule Even_Odd.induct)
apply auto
done

lemma EvenSucSucEven: "Even n \<Longrightarrow> Even (Suc(Suc n))"
apply (drule EvenSucOdd)
by (rule OddSucEven)

lemma EvenEvenSucSuc: "Even (Suc (Suc n)) \<Longrightarrow> Even n"
apply (subgoal_tac "\<forall> m m'. (Even m \<longrightarrow> (\<forall> k. (m = Suc k) \<longrightarrow> Odd k))
                        \<and> (Odd m' \<longrightarrow> (\<forall> k. (m' = Suc k) \<longrightarrow> Even k))")
apply (erule_tac x = "Suc(Suc n)" in allE)
apply (erule_tac x = "Suc n" in allE)
apply simp
apply (thin_tac "Even (Suc (Suc n))")
apply clarify
thm Even_Odd.induct
apply (rule Even_Odd.induct)
apply auto
done

subsection {* General Recursive Functions *}

fun is_ev ::    "nat \<Rightarrow> bool" where
is_ev_0:        "is_ev 0 = True" |
not_is_ev_1:    "is_ev (Suc 0) = False" |
suc_suc_is_ev:  "is_ev (Suc (Suc n)) = is_ev n"

thm is_ev.induct

thm is_ev.simps


lemma is_ev_Even: "is_ev n = Even n"
apply (induct_tac n rule: is_ev.induct)
apply (clarsimp)
apply simp
apply (subgoal_tac "\<forall> n m. (Even n \<longrightarrow> (n \<noteq> Suc 0)) \<and> (Odd m \<longrightarrow> m \<noteq> 0)")
apply (erule_tac x = "Suc 0" in allE)
apply clarsimp
apply (rule allI)+
apply (rule Even_Odd.induct)
apply auto
apply (drule EvenEvenSucSuc)
apply simp
done

end