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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy	Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,109 @@
+(*<*)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
+rtc_refl[iff]:  "(x,x) \<in> r*"
+rtc_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(*>*)