Homework 5

Definitions File

theory Defs
  imports "HOL-IMP.Big_Step" "HOL-IMP.Star"
begin

declare[[syntax_ambiguity_warning=false]]

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 scom = sSKIP
  | sAssign vname aexp                ("_ ::= _" [1000, 61] 61)
  | sSeq    scom  scom                  ("_;;/ _"  [60, 61] 60)
  | sWhile  aexp scom                  ("(WHILE _/ DO _)"  [0, 61] 61)
  | sSwitch aexp "(aexp * scom) list"  ("(SWITCH _/ CASES _)"  [0, 61] 61)



consts sbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool"

consts scom_to_com :: "scom \<Rightarrow> com"

consts ssmall_step :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool"

consts ssmall_steps :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool"

consts nsbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

declare fun_upd_apply[simp del](* helpful for the automation here *)

inductive sbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>s" 55) 

fun scom_to_com :: "scom \<Rightarrow> com"  where
  "scom_to_com _ = SKIP"

lemma big_step_scom_to_com_if_big_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (scom_to_com c, s) \<Rightarrow> t"
  sorry

lemma sbig_step_if_big_step_scom_to_com: "(scom_to_com c, s) \<Rightarrow> t \<Longrightarrow> (c, s) \<Rightarrow>s t"
  sorry

corollary "(c, s) \<Rightarrow>s t \<longleftrightarrow> (scom_to_com c, s) \<Rightarrow> t" inductive ssmall_step :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool" (infix "\<rightarrow>s" 55)
  sorry

abbreviation ssmall_steps :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool" (infix "\<rightarrow>s*" 55)
  where "x \<rightarrow>s* y \<equiv> star ssmall_step x y"

lemma ssmall_steps_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<rightarrow>s* (sSKIP, t)"
  sorry

lemma sbig_step_if_ssmall_steps: "cs \<rightarrow>s* (sSKIP, t) \<Longrightarrow> cs \<Rightarrow>s t"
  sorry

corollary "(c, s) \<Rightarrow>s t \<longleftrightarrow> (c, s) \<rightarrow>s* (sSKIP, t)" inductive nsbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>ns" 55)
  sorry

lemma nsbig_step_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<Rightarrow>ns t"
  sorry

lemma conjecture_true: "(c, s) \<Rightarrow>ns t \<Longrightarrow> \<exists>t. (c, s) \<Rightarrow>ns t \<and> (c, s) \<Rightarrow>s t"
  sorry

lemma conjecture_false: "\<exists>c s t. (c, s) \<Rightarrow>ns t \<and> \<not>(\<exists>t. (c, s) \<Rightarrow>ns t \<and> (c, s) \<Rightarrow>s t)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma big_step_scom_to_com_if_big_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (scom_to_com c, s) \<Rightarrow> t"
  by (rule Submission.big_step_scom_to_com_if_big_step)

lemma sbig_step_if_big_step_scom_to_com: "(scom_to_com c, s) \<Rightarrow> t \<Longrightarrow> (c, s) \<Rightarrow>s t"
  by (rule Submission.sbig_step_if_big_step_scom_to_com)

lemma ssmall_steps_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<rightarrow>s* (sSKIP, t)"
  by (rule Submission.ssmall_steps_if_sbig_step)

lemma sbig_step_if_ssmall_steps: "cs \<rightarrow>s* (sSKIP, t) \<Longrightarrow> cs \<Rightarrow>s t"
  by (rule Submission.sbig_step_if_ssmall_steps)

lemma nsbig_step_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<Rightarrow>ns t"
  by (rule Submission.nsbig_step_if_sbig_step)

end