Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Exercise 2 (Blocks Big-Step)

This is the task corresponding to exercise 2.

Resources

Download Files

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

Terms and Conditions