theory examAnnotatedProg
imports Main
begin

section "Question 2: Induction"

type_synonym vname = string
type_synonym val = int
type_synonym state = "vname \<Rightarrow> val"

datatype aexp = N int | V vname | Plus aexp aexp
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"

fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (\<not> bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"

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)
      | While  bexp bexp com    ("(WHILE _/ _ DO _)"  [0, 61] 61)

      
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)" |

While:   "bval I s \<Longrightarrow> (WHILE b I DO c,s) \<rightarrow>
            (IF b THEN c;; WHILE b I DO c ELSE SKIP,s)"


inductive_cases
  skip [elim!]:   "(SKIP, s) \<rightarrow> s'" and
  assign [elim!]: "(x ::= a, s) \<rightarrow> s'" and
  seq [elim!]:    "(c\<^sub>1;; c\<^sub>2, s) \<rightarrow> s'" and
  ite [elim!]:    "(IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<rightarrow> s'" and
  while:          "(WHILE b I DO c, s) \<rightarrow> s'"


text {*
(a) Define merge:: "com \<Rightarrow> com \<Rightarrow> com option" 
*}

  (*TODO*)


(*HINT:
  Check that your definition is correct with the lemmas below.

  If any of the below lemmas cannot be proved, it means your definition
  has a problem. If you want to keep going, you can assume the definition
  of merge by doing:
     consts merge:: "com \<Rightarrow> com \<Rightarrow> com option"
  and then sorry all the lemmas (and (b)), to be able to do question (c).
  You won't get any points for (a) or (b) but can give the other questions
  a try.
  *)

lemma mergeSKIPI:
  "merge SKIP SKIP = Some SKIP"
  by auto

lemma mergeAssignI:
  "merge (v::=e) (v::=e) = Some (v::=e)"
  by auto

lemma mergeSeqI:
  "\<lbrakk>merge c1 c1' = Some c1''; merge c2 c2' = Some c2''\<rbrakk> \<Longrightarrow>
    merge (c1;;c2) (c1';;c2') = Some (c1'';;c2'')"
  by auto

lemma mergeIteI:
  "\<lbrakk>merge c1 c1' = Some c1''; merge c2 c2' = Some c2''\<rbrakk> \<Longrightarrow>
    merge (IF b THEN c1 ELSE c2) (IF b THEN c1' ELSE c2') = Some (IF b THEN c1'' ELSE c2'')"
  by auto

lemma mergeWhileI:
  "merge c c' = Some c'' \<Longrightarrow>
    merge (WHILE b I DO c) (WHILE b I' DO c') = Some (WHILE b (And I I') DO c'')"
  by auto
  
 
  
text {* 
(b) Prove the mergeD lemma below.
*}


lemma mergeD:
  "merge c c' = Some c'' \<Longrightarrow>
  (c=SKIP \<and> c'=SKIP \<and> c'' = SKIP) \<or>
  (\<exists>v e. c=(v::=e) \<and> c'=(v::=e) \<and> c''=(v::=e)) \<or>
  (\<exists>c1 c2 c1' c2' c1'' c2''. 
       c=c1;;c2 \<and> c'=c1';;c2' \<and> c''=c1'';;c2'' \<and>
       merge c1 c1' = Some c1'' \<and> merge c2 c2' = Some c2'')\<or>
  (\<exists>b c1 c2 c1' c2' c1'' c2''. 
       c=IF b THEN c1 ELSE c2 \<and> 
       c'=IF b THEN c1' ELSE c2' \<and> 
       c''=IF b THEN c1'' ELSE c2'' \<and>
       merge c1 c1' = Some c1'' \<and> merge c2 c2' = Some c2'')\<or>
  (\<exists>b I c0 I' c0' c0''. 
       c = WHILE b I DO c0 \<and>
       c'= WHILE b I' DO c0' \<and>
       c''= WHILE b (And I I') DO c0'' \<and>
       merge c0 c0' = Some c0'')"     
  (* TODO *)
  oops
  
(* HINT: you might find it useful for (b) and/or (c) to split 
         the goal and/or assumptions using split rules such 
         as if_splits or option.splits, as shown in week04B_demo.
*)
  
text {*
(c) Prove the following lemma.
*}

   
lemma merge_small_step:
  "merge c c' = Some c'' \<Longrightarrow>
    (c,s) \<rightarrow> (d,t) \<Longrightarrow>
    (c',s) \<rightarrow> (d',t') \<Longrightarrow>
    (\<exists>d''. (merge d d'=Some d'' \<and> (c'',s) \<rightarrow> (d'',t))) " 
  (* TODO *)
  oops
  
text {*
(d) Prove the following lemma
*}
 
lemma merge_small_step_state:
  "(c,s) \<rightarrow> (d,t) \<Longrightarrow>
   (c',s) \<rightarrow> (d',t') \<Longrightarrow>
   merge c c' \<noteq> None \<Longrightarrow> t=t' "   
  (*TODO*)
  oops


text {*   
(e) Assuming the  @{text merge_small_step'} lemma,
    prove the @{text merge_small_step_iff} lemma.
*}

axiomatization where
 merge_small_step':
  "merge c c' = Some c'' \<Longrightarrow>
    (\<exists>d''. (merge d d'=Some d'' \<and> (c'',s) \<rightarrow> (d'',t))) \<Longrightarrow>
    ((c,s) \<rightarrow> (d,t) \<and>
    (c',s) \<rightarrow> (d',t))"    
  
lemma merge_small_step_iff:
  "merge c c' = Some c'' \<Longrightarrow>
    ((c,s) \<rightarrow> (d,t) \<and>
    (c',s) \<rightarrow> (d',t')) =
    ((\<exists>d''. (merge d d'=Some d'' \<and> (c'',s) \<rightarrow> (d'',t))) \<and> t=t')"
  (*TODO*)
  oops


(* Don't forget to answer Question 1 and Question 3 in exam.thy *)

end