# Theory WhileLang

```section "The definition of the While language"

theory WhileLang imports MiscLemmas Coinductive.Coinductive_List begin

(* -- AST and other types -- *)

type_synonym name = "char list"
type_synonym val = nat
type_synonym store = "name ⇒ val"
type_synonym exp = "store ⇒ val"

datatype prog =
Skip
| Assign name exp
| Print exp
| Seq prog prog
| If exp prog prog
| While exp prog

(* -- small-step semantics -- *)

type_synonym out = "val list"
type_synonym state = "store × out"

definition output_of :: "state ⇒ out" where
"output_of ≡ λ(_, out). out"

definition subst :: "name ⇒ exp ⇒ state ⇒ state" where
"subst n e ≡ λ(s, out). (s(n:= e s), out)"

definition print :: "exp ⇒ state ⇒ state" where
"print e ≡ λ(s, out). (s,  out @ [e s])"

definition guard :: "exp ⇒ state ⇒ bool" where
"guard x ≡ λ(s, _). x s ≠ 0"

inductive step :: "prog × state ⇒ prog × state ⇒ bool" where
step_skip: "step (Skip,s) (Skip,s)"
| step_assign: "step (Assign n x,s) (Skip, subst n x s)"
| step_print: "step (Print x,s) (Skip, print x s)"
| step_seq1: "step (Seq Skip q,s) (q,s)"
| step_seq2: "step (p0,s0) (p1,s1) ⟹ p0 ≠ Skip ⟹ step (Seq p0 q,s0) (Seq p1 q,s1)"
| step_if: "step (If x p q, s) ((if guard x s then p else q), s)"
| step_while: "step (While x p, s) (If x (Seq p (While x p)) Skip, s)"

declare step.intros[simp,intro]

inductive_cases skipE[elim!]: "step (Skip, s) ct"
inductive_cases assignE[elim!]: "step (Assign n x, s) ct"
inductive_cases printE[elim!]: "step (Print x, s) ct"
inductive_cases seqE[elim]: "step (Seq c1 c2, s) ct"
inductive_cases ifE[elim!]: "step (If x c1 c2, s) ct"
inductive_cases whileE[elim]: "step (While x p, s) ct"

lemmas step_induct = step.induct[split_format(complete)]

inductive terminates where
"star step (p, s) (Skip, t) ⟹ terminates s p t"

inductive diverges where
"∀t. ¬ terminates s p t
∧ out = lSup { llist_of out | out. ∃q t. star step (p, s) (q, t, out) }
⟹
diverges s p out"

(* -- sanity theorems -- *)

lemma step_exists':
"∃t. step (prog, (s, out)) t"
proof (induct prog)
case Skip
then show ?case by fastforce
next
case (Assign x1 x2)
then show ?case
apply clarsimp
apply (rule_tac x=Skip in exI)
apply (rule_tac x="fst (subst x1 x2 (s, out))" in exI)
apply (rule_tac x="snd (subst x1 x2 (s, out))" in exI)
by fastforce
next
case (Print x)
then show ?case
apply clarsimp
apply (rule_tac x=Skip in exI)
apply (rule_tac x="fst (print x (s, out))" in exI)
apply (rule_tac x="snd (print x (s, out))" in exI)
by fastforce
next
case (Seq prog1 prog2)
then show ?case
apply (case_tac "prog1 = Skip")
by fastforce+
next
case (If x1 prog1 prog2)
then show ?case by fastforce
next
case (While x1 prog)
then show ?case by fastforce
qed

theorem step_exists: (* one can always take a step *)
"∀s. ∃t. step s t"
using step_exists' by simp

theorem terminates_or_diverges: (* every program either terminates or diverges *)
"(∃t. terminates s p t) ∨ (∃output. diverges s p output)"
by (clarsimp simp: diverges.simps)

lemma step_deterministic':
"step (prog, st, out) t1 ⟹ step (prog, st, out) t2 ⟹ t1 = t2"
proof (induct prog arbitrary: t1 t2)
case Skip
then show ?case by clarsimp
next
case (Assign x1 x2)
then show ?case by clarsimp
next
case (Print x)
then show ?case by clarsimp
next
case (Seq prog1 prog2)
then show ?case by (elim seqE; clarsimp)
next
case (If x1 prog1 prog2)
then show ?case by clarsimp
next
case (While x1 prog)
then show ?case by (elim whileE; clarsimp)
qed

theorem step_deterministic:
"step s t1 ⟹ step s t2 ⟹ t1 = t2"
apply (cases s)
using step_deterministic' by clarsimp

lemma star_step_refl:
"star step (Skip, t1) (Skip, t2) ⟹ t1 = t2"
by (induct "(Skip, t1)" "(Skip, t2)" arbitrary: t1 t2 rule: star.induct; clarsimp)

theorem terminates_deterministic:
"terminates s p t1 ⟹ terminates s p t2 ⟹ t1 = t2"
proof (simp add: terminates.simps, induct "(p, s)" "(Skip, t1)" arbitrary: p s t1 rule: star.induct)
case refl
then show ?case
by (clarsimp intro!: star_step_refl)
next
case (step y)
then show ?case
apply (rotate_tac 3)
apply (erule star.cases)
apply clarsimp
apply simp
apply (drule (1) step_deterministic)
apply simp
apply (drule_tac x="fst ya" and y="snd ya" in meta_spec2)
by simp
qed

theorem diverges_deterministic:
"diverges s p t1 ⟹ diverges s p t2 ⟹ t1 = t2"