theory Exercise06
imports Main "HOL-IMP.Big_Step"
begin
section "Index"
section "Fuel your executions"
subsection "Step 1"
fun exec :: "com \ state \ nat \ state option" where
"exec _ s 0 = None"
| "exec SKIP s f = Some s"
| "exec (x::=v) s f = Some (s(x:=aval v s))"
| "exec (c1;;c2) s f = (
case exec c1 s f of
None \ None
| Some s' \ exec c2 s' f)"
(* add more clauses here *)
(* your definition needs to adhere to the following theorem: *)
theorem exec_equiv_bigstep: "(\i. exec c s f = Some s') \ (c,s) \ s'"
oops
(* the proof is optional (step 2) *)
subsection "Step 2 (optional)"
text \
You might need both \arbitrary\ and \rule\ in the same \induction\. If you have found
the correct induction invocation, the subgoals should go through automatically.
\
lemma exec_imp_bigstep: "exec c s f = Some s' \ (c,s) \ s'"
sorry
text \
For the other direction, prove a monotonicity lemma first:
If the execution terminates with fuel \f\, it terminates
with the same result using a larger amount of fuel \f' \ f\.
For this, first prove the following lemma:
\
lemma exec_add: "exec c s f = Some s' \ exec c s (f + k) = Some s'"
sorry
text \
Only the case for @{const While} requires some effort.
\emph{Hint:} Make a case distinction on the value of the condition \b\.
\
text \Now the monotonicity lemma that we want follows easily:\
lemma exec_mono: "exec c s f = Some s' \ f' \ f \ exec c s f' = Some s'"
by (auto simp: exec_add dest: le_Suc_ex)
text \
The main lemma is proved by induction over the big-step semantics. Recall
the adapted induction rule @{thm [source=true] big_step_induct} that nicely handles the
pattern \big_step (c,s) s'\.
\
lemma bigstep_imp_exec: "(c,s) \ s' \ \k. exec c s k = Some s'"
proof (induct rule: big_step_induct)
case (Skip s) have "exec SKIP s 1 = Some s" by auto
thus ?case by blast
next
case (Seq c1 s1 s2 c2 s3)
then obtain f1 f2 where "exec c1 s1 f1 = Some s2" "exec c2 s2 f2 = Some s3"
by auto
with exec_mono[of c1 s1 f1 s2] exec_mono[of c2 s2 f2 s3]
have
"exec c1 s1 (max f1 f2) = Some s2" and "exec c2 s2 (max f1 f2) = Some s3"
by auto
hence "exec (c1;;c2) s1 (max f1 f2) = Some s3" by (cases "max f1 f2") (auto simp add: add_ac)
thus ?case by blast
next
case (Assign x a s)
have "exec (x::=a) s 1 = Some (s(x:=aval a s))" by auto
thus ?case by blast
next
(* fill out the rest of the proof *)
oops
end