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.
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
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
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