theory Terms
imports Nominal "../QuotMain" "../QuotList"
begin

atom_decl name

text {* primrec seems to be genarally faster than fun *}

section {*** lets with binding patterns ***}

datatype trm1 =
  Vr1 "name"
| Ap1 "trm1" "trm1"
| Lm1 "name" "trm1"        --"name is bound in trm1"
| Lt1 "bp" "trm1" "trm1"   --"all variables in bp are bound in the 2nd trm1"
and bp =
  BUnit
| BVr "name"
| BPr "bp" "bp"

(* to be given by the user *)
primrec 
  bv1
where
  "bv1 (BUnit) = {}"
| "bv1 (BVr x) = {x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"

(* needs to be calculated by the package *)
primrec 
  fv_trm1 and fv_bp
where
  "fv_trm1 (Vr1 x) = {x}"
| "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)"
| "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}"
| "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)"
| "fv_bp (BUnit) = {}"
| "fv_bp (BVr x) = {x}"
| "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)"

(* needs to be stated by the package *)
overloading
  perm_trm1 \<equiv> "perm :: 'x prm \<Rightarrow> trm1 \<Rightarrow> trm1"   (unchecked)
  perm_bp \<equiv> "perm :: 'x prm \<Rightarrow> bp \<Rightarrow> bp" (unchecked)
begin

primrec
  perm_trm1 and perm_bp
where
  "perm_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)"
| "perm_trm1 pi (Ap1 t1 t2) = Ap1 (perm_trm1 pi t1) (perm_trm1 pi t2)"
| "perm_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (perm_trm1 pi t)"
| "perm_trm1 pi (Lt1 bp t1 t2) = Lt1 (perm_bp pi bp) (perm_trm1 pi t1) (perm_trm1 pi t2)"
| "perm_bp pi (BUnit) = BUnit"
| "perm_bp pi (BVr a) = BVr (pi \<bullet> a)"
| "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)"

end


section {*** lets with single assignments ***}

datatype trm2 =
  Vr2 "name"
| Ap2 "trm2" "trm2"
| Lm2 "name" "trm2"
| Lt2 "assign" "trm2"
and assign =
  As "name" "trm2"

(* to be given by the user *)
primrec 
  bv2
where
  "bv2 (As x t) = {x}"

(* needs to be calculated by the package *)
primrec
  fv_trm2 and fv_assign
where
  "fv_trm2 (Vr2 x) = {x}"
| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}"
| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
| "fv_assign (As x t) = (fv_trm2 t)"

(* needs to be stated by the package *)
overloading
  perm_trm2 \<equiv> "perm :: 'x prm \<Rightarrow> trm2 \<Rightarrow> trm2"   (unchecked)
  perm_assign \<equiv> "perm :: 'x prm \<Rightarrow> assign \<Rightarrow> assign" (unchecked)
begin

primrec
  perm_trm2 and perm_assign
where
  "perm_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
| "perm_trm2 pi (Ap2 t1 t2) = Ap2 (perm_trm2 pi t1) (perm_trm2 pi t2)"
| "perm_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (perm_trm2 pi t)"
| "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)"
| "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)"

end


section {*** lets with many assignments ***}

datatype trm3 =
  Vr3 "name"
| Ap3 "trm3" "trm3"
| Lm3 "name" "trm3"
| Lt3 "assigns" "trm3"
and assigns =
  ANil
| ACons "name" "trm3" "assigns"

(* to be given by the user *)
primrec 
  bv3
where
  "bv3 ANil = {}"
| "bv3 (ACons x t as) = {x} \<union> (bv3 as)"

primrec
  fv_trm3 and fv_assigns
where
  "fv_trm3 (Vr3 x) = {x}"
| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"
| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}"
| "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)"
| "fv_assigns (ANil) = {}"
| "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"

(* needs to be stated by the package *)
overloading
  perm_trm3 \<equiv> "perm :: 'x prm \<Rightarrow> trm3 \<Rightarrow> trm3"   (unchecked)
  perm_assigns \<equiv> "perm :: 'x prm \<Rightarrow> assigns \<Rightarrow> assigns" (unchecked)
begin

primrec
  perm_trm3 and perm_assigns
where
  "perm_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
| "perm_trm3 pi (Ap3 t1 t2) = Ap3 (perm_trm3 pi t1) (perm_trm3 pi t2)"
| "perm_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (perm_trm3 pi t)"
| "perm_trm3 pi (Lt3 as t) = Lt3 (perm_assigns pi as) (perm_trm3 pi t)"
| "perm_assigns pi (ANil) = ANil"
| "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)"

end


end