Homework 5

Definitions File

theory Defs imports "HOL-IMP.AExp" "HOL-IMP.BExp" begin



end

Template File

theory Submission imports Defs begin

datatype
com = Skip                    ("SKIP")
    | Assign 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)
    | Break                   ("BREAK")

inductive
  big_step :: "com \<times> state \<Rightarrow> bool \<times> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)

declare big_step.intros [intro]

lemmas big_step_induct = big_step.induct[split_format(complete)]
  sorry

inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
inductive_cases BreakE[elim!]: "(BREAK,s) \<Rightarrow> t"
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"

lemma assign_simp:
  "(x ::= a,s) \<Rightarrow> (brk,s') \<longleftrightarrow> (s' = s(x := aval a s) \<and> \<not>brk)"
  by auto

fun break_ok :: "com \<Rightarrow> bool" where
  "break_ok _ = undefined"

theorem ok_brk: "\<lbrakk>(c, s) \<Rightarrow> (brk, t); break_ok c\<rbrakk> \<Longrightarrow> \<not>brk"
  sorry

fun elim :: "com \<Rightarrow> com" where
  "elim _ = undefined"

abbreviation equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
  "c \<sim> c' \<equiv> (\<forall>s t. (c, s) \<Rightarrow> t  =  (c', s) \<Rightarrow> t)"

theorem elim_complete: "(c, s) \<Rightarrow> (b, s') \<Longrightarrow> (elim c, s) \<Rightarrow> (b, s')"
  sorry

theorem elim_sound: "(elim c, s) \<Rightarrow> (b, s') \<Longrightarrow> (c, s) \<Rightarrow> (b, s')"
  sorry

lemma "elim c \<sim> c"
  using elim_sound elim_complete by fast

fun exec :: "com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> (bool \<times> state) option" where where
  "exec _ = undefined"

value "(case (
    exec (
      WHILE (Bc True) DO
      IF (Less (V ''x'') (N 4))
        THEN ''x''::= (Plus (V ''x'') (N 1))
         ELSE BREAK
    ) <> 10
  ) of (Some (False, s)) \<Rightarrow>
    s ''x''
  ) = 4"

theorem exec_imp_bigstep: "exec c s f = Some s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
  sorry

theorem exec_add: "exec c s f = Some s' \<Longrightarrow> exec c s (f + k) = Some s'"
  sorry

lemma exec_mono: "exec c s f = Some (brk, s') \<Longrightarrow> f' \<ge> f \<Longrightarrow> exec c s f' = Some (brk, s')"
  by (auto simp: exec_add dest: le_Suc_ex)

theorem bigstep_imp_si:
  "(c,s) \<Rightarrow> (brk, s') \<Longrightarrow> \<exists>k. exec c s k = Some (brk, s')"
proof (induct rule: big_step_induct)
  case (Skip s) have "exec SKIP s 1 = Some (False, s)" by auto
  thus ?case by blast
next
  case (WhileTrue b s1 c s2 brk3 s3)
  then obtain f1 f2 where "exec c s1 f1 = Some (False, s2)"
    and "exec (WHILE b DO c) s2 f2 = Some (brk3, s3)" by auto
  with exec_mono[of c s1 f1 False s2 "max f1 f2"]
    exec_mono[of "WHILE b DO c" s2 f2 brk3 s3 "max f1 f2"] have
    "exec c s1 (max f1 f2) = Some (False, s2)"
    and "exec (WHILE b DO c) s2 (max f1 f2) = Some (brk3, s3)"
    by auto
  hence "exec (WHILE b DO c) s1 (Suc (max f1 f2)) = Some (brk3, s3)"
    using \<open>bval b s1\<close> by (auto simp add: add_ac)
  thus ?case by blast
next
  case (IfTrue b s c1 brk' t c2)
  then obtain k where "exec c1 s k = Some (brk', t)" by blast
  hence "exec (IF b THEN c1 ELSE c2) s k = Some (brk', t)"
  using \<open>bval b s\<close> by (cases k) auto
  thus ?case by blast
next
  sorry

lemma "(\<exists>k. exec c s k = Some (brk, s')) \<longleftrightarrow> (c,s) \<Rightarrow> (brk, s')"
  by (metis exec_imp_bigstep bigstep_imp_si)

end

Check File

theory Check imports Submission begin

theorem ok_brk: "\<lbrakk>(c, s) \<Rightarrow> (brk, t); break_ok c\<rbrakk> \<Longrightarrow> \<not>brk"
  by (rule Submission.ok_brk)

theorem elim_complete: "(c, s) \<Rightarrow> (b, s') \<Longrightarrow> (elim c, s) \<Rightarrow> (b, s')"
  by (rule Submission.elim_complete)

theorem elim_sound: "(elim c, s) \<Rightarrow> (b, s') \<Longrightarrow> (c, s) \<Rightarrow> (b, s')"
  by (rule Submission.elim_sound)

theorem exec_imp_bigstep: "exec c s f = Some s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
  by (rule Submission.exec_imp_bigstep)

theorem exec_add: "exec c s f = Some s' \<Longrightarrow> exec c s (f + k) = Some s'"
  by (rule Submission.exec_add)

theorem bigstep_imp_si:
  "(c,s) \<Rightarrow> (brk, s') \<Longrightarrow> \<exists>k. exec c s k = Some (brk, s')"
  by (rule Submission.bigstep_imp_si)

end