Theory Var_list

section ‹Circus variables›

theory Var_list
imports Main
begin

text ‹Circus variables are represented by a stack (list) of values. 
they are characterized by two functions, $select$ and $update$.
The Circus variable type is defined as a tuple ($select$ * $update$) with a 
list of values instead of a single value.›

type_synonym ('a, 'σ) var_list = "('σ ⇒ 'a list) * (('a list ⇒ 'a list) ⇒ 'σ ⇒ 'σ)"

text ‹The $select$ function returns the top value of the stack.›

definition select :: "('a, 'r) var_list ⇒ 'r ⇒ 'a"
where "select f ≡ λ A. hd ((fst f) A)"

text ‹The $increase$ function pushes a new value to the top of the stack.›

definition increase :: "('a, 'r) var_list ⇒ 'a ⇒ 'r ⇒ 'r"
where "increase f val ≡ (snd f) (λ l. val#l)"

text ‹The $increase0$ function pushes an arbitrary value to the top of the stack.›

definition increase0 :: "('a, 'r) var_list ⇒ 'r ⇒ 'r"
where "increase0 f ≡ (snd f) (λ l. ((SOME val. True)#l))"

text ‹The $decrease$ function pops the top value of the stack.›

definition decrease :: "('a, 'r) var_list ⇒ 'r ⇒ 'r"
where "decrease f ≡ (snd f) (λ l. (tl l))"

text ‹The $update$ function updates the top value of the stack.›

definition update :: "('a, 'r) var_list ⇒ ('a ⇒ 'a) ⇒ 'r ⇒ 'r"
where "update f upd ≡ (snd f) (λ l. (upd (hd l))#(tl l))"

text ‹The $update0$ function initializes the top of the stack with an arbitrary value.›

definition update0 :: "('a, 'r) var_list ⇒ 'r ⇒ 'r"
where "update0 f ≡ (snd f) (λ l. ((SOME upd. True) (hd l))#(tl l))"

axiomatization  where select_increase: "(select v (increase v a s)) = a"


text ‹The $VAR-LIST$ function allows to retrieve a Circus variable from its name.›

syntax "_VAR_LIST" :: "id ⇒ ('a, 'r) var_list"  (‹VAR'_LIST _›)
translations "VAR_LIST x" => "(x, _update_name x)"

end