Types = Main + Tactics + 

(* Theory of types, some of which are linear and some nonlinear. For
linear types, occurrences of positive and negative versions of the
variable are recorded separately; therefore we are catering for a
pi-calculus-like language. *)

(* Later, specific types  lty  and  nlty  must be defined; they
represent linear and nonlinear types respectively. Then define

datatype ty = LinT lty | NLinT nlty

Note that in general the definitions of lty and nlty will involve
ty. *)

(* In the following definitions, 'a stands for lty and 'b stands for
nlty. In later theories, these will be instantiated to the specific
types lty and nlty. *)

(* Number of occurrences of a linear variable. *)

datatype 'a oty = 
  Zero 
| One 'a

(* Record for positive and negative occurrences of a variable. *)

record 'a linv =
  pos :: 'a oty
  neg :: 'a oty

(* The type of a variable in an environment. *)

datatype ('a,'b) vty = 
  LinV "'a linv"
| NLinV 'b

constdefs linear :: "('a,'b) vty => bool"
"linear t == \ 
\ (case t of LinV x => True | NLinV y => False)"

constdefs unlim :: "('a,'b) vty => bool"
"unlim t == \ 
\ (case t of \ 
\    LinV x => (pos x = Zero & neg x = Zero) \ 
\  | NLinV y => True)"

constdefs null :: "('a,'b) vty => bool"
"null t == \ 
\ (case t of \ 
\    LinV x => (pos x = Zero & neg x = Zero) \ 
\  | NLinV y => False)"

constdefs cmp :: "('a,'b) vty => bool"
"cmp t == \ 
\ (case t of \ 
\    LinV x => (pos x ~= Zero & neg x ~= Zero) \ 
\  | NLinV y => True)"

constdefs bal :: "('a,'b) vty => bool"
"bal t == \ 
\ (case t of \ 
\    LinV x => (pos x = neg x) \ 
\  | NLinV y => True)"

constdefs canaddt :: "('a,'b) vty => ('a,'b) vty => bool"
"canaddt t u == \ 
\ (case t of \ 
\    LinV x => \ 
\      (case u of \ 
\         LinV y => ((pos x = Zero | pos y = Zero) & \ 
\                    (neg x = Zero | neg y = Zero)) \ 
\       | NLinV y => False) \ 
\  | NLinV x => \ 
\      (case u of \ 
\         LinV y => False \ 
\       | NLinV y => x = y))"

constdefs addocc :: "'a oty => 'a oty => 'a oty"
"addocc x y == (if x = Zero then y else x)"

constdefs addt :: "('a,'b) vty => ('a,'b) vty => ('a,'b) vty"
"addt t u == \ 
\ (case t of \ 
\    LinV x => \ 
\      (case u of \ 
\         LinV y => LinV (| pos = (addocc (pos x) (pos y)) , \ 
\                           neg = (addocc (neg x) (neg y)) |) \ 
\       | NLinV y => t) \ 
\  | NLinV x => t)"

constdefs skel :: "('a,'b) vty => ('a,'b) vty"
"skel t == \ 
\ (case t of \ 
\    LinV x => LinV (| pos = Zero , neg = Zero |) \ 
\  | NLinV y => t)"

end

