Homework 9.3

Definitions File

theory Defs imports "HOL-IMP.Big_Step" begin



end

Template File

theory Submission imports Defs begin

datatype event = Action string aexp | Test bexp

fun exec :: "state \<Rightarrow> event list \<Rightarrow> state option" where
"exec s [] = Some s" |
"exec s (Action x a # ts) = exec (s(x := aval a s)) ts" |
"exec s (Test b # ts) = (if bval b s then exec s ts else None)"

abbreviation "example \<equiv> [Action ''x'' (N 1), Test (Less (N 0) (V ''x''))]"
value "case (exec <> example) of Some t \<Rightarrow> t ''x''"

inductive trace :: "com \<Rightarrow> event list \<Rightarrow> bool"

abbreviation traces :: "com \<Rightarrow> event list set"

theorem big_traces: "(c,s) \<Rightarrow> t \<Longrightarrow> \<exists>ts \<in> traces c. exec s ts = Some t"
  sorry

theorem trace_big: "\<lbrakk>trace c ts; exec s ts = Some t\<rbrakk> \<Longrightarrow> (c,s) \<Rightarrow> t"
  sorry

lemma "(c,s) \<Rightarrow> t \<longleftrightarrow> (\<exists>ts \<in> traces c. exec s ts = Some t)"
  using big_traces trace_big by auto

end

Check File

theory Check imports Submission begin

theorem big_traces: "(c,s) \<Rightarrow> t \<Longrightarrow> \<exists>ts \<in> traces c. exec s ts = Some t"
  by (rule Submission.big_traces)

theorem trace_big: "\<lbrakk>trace c ts; exec s ts = Some t\<rbrakk> \<Longrightarrow> (c,s) \<Rightarrow> t"
  by (rule Submission.trace_big)

end