doc-src/TutorialI/Overview/LNCS/Ind.thy

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

(*<*)theory Ind = Main:(*>*)

section{*Inductive Definitions*}


subsection{*Even Numbers*}

subsubsection{*The Definition*}

consts even :: "nat set"
inductive even
intros
zero[intro!]: "0 \<in> even"
step[intro!]: "n \<in> even \<Longrightarrow> Suc(Suc n) \<in> even"

lemma [simp,intro!]: "2 dvd n \<Longrightarrow> 2 dvd Suc(Suc n)"
apply (unfold dvd_def)
apply clarify
apply (rule_tac x = "Suc k" in exI, simp)
done

subsubsection{*Rule Induction*}

text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
@{thm[display] even.induct[no_vars]}*}
(*<*)thm even.induct[no_vars](*>*)

lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
apply (erule even.induct)
apply simp_all
done

subsubsection{*Rule Inversion*}

inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even"
text{* @{thm[display] Suc_Suc_case[no_vars]} *}
(*<*)thm Suc_Suc_case(*>*)

lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even"
by blast


subsection{*Mutually Inductive Definitions*}

consts evn :: "nat set"
       odd :: "nat set"

inductive evn odd
intros
zero: "0 \<in> evn"
evnI: "n \<in> odd \<Longrightarrow> Suc n \<in> evn"
oddI: "n \<in> evn \<Longrightarrow> Suc n \<in> odd"

lemma "(m \<in> evn \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 2 dvd (Suc n))"
apply(rule evn_odd.induct)
by simp_all


subsection{*The Reflexive Transitive Closure*}

consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
inductive "r*"
intros
refl[iff]:  "(x,x) \<in> r*"
step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"

lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
by(blast intro: rtc.step);

lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
apply(erule rtc.induct)
oops

lemma rtc_trans[rule_format]:
  "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
apply(erule rtc.induct)
 apply(blast);
apply(blast intro: rtc.step);
done

text{*
\begin{exercise}
Show that the converse of @{thm[source]rtc.step} also holds:
@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
\end{exercise}*}

subsection{*The accessible part of a relation*}

consts  acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
inductive "acc r"
intros
  "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"

lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}"
thm wfI
apply(rule_tac A = "acc r" in wfI)
 apply (blast elim: acc.elims)
apply(simp(no_asm_use))
thm acc.induct
apply(erule acc.induct)
by blast

consts  accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
inductive "accs r"
intros
 "r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r"
monos Pow_mono

(*<*)end(*>*)