(** This is a template for homework 5. We have marked tasks that you have to do by "YOU: " Note: This template contains Isabelle errors. PLEASE ENSURE THAT YOUR SUBMISSION DOES NOT CONTAIN ERRORS. (I will subtract one point per Isabelle error that you leave in your submission, use sorry or oops to mark failed proof attempts) *) (*<*) theory hw05_tmpl (** YOU: Replace by naming scheme for homework *) imports "~~/src/HOL/IMP/BExp" begin (*>*) text \ \NumHomework{Break}{November 17} Note: This homework comes with a template file. You are strongly encouraged to use it! Your task is add a break command to the IMP language. The break command should immediately exit the innermost while loop. The new command datatype is: \ datatype com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;;/ _" [60, 61] 60) | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) | BREAK text \ The idea of the big-step semantics is to return not only a state, but also a break flag, which indicates a pending break. Modify/augment the big-step rules accordingly: \ inductive big_step :: "com \ state \ bool \ state \ bool" (infix "\" 55) (** YOU: Add rules. Hint: Use original big-step rules as template! *) (*<*) text{* Proof automation: *} text {* The introduction rules are good for automatically construction small program executions. The recursive cases may require backtracking, so we declare the set as unsafe intro rules. *} declare big_step.intros [intro] text{* The standard induction rule @{thm [display] big_step.induct [no_vars]} *} thm big_step.induct text{* This induction schema is almost perfect for our purposes, but our trick for reusing the tuple syntax means that the induction schema has two parameters instead of the @{text c}, @{text s}, and @{text s'} that we are likely to encounter. Splitting the tuple parameter fixes this: *} lemmas big_step_induct = big_step.induct[split_format(complete)] thm big_step_induct text {* @{thm [display] big_step_induct [no_vars]} *} subsection "Rule inversion" text{* What can we deduce from @{prop "(SKIP,s) \ t"} ? That @{prop "s = t"}. This is how we can automatically prove it: *} inductive_cases SkipE[elim!]: "(SKIP,s) \ t" thm SkipE inductive_cases BreakE[elim!]: "(BREAK,s) \ t" text{* This is an \emph{elimination rule}. The [elim] attribute tells auto, blast and friends (but not simp!) to use it automatically; [elim!] means that it is applied eagerly. Similarly for the other commands: *} inductive_cases AssignE[elim!]: "(x ::= a,s) \ t" thm AssignE inductive_cases SeqE[elim!]: "(c1;;c2,s1) \ s3" thm SeqE inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ t" thm IfE inductive_cases WhileE[elim]: "(WHILE b DO c,s) \ t" thm WhileE text{* Only [elim]: [elim!] would not terminate. *} lemma assign_simp: "(x ::= a,s) \ (brk,s') \ (s' = s(x := aval a s) \ \brk)" oops (*YOU: Proof should work by auto*) (*>*) text \Now, write a function that checks that breaks only occur in while-loops \ fun break_ok :: "com \ bool" where "break_ok SKIP \ True" (* YOU: Insert other equations *) text \Show that your function ensures that the break-flag is not set when executing a command\ lemma assumes "break_ok c" assumes "(c,s) \ (brk,t)" shows "\brk" (* YOU: Prove this *) oops text \ \NumHomework{Variables not occurring in command}{November 17} Write a function which checks whether a variable occurs in a command. (Hint: You need to write such functions also for Boolean and arithmetic expressions) \ fun occ :: "vname \ com \ bool" where "occ x (SKIP) \ False" (* YOU: Insert other equations. Define functions for aexp,bexp *) text \Show the following two lemmas, which state that a program does not modify, nor depends on variables that do not occur in it. Hint: For induction, use the customized @{text big_step_induct} rule, which you should have copied from @{text "Com.thy"}! \ lemma no_touch: assumes "\occ x c" assumes "(c,s) \ (brk,t)" shows "t x = s x" oops (* YOU: Prove this. *) lemma no_dep: assumes "\occ x c" assumes "(c,s) \ (brk,t)" shows "(c,s(x:=v)) \ (brk,t(x:=v))" oops (* YOU: Prove this. You may require auxiliary lemmas for aexp/bexp! *) text \ \NumHomework{Eliminating Breaks}{November 17} In this homework, you shall prove correct an elimination procedure for breaks, which we have already specified for you. The procedure works by using an auxiliary variable. We will assume that it does not occur in the original program. \ definition "breakvar \ ''__break__''" fun ebrk :: "com \ com" -- \Rules given in homework template!\ (*<*) where "ebrk SKIP = SKIP" | "ebrk (x ::= a) = (x ::= a)" | "ebrk (c1;;c2) = ebrk c1;;IF Less (V breakvar) (N 1) THEN ebrk c2 ELSE SKIP" | "ebrk (IF b THEN c1 ELSE c2) = IF b THEN ebrk c1 ELSE ebrk c2" | "ebrk (WHILE b DO c) = WHILE (And b (Less (V breakvar) (N 1))) DO ebrk c;; breakvar ::= N 0" | "ebrk BREAK = breakvar ::= N 1" (*>*) (*<*) (* INCLUDE IN TEMPLATE! *) (* These lemmas will help automating the proof! *) inductive_simps [simp]: "(SKIP,s) \ (brk,t)" lemma [simp]: "s x = a \ s(x:=a) = s" by auto lemma while_not_brk: assumes "(WHILE b DO c, s) \ (brk,t)" shows "\brk" using assms oops (* YOU: Prove this. This may work: by (induction "WHILE b DO c" _ _ _ rule: big_step_induct) auto *) corollary [simp]: "\(WHILE b DO c, s) \ (True,t)" oops (* YOU: using while_not_brk by blast *) declare no_touch[simp] (*>*) text \ The following lemma states one direction of the correctness of our construction: If we execute the original program, the modified program has the same execution, and, if and only if the original program has a pending break, @{text breakvar} is set. (Note that, as @{text breakvar} is initially zero and does not occur in @{text c}, it is also zero in @{text t} (cf lemma @{text no_touch})!) We give you a proof template here, you have to prove the interesting cases for loops, the other cases go through automatically! \ (* YOU: We assume that your big-step rules are called Seq1 for non-breaking sequential composition, WhileFalse, WhileTrue, and WhileBreak! Otherwise, you have to adjust the template. *) lemma assumes "\occ breakvar c" assumes "s breakvar = 0" assumes "(c,s) \ (brk,t)" shows "case brk of False \ (ebrk c, s) \ (False,t) | True \ (ebrk c, s) \ (False,t(breakvar := 1)) " using assms(3,1,2) proof (induction rule: big_step_induct) case (WhileFalse b s c) show ?case sorry (* YOU: Prove this *) next case (WhileTrue b s1 c s2 brk t) show ?case sorry (* YOU: Prove this *) next case (WhileBreak b s1 c s2) show ?case sorry (* YOU: Prove this *) qed (auto split: bool.splits elim!: Seq1 simp: assign_simp) (* YOU: If this qed-tactic should not work for you, first re-check your definitions. If it still does not work, you'll have to solve the non-working cases in Isar! (Writing sorry for these cases, with otherwise correct definitions and proofs, will result in loss of at most one point, if at all.) *) (*<*) end (*>*)