(**
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
(*>*)