Theory Current_Proof

section "Current Proofs"

theory Current_Proof
imports Current_Aux Stack_Proof
begin

lemma push_list [simp]: "list (push x current) = x # list current"
  by(induction x current rule: push.induct) auto

lemma pop_list [simp]: 
    "⟦0 < size current; invar current⟧ ⟹ fst (pop current) # tl (list current) = list current"
  by(induction current rule: pop.induct)(auto simp: size_not_empty list_not_empty)

lemma drop_first_list [simp]: "⟦invar current; 0 < size current⟧
  ⟹ list (drop_first current) = tl (list current)"
  by(induction current rule: pop.induct)(auto simp: drop_Suc)

lemma invar_push: "invar current ⟹ invar (push x current)"
  by(induction x current rule: push.induct) auto

lemma invar_pop: "⟦0 < size current; invar current; pop current = (x, current')⟧
   ⟹ invar current'"
  by(induction current arbitrary: x rule: pop.induct) auto

lemma invar_drop_first: "⟦0 < size current; invar current⟧ ⟹ invar (drop_first current)"
  using invar_pop
  by (metis eq_snd_iff)

lemma list_size [simp]: "⟦invar current; list current = []; 0 < size current⟧ ⟹ False"
  by(induction current)(auto simp: size_not_empty list_empty)

lemma size_new_push [simp]: "invar current ⟹ size_new (push x current) = Suc (size_new current)"
  by(induction x current rule: push.induct) auto

lemma size_push [simp]: "size (push x current) = Suc (size current)"
  by(induction x current rule: push.induct) auto

lemma size_new_pop [simp]: "⟦0 < size_new current; invar current ⟧
  ⟹ Suc (size_new (drop_first current)) = size_new current"
  by(induction current rule: pop.induct) auto

lemma size_pop [simp]: "⟦0 < size current; invar current ⟧
   ⟹ Suc (size (drop_first current)) = size current"
  by(induction current rule: pop.induct) auto

lemma size_pop_suc [simp]: "⟦0 < size current; invar current; pop current = (x, current') ⟧
   ⟹ Suc (size current') = size current"
  by(induction current rule: pop.induct) auto

lemma size_pop_sub: "⟦0 < size current; invar current; pop current = (x, current') ⟧
   ⟹ size current' = size current - 1"
  by(induction current rule: pop.induct) auto

lemma size_drop_first_sub: "⟦0 < size current; invar current ⟧
   ⟹ size (drop_first current) = size current - 1"
  by(induction current rule: pop.induct) auto

end