(*<*) theory ex04 imports Main begin (*>*) text \\ExerciseSheet{4}{11.~11.~2019}\ text \\Exercise{Rule Inversion} Recall the evenness predicate \ev\ from the lecture:\ inductive ev :: "nat \ bool" where ev0: "ev 0" | evSS: "ev n \ ev (Suc (Suc n))" text \Prove the converse of rule \evSS\ using rule inversion. Hint: There are two ways to proceed. First, you can write a structured Isar-style proof using the \cases\ method:\ lemma "ev (Suc (Suc n)) \ ev n" proof - assume "ev (Suc (Suc n))" then show "ev n" proof (cases) txt \\qquad ...\ (*<*) case evSS thus "ev n" . (*>*) qed qed text \\textit{Optional}: Alternatively, you can write a more automated proof by using the \textbf{inductive\_cases} command to generate elimination rules. These rules can then be used with ``\auto elim:\''. (If given the \[elim]\ attribute, \auto\ will use them by default.)\ inductive_cases evSS_elim: "ev (Suc (Suc n))" (*<*) lemma "ev (Suc (Suc n)) \ ev n" by (auto elim: evSS_elim) (*>*) text \ Next, prove that the natural number three (\Suc (Suc (Suc 0))\) is not even. Hint: You may proceed either with a structured proof, or with an automatic one. An automatic proof may require additional elimination rules from \textbf{inductive\_cases}. \ lemma "\ ev (Suc (Suc (Suc 0)))" (*<*) proof assume "ev (Suc (Suc (Suc 0)))" then show "False" proof (cases) assume "ev (Suc 0)" then show "False" proof (cases) qed qed qed inductive_cases evS0_elim: "ev (Suc 0)" lemma "\ ev (Suc (Suc (Suc 0)))" by (auto elim: evSS_elim evS0_elim) lemma "\ ev (Suc (Suc (Suc 0)))" by (auto elim: ev.cases) (*>*) text \ \Exercise{(Deterministic) labeled transition systems}\ text \{\bf From this sheet onward, you should write all your (non-trivial) proofs in Isar!}\ text \ A {\em labeled transition system} is a directed graph with edge labels. We represent it by a predicate that holds for the edges. \ type_synonym ('q,'l) lts = "'q \ 'l \ 'q \ bool" text \I.e., for an LTS @{term "\ :: ('q,'l) lts"} over nodes of type @{typ 'q} and labels of type @{typ 'l}, @{term "\ q l q'"} means that there is an edge from @{term q} to @{term q'} labeled with @{term l}.\ text \ A word from source node \u\ to target node \v\ is the sequence of edge labels one encounters when going from \u\ to \v\. Define a predicate @{term word}, such that @{term "word \ u w v"} holds iff $w$ is a word from $u$ to $v$. \ inductive word :: "('q,'l) lts \ 'q \ 'l list \ 'q \ bool" for \ (*<*) where empty: "word \ q [] q" | prepend: "\\ q l qh; word \ qh ls q'\ \ word \ q (l#ls) q'" (*>*) text \ A {\em deterministic} LTS has at most one transition for each node and label \ definition "det \ \ \q a q1 q2. \ q a q1 \ \ q a q2 \ q1 = q2" text \Show: For a deterministic LTS, the same word from the same source node leads to at most one target node, i.e., the target node is determined by the source node and the path \ lemma assumes det: "det \" shows "word \ q w q' \ word \ q w q'' \ q' = q''" (*<*) proof (induction rule: word.induct) case empty thus ?case by cases simp next case (prepend q a qh w q') from \word \ q (a # w) q''\ obtain qh' where 1: "\ q a qh'" and 2: "word \ qh' w q''" by cases from \\ q a qh\ 1 det[unfolded det_def] have [simp]: "qh=qh'" by auto from prepend.IH 2 show "q'=q''" by simp qed (*>*) text \\Exercise{Counting Elements}\ text \{\bf From this sheet onward, you should write all your (non-trivial) proofs in Isar!}\ text \Recall the count function, that counts how often a specified element occurs in a list:\ fun count :: "'a \ 'a list \ nat" where "count x [] = 0" | "count x (y#ys) = (if x=y then Suc (count x ys) else count x ys)" text \Show that, if an element occurs in the list (its count is positive), the list can be split into a prefix not containing the element, the element itself, and a suffix containing the element one times less\ lemma "count x xs = Suc n \ \p s. xs = p @ x # s \ count x p = 0 \ count x s = n" (*<*) proof (induction xs arbitrary: n) case Nil thus ?case by auto next case (Cons y ys) show ?case proof (cases "x=y") case [simp]: True from \count x (y # ys) = Suc n\ have "count x ys = n" by simp moreover have "y#ys = []@x#ys" by simp moreover have "count x [] = 0" by simp ultimately show ?thesis by blast next case [simp]: False from Cons.prems have "count x ys = Suc n" by simp from Cons.IH[OF this] obtain p s where "y#ys = (y#p) @ x # s" "count x (y#p) = 0" "count x s = n" by auto thus ?thesis by blast qed qed (*>*) (*<*) end (*>*)