header {* Remarks on Homework 2 *} theory remarks2 imports "~~/src/HOL/IMP/AExp" begin text {* Please do not submit multiple files, unless strictly necessary! *} text {* Please do not leave sledgehammer, quickcheck, nitpick, etc commands in your submission! It only slows down checking your submission, but has no additional value once the proof or counterexample is found*} text {* Please do not use semicolons after commands. While jEdit seems to parse them, ProofGeneral chokes on them, and I have to remove them by hand.*} text {* Unless otherwise indicated, do not copy stuff from IMP to your submission file, but just import the theories from IMP. *} text {* Keep in mind that priority of function application is highest in isabelle. For example, @{text "f a + 1"} is parsed as @{text "(f a) + 1"}, even if written as @{text "f a+1"}. *} (** When using complicated recursion patterns, the induction rule of the function is, in general, more appropriate than the datatypes induction rule. For example, look at the following (overly complicated) solution to 2.1: **) fun multn :: "nat \ aexp \ aexp" where "multn n (N i) = (N (int n * i))" | "multn 0 (V x) = (N 0)" | "multn (Suc 0) (V x) = (V x)" | "multn (Suc n) (V x) = Plus (multn n (V x)) (V x)" | "multn n (Plus a1 a2) = Plus (multn n a1) (multn n a2)" lemma "aval (multn n a) s = int n * aval a s" apply (induct n arbitrary: a) apply auto (* You are left with some subgoals here, that the simplifier cannot handle any more, because there is no matching equation in multn*) oops lemma "aval (multn n a) s = int n * aval a s" apply (induct a arbitrary: n) apply auto (* The same here *) oops (* So consider using the induction rule from the function, to avoid manual case splits: *) lemma "aval (multn n a) s = int n * aval a s" apply (induct n a rule: multn.induct) apply (auto simp: algebra_simps) done end