Exercise 2 (Blocks Big-Step)

Definitions File

theory Defs imports "HOL-IMP.Big_Step" begin
declare [[syntax_ambiguity_warning=false]]
no_syntax   "_Finset" :: "args \<Rightarrow> 'a set"    ("{(_)}")

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)
\<comment>\<open>New commands:\<close>
      | Block   com         ("{(_)}" [60] 61)
      | START

inductive
  big_step' :: "com \<times> state \<times> com \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
Skip: "(SKIP,s,c) \<Rightarrow> s" |
Assign: "(x ::= a,s,c) \<Rightarrow> (s(x := aval a s))" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1,c) \<Rightarrow> s\<^sub>2; (c\<^sub>2,s\<^sub>2,c) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2,s\<^sub>1,c) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s;  (c\<^sub>1,s,c) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s,c) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2,s,c) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s,c) \<Rightarrow> t" |
\<comment>\<open>New commands\<close>
Block: "(c,s,c) \<Rightarrow> t \<Longrightarrow> ({c},s,_) \<Rightarrow> t" |
Start: "(c,s,c) \<Rightarrow> t \<Longrightarrow> (START,s,c) \<Rightarrow> t"

declare big_step'.intros[intro]
lemmas big_step'_induct = big_step'.induct[split_format(complete)]
inductive_cases SkipE[elim!]: "(SKIP,s,d) \<Rightarrow> t"
inductive_cases AssignE[elim!]: "(x ::= a,s,d) \<Rightarrow> t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1,d) \<Rightarrow> s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s,d) \<Rightarrow> t"
inductive_cases BlockE[elim!]: "({c},s,d) \<Rightarrow> t"
inductive_cases JumpE[elim]: "(START,s,d) \<Rightarrow> t"

end

Template File

theory Submission imports Defs begin        

fun to_block :: "Com.com \<Rightarrow> com" where
  "to_block _ = undefined"

theorem preservation: "(c,s) \<Rightarrow> t \<Longrightarrow> (to_block c,s,cb) \<Rightarrow> t"
  sorry

end

Check File

theory Check imports Submission begin

theorem preservation: "(c,s) \<Rightarrow> t \<Longrightarrow> (to_block c,s,cb) \<Rightarrow> t"
  by (rule Submission.preservation)

end