theory II_kolokvijum_resenja imports Main "HOL-Library.Multiset" begin (* --------------------------------------------------------------------------------- *) (* 1 *) (* 1.1. Napisati funkciju merge_set koja od dva skupa (predstavljena listama prirodnih brojeva bez ponavljanja) formira njihovu uniju. Zahteva se da su obe liste sortirane i da ce rezultat biti takodje sortirana lista prirodnih brojeva. merge_set :: "nat list \ nat list \ nat list" *) (* Prikazati njen rezultat na narednom primeru: value "merge_set [1,3,5,7,9] [3,5,7,11,13]" *) (* 1.2. Dokazati da je fukcija dobro definisana i da se dobro slaze sa ugradjenim funkcijama. Dokazati prvo da je rezultujuca lista sortirana *) (* 1.3. Dokazati da se u rezultujucoj listi nalaze svi elementi koji se nalaze u polaznim listama. *) fun merge_set :: "nat list \ nat list \ nat list" where "merge_set [] ys = ys" | "merge_set xs [] = xs" | "merge_set (x # xs) (y # ys) = (if x < y then x # merge_set xs (y # ys) else if y < x then y # merge_set (x # xs) ys else x # merge_set xs ys)" value "merge_set [1,3,5,7,9] [3,5,7,11,13]" lemma merge_set_skup [simp]: "set (merge_set xs ys) = set xs \ set ys" apply (induction xs ys rule: merge_set.induct) apply auto done (* krace: by (induction xs ys rule: merge_set.induct) auto *) (* POCETAK - 1.zad *) lemma [simp]: assumes "sorted xs" "sorted ys" shows "sorted (merge_set xs ys)" using assms apply (induction xs ys rule: merge_set.induct) apply auto (* javlja se set (merge_set... i dodajemo lemu merge_set_skup *) (* nakon dodavanja leme ova lema prolazi *) done (* --------------------------------------------------------------------------------- *) (* 2 *) (* 2.1. Napisati funkciju quick_sort koja sortira ulaznu listu prirodnih brojeva primenom quick sort algoritma u kome se za pivot uzima prvi element. qsort :: "nat list \ nat list" *) (* Prikazati njen rezultat na narednom primeru: *) (* value "qsort [3,2,1,2,5,6]" *) (* 2.2. Dokazati da je rezultujuca lista sortirana *) (* 2.3. Dokazati da se u rezultujucoj listi nalaze svi elementi koji se nalaze u polaznim listama. *) fun qsort :: "nat list \ nat list" where "qsort [] = []" | "qsort (x # xs) = qsort (filter (\ y. y \ x) xs) @ [x] @ qsort (filter (\ y. y > x) xs)" value "qsort [3,2,1,2,5,6]" lemma set_qsort [simp]: "set (qsort xs) = set xs" apply (induction xs rule: qsort.induct) apply auto done (* POCETAK 2-zad*) lemma "sorted (qsort xs)" apply (induction xs rule: qsort.induct) apply auto (* javlja se sorted (_ @ _) pa trazimo takvu lemu *) find_theorems "sorted (_ @ _)" (* pronalazimo sorted_append i dodajemo je u skup lema *) apply (auto simp add: sorted_append) (* sada mozemo obrisati prethodni apply auto *) (* javlja se set (qsort _) i dodajemo lemu set_qsort *) done lemma filter_mset [simp]: fixes xs :: "nat list" (* bez informacije da se radi o prirodnim brojevima, nema na raspolaganju sve teoreme koje mogu da rade sa poredjenjem prirodnih brojeva *) shows "mset (filter (\ y. y\x) xs) + mset (filter (\ y. y>x) xs) = mset xs" apply (induction xs) apply auto (* bez fixes... automatski dokazivaci ne znaju da se snadju *) done lemma mset_qsort: "mset (qsort xs) = mset xs" apply (induction xs rule: qsort.induct) apply auto (* javlja se mset (filter ... i dodajemo lemu filter_mset *) done lemma filter_set: fixes xs :: "nat list" shows "set (filter (\ y. y\x) xs) \ set (filter (\ y. y>x) xs) = set xs" apply (induction xs) apply auto done (* --------------------------------------------------------------------------------- *) (* 3 *) (* 3.1. Definisati funkciju spoji_liste koja spaja sve liste koje se nalaze u listi lista prirodnih brojeva. spoji :: "nat list list \ nat list" *) (* Prikazati njen rezultat na narednom primeru: *) (* value "spoji [[2,3],[1,2,3],[5,2,3]]" *) (* 3.2. Dokazati da je ona ekvivalentna bibliotečkoj funkciji concat *) (* 3.3. Izraziti istu funkciju preko fold i dokazati ekvivalentnost sa rekurzivnom definicijom *) primrec spoji :: "nat list list \ nat list" where "spoji [] = []" | "spoji (x # xs) = x @ spoji xs" value "spoji [[2,3],[1,2,3],[5,2,3]]" lemma "spoji xs = concat xs" by (induction xs) auto lemma spoji_app [simp]: "spoji (xs @ ys) = spoji xs @ spoji ys" by (induction xs) auto thm rev_induct (* fold je zdesna pa je potrebna indukcija zdesna *) lemma "spoji xs = fold (\ x a. a @ x) xs []" apply (induction xs rule: rev_induct) apply auto (* javlja se spoji (_ @ _) pa dodajemo lemu spoji_app *) done (* --------------------------------------------------------------------------------- *) (* 4 *) (* Ako su data naredna dva sinonima tipova: *) type_synonym key_t = nat type_synonym val_t = nat (* 4.1. Definisati tip podataka binarnog drveta koja implementira mapu kojom se preslikavaju podaci tipa key_t u podatke tipa val_t. Drvo ce biti uredjeno po vrednostima kljuca. *) datatype tree_t = Null | Node key_t val_t tree_t tree_t (* 4.2. Definisati funkciju koja u datoj mapi kljucu k dodeljuje vrednost v ako kljuc ne postoji, ubaciti ga, a ako postoji, promeniti mu vrednost. assign :: "key_t \ val_t \ tree_t \ tree_t" *) primrec assign :: "key_t \ val_t \ tree_t \ tree_t" where "assign k v Null = Node k v Null Null" | "assign k v (Node k' v' left right) = (if k < k' then Node k' v' (assign k v left) right else if k > k' then Node k' v' left (assign k v right) else Node k v left right)" (* 4.3. Definisati funkciju koja odredjuje skup kljuceva u mapi. keys :: "tree_t \ key_t set" *) (* definisati funkciju koja odredjuje skup kljuceva u mapi *) primrec keys :: "tree_t \ key_t set" where "keys Null = {}" | "keys (Node k v left right) = {k} \ keys left \ keys right" (* 4.4. Dokazati da se nakon dodele vrednosti v kljucu k u skup kljuceva dodaje kljuc k (skup se ne menja, ako kljuc vec postoji). *) lemma [simp]: "keys (assign k v t) = {k} \ keys t" by (induction t) auto (* 4.5. Definisati funkciju koja u mapi ocitava vrednost kljuca k. Ako kljuc ne postoji u mapi, funkcija vraca podrazumevanu vrednost koja joj je navedena kao treci argument. lookup_default :: "tree_t \ key_t \ val_t \ val_t" *) primrec lookup_default :: "tree_t \ key_t \ val_t \ val_t" where "lookup_default Null k d = d" | "lookup_default (Node k' v' left right) k d = (if k < k' then lookup_default left k d else if k > k' then lookup_default right k d else v')" (* 4.6. Dokazati da se nakon pridruzivanja vrednosti v kljucu k dobija mapa kojoj se ocitavanjem kljuca k dobija vrednost v. *) lemma [simp]: "lookup_default (assign k v tree) k d = v" by (induction tree) auto (* 4.7. Dokazati da se ocitavanjem vrednosti pridruzene kljucu k koji ne postoji u mapi dobija podrazumevana vrednost *) lemma [simp]: assumes "k \ keys tree" shows "lookup_default tree k d = d" using assms by (induction tree) auto (* --------------------------------------------------------------------------------- *) (* 5 *) (* Data je sledeca definicija tipa prirodnih brojeva: *) datatype prirodni = Nula | Sledbenik prirodni (* 5.1. Definisati funkciju koja preslikava ovako zadat prirodni broj u nat u_nat :: "prirodni \ nat" *) primrec u_nat :: "prirodni \ nat" where "u_nat Nula = 0" | "u_nat (Sledbenik n) = u_nat n + 1" (* 5.2. Definisati funkciju kojom se sabiraju dva ovako zadata prirodna broja saberi :: "prirodni \ prirodni \ prirodni" *) primrec saberi :: "prirodni \ prirodni \ prirodni" where "saberi Nula n = n" | "saberi (Sledbenik m) n = Sledbenik (saberi m n)" (* 5.3. Dokazati da ova funkcija odgovara sabiranju na tipu nat *) lemma [simp]: "u_nat (saberi m n) = u_nat m + u_nat n" by (induction m) auto (* 5.4. Definisati funkciju kojom se mnoze dva ovako zadata prirodna broja pomnozi :: "prirodni \ prirodni \ prirodni" *) primrec pomnozi :: "prirodni \ prirodni \ prirodni" where "pomnozi Nula n = Nula" | "pomnozi (Sledbenik m) n = saberi (pomnozi m n) n" (* 5.5. Dokazati da ova funkcija odgovara mnozenju na tipu nat *) lemma [simp]: "u_nat (pomnozi m n) = u_nat m * u_nat n" by (induction m) auto end