Exercise 2

Definitions File

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

datatype com = SKIP
  | Assign vname aexp          ("_ ::= _" [1000, 61] 61)
  | Seq    com  com            ("_;;/ _"  [60, 61] 60)
  | If     bexp com com        ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
  | Loop   nat com             ("(LOOP _/ DO _)"  [0, 61] 61)

end

Template File

theory Submission 
  imports Defs
begin

section \<open>IMP\<close>

text \<open>
Consider a modification of IMP (@{typ com}) with loops of the form "\<open>LOOP n DO c\<close>", where \<open>c\<close>
is an IMP program and \<open>n\<close> a natural number denoting the number of times the
program \<open>c\<close> should be executed.

Complete the big-step semantics for this language by providing the missing rules for the
loop constructor. Do not modify the pre-defined big-step rules!

\<close>

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" |
IfTrue: "\<lbrakk> bval b s;  (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |

declare big_step.intros [intro]
inductive_cases SkipE[elim!]: "(SKIP,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"

text \<open>
Now complete the small-step semantics by providing \<^emph>\<open>one single missing rule\<close> for the loop constructor.
Do not modify the pre-defined small-step rules and do not use more than one rule! Your new rule must:
  \<^item> be properly small-step; that is, do not re-use the big-step semantics, only do a single step, etc.
  \<^item> not use Isabelle/HOL case analyses. In particular, do not use
    "@{term "if b then x else y"}" and "\<open>case x of ...\<close>";
    but you may very well use the other IMP constructors.
\<close>

inductive small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) where
Assign:  "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
Seq1:    "(SKIP;;c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" |
Seq2:    "(c\<^sub>1,s) \<rightarrow> (c\<^sub>1',s') \<Longrightarrow> (c\<^sub>1;;c\<^sub>2,s) \<rightarrow> (c\<^sub>1';;c\<^sub>2,s')" |
IfTrue:  "bval b s \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>1,s)" |
IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" |

text \<open>
Next show the equivalence between your big-step and small-step semantics by filling out the missing
proof steps below.
\<close>

abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55) where
  "x \<rightarrow>* y == star small_step x y"

declare small_step.intros[simp,intro]

inductive_cases sSkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
inductive_cases sAssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
inductive_cases sSeqE[elim]: "(c1;;c2,s) \<rightarrow> ct"
inductive_cases sIfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"

lemma star_seq2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;;c2,s) \<rightarrow>* (c1';;c2,s')"
proof(induction rule: star_induct)
  case refl thus ?case by simp
next
  case step
  thus ?case by (metis Seq2 star.step)
qed

lemma seq_comp [intro]: "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk> \<Longrightarrow> (c1;;c2, s1) \<rightarrow>* (SKIP,s3)"
by (blast intro: star.step star_seq2 star_trans)

declare star.step[intro]

lemma big_to_small: "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
  sorry

lemma small1_big_continue: "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
  by (induction arbitrary: t rule: small_step.induct) auto

lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
  sorry

text \<open>And finally, prove that all programs terminate:\<close>

lemma terminates: "\<exists>t. (c, s) \<Rightarrow> t"
  sorry



end

Check File

theory Check imports Submission
begin

end