theory Terms

imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" 

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) = {atom 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) = {atom x}"

| "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)"

| "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {atom x}"

| "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)"

| "fv_bp (BUnit) = {}"

| "fv_bp (BVr x) = {atom x}"

| "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)"

(* needs to be stated by the package *)

instantiation 

  trm1 and bp :: pt

begin

primrec

  permute_trm1 and permute_bp

where

  "permute_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)"

| "permute_trm1 pi (Ap1 t1 t2) = Ap1 (permute_trm1 pi t1) (permute_trm1 pi t2)"

| "permute_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (permute_trm1 pi t)"

| "permute_trm1 pi (Lt1 bp t1 t2) = Lt1 (permute_bp pi bp) (permute_trm1 pi t1) (permute_trm1 pi t2)"

| "permute_bp pi (BUnit) = BUnit"

| "permute_bp pi (BVr a) = BVr (pi \<bullet> a)"

| "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)"

lemma pt_trm1_bp_zero:

  fixes t::trm1

  and   b::bp

  shows "0 \<bullet> t = t"

  and   "0 \<bullet> b = b"

apply(induct t and b rule: trm1_bp.inducts)

apply(simp_all)

done

lemma pt_trm1_bp_plus:

  fixes t::trm1

  and   b::bp

  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"

  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"

apply(induct t and b rule: trm1_bp.inducts)

apply(simp_all)

done

instance

apply default

apply(simp_all add: pt_trm1_bp_zero pt_trm1_bp_plus)

done

end

inductive

  alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)

where

  a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)"

| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2"

| a3: "\<exists>pi. (fv_trm1 t - {atom a} = fv_trm1 s - {atom b} \<and> 

            (fv_trm1 t - {atom a})\<sharp>* pi \<and> 

            (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b)

       \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s"

| a4: "\<exists>pi.(t1 \<approx>1 t2 \<and>

           (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and>

           (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and>

           (pi \<bullet> s1 = s2)                    (* Optional: \<and> (pi \<bullet> b1 = b2) *)) 

       \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2"

lemma alpha1_equivp: "equivp alpha1" 

  sorry

quotient_type qtrm1 = trm1 / alpha1

  by (rule alpha1_equivp)

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) = {atom x}"

(* needs to be calculated by the package *)

primrec

  fv_trm2 and fv_assign

where

  "fv_trm2 (Vr2 x) = {atom x}"

| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"

| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom 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 *)

instantiation 

  trm2 and assign :: pt

begin

primrec

  permute_trm2 and permute_assign

where

  "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"

| "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"

| "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"

| "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"

| "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"

lemma pt_trm2_assign_zero:

  fixes t::trm2

  and   b::assign

  shows "0 \<bullet> t = t"

  and   "0 \<bullet> b = b"

apply(induct t and b rule: trm2_assign.inducts)

apply(simp_all)

done

lemma pt_trm2_assign_plus:

  fixes t::trm2

  and   b::assign

  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"

  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"

apply(induct t and b rule: trm2_assign.inducts)

apply(simp_all)

done

instance

apply default

apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)

done

end

inductive

  alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)

where

  a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"

| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"

| a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and> 

            (fv_trm2 t - {atom a})\<sharp>* pi \<and> 

            (pi \<bullet> t) \<approx>2 s \<and> 

            (pi \<bullet> a) = b)

       \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"

| a4: "\<exists>pi. (

         fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>

         (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>

         pi \<bullet> t1 = t2       (* \<and> (pi \<bullet> b1 = b2) *)

       ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"

lemma alpha2_equivp: "equivp alpha2" 

  sorry

quotient_type qtrm2 = trm2 / alpha2

  by (rule alpha2_equivp)

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) = {atom x} \<union> (bv3 as)"

primrec

  fv_trm3 and fv_assigns

where

  "fv_trm3 (Vr3 x) = {atom x}"

| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"

| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {atom 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 *)

instantiation

 trm3 and assigns :: pt

begin

primrec

  permute_trm3 and permute_assigns

where

  "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"

| "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"

| "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"

| "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"

| "permute_assigns pi (ANil) = ANil"

| "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"

lemma pt_trm3_assigns_zero:

  fixes t::trm3

  and   b::assigns

  shows "0 \<bullet> t = t"

  and   "0 \<bullet> b = b"

apply(induct t and b rule: trm3_assigns.inducts)

apply(simp_all)

done

lemma pt_trm3_assigns_plus:

  fixes t::trm3

  and   b::assigns

  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"

  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"

apply(induct t and b rule: trm3_assigns.inducts)

apply(simp_all)

done

instance

apply default

apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)

done

end

inductive

  alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)

where

  a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"

| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"

| a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and> 

             (fv_trm3 t - {atom a})\<sharp>* pi \<and> 

             (pi \<bullet> t) \<approx>3 s \<and> 

             (pi \<bullet> a) = b)

       \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"

| a4: "\<exists>pi. (

         fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>

         (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and>

         pi \<bullet> t1 = t2      (* \<and> (pi \<bullet> b1 = b2)  *)

       ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2"

lemma alpha3_equivp: "equivp alpha3" 

  sorry

quotient_type qtrm3 = trm3 / alpha3

  by (rule alpha3_equivp)

section {*** lam with indirect list recursion ***}

datatype trm4 =

  Vr4 "name"

| Ap4 "trm4" "trm4 list"

| Lm4 "name" "trm4"

thm trm4.recs

primrec

  fv_trm4 and fv_trm4_list

where

  "fv_trm4 (Vr4 x) = {atom x}"

| "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"

| "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {atom x}"

| "fv_trm4_list ([]) = {}"

| "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"

(* needs to be stated by the package *)

(* there cannot be a clause for lists, as *) 

(* permuteutations are  already defined in Nominal (also functions, options, and so on) *)

instantiation

  trm4 :: pt

begin

(* does not work yet *)

primrec

where

  "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"

| "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"

end

inductive

    alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)

and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) 

where

  a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"

| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"

       \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"

| a5: "[] \<approx>4list []"

| a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"

lemma alpha4_equivp: "equivp alpha4" sorry

lemma alpha4list_equivp: "equivp alpha4list" sorry

quotient_type 

  qtrm4 = trm4 / alpha4 and

  qtrm4list = "trm4 list" / alpha4list

  by (simp_all add: alpha4_equivp alpha4list_equivp)

end