theory Algoritmi_IX_cas_intro imports "HOL-Library.Multiset" "HOL-Library.Mapping" "HOL-Library.RBT_Mapping" begin (* primer korektnosti pretrage *) definition delioci :: "nat \ nat list" where "delioci n = filter (\ d. d dvd n) [1.. nat \ nat" where "nzd a b = (if b = 0 then a else nzd b (a mod b))" value "nzd 120 28" thm nat.induct thm nzd.simps thm nzd.induct declare nzd.simps [simp del] lemma "(nzd a b) dvd a \ (nzd a b) dvd b" (* apply (induction a b rule: nzd.induct) apply auto na ovaj nacin se zaglupi simplifikator i mora da se obrise nzd.simps iz simp *) proof (induction a b rule: nzd.induct) case (1 a b) show ?case proof (cases "b = 0") case True thus ?thesis (* using nzd.simps[of a 0] (* izbacili smo je iz simplifikatora ali je koristimo nakon instanciranja *) by simp *) by (simp add: nzd.simps[of a 0]) next case False hence "nzd a b = nzd b (a mod b)" (* using nzd.simps[of a b] by simp *) by (simp add: nzd.simps[of a b]) thus ?thesis thm dvd_mod_iff (* c dvd b \ c dvd a mod b = c dvd a *) using 1 `b \ 0` dvd_mod_iff by auto qed qed lemma "\ x. x dvd a \ x dvd b \ x dvd (nzd a b)" proof (induction a b rule: nzd.induct) case (1 a b) show ?case proof (cases "b = 0") case True thus ?thesis using nzd.simps[of a 0] by simp next case False thus ?thesis using 1 `b \ 0` using nzd.simps[of a b] dvd_mod_iff by auto qed qed lemma assumes "n > 0" shows "set (delioci n) = {d. d dvd n}" unfolding delioci_def using assms using dvd_pos_nat[of n] dvd_imp_le[of _ n] by force (* nema manjih od 1 i vecih od n *) (* van intervala pretrage nema resenja... za interval pretrage automatski sredi *) (* --------------------- izrazi ---------------------- *) type_synonym var_num = nat datatype exp = Var var_num | Const int | Add exp exp | Mult exp exp | Minus exp exp (* citanje iz memorije *) (* https://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/HOL-Library/Mapping.html *) type_synonym Memory = "(nat, int) mapping" definition read_memory where "read_memory m x = Mapping.lookup_default 0 m x" primrec value_exp_map:: "exp \ Memory \ int" where "value_exp_map (Var x) m = read_memory m x" | "value_exp_map (Const y) m = y" | "value_exp_map (Add exp1 exp2) m = (value_exp_map exp1 m) + (value_exp_map exp2 m)" | "value_exp_map (Mult exp1 exp2) m = (value_exp_map exp1 m) * (value_exp_map exp2 m)" | "value_exp_map (Minus exp1 exp2) m = (value_exp_map exp1 m) - (value_exp_map exp2 m)" definition val_map1 :: "Memory" where "val_map1 = Mapping.bulkload [1,2,3]" (* ukljucujemo rbt stabla da bi moglo da izvrsi racunanje *) value "value_exp_map (Mult (Var 2) (Add (Const 2) (Const 5))) val_map1" definition x5 :: "exp" where "x5 = Add (Var 0) (Const 3)" value "value_exp_map x5 val_map1" definition x6 :: "exp" where "x6 = Mult (Var 0) (Add (Const 2) (Const 5))" value "value_exp_map x6 val_map1" (* uvodimo novu operaciju citanja iz memorije *) datatype Operation = OpAdd | OpMult | OpMin | OpPush int | OpRead var_num (*citanje*) type_synonym Stack = "int list" fun executeOp :: "Operation \ Stack \ Memory \ Stack" where "executeOp OpMult (x # y # xs) m = (x * y) # xs" | "executeOp OpAdd (x # y # xs) m = (x + y) # xs" | "executeOp OpMin (x # y # xs) m = (x - y) # xs" | "executeOp (OpPush x) xs m = (x # xs)" | "executeOp (OpRead x) xs m = ((read_memory m x) # xs)" type_synonym Prog = "Operation list" primrec executeProg :: "Prog \ Stack \ Memory \ Stack" where "executeProg [] s m = s" | "executeProg (op # p) s m = executeOp op (executeProg p s m) m" primrec translate :: "exp \ Prog" where "translate (Var x) = [OpRead x]" | "translate (Const x) = [OpPush x]" | "translate (Add i1 i2) = [OpAdd] @ translate i1 @ translate i2" | "translate (Minus i1 i2) = [OpMin] @ translate i1 @ translate i2" | "translate (Mult i1 i2) = [OpMult] @ translate i1 @ translate i2" value "x5" value "value_exp_map x5 val_map1" value "translate x5" value "executeProg (translate x5) [] val_map1" (* -------------------------- spoji ------------------------*) (* definisati funkciju spoji koja spaja dve sortirane liste *) fun spoji :: "nat list \ nat list \ nat list" where ... value "spoji [1, 2, 3, 5] [2, 4, 6, 8]" (* dokazati da je ova funkcija dobro definisana *) (* 1 - da je spojena lista takodje sortirana *) (* 2 - da je skup elemenata u spojenoj listi jednak uniji elemenata osnovnih listi *) (* 3 - isto to za multiskup *) (* ----------------- mergesort ---------------------- *) (* definisati funkciju mergesort koja sortira listu merge sortom i koristi prethodno definisanu funkciju spoji i funkcija take i drop *) term take (* take n xs - prvih n elemenata liste xs *) term drop (* drop n xs - ono sto ostane kad se izbaci prvih n elemenata liste *) (* https://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/List.html *) find_theorems "drop _ _" thm append_take_drop_id (* take n xs @ drop n xs = xs *) fun mergesort :: "nat list \ nat list" where ... value "mergesort [3, 5, 1, 4, 8, 2]" (* dokazati da je ova funkcija dobro definisana *) (* 1 - da je generisana lista sortirana *) (* 2 - da je multiskup skup elemenata u generisanoj listi jednak multiskupu skupu elemenata pocetne liste *) (* ----------------- qsort ---------------------- *) (* definisati funkciju qsort koja sortira listu qsort algoritmo kada se za pivot uzme prvi element *) fun qsort :: "nat list \ nat list" where ... value "qsort [3, 4, 5, 1, 2]" value "qsort [3, 5, 1, 4, 8, 3, 2]" (* dokazati da je ova funkcija dobro definisana *) (* 1 - da je generisana lista sortirana *) (* 2 - da je multiskup skup elemenata u generisanoj listi jednak multiskupu skupu elemenata pocetne liste *) (* ------------------- sabiranje prirodnih brojeva ------------------- *) (* Exercise 2.9. Write a tail-recursive variant of the add function on nat : itadd. Tail-recursive means that in the recursive case, itadd needs to call itself directly: itadd (Suc m) n = itadd . . .. Prove itadd m n = add m n. *) primrec add :: "nat \ nat \ nat" where "add 0 n = n" | "add (Suc m) n = Suc (add m n)" (* definisati nasu funkciju koja izracunava vrednost n div 2 i dokazati da je dobro definisana *) fun div2 :: "nat \ nat" where ... (* definisati funkciju nzd i pokazati da je ona dobro definisana *) fun nzd :: "nat \ nat \ nat" where ... (* 1 - da je dobijeni broj stvarno delilac *) (* 2 - da je najveci delilac *) end