1 theory MyFirst |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 datatype 'a list = Nil | Cons 'a "'a list" |
|
6 |
|
7 fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
8 "app Nil ys = ys" | |
|
9 "app (Cons x xs) ys = Cons x (app xs ys)" |
|
10 |
|
11 fun rev :: "'a list \<Rightarrow> 'a list" where |
|
12 "rev Nil = Nil" | |
|
13 "rev (Cons x xs) = app (rev xs) (Cons x Nil)" |
|
14 |
|
15 value "rev(Cons True (Cons False Nil))" |
|
16 |
|
17 value "1 + (2::nat)" |
|
18 value "1 + (2::int)" |
|
19 value "1 - (2::nat)" |
|
20 value "1 - (2::int)" |
|
21 |
|
22 lemma app_Nil2 [simp]: "app xs Nil = xs" |
|
23 apply(induction xs) |
|
24 apply(auto) |
|
25 done |
|
26 |
|
27 lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)" |
|
28 apply(induction xs) |
|
29 apply(auto) |
|
30 done |
|
31 |
|
32 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)" |
|
33 apply (induction xs) |
|
34 apply (auto) |
|
35 done |
|
36 |
|
37 theorem rev_rev [simp]: "rev(rev xs) = xs" |
|
38 apply (induction xs) |
|
39 apply (auto) |
|
40 done |
|
41 |
|
42 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
43 "add 0 n = n" | |
|
44 "add (Suc m) n = Suc(add m n)" |
|
45 |
|
46 lemma add_02: "add m 0 = m" |
|
47 apply(induction m) |
|
48 apply(auto) |
|
49 done |
|
50 |
|
51 value "add 2 3" |
|
52 |
|
53 (**commutative-associative**) |
|
54 lemma add_04: "add m (add n k) = add k (add m n)" |
|
55 apply(induct) |
|
56 apply(auto) |
|
57 oops |
|
58 |
|
59 fun dub :: "nat \<Rightarrow> nat" where |
|
60 "dub 0 = 0" | |
|
61 "dub m = add m m" |
|
62 |
|
63 lemma dub_01: "dub 0 = 0" |
|
64 apply(induct) |
|
65 apply(auto) |
|
66 done |
|
67 |
|
68 lemma dub_02: "dub m = add m m" |
|
69 apply(induction m) |
|
70 apply(auto) |
|
71 done |
|
72 |
|
73 value "dub 2" |
|
74 |
|
75 fun trip :: "nat \<Rightarrow> nat" where |
|
76 "trip 0 = 0" | |
|
77 "trip m = add m (add m m)" |
|
78 |
|
79 lemma trip_01: "trip 0 = 0" |
|
80 apply(induct) |
|
81 apply(auto) |
|
82 done |
|
83 |
|
84 lemma trip_02: "trip m = add m (add m m)" |
|
85 apply(induction m) |
|
86 apply(auto) |
|
87 done |
|
88 |
|
89 value "trip 1" |
|
90 value "trip 2" |
|
91 |
|
92 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
93 "mull 0 0 = 0" | |
|
94 "mull m 0 = 0" | |
|
95 (**"mull m 1 = m" | **) |
|
96 "mull m n = m*n" |
|
97 |
|
98 (**Define a function that counts the |
|
99 number of occurrences of an element in a list **) |
|
100 (** |
|
101 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
|
102 "count " |
|
103 **) |
|
104 |
|
105 |
|
106 |
|
107 |
|
108 |
|
109 |
|
110 |
|
111 |
|
112 |
|
113 |
|