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