###### Cookies disclaimer

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.

# Homework 06.1

This is the task corresponding to the first part of homework 6.

## Resources

Download Files

### 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```

Terms and Conditions