equal
deleted
inserted
replaced
15 where |
15 where |
16 "fib 0 = 1" |
16 "fib 0 = 1" |
17 | "fib (Suc 0) = 1" |
17 | "fib (Suc 0) = 1" |
18 | "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
18 | "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
19 |
19 |
20 |
20 text {* partial simp and induction rules: *} |
21 text {* we get partial simp and induction rules: *} |
|
22 thm fib.psimps |
21 thm fib.psimps |
23 thm fib.pinduct |
22 thm fib.pinduct |
24 |
23 |
25 text {* There is also a cases rule to distinguish cases along the definition *} |
24 text {* There is also a cases rule to distinguish cases along the definition *} |
26 thm fib.cases |
25 thm fib.cases |
27 |
26 |
28 thm fib.domintros |
27 thm fib.domintros |
29 |
28 |
30 |
29 text {* total simp and induction rules: *} |
31 text {* Now termination: *} |
|
32 (*termination fib |
|
33 by (auto_term "less_than")*) |
|
34 |
|
35 thm fib.simps |
30 thm fib.simps |
36 thm fib.induct |
31 thm fib.induct |
37 |
|
38 |
32 |
39 section {* Currying *} |
33 section {* Currying *} |
40 |
34 |
41 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
35 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
42 where |
36 where |
60 shows "nz x = 0" |
54 shows "nz x = 0" |
61 using trm |
55 using trm |
62 by induct auto |
56 by induct auto |
63 |
57 |
64 termination nz |
58 termination nz |
65 apply (auto_term "less_than") -- {* Oops, it left us something to prove *} |
59 by (relation "less_than") (auto simp:nz_is_zero) |
66 by (auto simp:nz_is_zero) |
|
67 |
60 |
68 thm nz.simps |
61 thm nz.simps |
69 thm nz.induct |
62 thm nz.induct |
70 |
63 |
71 text {* Here comes McCarthy's 91-function *} |
64 text {* Here comes McCarthy's 91-function *} |