theory STLCHW
imports STLC
begin
inductive_cases wtv[elim!]: "\ \\<^isub>e Var x : A" and
wti[elim!]: "\ \\<^isub>e Const (IntC n) : A" and
wtb[elim!]: "\ \\<^isub>e Const (BoolC b) : A" and
wtp[elim!]: "\ \\<^isub>e PrimApp f e : A" and
wtlam[elim!]: "\ \\<^isub>e Lam x T s : A" and
wtlet[elim!]: "\ \\<^isub>s SLet x e s : A" and
wtret[elim!]: "\ \\<^isub>s SRet e : A" and
wtcall[elim!]: "\ \\<^isub>s SCall x e1 e2 s : A" and
wttailcall[elim!]: "\ \\<^isub>s STailCall e1 e2 : A"
inductive_cases
bool_int[elim!]: "wt_val (VConst (BoolC b)) IntT" and
int_any[elim!]: "wt_val (VConst (IntC n)) A" and
bool_any[elim!]: "wt_val (VConst (BoolC b)) A" and
clos_any[elim!]: "wt_val (Closure x T s \) A " and
clos_int[elim!]: "wt_val (Closure x T s \) IntT " and
const_fun[elim!]: "wt_val (VConst c) (A \ B)" and
clos_fun[elim!]: "wt_val (Closure x T s \) (A \ B)"
inductive_cases
wtek[elim!]: "[] : A \ B" and
wtk[elim!]: "(s,\)#k : A \ B"
inductive_cases wts[elim!]: "wt_state s A"
lemma delta_safe:
assumes wtop: "typeof_opr f = A \ B"
and wtv: "wt_val v A"
shows "\ v'. delta f v = Some v' \ wt_val v' B"
using wtop wtv
by (case_tac f) (case_tac v, auto, case_tac const, auto)+
lemma lookup_safe:
assumes wtg: "\ \ \" and l: "lookup x \ = Some A"
shows "\ v. lookup x \ = Some v \ wt_val v A"
using wtg l by (induct \) force+
text{*
We choose to prove the following lemma by the induction rule
for eval. An alternative would be to prove it by
induction on the typing derivation, but that approach requires
changing the statement of the lemma to fit a certain form
that is complicated by the fact that the typing relation
is really two mutually inductive relations (one for expressions
and the other for statements). Similarly, we could have
chosen to do induction on e, but that is also a bit more
complicated because the expression datatype is mutually
recursive with the statement datatype.
*}
lemma eval_safe:
assumes wte: "\ \\<^isub>e e : A"
and wtg: "\ \ \"
shows "\ v. eval e \ = Some v \ wt_val v A"
using wte wtg
apply (induct e \ arbitrary: A rule: eval.induct)
using lookup_safe apply force
apply (case_tac c) apply force apply force
using delta_safe apply force
apply force
done
lemma step_safe:
assumes wtsA: "wt_state s A"
shows "final s \ (\ s'. step s = Some s' \ wt_state s' A)"
using wtsA
proof (rule wts)
fix \ \ s' A' k
assume st: "s = (s', \, k)" and gr: "\ \ \" and wts: "\ \\<^isub>s s' : A'"
and wt_k: "k : A' \ A"
show ?thesis
proof (cases s')
case (SLet x e s2)
from wts SLet obtain B where wte: "\ \\<^isub>e e : B"
and wts2: "(x,B)#\ \\<^isub>s s2 : A'" by blast
from wte gr obtain v where v: "eval e \ = Some v"
and wtv: "wt_val v B" using eval_safe by blast
from v SLet st gr wts2 wt_k wtv show ?thesis by auto
next
case (SRet e)
show ?thesis
proof (cases k)
assume k: "k = []" from SRet st k have "final s" by simp
thus ?thesis by blast
next
fix f k' assume k: "k = f#k'"
from wts SRet have wte: "\ \\<^isub>e e : A'" by blast
from wte gr obtain v where v: "eval e \ = Some v"
and wtv: "wt_val v A'" using eval_safe by blast
from SRet st v wtv k wt_k show ?thesis by (case_tac f) auto
qed
next
case (SCall x e1 e2 s2)
from wts SCall obtain B C where wte1: "\ \\<^isub>e e1 : B \ C"
and wte2: "\ \\<^isub>e e2 : B" and wts2: "(x,C)#\ \\<^isub>s s2 : A'" by blast
from wte1 gr obtain v1 where v1: "eval e1 \ = Some v1"
and wtv1: "wt_val v1 (B \ C)" using eval_safe by blast
from wte2 gr obtain v2 where v2: "eval e2 \ = Some v2"
and wtv2: "wt_val v2 B" using eval_safe by blast
from SCall st v1 v2 wtv1 gr wtv2 wts2 wt_k show ?thesis
by (case_tac v1, auto, case_tac "const", auto)
next
case (STailCall e1 e2)
from wts STailCall obtain B where wte1: "\ \\<^isub>e e1 : B \ A'"
and wte2: "\ \\<^isub>e e2 : B" by blast
from wte1 gr obtain v1 where v1: "eval e1 \ = Some v1"
and wtv1: "wt_val v1 (B \ A')" using eval_safe by blast
from wte2 gr obtain v2 where v2: "eval e2 \ = Some v2"
and wtv2: "wt_val v2 B" using eval_safe by blast
from STailCall st v1 v2 wtv1 gr wtv2 wt_k show ?thesis
by (case_tac v1, auto, case_tac "const", auto)
qed
qed
text{*
For this lemma, we choose not to use the induction rule for steps
because that induction rule is a bit messy, with lots of cases
that can be dealt with in a similar fashion. In the following,
we just do proof by induction on n.
*}
lemma steps_safe:
assumes wtsA: "wt_state s A"
shows "steps n s = TimeOut \ (\ r. steps n s = r \ wt_result r A)"
using wtsA
proof (induct n arbitrary: s)
fix s have "steps 0 s = TimeOut" by simp
thus "steps 0 s = TimeOut \ (\r. steps 0 s = r \ wt_result r A)" by blast
next
fix n s
assume IH: "\s. wt_state s A \
steps n s = TimeOut \ (\r. steps n s = r \ wt_result r A)"
and wts: "wt_state s A"
{ assume "final s"
from this obtain e \ where s: "s = (SRet e, \, [])"
by (case_tac s, case_tac a, auto, case_tac c, auto)
from wts s obtain \ where wte: "\ \\<^isub>e e : A" and wtg: "\ \ \" by auto
from wte wtg obtain v where ev: "eval e \ = Some v" and wtv: "wt_val v A"
using eval_safe by blast
from s ev wtv have "\r. steps (Suc n) s = r \ wt_result r A"
by (case_tac v, auto, case_tac const, auto)
} moreover { assume fs: "\ final s"
from fs wts obtain s' where st: "step s = Some s'"
and wtsp: "wt_state s' A" using step_safe by blast
from wtsp IH have ssp:
"steps n s' = TimeOut \ (\r. steps n s' = r \ wt_result r A)" by blast
from ssp fs st have ss: "steps (Suc n) s = steps n s'"
by (auto,case_tac a,auto,case_tac b,auto)+
from ssp ss have "steps (Suc n) s = TimeOut \
(\r. steps (Suc n) s = r \ wt_result r A)" by simp
} ultimately show "steps (Suc n) s = TimeOut \
(\r. steps (Suc n) s = r \ wt_result r A)" by blast
qed
theorem type_safety:
assumes wts: "[] \\<^isub>s s : A"
shows "\ r. run s = r \ (r = TimeOut \ wt_result r A)"
proof -
from wts have 1: "wt_state (s,[],[]) A" by auto
let ?n = "1000000" and ?s = "(s,[],[])"
from 1 have 2:
"steps ?n ?s = TimeOut \ (\ r. steps ?n ?s = r \ wt_result r A)"
by (rule steps_safe)
moreover { assume "steps ?n ?s = TimeOut"
with 2 have "\ r. run s = r \ (r = TimeOut \ wt_result r A)"
by (auto simp: run_def)
} moreover { assume 3: "\ r. steps ?n ?s = r \ wt_result r A"
from 3 obtain r where 4: "steps ?n ?s = r" and 5: "wt_result r A" by blast
from 4 have 6: "run s = r" by (simp add: run_def)
from 6 5 have "\ r. run s = r \ (r = TimeOut \ wt_result r A)" by blast
} ultimately show ?thesis by blast
qed
end