32
|
1 |
theory Simple_Inductive_Package
|
164
|
2 |
imports Main "../Base"
|
|
3 |
uses "simple_inductive_package.ML"
|
32
|
4 |
begin
|
|
5 |
|
164
|
6 |
(*
|
|
7 |
simple_inductive
|
|
8 |
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
9 |
where
|
|
10 |
base: "trcl R x x"
|
|
11 |
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
|
|
12 |
|
|
13 |
thm trcl_def
|
|
14 |
thm trcl.induct
|
|
15 |
thm trcl.intros
|
|
16 |
|
|
17 |
simple_inductive
|
|
18 |
even and odd
|
|
19 |
where
|
|
20 |
even0: "even 0"
|
|
21 |
| evenS: "odd n \<Longrightarrow> even (Suc n)"
|
|
22 |
| oddS: "even n \<Longrightarrow> odd (Suc n)"
|
|
23 |
|
|
24 |
thm even_def odd_def
|
|
25 |
thm even.induct odd.induct
|
|
26 |
thm even0
|
|
27 |
thm evenS
|
|
28 |
thm oddS
|
|
29 |
thm even_odd.intros
|
|
30 |
|
|
31 |
simple_inductive
|
|
32 |
accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
33 |
where
|
177
|
34 |
accpartI: "(\<And>y. r y x \<Longrightarrow> accpart r y) \<Longrightarrow> accpart r x"
|
164
|
35 |
|
|
36 |
thm accpart_def
|
|
37 |
thm accpart.induct
|
|
38 |
thm accpartI
|
|
39 |
|
|
40 |
locale rel =
|
|
41 |
fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
42 |
|
|
43 |
simple_inductive (in rel) accpart'
|
|
44 |
where
|
|
45 |
accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
|
|
46 |
|
|
47 |
context rel
|
|
48 |
begin
|
|
49 |
thm accpartI'
|
|
50 |
thm accpart'.induct
|
|
51 |
end
|
|
52 |
|
|
53 |
thm rel.accpartI'
|
|
54 |
thm rel.accpart'.induct
|
|
55 |
*)
|
159
|
56 |
|
316
|
57 |
use "simple_inductive_package.ML"
|
32
|
58 |
|
159
|
59 |
|
32
|
60 |
end
|