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