Theory Types

theory Types
imports Star Complex_Main
header "A Typed Language"

theory Types imports Star Complex_Main begin

text {* We build on @{theory Complex_Main} instead of @{theory Main} to access
the real numbers. *}


subsection "Arithmetic Expressions"

datatype val = Iv int | Rv real

type_synonym vname = string
type_synonym state = "vname => val"

text_raw{*\snip{aexptDef}{0}{2}{% *}
datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp
text_raw{*}%endsnip*}

inductive taval :: "aexp => state => val => bool" where
"taval (Ic i) s (Iv i)" |
"taval (Rc r) s (Rv r)" |
"taval (V x) s (s x)" |
"taval a1 s (Iv i1) ==> taval a2 s (Iv i2)
==> taval (Plus a1 a2) s (Iv(i1+i2))"
|
"taval a1 s (Rv r1) ==> taval a2 s (Rv r2)
==> taval (Plus a1 a2) s (Rv(r1+r2))"


inductive_cases [elim!]:
"taval (Ic i) s v" "taval (Rc i) s v"
"taval (V x) s v"
"taval (Plus a1 a2) s v"

subsection "Boolean Expressions"

datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

inductive tbval :: "bexp => state => bool => bool" where
"tbval (Bc v) s v" |
"tbval b s bv ==> tbval (Not b) s (¬ bv)" |
"tbval b1 s bv1 ==> tbval b2 s bv2 ==> tbval (And b1 b2) s (bv1 & bv2)" |
"taval a1 s (Iv i1) ==> taval a2 s (Iv i2) ==> tbval (Less a1 a2) s (i1 < i2)" |
"taval a1 s (Rv r1) ==> taval a2 s (Rv r2) ==> tbval (Less a1 a2) s (r1 < r2)"

subsection "Syntax of Commands"
(* a copy of Com.thy - keep in sync! *)

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)
| While bexp com ("WHILE _ DO _" [0, 61] 61)


subsection "Small-Step Semantics of Commands"

inductive
small_step :: "(com × state) => (com × state) => bool" (infix "->" 55)
where
Assign: "taval a s v ==> (x ::= a, s) -> (SKIP, s(x := v))" |

Seq1: "(SKIP;;c,s) -> (c,s)" |
Seq2: "(c1,s) -> (c1',s') ==> (c1;;c2,s) -> (c1';;c2,s')" |

IfTrue: "tbval b s True ==> (IF b THEN c1 ELSE c2,s) -> (c1,s)" |
IfFalse: "tbval b s False ==> (IF b THEN c1 ELSE c2,s) -> (c2,s)" |

While: "(WHILE b DO c,s) -> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"

lemmas small_step_induct = small_step.induct[split_format(complete)]

subsection "The Type System"

datatype ty = Ity | Rty

type_synonym tyenv = "vname => ty"

inductive atyping :: "tyenv => aexp => ty => bool"
("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
where
Ic_ty: "Γ \<turnstile> Ic i : Ity" |
Rc_ty: "Γ \<turnstile> Rc r : Rty" |
V_ty: "Γ \<turnstile> V x : Γ x" |
Plus_ty: "Γ \<turnstile> a1 : τ ==> Γ \<turnstile> a2 : τ ==> Γ \<turnstile> Plus a1 a2 : τ"

text{* 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. *}


inductive btyping :: "tyenv => bexp => bool" (infix "\<turnstile>" 50)
where
B_ty: "Γ \<turnstile> Bc v" |
Not_ty: "Γ \<turnstile> b ==> Γ \<turnstile> Not b" |
And_ty: "Γ \<turnstile> b1 ==> Γ \<turnstile> b2 ==> Γ \<turnstile> And b1 b2" |
Less_ty: "Γ \<turnstile> a1 : τ ==> Γ \<turnstile> a2 : τ ==> Γ \<turnstile> Less a1 a2"

inductive ctyping :: "tyenv => com => bool" (infix "\<turnstile>" 50) where
Skip_ty: "Γ \<turnstile> SKIP" |
Assign_ty: "Γ \<turnstile> a : Γ(x) ==> Γ \<turnstile> x ::= a" |
Seq_ty: "Γ \<turnstile> c1 ==> Γ \<turnstile> c2 ==> Γ \<turnstile> c1;;c2" |
If_ty: "Γ \<turnstile> b ==> Γ \<turnstile> c1 ==> Γ \<turnstile> c2 ==> Γ \<turnstile> IF b THEN c1 ELSE c2" |
While_ty: "Γ \<turnstile> b ==> Γ \<turnstile> c ==> Γ \<turnstile> WHILE b DO c"

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

subsection "Well-typed Programs Do Not Get Stuck"

fun type :: "val => ty" where
"type (Iv i) = Ity" |
"type (Rv r) = Rty"

lemma [simp]: "type v = Ity <-> (∃i. v = Iv i)"
by (cases v) simp_all

lemma [simp]: "type v = Rty <-> (∃r. v = Rv r)"
by (cases v) simp_all

definition styping :: "tyenv => state => bool" (infix "\<turnstile>" 50)
where "Γ \<turnstile> s <-> (∀x. type (s x) = Γ x)"

lemma apreservation:
"Γ \<turnstile> a : τ ==> taval a s v ==> Γ \<turnstile> s ==> type v = τ"
apply(induction arbitrary: v rule: atyping.induct)
apply (fastforce simp: styping_def)+
done

lemma aprogress: "Γ \<turnstile> a : τ ==> Γ \<turnstile> s ==> ∃v. taval a s v"
proof(induction rule: atyping.induct)
case (Plus_ty Γ a1 t a2)
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
show ?case
proof (cases v1)
case Iv
with Plus_ty v show ?thesis
by(fastforce intro: taval.intros(4) dest!: apreservation)
next
case Rv
with Plus_ty v show ?thesis
by(fastforce intro: taval.intros(5) dest!: apreservation)
qed
qed (auto intro: taval.intros)

lemma bprogress: "Γ \<turnstile> b ==> Γ \<turnstile> s ==> ∃v. tbval b s v"
proof(induction rule: btyping.induct)
case (Less_ty Γ a1 t a2)
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
by (metis aprogress)
show ?case
proof (cases v1)
case Iv
with Less_ty v show ?thesis
by (fastforce intro!: tbval.intros(4) dest!:apreservation)
next
case Rv
with Less_ty v show ?thesis
by (fastforce intro!: tbval.intros(5) dest!:apreservation)
qed
qed (auto intro: tbval.intros)

theorem progress:
"Γ \<turnstile> c ==> Γ \<turnstile> s ==> c ≠ SKIP ==> ∃cs'. (c,s) -> cs'"
proof(induction rule: ctyping.induct)
case Skip_ty thus ?case by simp
next
case Assign_ty
thus ?case by (metis Assign aprogress)
next
case Seq_ty thus ?case by simp (metis Seq1 Seq2)
next
case (If_ty Γ b c1 c2)
then obtain bv where "tbval b s bv" by (metis bprogress)
show ?case
proof(cases bv)
assume "bv"
with `tbval b s bv` show ?case by simp (metis IfTrue)
next
assume "¬bv"
with `tbval b s bv` show ?case by simp (metis IfFalse)
qed
next
case While_ty show ?case by (metis While)
qed

theorem styping_preservation:
"(c,s) -> (c',s') ==> Γ \<turnstile> c ==> Γ \<turnstile> s ==> Γ \<turnstile> s'"
proof(induction rule: small_step_induct)
case Assign thus ?case
by (auto simp: styping_def) (metis Assign(1,3) apreservation)
qed auto

theorem ctyping_preservation:
"(c,s) -> (c',s') ==> Γ \<turnstile> c ==> Γ \<turnstile> c'"
by (induct rule: small_step_induct) (auto simp: ctyping.intros)

abbreviation small_steps :: "com * state => com * state => bool" (infix "->*" 55)
where "x ->* y == star small_step x y"

theorem type_sound:
"(c,s) ->* (c',s') ==> Γ \<turnstile> c ==> Γ \<turnstile> s ==> c' ≠ SKIP
==> ∃cs''. (c',s') -> cs''"

apply(induction rule:star_induct)
apply (metis progress)
by (metis styping_preservation ctyping_preservation)

end