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" Complex_Main
begin
definition null_state ("<>") where
"null_state \<equiv> \<lambda>x. 0"
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
"_State ms" == "_Update <> ms"
"_State (_updbinds b bs)" <= "_Update (_State b) bs"
end
theory Submission
imports Defs
begin
paragraph \<open>Arithmetic Expressions\<close>
datatype pval = Iv int | Rv real
datatype val = Ia "int \<Rightarrow> int" | Ra "int \<Rightarrow> real"
type_synonym vname = string
type_synonym state = "vname \<Rightarrow> val"
datatype aexp = Ic int | Rc real | Vidx vname aexp | Plus aexp aexp
inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> pval \<Rightarrow> bool" where
taval_Ic: "taval (Ic i) s (Iv i)" |
taval_Rc: "taval (Rc r) s (Rv r)" |
taval_PlusInt: "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2)
\<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
taval_PlusReal: "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
\<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
\<comment> \<open>New:\<close>
inductive_cases taval_elims:
"taval (Ic i) s v" "taval (Rc i) s v"
"taval (V x) s v"
"taval (Plus a1 a2) s v"
\<comment> \<open>New\<close>
"taval (Vidx x i) s v"
paragraph "Boolean Expressions"
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
"tbval (Bc v) s v" |
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
paragraph "Syntax of Commands"
datatype
com = SKIP
| Seq com com ("_;; _" [60, 61] 60)
| If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61)
| While bexp com ("WHILE _ DO _" [0, 61] 61)
\<comment> \<open>New:\<close>
| AssignIdx vname aexp aexp ("_[_] ::= _" [1000, 0, 61] 61)
| ArrayCpy vname vname ("_[] ::= _" [1000, 1000] 61)
| ArrayClear vname ("CLEAR _[]" [1000] 61)
paragraph "Small-Step Semantics of Commands"
inductive
small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
where
Seq1: "(SKIP;;c,s) \<rightarrow> (c,s)" |
Seq2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;;c2,s) \<rightarrow> (c1';;c2,s')" |
IfTrue: "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
\<comment> \<open>New:\<close>
lemmas small_step_induct = small_step.induct[split_format(complete)]
paragraph "The Type System"
datatype ty = Ity | Rty
type_synonym tyenv = "vname \<Rightarrow> ty"
inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
where
Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" |
Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
\<comment> \<open>New:\<close>
declare atyping.intros [intro!]
inductive_cases [elim!]:
"\<Gamma> \<turnstile> V x : \<tau>" "\<Gamma> \<turnstile> Ic i : \<tau>" "\<Gamma> \<turnstile> Rc r : \<tau>" "\<Gamma> \<turnstile> Plus a1 a2 : \<tau>" "\<Gamma> \<turnstile> Vidx x i : \<tau>"
text\<open>Warning: the ``:'' notation leads to syntactic ambiguities,
i.e. multiple parse trees, because ``:'' also stands for set membership.
In most situations Isabelle's type system will reject all but one parse tree,
but will still inform you of the potential ambiguity.\<close>
inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
where
B_ty: "\<Gamma> \<turnstile> Bc v" |
Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
declare btyping.intros [intro!]
inductive_cases [elim!]: "\<Gamma> \<turnstile> Not b" "\<Gamma> \<turnstile> And b1 b2" "\<Gamma> \<turnstile> Less a1 a2"
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
Skip_ty: "\<Gamma> \<turnstile> SKIP" |
Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;;c2" |
If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c" |
AssignIdx_ty: "\<Gamma> \<turnstile> i : Ity \<Longrightarrow> \<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma>(x) = \<tau> \<Longrightarrow> \<Gamma> \<turnstile> x[i] ::= a" |
Clear_ty: "\<Gamma> \<turnstile> CLEAR x[]" |
Copy_ty: "\<Gamma> x = \<tau> \<Longrightarrow> \<Gamma> y = \<tau> \<Longrightarrow> \<Gamma> \<turnstile> x[] ::= y"
declare ctyping.intros [intro!]
inductive_cases [elim!]:
"\<Gamma> \<turnstile> c1;;c2"
"\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
"\<Gamma> \<turnstile> WHILE b DO c"
\<comment> \<open>New\<close>
"\<Gamma> \<turnstile> x[i] ::= a"
"\<Gamma> \<turnstile> CLEAR x[]"
"\<Gamma> \<turnstile> x[] ::= y"
paragraph "Well-typed Programs Do Not Get Stuck"
fun ptype :: "pval \<Rightarrow> ty" where
"ptype (Iv i) = Ity" |
"ptype (Rv r) = Rty"
fun type :: "val \<Rightarrow> ty" where
"type (Ia i) = Ity" |
"type (Ra r) = Rty"
lemma ptype_eq_Ity[simp]: "ptype v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
by (cases v) simp_all
lemma ptype_eq_Rty[simp]: "ptype v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
by (cases v) simp_all
lemma type_eq_Ity[simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Ia i)"
by (cases v) simp_all
lemma type_eq_Rty[simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Ra 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)"
theorem apreservation:
"\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> ptype v = \<tau>"
sorry
theorem aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
sorry
theorem bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
sorry
theorem progress:
"\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
sorry
theorem styping_preservation:
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
sorry
theorem ctyping_preservation:
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'"
sorry
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
where "x \<rightarrow>* y == star small_step x y"
corollary 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''"
apply(induction rule:star_induct)
apply (metis progress)
by (metis styping_preservation ctyping_preservation)
text \<open>Hint: Note that the original proofs are highly automated. Do not expect your proofs
to be quite as automated!
Use Isar. Explicit rule inversion can be helpful. Recall that this can be achieved with
a proof snippet of the following form:\\
\<open>
from \<open>taval a s v\<close> show ?case
proof cases
\<close>
\<close>
end
theory Check imports Submission begin theorem apreservation: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> ptype v = \<tau>" by (rule Submission.apreservation) theorem aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v" by (rule Submission.aprogress) theorem bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v" by (rule Submission.bprogress) 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 styping_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'" by (rule Submission.styping_preservation) theorem ctyping_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'" by (rule Submission.ctyping_preservation) end