equal
deleted
inserted
replaced
48 apply(auto) |
48 apply(auto) |
49 done |
49 done |
50 |
50 |
51 value "add 2 3" |
51 value "add 2 3" |
52 |
52 |
53 lemma add_04: "add m (add n k) = add k (add m n)" |
53 (**commutative-associative**) |
54 apply(induct) |
54 lemma add_04: "add m (add n k) = add (add m n) k" |
55 apply(auto) |
55 apply(induct m) |
56 oops |
56 apply(simp_all) |
|
57 done |
|
58 |
|
59 lemma add_zero: "add n 0 = n" |
|
60 sorry |
|
61 |
|
62 lemma add_Suc: "add m (Suc n) = Suc (add m n)" |
|
63 sorry |
|
64 |
|
65 lemma add_comm: "add m n = add n m" |
|
66 apply(induct m) |
|
67 apply(simp add: add_zero) |
|
68 apply(simp add: add_Suc) |
|
69 done |
57 |
70 |
58 fun dub :: "nat \<Rightarrow> nat" where |
71 fun dub :: "nat \<Rightarrow> nat" where |
59 "dub 0 = 0" | |
72 "dub 0 = 0" | |
60 "dub m = add m m" |
73 "dub m = add m m" |
61 |
74 |
89 value "trip 2" |
102 value "trip 2" |
90 |
103 |
91 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
104 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
92 "mull 0 0 = 0" | |
105 "mull 0 0 = 0" | |
93 "mull m 0 = 0" | |
106 "mull m 0 = 0" | |
94 "mull m 1 = m" | |
107 (**"mull m 1 = m" | **) |
95 "mull m n = 0" |
108 (**"mull m (1::nat) = m" | **) |
|
109 (**"mull m (suc(0)) = m" | **) |
|
110 "mull m n = mull m (n-(1::nat))" |
96 |
111 |
|
112 (**Define a function that counts the |
|
113 number of occurrences of an element in a list **) |
97 (** |
114 (** |
98 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
115 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
99 "count " |
116 "count " |
100 **) |
117 **) |
|
118 |
|
119 fun sum :: "nat \<Rightarrow> nat" where |
|
120 "sum n = 0 + \<dots> + n" |
|
121 (* prove n = n * (n + 1) div 2 *) |
101 |
122 |
102 |
123 |
103 |
124 |
104 |
125 |
105 |
126 |
106 |
127 |
107 |
128 |
108 |
129 |
109 |
130 |
110 |
131 |
|
132 |