Homework 5

Definitions File

theory Defs
  imports Main "HOL-IMP.Small_Step"
begin

declare [[names_short]]


type_synonym ('q,'l) lts = "'q \<Rightarrow> 'l \<Rightarrow> 'q \<Rightarrow> bool"
inductive word :: "('q,'l) lts \<Rightarrow> 'q \<Rightarrow> 'l list \<Rightarrow> 'q \<Rightarrow> bool" for \<delta> where
  empty: "word \<delta> q [] q"
| prepend: "\<lbrakk>\<delta> q l p; word \<delta> p ls r\<rbrakk> \<Longrightarrow> word \<delta> q (l#ls) r"

type_synonym effect = "state \<Rightarrow> state option"
type_synonym 'q cfg = "('q,effect) lts"


consts eff_list :: "effect list \<Rightarrow> state \<Rightarrow> state option"

consts cfg :: "com cfg"


end

Template File

theory Submission
  imports Defs
begin

type_synonym effect = "state \<Rightarrow> state option"
type_synonym 'q cfg = "('q,effect) lts"

fun eff_list :: "effect list \<Rightarrow> state \<Rightarrow> state option"  where
  "eff_list _ = undefined"

inductive cfg :: "com cfg" where
  cfg_assign: "cfg (x ::= a) (\<lambda>s. Some (s(x:=aval a s))) (SKIP)"
| cfg_Seq2: "cfg c1 e c1' \<Longrightarrow> cfg (c1;;c2) e (c1';;c2)"
  

theorem eq_step: "(c,s) \<rightarrow> (c',s') \<longleftrightarrow> (\<exists>e. cfg c e c' \<and> e s = Some s')"
  sorry

theorem eq_path: "(c,s) \<rightarrow>* (c',s') \<longleftrightarrow> (\<exists>\<pi>. word cfg c \<pi> c' \<and> eff_list \<pi> s = Some s')"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem eq_step: "(c,s) \<rightarrow> (c',s') \<longleftrightarrow> (\<exists>e. cfg c e c' \<and> e s = Some s')"
  by (rule Submission.eq_step)

theorem eq_path: "(c,s) \<rightarrow>* (c',s') \<longleftrightarrow> (\<exists>\<pi>. word cfg c \<pi> c' \<and> eff_list \<pi> s = Some s')"
  by (rule Submission.eq_path)

end