11235
|
1 |
theory Ind = Main:
|
|
2 |
|
|
3 |
section{*Inductive Definitions*}
|
|
4 |
|
|
5 |
|
|
6 |
subsection{*Even Numbers*}
|
|
7 |
|
|
8 |
subsubsection{*The Definition*}
|
|
9 |
|
|
10 |
consts even :: "nat set"
|
|
11 |
inductive even
|
|
12 |
intros
|
|
13 |
zero[intro!]: "0 \<in> even"
|
|
14 |
step[intro!]: "n \<in> even \<Longrightarrow> Suc(Suc n) \<in> even"
|
|
15 |
|
|
16 |
lemma [simp,intro!]: "2 dvd n \<Longrightarrow> 2 dvd Suc(Suc n)"
|
|
17 |
apply (unfold dvd_def)
|
|
18 |
apply clarify
|
|
19 |
apply (rule_tac x = "Suc k" in exI, simp)
|
|
20 |
done
|
|
21 |
|
|
22 |
subsubsection{*Rule Induction*}
|
|
23 |
|
|
24 |
thm even.induct
|
|
25 |
|
|
26 |
lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
|
|
27 |
apply (erule even.induct)
|
|
28 |
apply simp_all
|
|
29 |
done
|
|
30 |
|
|
31 |
subsubsection{*Rule Inversion*}
|
|
32 |
|
|
33 |
inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even"
|
|
34 |
thm Suc_Suc_case
|
|
35 |
|
|
36 |
lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even"
|
|
37 |
by blast
|
|
38 |
|
|
39 |
|
|
40 |
subsection{*Mutually Inductive Definitions*}
|
|
41 |
|
|
42 |
consts evn :: "nat set"
|
|
43 |
odd :: "nat set"
|
|
44 |
|
|
45 |
inductive evn odd
|
|
46 |
intros
|
|
47 |
zero: "0 \<in> evn"
|
|
48 |
evnI: "n \<in> odd \<Longrightarrow> Suc n \<in> evn"
|
|
49 |
oddI: "n \<in> evn \<Longrightarrow> Suc n \<in> odd"
|
|
50 |
|
|
51 |
lemma "(m \<in> evn \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 2 dvd (Suc n))"
|
|
52 |
apply(rule evn_odd.induct)
|
|
53 |
by simp_all
|
|
54 |
|
|
55 |
|
|
56 |
subsection{*The Reflexive Transitive Closure*}
|
|
57 |
|
|
58 |
consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
|
|
59 |
inductive "r*"
|
|
60 |
intros
|
|
61 |
rtc_refl[iff]: "(x,x) \<in> r*"
|
|
62 |
rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
|
|
63 |
|
|
64 |
lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
|
|
65 |
by(blast intro: rtc_step);
|
|
66 |
|
|
67 |
lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
|
|
68 |
apply(erule rtc.induct)
|
|
69 |
oops
|
|
70 |
|
|
71 |
lemma rtc_trans[rule_format]:
|
|
72 |
"(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
|
|
73 |
apply(erule rtc.induct)
|
|
74 |
apply(blast);
|
|
75 |
apply(blast intro: rtc_step);
|
|
76 |
done
|
|
77 |
|
|
78 |
text{*
|
|
79 |
\begin{exercise}
|
|
80 |
Show that the converse of @{thm[source]rtc_step} also holds:
|
|
81 |
@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
|
|
82 |
\end{exercise}
|
|
83 |
*}
|
|
84 |
|
|
85 |
subsection{*The accessible part of a relation*}
|
|
86 |
|
|
87 |
consts
|
|
88 |
acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
|
|
89 |
inductive "acc r"
|
|
90 |
intros
|
11293
|
91 |
"(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
|
11235
|
92 |
|
11293
|
93 |
lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}"
|
|
94 |
thm wfI
|
|
95 |
apply(rule_tac A = "acc r" in wfI)
|
|
96 |
apply (blast elim:acc.elims)
|
|
97 |
apply(simp(no_asm_use))
|
|
98 |
thm acc.induct
|
|
99 |
apply(erule acc.induct)
|
|
100 |
by blast
|
11235
|
101 |
|
|
102 |
consts
|
|
103 |
accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
|
|
104 |
inductive "accs r"
|
|
105 |
intros
|
|
106 |
"r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r"
|
|
107 |
monos Pow_mono
|
|
108 |
|
|
109 |
end
|