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 |
53 (**commutative-associative**) |
54 (**commutative-associative**) |
54 lemma add_04: "add m (add n k) = add k (add m n)" |
55 lemma add_04: "add m (add n k) = add (add m n) k" |
55 apply(induct) |
56 apply(induct m) |
56 apply(auto) |
57 apply(simp_all) |
57 oops |
58 done |
|
59 |
|
60 lemma add_zero: "add n 0 = n" |
|
61 sorry |
|
62 |
|
63 lemma add_Suc: "add m (Suc n) = Suc (add m n)" |
|
64 sorry |
|
65 |
|
66 lemma add_comm: "add m n = add n m" |
|
67 apply(induct m) |
|
68 apply(simp add: add_zero) |
|
69 apply(simp add: add_Suc) |
|
70 done |
|
71 |
|
72 lemma add_odd: "add m (add n k) = add k (add m n)" |
|
73 apply(subst add_04) |
|
74 apply(subst (2) add_comm) |
|
75 apply(simp) |
|
76 done |
|
77 |
58 |
78 |
59 fun dub :: "nat \<Rightarrow> nat" where |
79 fun dub :: "nat \<Rightarrow> nat" where |
60 "dub 0 = 0" | |
80 "dub 0 = 0" | |
61 "dub m = add m m" |
81 "dub m = add m m" |
62 |
82 |
87 done |
107 done |
88 |
108 |
89 value "trip 1" |
109 value "trip 1" |
90 value "trip 2" |
110 value "trip 2" |
91 |
111 |
|
112 fun sum :: "nat \<Rightarrow> nat" where |
|
113 "sum 0 = 0" |
|
114 | "sum (Suc n) = (Suc n) + sum n" |
|
115 |
|
116 function sum1 :: "nat \<Rightarrow> nat" where |
|
117 "sum1 0 = 0" |
|
118 | "n \<noteq> 0 \<Longrightarrow> sum1 n = n + sum1 (n - 1)" |
|
119 apply(auto) |
|
120 done |
|
121 |
|
122 termination sum1 |
|
123 by (smt2 "termination" diff_less less_than_iff not_gr0 wf_less_than zero_neq_one) |
|
124 |
|
125 lemma "sum n = sum1 n" |
|
126 apply(induct n) |
|
127 apply(auto) |
|
128 done |
|
129 |
|
130 lemma "sum n = (\<Sum>i \<le> n. i)" |
|
131 apply(induct n) |
|
132 apply(simp_all) |
|
133 done |
|
134 |
92 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
135 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
136 "mull 0 0 = 0" | |
|
137 "mull m 0 = 0" | |
|
138 "mull m 1 = m" | |
|
139 (**"mull m (1::nat) = m" | **) |
|
140 (**"mull m (suc(0)) = m" | **) |
|
141 "mull m n = mull m (n-(1::nat))" |
|
142 apply(pat_completeness) |
|
143 apply(auto) |
|
144 |
|
145 done |
|
146 |
|
147 "mull 0 n = 0" |
|
148 | "mull (Suc m) n = add n (mull m n)" |
|
149 |
|
150 lemma test: "mull m n = m * n" |
|
151 sorry |
|
152 |
|
153 fun poww :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
154 "poww 0 n = 1" |
|
155 | "poww (Suc m) n = mull n (poww m n)" |
|
156 |
|
157 |
93 "mull 0 0 = 0" | |
158 "mull 0 0 = 0" | |
94 "mull m 0 = 0" | |
159 "mull m 0 = 0" | |
95 (**"mull m 1 = m" | **) |
160 (**"mull m 1 = m" | **) |
96 (**"mull m (1::nat) = m" | **) |
161 (**"mull m (1::nat) = m" | **) |
97 (**"mull m (suc(0)) = m" | **) |
162 (**"mull m (suc(0)) = m" | **) |
102 (** |
167 (** |
103 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
168 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
104 "count " |
169 "count " |
105 **) |
170 **) |
106 |
171 |
107 fun sum :: "nat \<Rightarrow> nat" where |
172 |
108 "sum n = 0 + \<dots> + n" |
|
109 (* prove n = n * (n + 1) div 2 *) |
173 (* prove n = n * (n + 1) div 2 *) |
110 |
174 |
111 |
175 |
112 |
176 |
113 |
177 |