theory a2
imports Main
begin

(*-------------------------------------------------------------*)
(* INTRODUCTION *)


(* The IMP language *)
(* ~~~~~~~~~~~~~~~~ *)

type_synonym  vname   = string
type_synonym  state = "vname \<Rightarrow> nat"
type_synonym  aexp  = "state \<Rightarrow> nat"
type_synonym  bexp  = "state \<Rightarrow> bool"

datatype
  com = SKIP
      | Assign vname aexp       ("_ :== _ " [60,60] 60)
      | Semi   com com          ("_;; _"  [50, 51] 50)
      | Cond   bexp com com     ("IF _ THEN _ ELSE _ FI"  [0,0,59] 60)
      | While  bexp com         ("WHILE _ DO _ OD"  [0,45] 60)

(* IMP semantics *)
(* ~~~~~~~~~~~~~ *)

inductive
  eval :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_/ \<Rightarrow> _" [60,60] 61)
where
  Skip [intro!,simp]:
  "(SKIP, s) \<Rightarrow> s"
|
  Assign [intro!,simp]:
  "(x :== a, s) \<Rightarrow> s (x := a s)"
|
  Semi [intro!]:
  "\<lbrakk> (c\<^sub>1,s) \<Rightarrow> s''; (c\<^sub>2,s'') \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (c\<^sub>1;; c\<^sub>2, s) \<Rightarrow> s'"
|
  IfTrue[intro]:
  "\<lbrakk> b s; (c\<^sub>1,s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2 FI, s) \<Rightarrow> s'"
|
  IfFalse[intro]:
  "\<lbrakk> \<not>b s; (c\<^sub>2,s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2 FI, s) \<Rightarrow> s'"
|
  WhileFalse[intro]:
  "\<not>b s \<Longrightarrow> (WHILE b DO c OD, s) \<Rightarrow> s"
|
  WhileTrue[intro]:
  "\<lbrakk>b s; (c,s) \<Rightarrow> s''; (WHILE b DO c OD, s'') \<Rightarrow> s'\<rbrakk> \<Longrightarrow> (WHILE b DO c OD, s) \<Rightarrow> s'"


(* The default induction rule only allows eval to
   have 2 parameters. We define a new induction rule eval_induct
   where we split the first tuple to get the 3 parameters c, s and s'*)

thm eval.induct
lemmas eval_induct = eval.induct[split_format(complete)]
thm eval_induct

(* We want to deduce from "(SKIP,s) \<Rightarrow> t" that "s = t".
   We want to deduce from "(x:==a,s) \<Rightarrow> t" that "t =  s(x := a s)".
   Etc.
   We do this with the following *)

inductive_cases
  skip [elim!]:   "(SKIP, s) \<Rightarrow> s'" and
  assign [elim!]: "(x :== a, s) \<Rightarrow> s'" and
  semi [elim!]:   "(c\<^sub>1;; c\<^sub>2, s) \<Rightarrow> s'" and
  "if" [elim!]:   "(IF b THEN c\<^sub>1 ELSE c\<^sub>2 FI, s) \<Rightarrow> s'" and
  while:          "(WHILE b DO c OD, s) \<Rightarrow> s'"

lemma skip_eq [simp]: "(SKIP, s) \<Rightarrow> s' = (s' = s)" by blast
lemma assign_eq [simp]: "(x :== a, s) \<Rightarrow> s' = (s' = s (x := a s))"  by blast

(* EXAMPLE PROGRAMS *)
(* ~~~~~~~~~~~~~~~~ *)

definition max :: com where
  "max \<equiv>
    (IF (\<lambda>s. s ''A'' > s ''B'')
     THEN ''R'' :== (\<lambda>s. s ''A'')
     ELSE ''R'' :== (\<lambda>s. s ''B'')
     FI)"

definition factorial :: com where
  "factorial \<equiv>
     ''B'' :== (\<lambda>s. 1);;
     WHILE (\<lambda>s. s ''A'' \<noteq> 0) DO
       ''B'' :== (\<lambda>s. s ''B'' * s ''A'');;
       ''A'' :== (\<lambda>s. s ''A'' - 1)
     OD"


(*---------------------------------------------------------*)
(* QUESTION 1:  Variable Assignment (10 marks) *)

(* (a) Define var_assig :: "com \<Rightarrow> vname set" (7 marks)*)

(* TODO *)

lemma assig_max: "var_assig max = {''R''}" by eval
lemma assig_factorial: "var_assig factorial = {''A'',''B''}" by eval



(* (b) Prove the following lemma (3 marks)*)

lemma eval_assig: "\<lbrakk> (c, s) \<Rightarrow> t; x \<notin> var_assig c \<rbrakk> \<Longrightarrow> s x = t x"
(* TODO *)
sorry





(*---------------------------------------------------------*)
(* QUESTION 2:  Equivalent programs (12 marks) *)

(* Definition of equivalent programs *)
definition
  equival :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
  "c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"

(* (a) Prove that  \<sim> is an equivalence relation (3 marks)*)
lemma equival_refl: "c\<sim>c"
(*TODO*)
sorry

lemma equival_sym: "(c\<sim>c')=(c'\<sim>c)"
(*TODO*)
sorry

lemma equival_trans: "\<lbrakk>x\<sim>y; y\<sim>z\<rbrakk>\<Longrightarrow> x\<sim>z"
(*TODO*)
sorry


(* (b) Prove the following lemma (2 marks) *)
lemma equival_semi: "\<lbrakk>c\<sim>c'; d\<sim>d'\<rbrakk>\<Longrightarrow> (c;;d)\<sim>(c';;d')"
(*TODO*)
sorry


(* (c) Prove the following lemma (2 marks) *)
lemma equival_if:
  "\<lbrakk>c\<sim>c'; d\<sim>d'\<rbrakk> \<Longrightarrow>
  IF b THEN c ELSE d FI\<sim> IF b THEN c' ELSE d' FI"
(*TODO*)
sorry

(* (d) Prove the following lemma (2 marks) *)
lemma equival_while_aux:
  "\<lbrakk>(p,s) \<Rightarrow> t; p=WHILE b DO c OD; c \<sim> c'\<rbrakk> \<Longrightarrow>
    (WHILE b DO c' OD,s) \<Rightarrow> t"
(*TODO*)
sorry

(* (e) Prove the following lemma (2 marks) *)
lemma equival_while:
  "c\<sim>c'\<Longrightarrow> WHILE b DO c OD \<sim> WHILE b DO c' OD"
  (*TODO*)
sorry



(*---------------------------------------------------------*)
(* QUESTION 3: The SKIP command (30 marks) *)

primrec equivtoskip :: "com \<Rightarrow> bool" where
"equivtoskip SKIP = True" |
"equivtoskip (x:==a) = False" |
"equivtoskip (c1;;c2) = (equivtoskip c1 \<and> equivtoskip c2)" |
"equivtoskip (IF b THEN c1 ELSE c2 FI) = (equivtoskip c1 \<and> equivtoskip c2)" |
"equivtoskip (WHILE b DO c OD) = False"

(* (a) Prove equivtoskip is correct (5 marks) *)

lemma equivtoskip_correct: "equivtoskip c \<Longrightarrow> c \<sim> SKIP"
  (*TODO*)
  sorry

(* (b) Find some program that behaves like SKIP but for 
       which equivtoskip returns False (5 marks) *)

lemma not_equivtoskip: "\<exists>c. c \<sim> SKIP \<and> \<not> equivtoskip c"
  (*TODO*)
sorry

(* (c) Define less_skip :: "com \<Rightarrow> com" (5 marks) *)

(*TODO*)
lemma less_skip1:
  "less_skip
     ((SKIP;;SKIP);; WHILE b DO (x :== a;; SKIP) OD)
 = WHILE b DO x :== a OD"
  (*TODO*)
  sorry

lemma less_skip2:
  "less_skip (IF b THEN (SKIP;;SKIP) ELSE (x :== a;; SKIP) FI) =
              (IF b THEN SKIP ELSE x :== a FI)"
  (*TODO*)
  sorry

lemma less_skip3:
  "less_skip (IF b THEN (SKIP;;SKIP) ELSE SKIP FI) = SKIP"
  (*TODO*)
  sorry

lemma less_skip4:
  "less_skip (WHILE b DO (SKIP;;SKIP) OD) = (WHILE b DO SKIP OD)"
  (*TODO*)
  sorry

(* (d) Prove less_skip is correct (15 marks) *)
lemma less_skip_correct: "less_skip c \<sim> c"
  (*TODO *)
  sorry



(*---------------------------------------------------------*)
(* QUESTION 4: Sequencing associativity (36 marks)*)

(* Tree structure *)
datatype tag = S | A vname aexp | C bexp | W bexp
datatype tree = Node tag "tree list" | Branch tree tree

(* Function from command to tree *)
fun com_to_tree where
  "com_to_tree SKIP = Node S []"
| "com_to_tree (Assign v a) = Node (A v a) []"
| "com_to_tree (Semi c1 c2) = Branch (com_to_tree c1) (com_to_tree c2)"
| "com_to_tree (Cond b c1 c2) = Node (C b) [com_to_tree c1, com_to_tree c2]"
| "com_to_tree (While b c) = Node (W b) [com_to_tree c]"

(* (a) Define function from tree to command:
       tree_to_com :: "tree \<Rightarrow> com"  (3 marks) *)

(* TODO *)

(* (b) Proof the following lemma (2 marks) *)

lemma com_to_tree_inverse:
  "tree_to_com (com_to_tree c) = c"
(* TODO *)
sorry

(* (c) Define wf_tree:: "tree \<Rightarrow> bool" and prove
       the following lemma (6 marks)*)

lemma tree_to_com_inverse[simp]:
  "wf_tree t \<Longrightarrow> com_to_tree (tree_to_com t) = t"
  (*TODO*)
  sorry

(* (d) Define Branch_assoc and prove its termination (10 marks) *)

  function Branch_assoc where
  "Branch_assoc (Branch (Branch t1 t2) t3) =
     Branch_assoc (Branch t1 (Branch t2 t3))"
|
  "Branch_assoc (Branch (Node t ls) t3) =
     Branch (Node t (map Branch_assoc ls)) (Branch_assoc t3)"
|
  "Branch_assoc (Node t ls) =
     Node t (map Branch_assoc ls)"
  (*TODO*)
  sorry

termination Branch_assoc
  apply (relation "inv_image (less_than <*lex*> less_than) (\<lambda>t. (size\<^sub>1 t, size\<^sub>2 t))")
 (*TODO*)
 sorry

(* (e) We first define map_Semi: *)
fun map_Semi where
  "map_Semi f (Semi c1 c2) = f (map_Semi f c1) (map_Semi f c2)"
| "map_Semi f (Cond b c1 c2) = Cond b (map_Semi f c1) (map_Semi f c2)"
| "map_Semi f (While b c) = While b (map_Semi f c)"
| "map_Semi f x = x"

  (* Now define Semi_assoc1:: "com \<Rightarrow> com \<Rightarrow> com"  such
     that you can prove Branch_assoc_map (10 marks) *)

fun Semi_assoc1 where (* TODO *)

lemma Branch_assoc_map:
  "wf_tree t \<Longrightarrow> tree_to_com (Branch_assoc t) = map_Semi Semi_assoc1 (tree_to_com t)"
 (*TODO*)
 sorry


 (* (f) Prove that the transformation preserves the semantics (5 marks) *)

 theorem Branch_assoc_eval:
 "(c,s) \<Rightarrow> s' \<Longrightarrow> (tree_to_com (Branch_assoc (com_to_tree c)),s) \<Rightarrow> s'"
  (*TODO*)
  sorry



(*---------------------------------------------------------*)
section \<open> Compilation (12 marks) \<close>


(* LAB language *)
(* ~~~~~~~~~~~~ *)

type_synonym  label   = nat

datatype lcom =
        LAssign vname aexp
      | Label   label
      | LCGoto  bexp label
      | LGoto   label

type_synonym lprog =  "lcom list"

(* EXAMPLES *)
(* ~~~~~~~~ *)


definition
  lmax :: lprog where
  "lmax \<equiv>   [
               LCGoto (\<lambda>s. s ''A'' \<le> s ''B'') 0,
               LAssign ''R'' (\<lambda>s. s ''A''),
               LGoto 1,
               Label 0,
               LAssign ''R'' (\<lambda>s. s ''B''),
               Label 1]"

definition
  lfactorial :: lprog where
  "lfactorial \<equiv> [ LAssign ''B'' (\<lambda>s. 1),
                  Label 1,
                  LCGoto (\<lambda>s. s ''A'' = 0) 0,
                  LAssign ''B'' (\<lambda>s. s ''B'' * s ''A''),
                  LAssign ''A'' (\<lambda>s. s ''A'' - 1),
                  LGoto 1,
                  Label 0]"

(* Define compile::"com \<Rightarrow> lprog" such that you can prove
   compile_max and compile_factorial. You may need a helper
   function compile' :: "com \<Rightarrow> label\<Rightarrow> lprog \<times> label" *)


lemma compile_max: "compile max =lmax"
  (*TODO*)
  sorry

lemma compile_factorial: "compile factorial =lfactorial"
  (*TODO*)
  sorry



end