Homework 7_1

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