Theory VName

section‹Variables›
text‹Variables can either be inputs or registers. Here we define the \texttt{vname} datatype which
allows us to write expressions in terms of variables and case match during evaluation. We also make
the \texttt{vname} datatype a member of linorder such that we can establish a linear order on
arithmetic expressions, guards, and subsequently transitions.›

theory VName
imports Main
begin

text_raw‹\snip{vnametype}{1}{2}{%›
datatype vname = I nat | R nat
text_raw‹}%endsnip›

instantiation vname :: linorder begin
text_raw‹\snip{vnameorder}{1}{2}{%›
fun less_vname :: "vname ⇒ vname ⇒ bool" where
  "(I n1) < (R n2) = True" |
  "(R n1) < (I n2) = False" |
  "(I n1) < (I n2) = (n1 < n2)" |
  "(R n1) < (R n2) = (n1 < n2)"
text_raw‹}%endsnip›

definition less_eq_vname :: "vname ⇒ vname ⇒ bool" where
  "less_eq_vname v1 v2 = (v1 < v2 ∨ v1 = v2)"
declare less_eq_vname_def [simp]

instance
  apply standard
      apply (auto elim: less_vname.elims)
  subgoal for x y z
    apply (cases x; cases y; cases z)
           apply simp_all
    done
  done
end

end