Lets are ok.
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)"
print_theorems
(* 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)
apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
done
lemma rfv_trm1_eqvt[eqvt]:
shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
apply (induct t)
apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
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(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt rfv_trm1_eqvt)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: atom_eqvt Diff_eqvt rfv_trm1_eqvt insert_eqvt empty_eqvt)
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(simp add: rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: atom_eqvt rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
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
"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
permute_trm4 and permute_trm4_list
where
"permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)"
| "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"
| "permute_trm4_list pi ([]) = []"
| "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)"
lemma pt_trm4_list_zero:
fixes t::trm4
and ts::"trm4 list"
shows "0 \<bullet> t = t"
and "permute_trm4_list 0 ts = ts"
apply(induct t and ts rule: trm4.inducts)
apply(simp_all)
done
lemma pt_trm4_list_plus:
fixes t::trm4
and ts::"trm4 list"
shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
and "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)"
apply(induct t and ts rule: trm4.inducts)
apply(simp_all)
done
instance
apply(default)
apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus)
done
end
(* "repairing" of the permute function *)
lemma repaired:
fixes ts::"trm4 list"
shows "permute_trm4_list p ts = p \<bullet> ts"
apply(induct ts)
apply(simp_all)
done
thm permute_trm4_permute_trm4_list.simps
thm permute_trm4_permute_trm4_list.simps[simplified repaired]
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"
| a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and>
(fv_trm4 t - {atom a})\<sharp>* pi \<and>
(pi \<bullet> t) \<approx>4 s \<and>
(pi \<bullet> a) = b)
\<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)
datatype rtrm5 =
rVr5 "name"
| rAp5 "rtrm5" "rtrm5"
| rLt5 "rlts" "rtrm5"
and rlts =
rLnil
| rLcons "name" "rtrm5" "rlts"
primrec
rbv5
where
"rbv5 rLnil = {}"
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
primrec
rfv_trm5 and rfv_lts
where
"rfv_trm5 (rVr5 n) = {atom n}"
| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - rbv5 lts) \<union> (rfv_lts lts - rbv5 lts)"
| "rfv_lts (rLnil) = {}"
| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
instantiation
rtrm5 and rlts :: pt
begin
primrec
permute_rtrm5 and permute_rlts
where
"permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
| "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)"
| "permute_rlts pi (rLnil) = rLnil"
| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
lemma pt_rtrm5_zero:
fixes t::rtrm5
and l::rlts
shows "0 \<bullet> t = t"
and "0 \<bullet> l = l"
apply(induct t and l rule: rtrm5_rlts.inducts)
apply(simp_all)
done
lemma pt_rtrm5_plus:
fixes t::rtrm5
and l::rlts
shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
and "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
apply(induct t and l rule: rtrm5_rlts.inducts)
apply(simp_all)
done
instance
apply default
apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
done
end
inductive
alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
and
alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
where
a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
| a3: "\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
(rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
(pi \<bullet> (rbv5 l1) = rbv5 l2))
\<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
| a4: "rLnil \<approx>l rLnil"
| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
print_theorems
lemma alpha5_inj:
"((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
"(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
"(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
(rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
(pi \<bullet> (rbv5 l1) = rbv5 l2)))"
"rLnil \<approx>l rLnil"
"(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"
apply -
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alpha5.cases)
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alpha5.cases)
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alpha5.cases)
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alphalts.cases)
apply (simp_all add: alpha5_alphalts.intros)
done
lemma alpha5_equivps:
shows "equivp alpha5"
and "equivp alphalts"
sorry
quotient_type
trm5 = rtrm5 / alpha5
and
lts = rlts / alphalts
by (auto intro: alpha5_equivps)
quotient_definition
"Vr5 :: name \<Rightarrow> trm5"
as
"rVr5"
quotient_definition
"Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
as
"rAp5"
quotient_definition
"Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
as
"rLt5"
quotient_definition
"Lnil :: lts"
as
"rLnil"
quotient_definition
"Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
as
"rLcons"
quotient_definition
"fv_trm5 :: trm5 \<Rightarrow> atom set"
as
"rfv_trm5"
quotient_definition
"fv_lts :: lts \<Rightarrow> atom set"
as
"rfv_lts"
quotient_definition
"bv5 :: lts \<Rightarrow> atom set"
as
"rbv5"
lemma alpha5_rfv:
"(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
"(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
apply(induct rule: alpha5_alphalts.inducts)
apply(simp_all add: alpha_gen)
apply(erule conjE)+
apply(erule exE)
apply(erule conjE)+
apply simp
done
lemma [quot_respect]:
"(op = ===> alpha5 ===> alpha5) permute permute"
"(op = ===> alphalts ===> alphalts) permute permute"
"(op = ===> alpha5) rVr5 rVr5"
"(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
"(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
"(alphalts ===> op =) rfv_lts rfv_lts"
"(alphalts ===> op =) rbv5 rbv5"
sorry
instantiation trm5 and lts :: pt
begin
quotient_definition
"permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
as
"permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
quotient_definition
"permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
as
"permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
lemma permute_trm5_lts:
"pi \<bullet> (Vr5 a) = Vr5 (pi \<bullet> a)"
"pi \<bullet> (Ap5 t1 t2) = Ap5 (pi \<bullet> t1) (pi \<bullet> t2)"
"pi \<bullet> (Lt5 ls t) = Lt5 (pi \<bullet> ls) (pi \<bullet> t)"
"pi \<bullet> Lnil = Lnil"
"pi \<bullet> (Lcons n t ls) = Lcons (pi \<bullet> n) (pi \<bullet> t) (pi \<bullet> ls)"
by (lifting permute_rtrm5_permute_rlts.simps)
lemma trm5_lts_zero:
"0 \<bullet> (x\<Colon>trm5) = x"
"0 \<bullet> (y\<Colon>lts) = y"
sorry
lemma trm5_lts_plus:
"(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
"(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
sorry
instance
apply default
apply (simp_all add: trm5_lts_zero trm5_lts_plus)
done
end
lemma alpha5_INJ:
"((Vr5 a) = (Vr5 b)) = (a = b)"
"(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)"
"(Lt5 l1 t1 = Lt5 l2 t2) =
(\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2) \<and>
(bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2) \<and>
(pi \<bullet> (bv5 l1) = bv5 l2)))"
"Lnil = Lnil"
"(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (ls1 = ls2 \<and> t1 = t2 \<and> n1 = n2)"
unfolding alpha_gen
apply(lifting alpha5_inj[unfolded alpha_gen])
done
lemma bv5[simp]:
"bv5 Lnil = {}"
"bv5 (Lcons n t ltl) = {atom n} \<union> bv5 ltl"
by (lifting rbv5.simps)
lemma fv_trm5_lts[simp]:
"fv_trm5 (Vr5 n) = {atom n}"
"fv_trm5 (Ap5 t s) = fv_trm5 t \<union> fv_trm5 s"
"fv_trm5 (Lt5 lts t) = fv_trm5 t - bv5 lts \<union> (fv_lts lts - bv5 lts)"
"fv_lts Lnil = {}"
"fv_lts (Lcons n t ltl) = fv_trm5 t \<union> fv_lts ltl"
by (lifting rfv_trm5_rfv_lts.simps)
lemma lets_ok:
"(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
apply (subst alpha5_INJ)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
apply (simp only: alpha_gen)
apply (simp add: permute_trm5_lts)
sorry
end