Homework 8

Definitions File

theory Defs
  imports "HOL-IMP.AExp"
begin

definition "is_false (x :: int) \<equiv> x = 0"
definition "is_true (x :: int) \<equiv> \<not>(is_false x)"

lemma is_false_iff_eq_zero [iff]: "is_false x \<longleftrightarrow> x = 0" unfolding is_false_def by simp
lemma is_true_iff_neq_zero [iff]: "is_true x \<longleftrightarrow> x \<noteq> 0" unfolding is_true_def by simp

datatype com = SKIP
  | Assign vname aexp                ("_ ::= _" [1000, 61] 61)
  | Seq    com  com                  ("_;;/ _"  [60, 61] 60)
  | While  aexp com                  ("(WHILE _/ DO _)"  [0, 61] 61)
  | Switch aexp "(aexp * com) list"  ("(SWITCH _/ CASES _)"  [0, 61] 61)

inductive big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55) where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk>(c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3\<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
WhileFalse: "is_false (aval a s) \<Longrightarrow> (WHILE a DO c,s) \<Rightarrow> s" |
WhileTrue: "\<lbrakk>is_true (aval a s\<^sub>1); (c,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (WHILE a DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3\<rbrakk> \<Longrightarrow> (WHILE a DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
SwitchEmpty: "(SWITCH x CASES [],s) \<Rightarrow> s" |
SwitchTrue: "aval a1 s = aval a2 s \<Longrightarrow> (c,s) \<Rightarrow> s' \<Longrightarrow> (SWITCH a1 CASES ((a2,c)#acs), s) \<Rightarrow> s'" |
SwitchFalse: "(SWITCH a1 CASES acs,s) \<Rightarrow> s' \<Longrightarrow> (SWITCH a1 CASES ((a2,c)#acs), s) \<Rightarrow> s'"

code_pred big_step .
declare big_step.intros[intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]

inductive_cases sSkipE[elim!]: "(SKIP,s) \<Rightarrow> s'"
inductive_cases sAssignE[elim!]: "(x ::= a,s) \<Rightarrow> s'"
inductive_cases sSeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
inductive_cases sWhileE[elim]: "(WHILE a DO c, s) \<Rightarrow> s'"
inductive_cases sSwitch_nilE[elim!]: "(SWITCH a1 CASES [], s) \<Rightarrow> s'"
inductive_cases sSwitch_consE[elim!]: "(SWITCH a1 CASES ((a2, c)#acs), s) \<Rightarrow> s'"
declare [[coercion_enabled]] 
declare [[coercion "int :: nat \<Rightarrow> int"]]


type_synonym com_den = "(state \<times> state) set"

definition W :: "(state \<Rightarrow> bool) \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
"W db dc = (\<lambda>dw. {(s,t). if db s then (s,t) \<in> dc O dw else s=t})"

lemma W_mono: "mono (W b r)"
  by (unfold W_def mono_def) auto

abbreviation Big_step :: "com \<Rightarrow> com_den" where
"Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}"


consts D :: "com \<Rightarrow> com_den"


end

Template File

theory Submission
  imports Defs
begin

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

lemma D_if_big_step: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> D(c)"
  sorry

lemma Big_step_if_D: "(s,t) \<in> D(c) \<Longrightarrow> (s,t) \<in> Big_step c"
  sorry

theorem denotational_is_big_step:
  "(s,t) \<in> D(c)  =  ((c,s) \<Rightarrow> t)"
by (blast intro: D_if_big_step Big_step_if_D[simplified])

end

Check File

theory Check
  imports Submission
begin

lemma D_if_big_step: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> D(c)"
  by (rule Submission.D_if_big_step)

lemma Big_step_if_D: "(s,t) \<in> D(c) \<Longrightarrow> (s,t) \<in> Big_step c"
  by (rule Submission.Big_step_if_D)

end