Theory Types

section "A Typed Language"

theory Types imports Star Complex_Main begin

text ‹We build on theoryComplex_Main instead of theoryMain to access
the real numbers.›

subsection "Arithmetic Expressions"

datatype val = Iv int | Rv real

type_synonym vname = string
type_synonym state = "vname  val"

datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp

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! *)

  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"

  small_step :: "(com × state)  (com × state)  bool" (infix "" 55)
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_/ / (_ :/ _))" [50,0,50] 50)
Ic_ty: "Γ  Ic i : Ity" |
Rc_ty: "Γ  Rc r : Rty" |
V_ty: "Γ  V x : Γ x" |
Plus_ty: "Γ  a1 : τ  Γ  a2 : τ  Γ  Plus a1 a2 : τ"

declare atyping.intros [intro!]
inductive_cases [elim!]:
  "Γ  V x : τ" "Γ  Ic i : τ" "Γ  Rc r : τ" "Γ  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 "" 50)
B_ty: "Γ  Bc v" |
Not_ty: "Γ  b  Γ  Not b" |
And_ty: "Γ  b1  Γ  b2  Γ  And b1 b2" |
Less_ty: "Γ  a1 : τ  Γ  a2 : τ  Γ  Less a1 a2"

declare btyping.intros [intro!]
inductive_cases [elim!]: "Γ  Not b" "Γ  And b1 b2" "Γ  Less a1 a2"

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

declare ctyping.intros [intro!]
inductive_cases [elim!]:
  "Γ  x ::= a"  "Γ  c1;;c2"
  "Γ  IF b THEN c1 ELSE c2"
  "Γ  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 type_eq_Ity[simp]: "type v = Ity  (i. v = Iv i)"
by (cases v) simp_all

lemma type_eq_Rty[simp]: "type v = Rty  (r. v = Rv r)"
by (cases v) simp_all

definition styping :: "tyenv  state  bool" (infix "" 50)
where "Γ  s    (x. type (s x) = Γ x)"

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

lemma aprogress: "Γ  a : τ  Γ  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)
    case Rv
    with Plus_ty v show ?thesis
      by(fastforce intro: taval.intros(5) dest!: apreservation)
qed (auto intro: taval.intros)

lemma bprogress: "Γ  b  Γ  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)
    case Rv
    with Less_ty v show ?thesis
      by (fastforce intro!: tbval.intros(5) dest!:apreservation)
qed (auto intro: tbval.intros)

theorem progress:
  "Γ  c  Γ  s  c  SKIP  cs'. (c,s)  cs'"
proof(induction rule: ctyping.induct)
  case Skip_ty thus ?case by simp
  case Assign_ty 
  thus ?case by (metis Assign aprogress)
  case Seq_ty thus ?case by simp (metis Seq1 Seq2)
  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)
    assume "¬bv"
    with tbval b s bv show ?case by simp (metis IfFalse)
  case While_ty show ?case by (metis While)

theorem styping_preservation:
  "(c,s)  (c',s')  Γ  c  Γ  s  Γ  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')  Γ  c  Γ  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')  Γ  c  Γ  s  c'  SKIP
    cs''. (c',s')  cs''"
apply(induction rule:star_induct)
apply (metis progress)
by (metis styping_preservation ctyping_preservation)