Homework 5_1

Definitions File

theory Defs
  imports "HOL-IMP.BExp" "HOL-IMP.Star"
begin

datatype
  com = SKIP
  | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
  | Seq    com  com         ("_;;/ _"  [60, 61] 60)
  | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
  | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
  | THROW
  | Attempt com com         ("(ATTEMPT _/ CLEANUP _)"  [0, 61] 61)


consts big_step :: "com \<times> state \<Rightarrow> com \<times> state \<Rightarrow> bool"

consts small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

paragraph "Step 1"

inductive big_step :: "com \<times> state \<Rightarrow> com \<times> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
  

paragraph "Step 2"

lemmas big_step_induct = big_step.induct[split_format(complete)]
declare big_step.intros[intro]

paragraph "Step 3"

lemma big_step_result: "(c,s) \<Rightarrow> (c',s') \<Longrightarrow> (c' = SKIP \<or> c' = THROW)"
  sorry

paragraph "Step 4"

inductive small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
  

abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
  where "x \<rightarrow>* y == star small_step x y"

declare small_step.intros[simp,intro]

lemma big_to_small: "cs \<Rightarrow> xt \<Longrightarrow> cs \<rightarrow>* xt"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma big_step_result: "(c,s) \<Rightarrow> (c',s') \<Longrightarrow> (c' = SKIP \<or> c' = THROW)"
  by (rule Submission.big_step_result)

lemma big_to_small: "cs \<Rightarrow> xt \<Longrightarrow> cs \<rightarrow>* xt"
  by (rule Submission.big_to_small)

end