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 (add m n) k" |
|
55 apply(induct m) |
|
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 |
|
70 |
|
71 fun dub :: "nat \<Rightarrow> nat" where |
|
72 "dub 0 = 0" | |
|
73 "dub m = add m m" |
|
74 |
|
75 lemma dub_01: "dub 0 = 0" |
|
76 apply(induct) |
|
77 apply(auto) |
|
78 done |
|
79 |
|
80 lemma dub_02: "dub m = add m m" |
|
81 apply(induction m) |
|
82 apply(auto) |
|
83 done |
|
84 |
|
85 value "dub 2" |
|
86 |
|
87 fun trip :: "nat \<Rightarrow> nat" where |
|
88 "trip 0 = 0" | |
|
89 "trip m = add m (add m m)" |
|
90 |
|
91 lemma trip_01: "trip 0 = 0" |
|
92 apply(induct) |
|
93 apply(auto) |
|
94 done |
|
95 |
|
96 lemma trip_02: "trip m = add m (add m m)" |
|
97 apply(induction m) |
|
98 apply(auto) |
|
99 done |
|
100 |
|
101 value "trip 1" |
|
102 value "trip 2" |
|
103 |
|
104 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
105 "mull 0 0 = 0" | |
|
106 "mull m 0 = 0" | |
|
107 (**"mull m 1 = m" | **) |
|
108 (**"mull m (1::nat) = m" | **) |
|
109 (**"mull m (suc(0)) = m" | **) |
|
110 "mull m n = mull m (n-(1::nat))" |
|
111 |
|
112 (**Define a function that counts the |
|
113 number of occurrences of an element in a list **) |
|
114 (** |
|
115 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
|
116 "count " |
|
117 **) |
|
118 |
|
119 fun sum :: "nat \<Rightarrow> nat" where |
|
120 "sum n = 0 + \<dots> + n" |
|
121 (* prove n = n * (n + 1) div 2 *) |
|
122 |
|
123 |
|
124 |
|
125 |
|
126 |
|
127 |
|
128 |
|
129 |
|
130 |
|
131 |
|
132 |
|