Homework 06

Definitions File

theory Defs
  imports "IMP.Wp_Demo" "IMP.Small_Step"
begin

end

Template File

theory Submission
  imports Defs
begin

definition "square \<equiv> 
  ''z'' ::= N 1;;
  ''a'' ::= N 0;;
   WHILE Less (N 0) (V ''n'') DO (
     ''a'' ::= Plus (V ''a'') (V ''z'');;
     ''z'' ::= Plus (V ''z'') (N 2);; 
     ''n'' ::= Plus (V ''n'') (N (-1))
   )"

theorem square_correct: "s ''n'' \<equiv> n \<Longrightarrow> n \<ge> 0 \<Longrightarrow> wlp square (\<lambda>s'. let a = s' ''a'' in a = n*n) s"
  sorry

fun cfg_step :: "com * state \<Rightarrow> com * state" where
  "cfg_step _ = undefined"

theorem small_step_cfg_step: "cs \<rightarrow> cs' \<Longrightarrow> cfg_step cs = cs'"
  sorry

theorem final_cfg_step: "final cs \<Longrightarrow> cfg_step cs = cs"
  sorry

fun cfg_steps :: "nat \<Rightarrow> com * state \<Rightarrow> com * state" where
  "cfg_steps 0 cs = cs" |
  "cfg_steps (Suc n) cs = cfg_steps n (cfg_step cs)"

theorem small_steps_cfg_steps:
  "cs \<rightarrow>* cs' \<Longrightarrow> \<exists>n. cfg_steps n cs = cs'"
  sorry

theorem cfg_steps_small_steps:
  "cfg_steps n cs = cs' \<Longrightarrow> cs \<rightarrow>* cs'"
  sorry

corollary cfg_steps_correct:
  "cs \<rightarrow>* cs' \<longleftrightarrow> (\<exists>n. cfg_steps n cs = cs')"
  by (metis small_steps_cfg_steps cfg_steps_small_steps)

definition
  "is_sim R step step' \<equiv> \<forall>a b a'. R a b \<and> step a a' \<longrightarrow> (\<exists>b'. R a' b' \<and> step' b b')"

lemma is_sim_star:
  assumes "is_sim R step step'" "R a b" "step\<^sup>*\<^sup>* a a'"
  shows "\<exists>b'. R a' b' \<and> step'\<^sup>*\<^sup>* b b'"
  sorry

inductive terminating for step where
  "terminating step x"

theorem terminating_simulation:
  assumes "is_sim R step step'" "terminating step' b" "R a b"
  shows "terminating step a"
  sorry


theorem wlp_whileI':
  assumes INIT: "I s\<^sub>0"
  assumes STEP: "\<And>s. I s \<Longrightarrow> (if bval b s then wlp c I s else Q s)"
  shows "wlp (WHILE b DO c) Q s\<^sub>0"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem square_correct: "s ''n'' \<equiv> n \<Longrightarrow> n \<ge> 0 \<Longrightarrow> wlp square (\<lambda>s'. let a = s' ''a'' in a = n*n) s"
  by (rule Submission.square_correct)

theorem small_step_cfg_step: "cs \<rightarrow> cs' \<Longrightarrow> cfg_step cs = cs'"
  by (rule Submission.small_step_cfg_step)

theorem final_cfg_step: "final cs \<Longrightarrow> cfg_step cs = cs"
  by (rule Submission.final_cfg_step)

theorem small_steps_cfg_steps:
  "cs \<rightarrow>* cs' \<Longrightarrow> \<exists>n. cfg_steps n cs = cs'"
  by (rule Submission.small_steps_cfg_steps)

theorem cfg_steps_small_steps:
  "cfg_steps n cs = cs' \<Longrightarrow> cs \<rightarrow>* cs'"
  by (rule Submission.cfg_steps_small_steps)

theorem terminating_simulation:
  assumes "is_sim R step step'" "terminating step' b" "R a b"
  shows "terminating step a"
  using assms by (rule Submission.terminating_simulation)

theorem wlp_whileI':
  assumes INIT: "I s\<^sub>0"
  assumes STEP: "\<And>s. I s \<Longrightarrow> (if bval b s then wlp c I s else Q s)"
  shows "wlp (WHILE b DO c) Q s\<^sub>0"
  using assms by (rule Submission.wlp_whileI')

end