(*<*) theory sol06_2 imports "~~/src/HOL/IMP/Small_Step" "~~/src/HOL/IMP/Compiler" begin (*>*) text {* \ExerciseSheet{6}{17.~11.~2015} *} text {* \Exercise{While Free Programs} {\bf a}) Show that while-free programs always terminate, i.e., show that for any while-free command and any state, the big-step semantics yields a result state. {\bf b}) Show that non-terminating programs contain a while loop, i.e., show that all commands, for which there is a state such that the big-step semantics yields no result, contain a while loop. *} (*<*) fun while_free :: "com \ bool" where "while_free SKIP \ True" | "while_free (Assign _ _) \ True" | "while_free (Seq c1 c2) \ while_free c1 \ while_free c2" | "while_free (If b c1 c2) \ while_free c1 \ while_free c2" | "while_free (While b c) \ False" lemma while_free_term: assumes "while_free c" shows "\s'. (c,s) \ s'" using assms apply (induction c arbitrary: s) apply (auto) apply (metis Seq) by (metis big_step.IfFalse big_step.IfTrue) lemma nonterm_contains_while: assumes "\(\s'. (c,s) \ s')" shows "\while_free c" using assms apply (induction c arbitrary: s) apply auto by (metis big_step.IfFalse big_step.IfTrue) (*>*) (*<*) end (*>*)