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 text{* Rule induction for set @{term even}, @{thm[source]even.induct}: |
|
25 @{thm[display] even.induct[no_vars]}*} |
|
26 (*<*)thm even.induct[no_vars](*>*) |
|
27 |
|
28 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n" |
|
29 apply (erule even.induct) |
|
30 apply simp_all |
|
31 done |
|
32 |
|
33 subsubsection{*Rule Inversion*} |
|
34 |
|
35 inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even" |
|
36 text{* @{thm[display] Suc_Suc_case[no_vars]} *} |
|
37 (*<*)thm Suc_Suc_case(*>*) |
|
38 |
|
39 lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even" |
|
40 by blast |
|
41 |
|
42 |
|
43 subsection{*Mutually Inductive Definitions*} |
|
44 |
|
45 consts evn :: "nat set" |
|
46 odd :: "nat set" |
|
47 |
|
48 inductive evn odd |
|
49 intros |
|
50 zero: "0 \<in> evn" |
|
51 evnI: "n \<in> odd \<Longrightarrow> Suc n \<in> evn" |
|
52 oddI: "n \<in> evn \<Longrightarrow> Suc n \<in> odd" |
|
53 |
|
54 lemma "(m \<in> evn \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 2 dvd (Suc n))" |
|
55 apply(rule evn_odd.induct) |
|
56 by simp_all |
|
57 |
|
58 |
|
59 subsection{*The Reflexive Transitive Closure*} |
|
60 |
|
61 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) |
|
62 inductive "r*" |
|
63 intros |
|
64 rtc_refl[iff]: "(x,x) \<in> r*" |
|
65 rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
|
66 |
|
67 lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*" |
|
68 by(blast intro: rtc_step); |
|
69 |
|
70 lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
|
71 apply(erule rtc.induct) |
|
72 oops |
|
73 |
|
74 lemma rtc_trans[rule_format]: |
|
75 "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" |
|
76 apply(erule rtc.induct) |
|
77 apply(blast); |
|
78 apply(blast intro: rtc_step); |
|
79 done |
|
80 |
|
81 text{* |
|
82 \begin{exercise} |
|
83 Show that the converse of @{thm[source]rtc_step} also holds: |
|
84 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"} |
|
85 \end{exercise}*} |
|
86 |
|
87 subsection{*The accessible part of a relation*} |
|
88 |
|
89 consts acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
|
90 inductive "acc r" |
|
91 intros |
|
92 "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
|
93 |
|
94 lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}" |
|
95 thm wfI |
|
96 apply(rule_tac A = "acc r" in wfI) |
|
97 apply (blast elim: acc.elims) |
|
98 apply(simp(no_asm_use)) |
|
99 thm acc.induct |
|
100 apply(erule acc.induct) |
|
101 by blast |
|
102 |
|
103 consts 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(*>*) |
|