Homework 9

Definitions File

theory Defs
  imports "HOL-IMP.Small_Step" "HOL-IMP.Star" "HOL-IMP.Hoare"
begin

declare [[names_short]]

type_synonym ('n,'l) flowgraph = "'n \<Rightarrow> 'l \<Rightarrow> 'n \<Rightarrow> bool"

datatype label = Assign vname aexp | Cond bexp | Skip


consts step :: "('n\<times>'s) \<Rightarrow> ('n\<times>'s) \<Rightarrow> bool"

consts enabled :: "label \<Rightarrow> state \<Rightarrow> bool"

consts effect :: "label \<Rightarrow> state \<Rightarrow> state"

consts cfg :: "com \<Rightarrow> label \<Rightarrow> com \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

type_synonym ('n,'l) flowgraph = "'n \<Rightarrow> 'l \<Rightarrow> 'n \<Rightarrow> bool"

locale flowgraph =
  fixes G :: "('n,'l) flowgraph"
  fixes enabled :: "'l \<Rightarrow> 's \<Rightarrow> bool"
  fixes effect :: "'l \<Rightarrow> 's \<Rightarrow> 's"
begin

inductive step :: "('n\<times>'s) \<Rightarrow> ('n\<times>'s) \<Rightarrow> bool" 

abbreviation "steps \<equiv> star step"

context
  fixes I :: "'n \<Rightarrow> ('s \<Rightarrow> bool)"
  assumes preserve: "\<lbrakk> I n s; G n l n'; enabled l s \<rbrakk> \<Longrightarrow> I n' (effect l s)"
begin  

lemma preserves:
  assumes "steps (n,s) (n',s')"
      and "I n s"
  shows "I n' s'"
  sorry

end

end

fun enabled :: "label \<Rightarrow> state \<Rightarrow> bool"  where
  "enabled _ = undefined"

fun effect :: "label \<Rightarrow> state \<Rightarrow> state"  where
  "effect _ = undefined"

inductive cfg :: "com \<Rightarrow> label \<Rightarrow> com \<Rightarrow> bool" 
  where
    "cfg (x::=a) (Assign x a) SKIP"
  | "cfg (IF b THEN c1 ELSE c2) (Cond (Not b)) c2"
    

code_pred cfg .

interpretation flowgraph cfg enabled effect .

thm preserves

lemma steps_eq: "cs \<rightarrow>* cs' \<longleftrightarrow> steps cs cs'"
  sorry

lemma floyd:
  assumes PRE: "\<And>s. P s \<Longrightarrow> I c s"
      and PRES: "\<And>n s c l c'. \<lbrakk>cfg c l c'; I c s; enabled l s \<rbrakk> \<Longrightarrow> I c' (effect l s)"
      and POST: "\<And>s. I SKIP s \<Longrightarrow> Q s"
  shows "\<Turnstile> {P} c {Q}"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma steps_eq: "cs \<rightarrow>* cs' \<longleftrightarrow> steps cs cs'"
  by (rule Submission.steps_eq)

lemma floyd: "(\<And>s. P s \<Longrightarrow> I c s) \<Longrightarrow> (\<And>n s c l c'. \<lbrakk>cfg c l c'; I c s; enabled l s \<rbrakk> \<Longrightarrow> I c' (effect l s)) \<Longrightarrow> (\<And>s. I SKIP s \<Longrightarrow> Q s) \<Longrightarrow> \<Turnstile> {P} c {Q}"
  by (rule Submission.floyd)

end