Mine

theory Hw03
imports Main AExp
begin

(* Hw 3.1 *)
datatype aexp' = N' int | V' vname | PI' vname | Plus' aexp' aexp'

fun aval' :: "aexp' ⇒ state ⇒ val × state" where
"aval' (N' n) s = (n, s)" |
"aval' (V' x ) s = (s x , s)" |
"aval' (PI' x ) s = (s x , s(x :=s x+1 ))" |
"aval' (Plus' a1 a2 ) s =
  (case aval' a1 s of (v1 , s') ⇒
    (case aval' a2 s' of (v2 , s'') ⇒ (v1 + v2 , s'')))"

abbreviation "hd2 xs == hd(tl xs)"
abbreviation "tl2 xs == tl(tl xs)"

datatype instr = LOADI val | LOAD vname | PILOAD vname | ADD
type_synonym stack = "val list"

fun exec1 :: "instr ⇒ (state × stack ) ⇒ (state × stack )" where
  "exec1 (LOADI n) (s, stk) = (s, (n)#stk)" |
  "exec1 (LOAD v) (s, stk) = (s, (s v)#stk)" |
  "exec1 (PILOAD x) (s, stk) = (s(x:=s x + 1), (s x)#stk)" | 
  "exec1 ADD (s, stk) = (s, (hd stk + hd2 stk)#(tl2 stk))"

fun exec :: "instr list ⇒ (state × stack) ⇒ (state × stack)" where
  "exec [] tpl = tpl" |
  "exec (i#is) (s, stk) = (exec is (exec1 i (s, stk)) )"

fun comp :: "aexp' ⇒ instr list" where
  "comp (N' v) = [LOADI v]" |
  "comp (V' x) = [LOAD x]" |
  "comp (PI' x) = [PILOAD x]" |
  "comp (Plus' a1 a2) = ((comp a1)@(comp a2))@[ADD]"

value "comp (Plus' (N' 3) (N' 5))"
value "exec (comp (Plus' (N' 3) (N' 5)) ) (<>, [EOF])"
value "exec [LOADI 5, LOAD ''y'', ADD] (<''x'' := 42, ''y'' := 43>, [50])" (* [48, 50] *)
value "exec ( comp (Plus' (Plus' (N' 5) (PI' x)) (V' x)) ) (<x:=1>, [EOF])" (* [8, EOF] *)



lemma exec_app: "exec (i1 @ i2) (s, stk) = exec i2 (exec i1 (s, stk))"
apply(induct i1 arbitrary:  s stk)
apply(auto)
apply(metis PairE) (* thx sledgehammer *)
done


theorem exec_comp: "exec (comp a) (s,stk) = (case aval' a s of (v ,s') ⇒ (s', v#stk))"
apply(induct a arbitrary: s stk s' v v')
apply(auto)
apply(simp split: prod.split)
apply(auto)
apply(simp add: exec_app)
done

(* that would be my formulation of the 'correctness' *)
lemma exec_comp_same: "(case exec (comp a) (s, stk) of (s', stk') ⇒ (hd stk', s') = aval' a s )"
apply(induct a arbitrary: s stk)
apply(auto split: prod.split)
apply(auto simp add: exec_comp exec_app)
done

(* Hw 3.2 *)

(* stack underflow test *)
value "exec [LOADI 3, ADD] (<>, [])"

(* instr: LOADI val | LOAD vname | PILOAD vname | ADD *)
(** inductive can_exec :: "nat ⇒ instr list ⇒ nat ⇒ bool" where
c0:  "can_exec n [] n" |
c1:  "can_exec n (is) n' ⟹ can_exec n (is@[(LOAD _)]) (Suc n')" |
c2:  "can_exec n (is) n' ⟹ can_exec n (is@[(LOADI _)]) (Suc n')" |
c3:  "can_exec n (is) n' ⟹ can_exec n (is@[(PILOAD _)]) (Suc n')" | 
c4:  "can_exec n is (Suc (Suc n')) ⟹ can_exec n (is@[ADD]) (Suc n')" *)


(** inductive can_exec :: "nat ⇒ instr list ⇒ nat ⇒ bool" where
c0:  "can_exec n [] n" | 
c1:  "can_exec n is n' ⟹ can_exec (Suc n) is n'" |
c2:  "can_exec (Suc n) is n' ⟹ can_exec n ((LOAD _)#is)  n'" |
c3:  "can_exec (Suc n) is n' ⟹ can_exec n ((LOADI _)#is) (n')" | 
c4:  "can_exec (Suc n) is n' ⟹ can_exec n ((PILOAD _)#is) (n')" |
c5:  "can_exec (Suc (Suc n)) is n' ⟹ can_exec (Suc (Suc n)) (ADD#is) (Suc n')" |
c6:  "can_exec n is (Suc n') ⟹ can_exec (Suc n) is n'" **)

inductive can_exec :: "nat ⇒ instr list ⇒ nat ⇒ bool" where
c0:  "can_exec n [] n" | 
c1:  "can_exec n is n' ⟹ can_exec (Suc n) is n'" | 
c2:  "can_exec (Suc n) is n' ⟹ can_exec n ((LOAD _)#is)  (n')" |
c3:  "can_exec (Suc n) is n' ⟹ can_exec n ((LOADI _)#is) (n')" | 
c4:  "can_exec (Suc n) is n' ⟹ can_exec n ((PILOAD _)#is) (n')" |
c5:  "can_exec (Suc n) is n' ⟹ can_exec (Suc (Suc n)) (ADD#is) (n')" 
(* c6:  "can_exec n is (Suc n') ⟹ can_exec (Suc n) is n'" *)



(* test *)
thm c5[OF c1[OF c1[OF c0[of 0]]]]
lemma "can_exec (Suc (Suc 0)) [ADD] (Suc 0)"
apply(simp add: can_exec.intros)
done

(* test *)
lemma "can_exec (Suc 0) [ADD] (Suc 0)"
apply(rule c1)
oops

lemma "can_exec 0 [LOAD x ] (Suc 0)"
apply(rule can_exec.intros)
apply(rule can_exec.intros)
done


(* test *)
lemma "can_exec 0 [LOAD x , LOADI v] (Suc (Suc 0))"
apply(simp add: can_exec.intros)
done


thm c2[OF c3[OF c5[OF c1[OF c1[OF c0[of 0]]]]]]
lemma "can_exec 0 [LOAD x , LOADI v , ADD] (Suc 0 )"
apply(auto simp add: can_exec.intros)
done

lemma "can_exec (Suc (Suc 0 )) [PILOAD x , ADD, ADD, LOAD y] (Suc (Suc 0 ))"
apply(auto simp add: can_exec.intros)
done


(* NOT provable *)
lemma "can_exec (Suc 0 ) [PILOAD x , ADD, ADD, LOAD y] (Suc 0 )"
apply(auto simp add: can_exec.intros)
apply(rule c4)
apply(rule c5) (* cannot go on, resulting stack empty *)
oops

(* nitpick always tries to report the following as counter example! *)
lemma "can_exec 0 (comp (PI' a)) (Suc 0)"
apply(simp add: can_exec.intros)
done



theorem "can_exec n (comp a) (Suc n)"
apply(induct a arbitrary: n)
apply(auto simp add: can_exec.intros)
done

end