theory Terms

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

begin

atom_decl name

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

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

datatype rtrm1 =

  rVr1 "name"

| rAp1 "rtrm1" "rtrm1"

| rLm1 "name" "rtrm1"        --"name is bound in trm1"

| rLt1 "bp" "rtrm1" "rtrm1"   --"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 

  rfv_trm1 and rfv_bp

where

  "rfv_trm1 (rVr1 x) = {atom x}"

| "rfv_trm1 (rAp1 t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2)"

| "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}"

| "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)"

| "rfv_bp (BUnit) = {}"

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

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

(* needs to be stated by the package *)

instantiation 

  rtrm1 and bp :: pt

begin

primrec

  permute_rtrm1 and permute_bp

where

  "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)"

| "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"

| "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)"

| "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 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_rtrm1_bp_zero:

  fixes t::rtrm1

  and   b::bp

  shows "0 \<bullet> t = t"

  and   "0 \<bullet> b = b"

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

apply(simp_all)

done

lemma pt_rtrm1_bp_plus:

  fixes t::rtrm1

  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: rtrm1_bp.inducts)

apply(simp_all)

done

instance

apply default

apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus)

done

end

inductive

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

where

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

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

| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"

| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"

lemma alpha1_inj:

"(rVr1 a \<approx>1 rVr1 b) = (a = b)"

"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"

"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))"

"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))"

apply -

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

done

(* Shouyld we derive it? But bv is given by the user? *)

lemma bv1_eqvt[eqvt]:

  shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"

  apply (induct x)

done

lemma rfv_trm1_eqvt[eqvt]:

  shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"

  apply (induct t)

  done

lemma alpha1_eqvt:

  shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"

  apply (induct t s rule: alpha1.inducts)

  apply (simp_all add:eqvts alpha1_inj)

  apply (erule exE)

  apply (rule_tac x="pi \<bullet> pia" in exI)

  apply (simp add: alpha_gen)

  apply(erule conjE)+

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

  apply(simp add: permute_eqvt[symmetric])

  apply (erule exE)

  apply (rule_tac x="pi \<bullet> pia" in exI)

  apply (simp add: alpha_gen)

  apply(erule conjE)+

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

  apply(simp add: permute_eqvt[symmetric])

  done

lemma alpha1_equivp: "equivp alpha1" 

  sorry

quotient_type trm1 = rtrm1 / alpha1

  by (rule alpha1_equivp)

quotient_definition

  "Vr1 :: name \<Rightarrow> trm1"

as

  "rVr1"

quotient_definition

  "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"

as

  "rAp1"

quotient_definition

  "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"

as

  "rLm1"

quotient_definition

  "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"

as

  "rLt1"

quotient_definition

  "fv_trm1 :: trm1 \<Rightarrow> atom set"

as

  "rfv_trm1"

lemma alpha_rfv1:

  shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"

  apply(induct rule: alpha1.induct)

  apply(simp_all add: alpha_gen.simps)

  done

lemma [quot_respect]:

 "(op = ===> alpha1) rVr1 rVr1"

 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"

 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"

 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"

apply (auto intro: alpha1.intros)

apply(rule a3) apply (rule_tac x="0" in exI)

apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)

apply(rule a4) apply assumption apply (rule_tac x="0" in exI)

apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)

done

lemma [quot_respect]:

  "(op = ===> alpha1 ===> alpha1) permute permute"

apply auto

apply (rule alpha1_eqvt)

apply simp

done

lemma [quot_respect]:

  "(alpha1 ===> op =) rfv_trm1 rfv_trm1"

apply (simp add: alpha_rfv1)

done

lemma trm1_bp_induct: "

\<lbrakk>\<And>name. P1 (Vr1 name);

 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);

 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);

 \<And>bp rtrm11 rtrm12.

    \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);

 P2 BUnit; \<And>name. P2 (BVr name);

 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>

\<Longrightarrow> P1 rtrma \<and> P2 bpa"

apply (lifting rtrm1_bp.induct)

done

lemma trm1_bp_inducts: "

\<lbrakk>\<And>name. P1 (Vr1 name);

 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);

 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);

 \<And>bp rtrm11 rtrm12.

    \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);

 P2 BUnit; \<And>name. P2 (BVr name);

 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>

\<Longrightarrow> P1 rtrma"

"\<lbrakk>\<And>name. P1 (Vr1 name);

 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);

 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);

 \<And>bp rtrm11 rtrm12.

    \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);

 P2 BUnit; \<And>name. P2 (BVr name);

 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>

\<Longrightarrow> P2 bpa"

by (lifting rtrm1_bp.inducts)

instantiation trm1 and bp :: pt

begin

quotient_definition

  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"

as

  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"

lemma permute_trm1 [simp]:

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

  and   "pi \<bullet> Ap1 t1 t2 = Ap1 (pi \<bullet> t1) (pi \<bullet> t2)"

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

  and   "pi \<bullet> Lt1 b t s = Lt1 (pi \<bullet> b) (pi \<bullet> t) (pi \<bullet> s)"

apply -

apply(lifting permute_rtrm1_permute_bp.simps(1))

apply(lifting permute_rtrm1_permute_bp.simps(2))

apply(lifting permute_rtrm1_permute_bp.simps(3))

apply(lifting permute_rtrm1_permute_bp.simps(4))

done

instance

apply default

apply(induct_tac [!] x rule: trm1_bp_inducts(1))

apply(simp_all)

done

end

lemma fv_trm1:

"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)"

apply -

apply (lifting rfv_trm1_rfv_bp.simps(1))

apply (lifting rfv_trm1_rfv_bp.simps(2))

apply (lifting rfv_trm1_rfv_bp.simps(3))

apply (lifting rfv_trm1_rfv_bp.simps(4))

done

lemma fv_trm1_eqvt:

  shows "(p \<bullet> fv_trm1 t) = fv_trm1 (p \<bullet> t)"

apply(lifting rfv_trm1_eqvt)

done

lemma alpha1_INJ:

"(Vr1 a = Vr1 b) = (a = b)"

"(Ap1 t1 s1 = Ap1 t2 s2) = (t1 = t2 \<and> s1 = s2)"

"(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))"

"(Lt1 b1 t1 s1 = Lt1 b2 t2 s2) = (t1 = t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen (op =) fv_trm1 pi ((bv1 b2), s2))))"

unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen])

done

lemma lm1_supp_pre:

  shows "(supp (atom x, t)) supports (Lm1 x t) "

apply(simp add: supports_def)

apply(fold fresh_def)

apply(simp add: fresh_Pair swap_fresh_fresh)

apply(clarify)

apply(subst swap_at_base_simps(3))

apply(simp_all add: fresh_atom)

done

lemma lt1_supp_pre:

  shows "(supp (x, t, s)) supports (Lt1 t x s) "

apply(simp add: supports_def)

apply(fold fresh_def)

apply(simp add: fresh_Pair swap_fresh_fresh)

done

lemma bp_supp: "finite (supp (bp :: bp))"

  apply (induct bp)

  apply(simp_all add: supp_def)

  apply (fold supp_def)

  apply (simp add: supp_at_base)

  apply(simp add: Collect_imp_eq)

  apply(simp add: Collect_neg_eq[symmetric])

  apply (fold supp_def)

  apply (simp)

  done

instance trm1 :: fs

apply default

apply(induct_tac x rule: trm1_bp_inducts(1))

apply(simp_all)

apply(simp add: supp_def alpha1_INJ eqvts)

apply(simp add: supp_def[symmetric] supp_at_base)

apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)

apply(simp add: Collect_imp_eq Collect_neg_eq)

apply(rule supports_finite)

apply(rule lm1_supp_pre)

apply(simp add: supp_Pair supp_atom)

apply(rule supports_finite)

apply(rule lt1_supp_pre)

apply(simp add: supp_Pair supp_atom bp_supp)

done

lemma supp_fv:

  shows "supp t = fv_trm1 t"

apply(induct t rule: trm1_bp_inducts(1))

apply(simp_all)

apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)

apply(simp only: supp_at_base[simplified supp_def])

apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)

apply(simp add: Collect_imp_eq Collect_neg_eq)

apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")

apply(simp add: supp_Abs fv_trm1)

apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)

apply(simp add: alpha1_INJ)

apply(simp add: Abs_eq_iff)

apply(simp add: alpha_gen.simps)

apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])

apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")

apply(simp add: supp_Abs fv_trm1)

apply(simp (no_asm) add: supp_def)

apply(simp add: alpha1_INJ)

apply(simp add: Abs_eq_iff)

apply(simp add: alpha_gen)

apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)

apply(simp add: Collect_imp_eq Collect_neg_eq)

done

lemma trm1_supp:

  "supp (Vr1 x) = {atom x}"

  "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"

  "supp (Lm1 x t) = (supp t) - {atom x}"

  "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"

  by (simp_all only: supp_fv fv_trm1)

lemma trm1_induct_strong:

  assumes "\<And>name b. P b (Vr1 name)"

  and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"

  and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"

  and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"

  shows   "P a rtrma"

sorry

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