Theory Execute
theory Execute
imports secTypes
begin
section ‹Executing the small step semantics›
code_pred (modes: i => o => bool as exec_red, i => i * o => bool, i => o * i => bool, i => i => bool) red .
thm red.equation
definition [code]: "one_step x = Predicate.the (exec_red x)"
lemmas [code_pred_intro] = typeVal[where lev = Low] typeVal[where lev = High]
typeVar
typeBinOp1 typeBinOp2[where lev = Low] typeBinOp2[where lev = High] typeBinOp3[where lev = Low]
code_pred (modes: i => i => o => bool as compute_secExprTyping,
i => i => i => bool as check_secExprTyping) secExprTyping
proof -
case secExprTyping
from secExprTyping.prems show thesis
proof
fix Γ V lev assume "x = Γ" "xa = Val V" "xb = lev"
from secExprTyping(1-2) this show thesis by (cases lev) auto
next
fix Γ Vn lev
assume "x = Γ" "xa = Var Vn" "xb = lev" "Γ Vn = Some lev"
from secExprTyping(3) this show thesis by (auto simp add: Predicate.eq_is_eq)
next
fix Γ e1 e2 bop
assume "x = Γ" "xa = e1«bop» e2" "xb = Low"
"Γ ⊢ e1 : Low" "Γ ⊢ e2 : Low"
from secExprTyping(4) this show thesis by auto
next
fix Γ e1 e2 lev bop
assume "x = Γ" "xa = e1«bop» e2" "xb = High"
"Γ ⊢ e1 : High" "Γ ⊢ e2 : lev"
from secExprTyping(5-6) this show thesis by (cases lev) (auto)
next
fix Γ e1 e2 lev bop
assume "x = Γ" "xa = e1«bop» e2" "xb = High"
"Γ ⊢ e1 : lev" "Γ ⊢ e2 : High"
from secExprTyping(6-7) this show thesis by (cases lev) (auto)
qed
qed
lemmas [code_pred_intro] = typeSkip[where T=Low] typeSkip[where T=High]
typeAssH[where T = Low] typeAssH[where T=High]
typeAssL typeSeq typeWhile typeIf typeConvert
code_pred (modes: i => o => i => bool as compute_secComTyping,
i => i => i => bool as check_secComTyping) secComTyping
proof -
case secComTyping
from secComTyping.prems show thesis
proof
fix Γ T assume "x = Γ" "xa = T" "xb = Skip"
from secComTyping(1-2) this show thesis by (cases T) auto
next
fix Γ V T e assume "x = Γ" "xa = T" "xb = V:=e" "Γ V = Some High"
from secComTyping(3-4) this show thesis by (cases T) (auto)
next
fix Γ e V
assume "x = Γ" "xa = Low" "xb = V:=e" "Γ ⊢ e : Low" "Γ V = Some Low"
from secComTyping(5) this show thesis by auto
next
fix Γ T c1 c2
assume "x = Γ" "xa = T" "xb = Seq c1 c2" "Γ,T ⊢ c1" "Γ,T ⊢ c2"
from secComTyping(6) this show thesis by auto
next
fix Γ b T c
assume "x = Γ" "xa = T" "xb = while (b) c" "Γ ⊢ b : T" "Γ,T ⊢ c"
from secComTyping(7) this show thesis by auto
next
fix Γ b T c1 c2
assume "x = Γ" "xa = T" "xb = if (b) c1 else c2" "Γ ⊢ b : T" "Γ,T ⊢ c1" "Γ,T ⊢ c2"
from secComTyping(8) this show thesis by blast
next
fix Γ c
assume "x = Γ" "xa = Low" "xb = c" "Γ,High ⊢ c"
from secComTyping(9) this show thesis by blast
qed
qed
thm secComTyping.equation
subsection ‹An example taken from Volpano, Smith, Irvine›
definition "com = if (Var ''x'' «Eq» Val (Intg 1)) (''y'' := Val (Intg 1)) else (''y'' := Val (Intg 0))"
definition "Env = map_of [(''x'', High), (''y'', High)]"
values "{T. Env ⊢ (Var ''x'' «Eq» Val (Intg 1)): T}"
value "Env, High ⊢ com"
value "Env, Low ⊢ com"
values 1 "{T. Env, T ⊢ com}"
definition "Env' = map_of [(''x'', Low), (''y'', High)]"
value "Env', Low ⊢ com"
value "Env', High ⊢ com"
values 1 "{T. Env, T ⊢ com}"
end