Homework 06.1

Definitions File

theory Defs
  imports "HOL-IMP.Star" Complex_Main
begin

datatype val = Iv int | Pv val val

type_synonym vname = string
type_synonym state = "vname ⇒ val"

datatype aexp =  N int | V vname | Plus aexp aexp | Pair aexp aexp

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

datatype
  com = SKIP 
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | AssignP "vname × 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)


datatype ty = Ity | Pty ty ty

type_synonym tyenv = "vname ⇒ ty"

fun type :: "val ⇒ ty" where
"type (Iv i) = Ity" |
"type (Pv v1 v2) = Pty (type v1) (type v2)"

text ‹∗‹Hint›: Add a similar lemma for ‹Pty››
lemma type_eq_Ity[simp]: "type v = Ity ⟷ (∃i. v = Iv i)"
  by (cases v) simp_all

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

end

Template File

theory Submission
  imports Defs
begin

inductive taval :: "aexp ⇒ state ⇒ val ⇒ bool" where
"taval (N i) s (Iv i)" |
"taval (V x) s (s x)"
― ‹Your cases here›

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

― ‹Nothing to do here:›
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)"

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)"
― ‹Your cases here›

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

inductive atyping :: "tyenv ⇒ aexp ⇒ ty ⇒ bool"
  ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50)
where
Ic_ty: "Γ ⊢ N i : Ity" |
V_ty: "Γ ⊢ V x : Γ x"
― ‹Your cases here›

declare atyping.intros [intro!]
inductive_cases [elim!]:
  "Γ ⊢ V x : τ" "Γ ⊢ N i : τ" "Γ ⊢ Plus a1 a2 : τ" "Γ ⊢ Pair a1 a2 : τ"


― ‹Nothing to do:›
inductive btyping :: "tyenv ⇒ bexp ⇒ bool" (infix "⊢" 50)
where
B_ty: "Γ ⊢ Bc v" |
Not_ty: "Γ ⊢ b ⟹ Γ ⊢ Not b" |
And_ty: "Γ ⊢ b1 ⟹ Γ ⊢ b2 ⟹ Γ ⊢ And b1 b2" |
Less_ty: "Γ ⊢ a1 : Ity ⟹ Γ ⊢ a2 : Ity ⟹ Γ ⊢ 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"
― ‹Your cases here›

declare ctyping.intros [intro!]
inductive_cases [elim!]:
  "Γ ⊢ x ::= a" "Γ ⊢ x ::== a"  "Γ ⊢ c1;;c2"
  "Γ ⊢ IF b THEN c1 ELSE c2"
  "Γ ⊢ WHILE b DO c"



theorem apreservation:
  "Γ ⊢ a : τ ⟹ taval a s v ⟹ Γ ⊢ s ⟹ type v = τ"
  sorry

theorem aprogress: "Γ ⊢ a : τ ⟹ Γ ⊢ s ⟹ ∃v. taval a s v"
  sorry

lemma bprogress: "Γ ⊢ b ⟹ Γ ⊢ s ⟹ ∃v. tbval b s v"
proof(induction rule: btyping.induct)
  case (Less_ty Γ a1 a2)
  then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
    by (metis aprogress)
  with Less_ty show ?case
    by (fastforce intro!: tbval.intros(4) dest!:apreservation)
qed (auto intro: tbval.intros)

theorem progress:
  "Γ ⊢ c ⟹ Γ ⊢ s ⟹ c ≠ SKIP ⟹ ∃cs'. (c,s) → cs'"
  sorry

theorem styping_preservation:
  "(c,s) → (c',s') ⟹ Γ ⊢ c ⟹ Γ ⊢ s ⟹ Γ ⊢ s'"
  sorry

theorem ctyping_preservation:
  "(c,s) → (c',s') ⟹ Γ ⊢ c ⟹ Γ ⊢ c'"
  sorry

abbreviation small_steps :: "com * state ⇒ com * state ⇒ bool" (infix "→*" 55)
where "x →* y == star small_step x y"
corollary 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)

end

Check File

theory Check
  imports Submission
begin

theorem apreservation:
  "Γ ⊢ a : τ ⟹ taval a s v ⟹ Γ ⊢ s ⟹ type v = τ"
  by (rule Submission.apreservation)

theorem aprogress: "Γ ⊢ a : τ ⟹ Γ ⊢ s ⟹ ∃v. taval a s v"
  by (rule Submission.aprogress)

theorem progress:
  "Γ ⊢ c ⟹ Γ ⊢ s ⟹ c ≠ SKIP ⟹ ∃cs'. (c,s) → cs'"
  by (rule Submission.progress)

theorem styping_preservation:
  "(c,s) → (c',s') ⟹ Γ ⊢ c ⟹ Γ ⊢ s ⟹ Γ ⊢ s'"
  by (rule Submission.styping_preservation)

theorem ctyping_preservation:
  "(c,s) → (c',s') ⟹ Γ ⊢ c ⟹ Γ ⊢ c'"
  by (rule Submission.ctyping_preservation)

end