theory exam_14 imports AutoCorres.AutoCorres begin text \ This theory is designed to be loaded with the AutoCorres logic/image via e.g. L4V_ARCH=X64 isabelle jedit -d autocorres-1.10 -l AutoCorres exam_14.thy OR: L4V_ARCH=ARM isabelle jedit -d autocorres-1.10 -l AutoCorres exam_14.thy \ section "Question 1: Lambda Calculus" text \ (a) -- (c): Write your answers as Isabelle comments or include them in a separate .pdf or .txt file. \ section "Question 2: Induction" text \ (a-i) \ inductive_set pal_lists where pal_nil: "\" text \ (a-ii) \ lemma pal_lists_Cons: "xs \ pal_lists ==> x # xs \ pal_lists" sorry text \ (a-iii) \ lemma pal_univ: "xs \ pal_lists" sorry text \ (a-iv) \ lemma pal_induct: assumes nil: "P []" assumes one: "\x. P [x]" assumes two: "\a xs b. P xs \ P (a # xs @ [b])" shows "P list" sorry text \ (b) \ (* define palindrome *) text \ (c) \ lemma pal_eq: "palindrome (a # xs @ [b]) \ a = b" sorry text \ (d) \ text \ (e) \ lemma "palindrome xs = (xs \ palindromes)" sorry section "C Verification" external_file "divmod.c" install_C_file "divmod.c" autocorres [unsigned_word_abs = divmod even] "divmod.c" context divmod begin text \ (a) -- (b): Write your answers as Isabelle comments or include them in a separate .pdf or .txt file. \ text \ (c) \ definition divmod_spec :: "nat \ nat \ nat \ nat" where "divmod_spec n m domod \ if domod \ 0 then n mod m else n div m" lemma divmod'_correct: "ovalid (\_. True) (divmod' n m domod) (\r s. r = divmod_spec n m domod)" sorry text \ (d): replace PRE below with a suitable weakest precondition and prove it correct \ lemma divmod'_wp: "ovalid PRE (divmod' n m domod) Q" sorry text \ (e) \ lemma even'_correct: "ovalid (\_. True) (even' n) (\r s. r = (if even n then 1 else 0))" sorry text \ (f): Write your answer as an Isabelle comment or in a separate .pdf or .txt file \ end text \ Bonus question: Recursive functions \ datatype regexp = Atom char | Alt regexp regexp | Conc regexp regexp (infixl "\" 60) | Star regexp | Neg regexp (* Match everything: *) definition "Univ = Alt (Neg (Atom (CHR ''x''))) (Atom (CHR ''x''))" (* Match nothing: *) definition "null = Neg Univ" (* Match only the empty string: *) definition "epsilon = Star null" (* For examples/testing. *) primrec string :: "char list \ regexp" where "string [] = epsilon" | "string (x#xs) = Atom x \ string xs" (* Automatically coerce type "char list" into "regexp" using the function "string" *) declare [[coercion string, coercion_enabled]] term "Star ''abc''" (* A set of strings repeated 0 or more times *) inductive_set star :: "string set \ string set" for L where star_empty[simp,intro!]: "[] \ star L" | star_app[elim]: "\ u \ L; v \ star L \ \ u@v \ star L" (* The concatenation of two sets of strings *) definition conc :: "string set \ string set \ string set" where "conc A B \ { xs@ys |xs ys. xs \ A \ ys \ B}" (* The sets of strings matched by an expression *) primrec lang :: "regexp \ string set" where "lang (Atom c) = {[c]}" | "lang (Alt e1 e2) = lang e1 \ lang e2" | "lang (Conc e1 e2) = conc (lang e1) (lang e2)" | "lang (Star e) = star (lang e)" | "lang (Neg e) = -lang e" (* ------------------------------------------------------------ *) (* New for the exam: *) primrec split :: "('a list \ bool) \ ('a list \ bool) \ 'a list \ 'a list \ bool" where "split P Q xs [] = (P xs \ Q [])" | "split P Q xs (y#ys) = (P xs \ Q (y#ys) \ split P Q (xs@[y]) ys)" (* --------- 1a ------------ *) lemma split_eq[simp]: "split P Q xs ys = (\as bs. ys = as @ bs \ P (xs@as) \ Q bs)" sorry (* TODO *) lemma split_cong[fundef_cong,cong]: "\ xs = xs'; ys = ys'; P = P'; \bs. length bs \ length ys' \ Q bs = Q' bs \ \ split P Q xs ys = split P' Q' xs' ys'" by force declare nat_le_Suc_less[simp] (* Executable version of determining a regular expression match with negation. *) fun matches :: "regexp \ string \ bool" where "matches (Atom c) cs = (cs = [c])" | "matches (Alt r1 r2) cs = (matches r1 cs \ matches r2 cs)" | "matches (Conc r1 r2) cs = split (matches r1) (matches r2) [] cs" | "matches (Neg r) cs = (\ matches r cs)" | "matches (Star r) cs = (cs \ [] \ split (matches r) (matches (Star r)) [hd cs] (tl cs))" (* Unfold matches_Star manually with "subst" *) lemmas matches_Star[simp del] = matches.simps(5) (* Examples *) value "matches (Star (Alt ''ab'' ''a'')) ''''" value "matches (Star (Alt ''ab'' ''a'')) ''ababa''" value "matches (Star (Alt ''ab'' ''a'')) ''abba''" value "matches (Neg (Star (Alt ''ab'' ''a''))) ''abba''" (* --------- 1b ------------ *) lemma matches_string: "matches (string xs) cs = (cs = xs)" sorry (* TODO: prove; find suitable helper lemmas *) (* --------- 1c ------------ *) lemma star_cons_append[elim]: "\ a # as \ L; bs \ star L\ \ a # as @ bs \ star L" sorry (* TODO *) lemma star_cases: "xs \ star A \ xs = [] \ (\u v. xs = u@v \ u \ A \ v \ star A \ u \ [])" by (induct rule: star.induct) auto lemma star_cons_case[dest!]: "x#xs \ star L \ (\u v. xs = u@v \ x#u \ L \ v \ star L)" sorry (* TODO *) lemma matches_correct: "matches r cs = (cs \ lang r)" sorry (* TODO *) end