equal
deleted
inserted
replaced
1 theory Ind = Main: |
1 (*<*)theory Ind = Main:(*>*) |
2 |
2 |
3 section{*Inductive Definitions*} |
3 section{*Inductive Definitions*} |
4 |
4 |
5 |
5 |
6 subsection{*Even Numbers*} |
6 subsection{*Even Numbers*} |
19 apply (rule_tac x = "Suc k" in exI, simp) |
19 apply (rule_tac x = "Suc k" in exI, simp) |
20 done |
20 done |
21 |
21 |
22 subsubsection{*Rule Induction*} |
22 subsubsection{*Rule Induction*} |
23 |
23 |
24 thm even.induct |
24 text{* Rule induction for set @{term even}, @{thm[source]even.induct}: |
|
25 @{thm[display] even.induct[no_vars]} |
|
26 *} |
|
27 (*<*)thm even.induct[no_vars](*>*) |
25 |
28 |
26 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n" |
29 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n" |
27 apply (erule even.induct) |
30 apply (erule even.induct) |
28 apply simp_all |
31 apply simp_all |
29 done |
32 done |
30 |
33 |
31 subsubsection{*Rule Inversion*} |
34 subsubsection{*Rule Inversion*} |
32 |
35 |
33 inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even" |
36 inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even" |
34 thm Suc_Suc_case |
37 text{* @{thm[display] Suc_Suc_case[no_vars]} *} |
|
38 (*<*)thm Suc_Suc_case(*>*) |
35 |
39 |
36 lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even" |
40 lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even" |
37 by blast |
41 by blast |
38 |
42 |
39 |
43 |
82 \end{exercise} |
86 \end{exercise} |
83 *} |
87 *} |
84 |
88 |
85 subsection{*The accessible part of a relation*} |
89 subsection{*The accessible part of a relation*} |
86 |
90 |
87 consts |
91 consts acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
88 acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
|
89 inductive "acc r" |
92 inductive "acc r" |
90 intros |
93 intros |
91 "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
94 "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
92 |
95 |
93 lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}" |
96 lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}" |
97 apply(simp(no_asm_use)) |
100 apply(simp(no_asm_use)) |
98 thm acc.induct |
101 thm acc.induct |
99 apply(erule acc.induct) |
102 apply(erule acc.induct) |
100 by blast |
103 by blast |
101 |
104 |
102 consts |
105 consts accs :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
103 accs :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
|
104 inductive "accs r" |
106 inductive "accs r" |
105 intros |
107 intros |
106 "r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r" |
108 "r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r" |
107 monos Pow_mono |
109 monos Pow_mono |
108 |
110 |
109 end |
111 (*<*)end(*>*) |