(* An Isabelle HOL theory of the linear pi calculus, 
   using a metalanguage. No base types and no recursive types. *)

Pi = Subst +

(* Types for linear pi calculus *)

datatype lty  = LChan "((lty,nlty) env)" 

and      nlty = NLChan "((lty,nlty) env)"

types pienv = "(lty,nlty) env"

(* Datatype of constants *)

datatype con = 
  Nl        (* was "Nil" but this clashes with the empty list *)
| Par 
| Rep 
| New nat pienv 
| In  nat pienv
| Out nat 
| Lam

(* The type of pi terms *)

types pi = con meta

(* Constructors for pi terms *)

constdefs NIL :: pi
"NIL == mAPP (mCon Nl) []"

constdefs PAR :: "pi => pi => pi"
"PAR p q == mAPP (mCon Par) [p,q]"

constdefs REP :: "pi => pi"
"REP p == mAPP (mCon Rep) [p]"

constdefs NEW :: "nat => pienv => pi => pi"
"NEW n ts p == mAPP (mCon (New n ts)) [mABS n (mAPP (mCon Lam) [p])]"

(* Note the use of an additional constructor, Lam, to "protect"
p. This is so that we can prove injectivity theorems for NEW and
IN. This in turn is necessary in order to prove an elimination theorem
for NEW. *)

constdefs IN :: "Meta.var => nat => pienv => pi => pi"
"IN x n ts p == \ 
\ mAPP (mCon (In n ts)) \ 
\   [mABS n (mAPP (mCon Lam) [p]), mVar x]"

constdefs OUT :: "Meta.var => nat => Meta.var list => pi => pi"
"OUT x n xs p == \ 
\ mAPP (mApp (mCon (Out n)) p) \ 
\   (map mVar (x # xs))"

(* Structural congruence. *)

consts SCONG :: "(pi * pi) set"
inductive SCONG
intrs
  alpha "p = q ==> (p,q) : SCONG"
  symm  "(p,q):SCONG ==> (q,p):SCONG"
  trans "[| (p,q):SCONG ; (q,r):SCONG |] ==> (p,r):SCONG"
  nilC  "(NIL,NIL):SCONG"
  parC  "[| (p1,p2):SCONG ; (q1,q2):SCONG |] ==> (PAR p1 q1,PAR p2 q2):SCONG"
  repC  "(p,q):SCONG ==> (REP p,REP q):SCONG"
  newC  "(p,q):SCONG ==> (NEW n ts p,NEW n ts q):SCONG"
  inC   "(p,q):SCONG ==> (IN x n ts p,IN x n ts q):SCONG"
  outC  "(p,q):SCONG ==> (OUT x n xs p,OUT x n xs q):SCONG"
  par_comm  "(PAR p q,PAR q p):SCONG"
  par_assoc "(PAR p (PAR q r),PAR (PAR p q) r):SCONG"
  par_nil   "(PAR p NIL,p):SCONG"
  rep_nil   "(REP NIL,NIL):SCONG"
  rep_def   "(REP p,PAR p (REP p)):SCONG"
  new_merge "length us = m ==> \ 
\            (NEW n ts (NEW m us p) , NEW (m + n) (us @ ts) p) : SCONG"
  new_par   "(NEW n ts (PAR (lift 0 n p) q),PAR p (NEW n ts q)):SCONG"

constdefs SCONGREL :: "pi => pi => bool" (infixl "===" 300)
"p === q == (p,q):SCONG"

(* Reduction. *)

datatype redch = Tau | Ch nat

consts newch :: "nat => redch => redch"
primrec
"newch n Tau    = Tau"
"newch n (Ch x) = (if x < n then Tau else Ch (x - n))"

consts usechan :: "redch => ('a,'b) env => ('a,'b) env"
primrec
"usechan Tau    G = G"
"usechan (Ch x) G = usetype x G"

consts balchan :: "redch => ('a,'b) env => bool"
primrec
"balchan Tau    G = True"
"balchan (Ch x) G = bal (typeof x G)"

consts RED :: "(pi * redch * pi) set"
inductive RED
intrs
  comm "index x = index y ==> \ 
\       (PAR (OUT x m xs p) (IN y n ts q) , Ch (index x) , \ 
\        PAR p (SUB q (map (%a. (index a) + n) xs))) : RED"
  new  "(p , x , q) : RED ==> \ 
\        (NEW n ts p , newch n x , NEW n (usechan x ts) q) : RED"
  par  "(p , x , q) : RED ==> (PAR p r , x , PAR q r) : RED"
  cong "[| p1 === p ; (p , x , q) : RED ; q === q1 |] ==> (p1 , x , q1) : RED"

(* Typed processes *)

types

tic = "pienv * pi"

consts TYPED :: "tic set"
inductive TYPED
intrs

nilI 
"unlimited G ==> (G , NIL) : TYPED"

parI 
"[| (G , p) : TYPED ; (H , q) : TYPED ; canaddenv G H |] ==> \ 
\       (addenv G H , PAR p q) : TYPED"

repI 
"[| unlimited G ; (G , p) : TYPED |] ==> (G , REP p) : TYPED"

newI 
"[| (ts @ G , p) : TYPED ; length ts = n ; balanced ts |] ==> \ 
\       (G , NEW n ts p) : TYPED"

linI 
"[| (ts @ G , p) : TYPED ; length ts = n ; index x = i ; i < length G ; \ 
\  tag x = Neg ; \ 
\  canaddtypetoenv G i (LinV (| pos = Zero, neg = One (LChan ts) |)) |] ==> \ 
\ (addtypetoenv G i (LinV (| pos = Zero, neg = One (LChan ts) |)), \ 
\  IN x n ts p) : TYPED"

nlinI 
"[| (ts @ G , p) : TYPED ; length ts = n ; index x = i ; i < length G ; \ 
\  tag x = Both ; \ 
\  canaddtypetoenv G i (NLinV (NLChan ts)) |] ==> \ 
\ (addtypetoenv G i (NLinV (NLChan ts)) , IN x n ts p) : TYPED"

loutI 
"[| (G , p) : TYPED ; length xs = n ; index x = j ; tag x = Pos ; \ 
\  map index xs = js ; allless js (length G) ; j < length G ; \ 
\  map tag xs = tgs ; tvoccs ts tgs ; \ 
\  canaddtypetoenv (addtoenv G js ts) \ 
\   j (LinV (| pos = One (LChan ts), neg = Zero |)) ; \
\  canaddtoenv G js ts |] ==> \ 
\ (addtypetoenv (addtoenv G js ts) \ 
\   j (LinV (| pos = One (LChan ts), neg = Zero |)), \ 
\  OUT x n xs p) : TYPED" 

nloutI 
"[| (G , p) : TYPED ; length xs = n ; index x = j ; tag x = Both ; \ 
\  map index xs = js ; allless js (length G) ; j < length G ; \ 
\  map tag xs = tgs ; tvoccs ts tgs ; \ 
\  canaddtypetoenv (addtoenv G js ts) j (NLinV (NLChan ts)) ; \ 
\  canaddtoenv G js ts |] ==> \ 
\ (addtypetoenv (addtoenv G js ts) j (NLinV (NLChan ts)) , OUT x n xs p) : TYPED" 

(*
consts TYPED :: "tic set"
inductive TYPED
intrs
nilI "unlimited G ==> (G , NIL) : TYPED"
parI "[| (G , p) : TYPED ; (H , q) : TYPED ; canaddenv G H ; \ 
\        I = addenv G H |] ==> \ 
\       (I , PAR p q) : TYPED"
repI "[| unlimited G ; (G , p) : TYPED |] ==> (G , REP p) : TYPED"
newI "[| (ts @ G , p) : TYPED ; length ts = n ; balanced ts |] ==> \ 
\       (G , NEW n ts p) : TYPED"
linI "[| (ts @ G , p) : TYPED ; length ts = n ; index x = i ; i < length G ; \ 
\        tag x = Neg ; \ 
\        canaddtypetoenv G i (LinV (linv.make Zero (One (LChan ts)))) ; \ 
\        H = addtypetoenv G i (LinV (linv.make Zero (One (LChan ts)))) |] ==> \ 
\       (H , IN x n ts p) : TYPED"
nlinI "[| (ts @ G , p) : TYPED ; length ts = n ; index x = i ; i < length G ; \ 
\        tag x = Both ; \ 
\        canaddtypetoenv G i (NLinV (NLChan ts)) ; \ 
\        H = addtypetoenv G i (NLinV (NLChan ts)) |] ==> \ 
\       (H , IN x n ts p) : TYPED"
loutI "[| (G , p) : TYPED ; length xs = n ; index x = j ; tag x = Pos ; \ 
\         map index xs = js ; allless js (length G) ; j < length G ; \ 
\         map tag xs = tgs ; tvoccs ts tgs ; \  
\         canaddtoenv G (j # js) ((LinV (linv.make (One (LChan ts)) Zero)) # ts) ; \ 
\  H = addtoenv G (j # js) ((LinV (linv.make (One (LChan ts)) Zero)) # ts) |] ==> \ 
\       (H , OUT x n xs p) : TYPED" 
nloutI "[| (G , p) : TYPED ; length xs = n ; index x = j ; tag x = Both ; \ 
\         map index xs = js ; allless js (length G) ; j < length G ; \ 
\         map tag xs = tgs ; tvoccs ts tgs ; \ 
\         canaddtoenv G (j # js) ((NLinV (NLChan ts)) # ts) ; \ 
\         H = addtoenv G (j # js) ((NLinV (NLChan ts)) # ts) |] ==> \ 
\       (H , OUT x n xs p) : TYPED" 
*)

constdefs TYPEDREL :: "pienv => pi => bool" (infixl "|-" 30)
"G |- p == (G,p) : TYPED"

end