Theory Execute

(*  Author:     Lukas Bulwahn, TU Muenchen, 2009  *)

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