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.

# Homework 7_1

This is the task corresponding to homework 7_1.

## Resources

### Definitions File

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

declare [[names_short]]
declare [[syntax_ambiguity_warning=false]]

paragraph "Preparation 1"

datatype val = Iv int | Bv bool

type_synonym vname = string
type_synonym state = "vname \<Rightarrow> val"

datatype exp =
N int | V vname | Plus exp exp |  Bc bool | Not exp | And exp exp | Less exp exp

datatype
com = SKIP
| Assign vname exp       ("_ ::= _" [1000, 61] 61)
| Seq    com  com         ("_;; _"  [60, 61] 60)
| If     exp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
| While  exp com         ("WHILE _ DO _"  [0, 61] 61)

inductive eval :: "exp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
"eval (N i) s (Iv i)" |
"eval (V x) s (s x)" |
"eval a\<^sub>1 s (Iv i\<^sub>1) \<Longrightarrow> eval a\<^sub>2 s (Iv i\<^sub>2) \<Longrightarrow> eval (Plus a\<^sub>1 a\<^sub>2) s (Iv (i\<^sub>1 + i\<^sub>2))" |
"eval (Bc v) s (Bv v)" |
"eval b s (Bv bv) \<Longrightarrow> eval (Not b) s (Bv (\<not>bv))" |
"eval b\<^sub>1 s (Bv bv\<^sub>1) \<Longrightarrow> eval b\<^sub>2 s (Bv bv\<^sub>2) \<Longrightarrow> eval (And b\<^sub>1 b\<^sub>2) s (Bv (bv\<^sub>1 \<and> bv\<^sub>2))" |
"eval a\<^sub>1 s (Iv i\<^sub>1) \<Longrightarrow> eval a\<^sub>2 s (Iv i\<^sub>2) \<Longrightarrow> eval (Less a\<^sub>1 a\<^sub>2) s (Bv (i\<^sub>1 < i\<^sub>2))"

inductive_cases [elim!]:
"eval (N i) s v"
"eval (V x) s v"
"eval (Plus a1 a2) s v"
"eval (Bc b) s v"
"eval (Not b) s v"
"eval (And b1 b2) s v"
"eval (Less a1 a2) s v"

paragraph "preparation 2"

inductive
small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
where
Assign:  "eval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
Seq1:   "(SKIP;;c,s) \<rightarrow> (c,s)" |
Seq2:   "(c\<^sub>1,s) \<rightarrow> (c\<^sub>1\<^sub>',s') \<Longrightarrow> (c\<^sub>1;;c\<^sub>2,s) \<rightarrow> (c\<^sub>1\<^sub>';;c\<^sub>2,s')" |
IfTrue:  "eval b s (Bv True) \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>1,s)" |
IfFalse: "eval b s (Bv False) \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" |
While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"

lemmas small_step_induct = small_step.induct[split_format(complete)]
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool"
(infix "\<rightarrow>*" 55) where
"x \<rightarrow>* y == star small_step x y"

paragraph "Preparation 3"

datatype ty = Ity | Bty
type_synonym tyenv = "vname \<Rightarrow> ty"

inductive etyping :: "tyenv \<Rightarrow> exp \<Rightarrow> ty \<Rightarrow> bool"
("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)  where
Ic_ty: "\<Gamma> \<turnstile> N i : Ity" |
V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
Plus_ty: "\<Gamma> \<turnstile> a\<^sub>1 : Ity \<Longrightarrow> \<Gamma> \<turnstile> a\<^sub>2 : Ity \<Longrightarrow> \<Gamma> \<turnstile> Plus a\<^sub>1 a\<^sub>2 : Ity" |
B_ty: "\<Gamma> \<turnstile> Bc v : Bty" |
Not_ty: "\<Gamma> \<turnstile> b : Bty \<Longrightarrow> \<Gamma> \<turnstile> Not b : Bty" |
And_ty: "\<Gamma> \<turnstile> b\<^sub>1 : Bty \<Longrightarrow> \<Gamma> \<turnstile> b\<^sub>2 : Bty \<Longrightarrow> \<Gamma> \<turnstile> And b\<^sub>1 b\<^sub>2 : Bty" |
Less_ty: "\<Gamma> \<turnstile> a\<^sub>1 : Ity \<Longrightarrow> \<Gamma> \<turnstile> a\<^sub>2 : Ity \<Longrightarrow> \<Gamma> \<turnstile> Less a\<^sub>1 a\<^sub>2 : Bty"

inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
Skip_ty: "\<Gamma> \<turnstile> SKIP" |
Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma> x \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
Seq_ty: "\<Gamma> \<turnstile> c\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> c\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> c\<^sub>1;;c\<^sub>2" |
If_ty: "\<Gamma> \<turnstile> b : Bty \<Longrightarrow> \<Gamma> \<turnstile> c\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> c\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2" |
While_ty: "\<Gamma> \<turnstile> b : Bty \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"

inductive_cases [elim!]:
"\<Gamma> \<turnstile> x ::= a"
"\<Gamma> \<turnstile> c1;;c2"
"\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
"\<Gamma> \<turnstile> WHILE b DO c"

fun type :: "val \<Rightarrow> ty" where
"type (Iv i) = Ity" |
"type (Bv r) = Bty"

lemma type_eq_Ity[simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
by (cases v) simp_all

lemma type_eq_Bty[simp]: "type v = Bty \<longleftrightarrow> (\<exists>r. v = Bv r)"
by (cases v) simp_all

definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50) where
"\<Gamma> \<turnstile> s  \<longleftrightarrow>  (\<forall>x. type (s x) = \<Gamma> x)"

end```

### Template File

```theory Submission
imports Defs
begin

theorem progress: "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
sorry

theorem type_sound:
"(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem progress: "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
by (rule Submission.progress)

theorem type_sound: "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
by (rule Submission.type_sound)

end```

Terms and Conditions