(*<*) theory ex03 imports "HOL-IMP.ASM" "HOL-IMP.BExp" begin (*>*) text \\ExerciseSheet{3}{04.11.2019}\ text \\Exercise{Reflexive Transitive Closure} A binary relation is expressed by a predicate of type @{text "R :: 's \ 's \ bool"}. Intuitively, @{text "R s t"} represents a single step from state @{text "s"} to state @{text "t"}. The reflexive, transitive closure @{text "R\<^sup>*"} of @{text "R"} is the relation that contains a step @{text "R\<^sup>* s t"}, iff @{text "R"} can step from @{text "s"} to @{text "t"} in any number of steps (including zero steps). Formalize the reflexive transitive closure as an inductive predicate: \ inductive star :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" (*<*) for r where refl: "star r x x" | step: "r x y \ star r y z \ star r x z" (*>*) text \When doing so, you have the choice to append or prepend a step. In any case, the following two lemmas should hold for your definition:\ lemma star_prepend: "\r x y; star r y z\ \ star r x z" (*<*) by (rule step) (*>*) lemma star_append: "\ star r x y; r y z \ \ star r x z" (*<*) by (induct rule: star.induct) (auto intro: star.intros) (*>*) text \Now, formalize the star predicate again, this time the other way round:\ inductive star' :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" (*<*) for r where refl': "star' r x x" | step': "\star' r x y; r y z\ \ star' r x z" (*>*) (*<*) lemma star'_prepend: "\star' r y z; r x y\ \ star' r x z" apply (induction rule: star'.induct) apply (auto intro: star'.intros) done (*>*) text \Prove the equivalence of your two formalizations:\ lemma "star r x y = star' r x y" (*<*) proof assume "star r x y" thus "star' r x y" by induct (auto intro: star'.intros star'_prepend) next assume "star' r x y" thus "star r x y" by induct (auto intro: star.intros star_append) qed (*>*) text \\Exercise{Avoiding Stack Underflow}\ text \A \emph{stack underflow} occurs when executing an instruction on a stack containing too few values---e.g., executing an @{text ADD} instruction on an stack of size less than two. A well-formed sequence of instructions (e.g., one generated by @{text comp}) should never cause a stack underflow.\ (* Alternative: functional solution: *) text \ In this exercise, you will define a semantics for the stack-machine that throws an exception if the program underflows the stack. \ text \Modify the @{text "exec1"} and @{text "exec"} - functions, such that they return an option value, @{text "None"} indicating a stack-underflow.\ fun exec1 :: "instr \ state \ stack \ stack option" (*<*) where "exec1 (LOADI n) _ stk = Some (n # stk)" | "exec1 (LOAD x) s stk = Some (s(x) # stk)" | "exec1 ADD _ stk = ( case stk of a # b # c \ Some ((a + b) # c) | _ \ None)" (*>*) fun exec :: "instr list \ state \ stack \ stack option" (*<*) where "exec [] _ stk = Some stk" | "exec (i#is) s stk = (case exec1 i s stk of Some stk \ exec is s stk | None \ None)" (*>*) text \ Now adjust the proof of theorem @{text "exec_comp"} to show that programs output by the compiler never underflow the stack: \ (*<*) lemma exec_append[simp]: "exec (is1@is2) s stk = (case exec is1 s stk of Some stk \ exec is2 s stk | None \ None)" apply(induction is1 arbitrary: stk) apply (auto split: option.split) done (*>*) theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)" (*<*) apply(induction a arbitrary: stk) apply (auto) done (*>*) text \\Exercise{A Structured Proof on Relations}\ text \ We consider two binary predicates \T\ and \A\ and assume that \T\ is total, \A\ is antisymmetric and \T\ is a subset of \A\. Show with a structured, Isar-style proof that then \A\ is also a subset of \T\: \ (*<*) lemma structured_proof: (*>*) assumes "\ x y. T x y \ T y x" and "\ x y. A x y \ A y x \ x = y" and "\ x y. T x y \ A x y" shows "A x y \ T x y" (* using assms by blast *) (*<*) proof fix x y assume "A x y" from assms(1) have "T x y \ T y x" by simp then show "T x y" proof assume "T x y" then show ?thesis . next assume "T y x" with assms(3) have "A y x" by simp with \A x y\ assms(2) have "x = y" by simp with \T y x\ show ?thesis by simp qed qed (*<*) end (*>*)