Homework 05

Definitions File

theory Defs
imports "HOL-IMP.Small_Step"
begin

end

Template File

theory Submission
  imports Defs
begin

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 \<rightharpoonup> state"
type_synonym 'q cfg = "('q,effect) lts"

fun eff_list :: "effect list \<Rightarrow> state \<rightharpoonup> state" 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