theory a2 imports Main begin section "1. Lists as multisets" text \ This question explores lists as multisets. A list @{term "[0,0,0,2,1,3,2]"} can be seen as a multiset containing 0,1,2,3, with multiplicity 3,1,2,1, respectively. Isabelle has a built-in function @{term count_list} that gives multiplicity \ value "count_list [0::nat,0,0,2,1,3,2] (0::nat)" text \ In the following, instead of using this count_list, we define multiplicity as a finite map @{term m_count} and prove some properties about it. In working on these questions, the @{text ext} lemma can be useful. Also, it is often useful (and necessary) to fine control the simplifier by using "simp only:", "simp (no_asm_simp)", etc. \ subsection "1.1 Multiplicity function for lists as multisets" text \ We define {@term m_count}, as below. It converts a list as a multiset to a function that returns @{term "nat option"}: @{term "m_count ls x"} returns @{term None} if @{term x} does not appear in @{term ls} and returns @{term "Some n"} if @{term x} appears @{term "n+1"} times in @{term ls}. The @{term nat} value is offset by 1 because we start from @{term "Some 0"} when @{term x} appears once in @{term ls}. \ primrec m_count :: "'a list \ ('a, nat) map" where "m_count [] = Map.empty" | "m_count (a#as) = (case (m_count as) a of None \ (m_count as)(a\0) | Some n \ (m_count as)(a\Suc n))" print_theorems value "m_count [0::nat,0,0,2,1,3,2] 0" text \ 1-(a) State the correspondence between Isabelle's @{term count_list} and @{term m_count} as logical equality and prove it. \ lemma "count_list ls x = TODO" (* replace TODO this line with an appropriate formula about m_count *) (* TODO *) (* then prove it *) sorry text \ 1-(b) Prove that @{term "m_count ls x = None"} is equivalent to @{term x} not being a member of @{term ls}.\ lemma m_notin: "m_count ls x = None \ x \ set ls" (* TODO *) sorry subsection "1.2 Ordering on multisets" text \ We can define an ordering on multisets: @{term "ls1 \ ls2"} holds if, for any @{term "x::'a"}, the multiplicity of @{term x} is higher in @{term ls2} than in @{term ls1}. This ordering is defined in terms of @{term m_count} as below: \ definition le :: "('a, nat) map \ ('a, nat) map \ bool" where "le m1 m2 \ \x. case (m1 x, m2 x) of (Some a, Some b) \ a \ b | (Some a, None) \ False | (None, _) \ True" text \ 1-(c) Give two examples of multisets @{term my_ls1}, @{term my_ls2} such that @{term "le (m_count my_ls1) (m_count my_ls2)"} holds. Then show that @{term le} is defined correctly by proving it. \ (* replace the two undefined below with your multisets *) definition "my_ls1 = undefined" definition "my_ls2 = undefined" lemma le_example: "le (m_count my_ls1) (m_count my_ls2)" (* TODO *) oops text \ 1-(d) Prove that adding an element to a list by @{term Cons} always gives a list greater than the original list.\ lemma le_m_count: "le (m_count ls) (m_count (x#ls))" (* TODO *) sorry text \ 1-(e) Prove that @{term m_count} is preserved by changing the order of the elements in the list. \ lemma m_count_perm: "ls = xs @ x # ys \ m_count ls = m_count (x # xs @ ys)" (* TODO *) sorry subsection "1.3 Addition of multisets" text \Next, we consider addition of two multisets. For lists as multisets, this corresponds to @{term append}. We can also consider addition of multiplicity functions, which is defined for @{term m_count} as below: \ definition m_add :: "('a, nat) map \ ('a, nat) map \ ('a,nat) map" where "m_add m1 m2 \ \x. case (m1 x, m2 x) of (Some a, Some b) \ Some (a + b + 1) | (Some a, None) \ m1 x | (None, _) \ m2 x" text \ 1-(f) Prove that the empty map is an identity for addition of maps (both for left and right). \ lemma m_add_empty[simp]: "m_add Map.empty m = m" (* TODO *) sorry lemma m_add_empty2[simp]: "m_add m Map.empty = m" (* TODO *) sorry text \ 1-(g) Prove that @{term m_add} correctly returns the multiplicity of added multisets, i.e., two lists appended by Isabelle @{term append}.\ lemma m_add_append: "m_add (m_count ls1) (m_count ls2) = m_count (append ls1 ls2)" (* TODO *) sorry subsection "1.4 Sorting of multisets" text \ Consider the simple sorting function defined as below: \ primrec insort' :: "'a::ord \ 'a list \ 'a list" where "insort' x [] = [x]" | "insort' x (y#ys) = (if x \ y then (x#y#ys) else y#(insort' x ys))" definition sort' :: "('a::ord) list \ 'a list" where "sort' xs = foldr insort' xs []" text \ 1-(h) With respect to the above sorting function, prove that the sorting of a list does not change the multiset it represents; in other words, that @{term sort'} preserves multiplicity. \ lemma m_count_sort': "m_count (sort' ls) = m_count ls" (* TODO *) sorry subsection "1.5 Union of multisets" text \ We now consider a union of two multisets, whose multiplicity can be given by the following function: \ definition m_union :: "('a, nat) map \ ('a, nat) map \ ('a,nat) map" where "m_union m1 m2 \ \x. case (m1 x, m2 x) of (Some a, Some b) \ Some (max a b) | (Some a, None) \ m1 x | (None, _) \ m2 x" text \ The union @{text m_Un} of two lists as multisets can be defined as follows: \ primrec m_Un' :: "'a list \ 'a list \ 'a list \ 'a list" where "m_Un' [] ys ac = ys @ ac" | "m_Un' (x#xs) ys ac = (if x \ set ys then m_Un' xs (remove1 x ys) (x#ac) else m_Un' xs ys (x#ac))" definition m_Un where "m_Un l1 l2 = m_Un' l1 l2 []" text \ 1-(i) Prove the following lemma about @{term m_Un'} and @{term append}. \ lemma ac_append: "m_Un' l1 l2 (ac @ ls) = (m_Un' l1 l2 ac) @ ls" (* TODO *) sorry text \ 1-(j) Prove the following lemma about @{term remove1} and @{term m_count}. \ lemma m_count_remove1: "m_count (remove1 a ls) = (case m_count ls a of None \ m_count ls | Some n \ if n = 0 then (m_count ls)(a := None) else (m_count ls)(a:= map_option (\x. x - 1) (m_count ls a)))" (* TODO *) sorry text \ 1-(k) Prove the correctness of @{term m_Un} with respect to @{term m_union}. \ lemma m_count_union: "m_count (m_Un l1 l2) = m_union (m_count l1) (m_count l2)" (* TODO *) sorry (*---------------------------------------------------------*) section "2. Compiler for arithmetic expressions" (* Syntax of the language *) type_synonym vname = string type_synonym val = int datatype aexp = N val | V vname | Plus aexp aexp (* Evaluation function *) type_synonym vstate = "vname \ val" primrec eval :: "aexp \ vstate \ val" where "eval (N n) s = n" | "eval (V x) s = s x" | "eval (Plus e1 e2) s = eval e1 s + eval e2 s" (* Programs for the register machine *) type_synonym reg = nat datatype prog = LoadI reg val | Load reg vname | Add reg reg | Seq prog prog ("_ ;; _" 100) | Skip (* Compiler from expression to register programs *) primrec compile :: "aexp \ reg \ prog \ reg" where "compile (N n) r = (LoadI r n, r + 1)" | "compile (V x) r = (Load r x, r + 1)" | "compile (Plus e1 e2) r1 = (let (p1, r2) = compile e1 r1; (p2, r3) = compile e2 r2 in ((Seq p1 (Seq p2 (Add r1 r2))), r3))" (* ---------- *) text\ 2-(a): Give an example of an arithmetic expression which evaluates to 7 and uses @{term Plus} twice or more. Prove that your example actually evaluates to 7. \ (* TODO *) text\ 2-(b): Prove that the compiler always returns a register identifier strictly higher than the one given to it. \ lemma compile_reg_increase: "compile e r = (p, r') \ r' > r" (* TODO *) sorry (* ---------- *) subsection "2.1 Target machine big-step semantics and compiler correctness" (* Big step operational semantics to programs for the register machine *) type_synonym rstate = "reg \ val" type_synonym mstate = "rstate \ vstate \ prog" inductive sem :: "mstate \ rstate \ bool" ("_ \ _" [0,60] 61) where sem_LoadI: "(rs, \, LoadI r n) \ rs(r := n)" | sem_Load: "(rs, \, Load r v) \ rs(r := \ v)" | sem_Add: "(rs, \, Add r1 r2) \ rs(r1 := rs r1 + rs r2)" | sem_Seq: "\(rs, \, p) \ rs'; (rs', \, q) \ rs''\ \ (rs, \, p ;; q) \ rs''" (* ---------- *) text\ 2-(c): Prove that the register machine semantics is deterministic. \ lemma sem_det: "\(rs, \, e) \ rs'; (rs, \, e) \ rs''\ \ rs' = rs''" (* TODO *) sorry text\ 2-(d): Prove that the compiler produces programs that do not modify any registers of identifier lower than the register identifier given to it. \ lemma compile_no_modify_lower_reg: "compile e r = (p, r') \ (rs, \, p) \ rs' \ r'' < r \ rs' r'' = rs r''" (* TODO *) sorry text\ 2-(e): Prove that the compiler produces programs that, when executed, yield the value of the expression in the register *provided* as the argument to @{term compile} in the final @{term rstate} according to the program's big-step semantics. \ lemma compile_correct: "compile e r = (p, r') \ (rs, \, p) \ rs' \ rs' r = eval e \" (* TODO *) sorry (* ---------- *) (* Small-step semantics *) inductive s_sem :: "mstate \ mstate \ bool" ("_ \ _" 100) where "(rs, \, LoadI r n) \ (rs(r := n), \, Skip)" | "(rs, \, Load r v) \ (rs(r := \ v), \, Skip)" | "(rs, \, Add r1 r2) \ (rs(r1 := rs r1 + rs r2), \, Skip)" | "(rs, \, p) \ (rs', \, p') \ (rs, \, p ;; q) \ (rs', \, p' ;; q)" | "(rs, \, Skip ;; p) \ (rs, \, p)" primrec term_with_n_Suc :: "nat \ aexp" where "term_with_n_Suc 0 = N 0" | "term_with_n_Suc (Suc n) = (Plus (term_with_n_Suc n) (N 0))" (* ---------- *) text\ 2-(f): Define a function s_sem_n:: nat \ mstate \ mstate \ bool that executes n steps of the small-step semantics. \ primrec s_sem_n :: "nat \ mstate \ mstate \ bool" where TODO text\ 2-(g): Prove that two executions of resp. n and m steps according to s_sem_n compose into a single execution of (n+m) steps if their resp. final and initial machine state match. \ lemma s_sem_n_add: "s_sem_n n ms ms' \ s_sem_n m ms' ms'' \ s_sem_n (n+m) ms ms''" (* TODO *) sorry text\ 2-(h): Prove that if p executes to p' in n steps according to s_sem_n, then p ;; q will execute to p' ;; q in n steps with all other parts of the state being the same as in the original execution. \ lemma s_sem_n_Seq: "s_sem_n n (rs, \, p) (rs', \, p') \ s_sem_n n (rs, \, p;;q) (rs', \, p';;q)" (* TODO *) sorry text\ 2-(i): Prove that if a program executes in the big-step semantics to a resulting rstate rs', then it executes in the small-step semantics to the same resulting rstate and the resulting program Skip with no changes to the vstate. \ lemma s_sem_n_correct: "ms \ rs' \ \n. s_sem_n n ms (rs', fst (snd ms), Skip)" (* TODO *) sorry text\ 2-(j): Prove that compiling a "term_with_n_Suc h" will use a number of registers that is indeed strictly lower bounded by h. \ lemma compile_term_with_n_Suc_lower_bound_n: "h < snd (compile (term_with_n_Suc h) r) - r" (* TODO *) sorry text\ 2-(k): Using this fact, prove that there is no universal bound on the number of registers used for any compiled program. \ lemma compile_has_no_universal_register_bound: "\ (\h. (\p. h \ snd (compile p r) - r))" (* TODO *) sorry (*---------------------------------------------------------*) end