theory a2
imports Main
begin


(**********************************************)
(* PART 1: "Compiling Arithmetic Expressions" *)
(**********************************************)


(* Syntax of the language *)
datatype expr = BinOp "(nat \<Rightarrow> nat \<Rightarrow> nat)" expr expr |
                UnOp "(nat \<Rightarrow> nat)" expr |
                Const nat

definition
  plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "plus \<equiv> (\<lambda>a b. a + b)"
  
lemma "plus = (op +)"
  by(simp add: plus_def)

(* Evaluation function *)
primrec
  eval :: "expr \<Rightarrow> nat"
where
  "eval (Const n) = n" |
  "eval (BinOp f a b) = f (eval a) (eval b)" |
  "eval (UnOp f a) = f (eval a)"

lemma "eval (BinOp (op +) (Const 2) (Const 3)) = 5"
  by simp
  
(* Programs for the stack machine *)
datatype stackp = Push nat |
                  DoUnOp "nat \<Rightarrow> nat" |
                  DoBinOp "nat \<Rightarrow> nat \<Rightarrow> nat" |
                  Seq stackp stackp ("_ ;; _")  |
                  Skip

type_synonym stack = "nat list"

(* Big step operational semantics to programs for the stack machine *)
inductive
  sem :: "stack \<Rightarrow> stackp \<Rightarrow> stack \<Rightarrow> bool" ("\<langle>_, _\<rangle> \<Down> _")
where
  sem_Push: "sem s (Push n) (n#s)" |
  sem_DoBinOp: "sem (a#b#s) (DoBinOp f) ((f a b)#s)" |
  sem_DoUnOp: "sem (a#s) (DoUnOp f) ((f a)#s)" |
  sem_Seq: "\<lbrakk>sem s a t; sem t b u\<rbrakk> \<Longrightarrow> sem s (Seq a b) u"

(* Simple compiler from expression to stack programs *)
primrec
  compile  :: "expr \<Rightarrow> stackp" 
where
  "compile (Const n) = Push n" |
  "compile (BinOp f a b) = Seq (compile b) (Seq (compile a) (DoBinOp f))" |
  "compile (UnOp f a) = Seq (compile a) (DoUnOp f)"

(* ---------- *)
(* Question 1 *)
(* ---------- *)

(* (a) Prove that the stack machine semantics is deterministic *)
lemma sem_det:
  "sem s e t \<Longrightarrow> sem s e u \<Longrightarrow> u = t"
  (***TODO***)
  oops

(* (b) Prove that the compiler is correct *)
lemma compile_correct:
  "sem s (compile e) ((eval e)#s)"
  (***TODO***)
  oops
  
(* (c) Prove that whether an expression can evaluate 
       depends only on the size of the initial stack *)
lemma sem_stack_content_agnostic:
  "sem s p t \<Longrightarrow> \<forall>s'. length s' = length s \<longrightarrow> (\<exists>t'. sem s' p t')"
  (***TODO***)
  oops
  
  
(* ---------- *)
(* Question 2 *)
(* ---------- *)

(* Sufficient initial stack size *)
definition
  reqd_init_stack :: "stackp \<Rightarrow> nat \<Rightarrow> bool"
where
  "reqd_init_stack p h \<equiv> (\<exists>s t. \<langle>s,p\<rangle> \<Down> t) \<longrightarrow> (\<forall>s. length s \<ge> h \<longrightarrow> (\<exists>t. \<langle>s,p\<rangle> \<Down> t))"

(* (a) Prove that compiled expressions require no initial stack *)
lemma compile_reqd_init_stack:
  "reqd_init_stack (compile e) 0"
  (***TODO***)
  oops

(* (b) Minimal initial stack length for atomic programs *)
lemma reqd_init_stack_Push:
  "reqd_init_stack (Push n) TODO"
  (***TODO***)
  oops

lemma reqd_init_stack_DoUnOp:
  "reqd_init_stack (DoUnOp f) TODO"
  (***TODO***)
  oops

lemma reqd_init_stack_DoBinOp:
  "reqd_init_stack (DoBinOp f) TODO"
  (***TODO***)
  oops
  
lemma reqd_init_stack_Skip:
  "reqd_init_stack Skip  TODO"
  (***TODO***)
  oops
  
(* (c) Minimal initial stack length for Seq *)
lemma reqd_init_stack_Seq:
  "\<lbrakk>(reqd_init_stack p1) n; (reqd_init_stack p2 m)\<rbrakk>
       \<Longrightarrow> (reqd_init_stack (Seq p1 p2) TODO)"
  (****TODO***)
  oops

(* (d) Define a function that given a program p 
       calculates an appropriate stack length h
       such that reqd_init_stack p h holds *)
(*     
primrec
  sufficient_init_stack :: "stackp \<Rightarrow> nat"
where
  ***TODO***
*)  

(* (e) Prove your function from (d) correct *)
lemma sufficient_init_stack_is_reqd_init_stack:
  "reqd_init_stack p (sufficient_init_stack p)"
  (***TODO***)
  oops



  
(* ---------- *)
(* Question 3 *)
(* ---------- *)

(*  Small-step semantics *)
inductive
  sems :: "stack \<Rightarrow> stackp \<Rightarrow> stack \<Rightarrow> stackp \<Rightarrow> bool"
where
  "sems s (Push n) (n#s) Skip" |
  "sems (a#b#s) (DoBinOp f) ((f a b)#s) Skip" |
  "sems (a#s) (DoUnOp f) ((f a)#s) Skip" |
  "sems s a s' a' \<Longrightarrow> sems s (Seq a b) s' (Seq a' b)" |
  "sems s (Seq Skip b) s b"


  
(* (a) Define a function semsn:: nat \<Rightarrow> stack \<Rightarrow> stackp \<Rightarrow> stack \<Rightarrow> stackp \<Rightarrow> bool
       that executes n steps of the small-step semantics *)

   
primrec
  semsn :: "nat \<Rightarrow> stack \<Rightarrow> stackp \<Rightarrow> stack \<Rightarrow> stackp \<Rightarrow> bool"
where
  "semsn 0 s a s' a' = TODO1" |
  "semsn (Suc n) s a s' a' = TODO2"

(* (b) Prove that if a program a executes in the big-step semantics to a 
       resulting stack t from an initial stack s, then it executes in the
       small-step semantics to the same resulting stack and the resulting
       program Skip. *)  
lemma semsn_correct:
  "sem s a t \<Longrightarrow> \<exists>n. semsn n s a t Skip"
  (***TODO***)
  oops

(* (c) Prove that there is no universal stack bound for any compiled program *)
(* Predicate stating that stack size h is a stack bound for program p *)
definition
  stack_bound :: "stackp \<Rightarrow> nat \<Rightarrow> bool"
where
  "stack_bound p h \<equiv> \<forall>s n s' p'. semsn n s p s' p' \<longrightarrow>  length s' - length s \<le> h"
  
primrec
  prog_using_Suc :: "nat \<Rightarrow> expr"
where
  "prog_using_Suc 0 = Const 0" |
  "prog_using_Suc (Suc n) = (BinOp (op +) (prog_using_Suc n) (Const 0))"
  
lemma compile_has_no_universal_stack_bound:
  "\<not> (\<exists>h. (\<forall>p. stack_bound (compile p) h))"
  oops
 

(****************************************)
(* PART 2: "Rewriting rules for groups" *)
(****************************************)
  

(* Replace A-H below by equation stating that e is left- and right-neutral,
   and that i is left- and right-inverse, for the \<star> operator.
  
   Justify why your set of rules is confluent and terminating.
   (why it is safe to add them to the simp set)
*)

axiomatization
  e:: 'a and
  op:: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<star>" 70)  and
  i:: "'a \<Rightarrow> 'a" 
where
  neutral_left[simp]: "A = B" and
  neutral_right[simp]: "C = D" and
  inverse_left[simp]: "E = F" and
  inverse_right[simp]: "G = H"
   
end