Theory On_Stack

```(* Currently not used, but may be of general use. Keep in Aux! *)
theory On_Stack
imports Collections.Refine_Dflt
begin
subsection ‹Implementation of a stack with efficient on-stack operation›
text ‹This generic implementation combines a stack implementation and
a set implementation that is used to keep track of the elements on the stack.
It requires a distinct stack, i.e., no duplicate elements on the stack.

Note that this generic implementation has to be instantiated to a
concrete stack-relation in order to avoid looping of the autoref-tool,
which otherwise tries to instantiate the stack-implementation with itself
indefinitely often.
›

definition stack_rel_internal_def: "stack_rel lrel srel vrel ≡ {
((li,si),l). (li,l)∈⟨vrel⟩lrel ∧ (si,set l)∈⟨vrel⟩srel ∧ distinct l}"

lemma stack_rel_def: "⟨vrel⟩stack_rel lrel srel ≡ {
((li,si),l). (li,l)∈⟨vrel⟩lrel ∧ (si,set l)∈⟨vrel⟩srel ∧ distinct l}"
unfolding stack_rel_internal_def relAPP_def by auto

lemmas [autoref_rel_intf]
= REL_INTFI[of "stack_rel lrel srel" i_list for lrel srel]

context
fixes lrel :: "('xi × 'x) set ⇒ ('xli × 'x list) set"
and srel :: "('xi × 'x) set ⇒ ('xsi × 'x set) set"
begin

context begin interpretation autoref_syn .

lemma autoref_stack_empty[OF GEN_OP_D GEN_OP_D]:
assumes "(el,[])∈⟨vrel⟩lrel"
assumes "(es,{})∈⟨vrel⟩srel"
shows "((el,es),[]) ∈ ⟨vrel⟩stack_rel lrel srel"
using assms unfolding stack_rel_def
by auto

primrec stack_push::"_::type"
where "stack_push push ins (el,es) v = (push el v, ins v es)"

lemma autoref_stack_push:
assumes "GEN_OP push op_list_append_elem (⟨vrel⟩lrel → vrel → ⟨vrel⟩lrel)"
assumes "GEN_OP ins insert (vrel → ⟨vrel⟩srel → ⟨vrel⟩srel)"
assumes "SIDE_PRECOND (v∉set l)"
assumes "(vi,v)∈vrel"
assumes "(si,l)∈⟨vrel⟩stack_rel lrel srel"
shows "(stack_push push ins si vi,
(OP op_list_append_elem ::: ⟨vrel⟩stack_rel lrel srel → vrel → ⟨vrel⟩stack_rel lrel srel)
\$l\$v) ∈ ⟨vrel⟩stack_rel lrel srel"
using assms unfolding stack_rel_def
apply auto
apply (unfold op_list_append_elem_def[symmetric])
apply parametricity+
done

lemma autoref_stack_sng:
assumes "GEN_OP lsng op_list_singleton (vrel → ⟨vrel⟩lrel)"
assumes "GEN_OP sins insert (vrel → ⟨vrel⟩srel → ⟨vrel⟩srel)"
assumes "GEN_OP semp {} (⟨vrel⟩srel)"
shows "(λv. (lsng v, sins v semp),op_list_singleton)
∈ vrel → ⟨vrel⟩stack_rel lrel srel"
using assms
unfolding stack_rel_def autoref_tag_defs
by (fastforce simp: op_list_singleton_def[abs_def] dest: fun_relD)

primrec stack_pop::"_::type"
where "stack_pop lpop ltop del (el,es)
= (let v = ltop el; el = lpop el; es = del v es in (el,es))"

lemma autoref_stack_pop:
assumes POPR: "⋀el l. ⟦ (el,l)∈⟨vrel⟩lrel; l≠[] ⟧
⟹ (lpop el,(OP butlast ::: ⟨vrel⟩lrel → ⟨vrel⟩lrel)\$l)∈ ⟨vrel⟩lrel"
assumes TOPR: "⋀el l. ⟦ (el,l)∈⟨vrel⟩lrel; l≠[] ⟧
⟹ (ltop el,(OP last ::: ⟨vrel⟩lrel → vrel)\$l)∈ vrel"
assumes DELR: "GEN_OP del op_set_delete (vrel → ⟨vrel⟩srel → ⟨vrel⟩srel)"
assumes NE: "SIDE_PRECOND (l ≠ [])"
assumes R: "(si,l)∈⟨vrel⟩stack_rel lrel srel"
shows "(stack_pop lpop ltop del si,
(OP butlast ::: ⟨vrel⟩stack_rel lrel srel → ⟨vrel⟩stack_rel lrel srel)
\$l) ∈ ⟨vrel⟩stack_rel lrel srel"
proof -
note POPR TOPR DELR
note [param] = this[unfolded autoref_tag_defs]

have AUX: "set (butlast l) = op_set_delete (last l) (set l)"
using NE R unfolding stack_rel_def
by (cases l rule: rev_cases) auto

show ?thesis
using NE R unfolding stack_rel_def autoref_tag_defs
apply (clarsimp simp: distinct_butlast, intro conjI)
apply parametricity
apply (subst AUX)
apply parametricity
done
qed

lemma autoref_stack_set:
shows "(snd, set) ∈ ⟨vrel⟩stack_rel lrel srel → ⟨vrel⟩srel"
unfolding stack_rel_def
by auto

lemma autoref_stack_is_Nil:
assumes "GEN_OP ini is_Nil (⟨vrel⟩lrel → bool_rel)"
shows "(ini o fst, is_Nil) ∈ ⟨vrel⟩stack_rel lrel srel → bool_rel"
using assms unfolding stack_rel_def
by (auto dest: fun_relD)

lemma autoref_stack_ltop:
assumes TOPR: "⋀el l. ⟦ (el,l)∈⟨vrel⟩lrel; l≠[] ⟧
⟹ (ltop el,(OP last ::: ⟨vrel⟩lrel → vrel)\$l)∈ vrel"
assumes NE: "SIDE_PRECOND (l ≠ [])"
assumes R: "(si,l)∈⟨vrel⟩stack_rel lrel srel"
shows "(ltop (fst si), (OP last ::: ⟨vrel⟩stack_rel lrel srel → vrel)\$l) ∈ vrel"
using assms unfolding stack_rel_def
by (auto dest: fun_relD)

lemmas stack_autoref_rules
= autoref_stack_empty autoref_stack_push autoref_stack_sng autoref_stack_pop
autoref_stack_set autoref_stack_is_Nil autoref_stack_ltop

end

end

abbreviation "as_ahs_stack_rel ≡ stack_rel as_rel dflt_ahs_rel"
lemmas as_ahs_stack_rules
= stack_autoref_rules[where lrel = as_rel and srel = dflt_ahs_rel]

schematic_goal
notes [autoref_rules] = as_ahs_stack_rules
shows "(?c::?'c, set (butlast ([1::nat]@[2]))) ∈ ?R"
apply (autoref (trace,keep_goal))
done

end

```