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

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