theory LamEx
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"
begin
(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
lemma in_permute_iff:
shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
apply(unfold mem_def permute_fun_def)[1]
apply(simp add: permute_bool_def)
done
lemma fresh_star_permute_iff:
shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
apply(simp add: fresh_star_def)
apply(auto)
apply(drule_tac x="p \<bullet> xa" in bspec)
apply(unfold mem_def permute_fun_def)[1]
apply(simp add: eqvts)
apply(simp add: fresh_permute_iff)
apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
apply(simp)
apply(drule_tac x="- p \<bullet> xa" in bspec)
apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
apply(simp)
apply(simp)
done
lemma fresh_minus_perm:
fixes p::perm
shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
apply(simp add: fresh_def)
apply(simp only: supp_minus_perm)
done
lemma fresh_plus:
fixes p q::perm
shows "\<lbrakk>a \<sharp> p; a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
unfolding fresh_def
using supp_plus_perm
apply(auto)
done
lemma fresh_star_plus:
fixes p q::perm
shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
unfolding fresh_star_def
by (simp add: fresh_plus)
atom_decl name
datatype rlam =
rVar "name"
| rApp "rlam" "rlam"
| rLam "name" "rlam"
fun
rfv :: "rlam \<Rightarrow> atom set"
where
rfv_var: "rfv (rVar a) = {atom a}"
| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
| rfv_lam: "rfv (rLam a t) = (rfv t) - {atom a}"
instantiation rlam :: pt
begin
primrec
permute_rlam
where
"permute_rlam pi (rVar a) = rVar (pi \<bullet> a)"
| "permute_rlam pi (rApp t1 t2) = rApp (permute_rlam pi t1) (permute_rlam pi t2)"
| "permute_rlam pi (rLam a t) = rLam (pi \<bullet> a) (permute_rlam pi t)"
instance
apply default
apply(induct_tac [!] x)
apply(simp_all)
done
end
instantiation rlam :: fs
begin
lemma neg_conj:
"\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
by simp
lemma infinite_Un:
"infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
by simp
instance
apply default
apply(induct_tac x)
(* var case *)
apply(simp add: supp_def)
apply(fold supp_def)[1]
apply(simp add: supp_at_base)
(* app case *)
apply(simp only: supp_def)
apply(simp only: permute_rlam.simps)
apply(simp only: rlam.inject)
apply(simp only: neg_conj)
apply(simp only: Collect_disj_eq)
apply(simp only: infinite_Un)
apply(simp only: Collect_disj_eq)
apply(simp)
(* lam case *)
apply(simp only: supp_def)
apply(simp only: permute_rlam.simps)
apply(simp only: rlam.inject)
apply(simp only: neg_conj)
apply(simp only: Collect_disj_eq)
apply(simp only: infinite_Un)
apply(simp only: Collect_disj_eq)
apply(simp)
apply(fold supp_def)[1]
apply(simp add: supp_at_base)
done
end
(* for the eqvt proof of the alpha-equivalence *)
declare permute_rlam.simps[eqvt]
lemma rfv_eqvt[eqvt]:
shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)"
apply(induct t)
apply(simp_all)
apply(simp add: permute_set_eq atom_eqvt)
apply(simp add: union_eqvt)
apply(simp add: Diff_eqvt)
apply(simp add: permute_set_eq atom_eqvt)
done
inductive
alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
where
a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
\<Longrightarrow> rLam a t \<approx> rLam b s"
text {* should be automatic with new version of eqvt-machinery *}
lemma alpha_eqvt:
shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
apply(induct rule: alpha.induct)
apply(simp add: a1)
apply(simp add: a2)
apply(simp)
apply(rule a3)
apply(erule conjE)
apply(erule exE)
apply(erule conjE)
apply(rule_tac x="pi \<bullet> pia" in exI)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(rule conjI)
apply(subst permute_eqvt[symmetric])
apply(simp)
apply(subst permute_eqvt[symmetric])
apply(simp)
done
lemma alpha_refl:
shows "t \<approx> t"
apply(induct t rule: rlam.induct)
apply(simp add: a1)
apply(simp add: a2)
apply(rule a3)
apply(rule_tac x="0" in exI)
apply(simp_all add: fresh_star_def fresh_zero_perm)
done
lemma alpha_sym:
shows "t \<approx> s \<Longrightarrow> s \<approx> t"
apply(induct rule: alpha.induct)
apply(simp add: a1)
apply(simp add: a2)
apply(rule a3)
apply(erule exE)
apply(rule_tac x="- pi" in exI)
apply(simp)
apply(simp add: fresh_star_def fresh_minus_perm)
apply(rule conjI)
apply(erule conjE)+
apply(rotate_tac 3)
apply(drule_tac pi="- pi" in alpha_eqvt)
apply(simp)
apply(clarify)
apply(simp)
done
lemma alpha_trans:
shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
apply(induct arbitrary: t3 rule: alpha.induct)
apply(erule alpha.cases)
apply(simp_all)
apply(simp add: a1)
apply(rotate_tac 4)
apply(erule alpha.cases)
apply(simp_all)
apply(simp add: a2)
apply(rotate_tac 1)
apply(erule alpha.cases)
apply(simp_all)
apply(erule conjE)+
apply(erule exE)+
apply(erule conjE)+
apply(rule a3)
apply(rule_tac x="pia + pi" in exI)
apply(simp add: fresh_star_plus)
apply(drule_tac x="- pia \<bullet> sa" in spec)
apply(drule mp)
apply(rotate_tac 8)
apply(drule_tac pi="- pia" in alpha_eqvt)
apply(simp)
apply(rotate_tac 11)
apply(drule_tac pi="pia" in alpha_eqvt)
apply(simp)
done
lemma alpha_equivp:
shows "equivp alpha"
apply(rule equivpI)
unfolding reflp_def symp_def transp_def
apply(auto intro: alpha_refl alpha_sym alpha_trans)
done
lemma alpha_rfv:
shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
apply(induct rule: alpha.induct)
apply(simp_all)
done
quotient_type lam = rlam / alpha
by (rule alpha_equivp)
quotient_definition
"Var :: name \<Rightarrow> lam"
as
"rVar"
quotient_definition
"App :: lam \<Rightarrow> lam \<Rightarrow> lam"
as
"rApp"
quotient_definition
"Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
as
"rLam"
quotient_definition
"fv :: lam \<Rightarrow> atom set"
as
"rfv"
lemma perm_rsp[quot_respect]:
"(op = ===> alpha ===> alpha) permute permute"
apply(auto)
apply(rule alpha_eqvt)
apply(simp)
done
lemma rVar_rsp[quot_respect]:
"(op = ===> alpha) rVar rVar"
by (auto intro: a1)
lemma rApp_rsp[quot_respect]:
"(alpha ===> alpha ===> alpha) rApp rApp"
by (auto intro: a2)
lemma rLam_rsp[quot_respect]:
"(op = ===> alpha ===> alpha) rLam rLam"
apply(auto)
apply(rule a3)
apply(rule_tac x="0" in exI)
unfolding fresh_star_def
apply(simp add: fresh_star_def fresh_zero_perm)
apply(simp add: alpha_rfv)
done
lemma rfv_rsp[quot_respect]:
"(alpha ===> op =) rfv rfv"
apply(simp add: alpha_rfv)
done
section {* lifted theorems *}
lemma lam_induct:
"\<lbrakk>\<And>name. P (Var name);
\<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
\<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk>
\<Longrightarrow> P lam"
apply (lifting rlam.induct)
done
instantiation lam :: pt
begin
quotient_definition
"permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam"
as
"permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam"
lemma permute_lam [simp]:
shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
apply(lifting permute_rlam.simps)
done
instance
apply default
apply(induct_tac [!] x rule: lam_induct)
apply(simp_all)
done
end
lemma fv_lam [simp]:
shows "fv (Var a) = {atom a}"
and "fv (App t1 t2) = fv t1 \<union> fv t2"
and "fv (Lam a t) = fv t - {atom a}"
apply(lifting rfv_var rfv_app rfv_lam)
done
lemma a1:
"a = b \<Longrightarrow> Var a = Var b"
by (lifting a1)
lemma a2:
"\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
by (lifting a2)
lemma a3:
"\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk>
\<Longrightarrow> Lam a t = Lam b s"
apply (lifting a3)
done
lemma alpha_cases:
"\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
\<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
\<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s;
\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk>
\<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (lifting alpha.cases)
(* not sure whether needed *)
lemma alpha_induct:
"\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
\<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
\<And>t a s b.
\<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and>
(fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk>
\<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
\<Longrightarrow> qxb qx qxa"
by (lifting alpha.induct)
(* should they lift automatically *)
lemma lam_inject [simp]:
shows "(Var a = Var b) = (a = b)"
and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
apply(lifting rlam.inject(1) rlam.inject(2))
apply(regularize)
prefer 2
apply(regularize)
prefer 2
apply(auto)
apply(drule alpha.cases)
apply(simp_all)
apply(simp add: alpha.a1)
apply(drule alpha.cases)
apply(simp_all)
apply(drule alpha.cases)
apply(simp_all)
apply(rule alpha.a2)
apply(simp_all)
done
lemma rlam_distinct:
shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
and "\<not>(rVar nam \<approx> rLam nam' rlam')"
and "\<not>(rLam nam' rlam' \<approx> rVar nam)"
and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
apply auto
apply (erule alpha.cases)
apply (simp_all only: rlam.distinct)
apply (erule alpha.cases)
apply (simp_all only: rlam.distinct)
apply (erule alpha.cases)
apply (simp_all only: rlam.distinct)
apply (erule alpha.cases)
apply (simp_all only: rlam.distinct)
apply (erule alpha.cases)
apply (simp_all only: rlam.distinct)
apply (erule alpha.cases)
apply (simp_all only: rlam.distinct)
done
lemma lam_distinct[simp]:
shows "Var nam \<noteq> App lam1' lam2'"
and "App lam1' lam2' \<noteq> Var nam"
and "Var nam \<noteq> Lam nam' lam'"
and "Lam nam' lam' \<noteq> Var nam"
and "App lam1 lam2 \<noteq> Lam nam' lam'"
and "Lam nam' lam' \<noteq> App lam1 lam2"
apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
done
lemma var_supp1:
shows "(supp (Var a)) = (supp a)"
apply (simp add: supp_def)
done
lemma var_supp:
shows "(supp (Var a)) = {a:::name}"
using var_supp1 by (simp add: supp_at_base)
lemma app_supp:
shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"
apply(simp only: permute_lam supp_def lam_inject)
apply(simp add: Collect_imp_eq Collect_neg_eq)
done
(* needs thinking *)
lemma lam_supp1:
shows "(supp (atom x, t)) supports (Lam 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 lam_fsupp1:
assumes a: "finite (supp t)"
shows "finite (supp (Lam x t))"
apply(rule supports_finite)
apply(rule lam_supp1)
apply(simp add: a supp_Pair supp_atom)
done
instance lam :: fs
apply(default)
apply(induct_tac x rule: lam_induct)
apply(simp add: var_supp)
apply(simp add: app_supp)
apply(simp add: lam_fsupp1)
done
lemma lam_fresh1:
assumes f: "finite (supp t)"
and a1: "b \<sharp> t"
and a2: "atom a \<noteq> b"
shows "b \<sharp> Lam a t"
proof -
have "\<exists>c. c \<sharp> (b, a ,t, Lam a t)" sorry
then obtain c where fr1: "c \<noteq> b"
and fr2: "c \<noteq> atom a"
and fr3: "c \<sharp> t"
and fr4: "c \<sharp> Lam a t"
and fr5: "sort_of b = sort_of c"
apply(auto simp add: fresh_Pair fresh_atom)
sorry
have e: "(c \<rightleftharpoons> b) \<bullet> (Lam a t) = Lam a ((c \<rightleftharpoons> b) \<bullet> t)" using a2 fr1 fr2
by simp
from fr4 have "((c \<rightleftharpoons> b) \<bullet>c) \<sharp> ((c \<rightleftharpoons> b) \<bullet>(Lam a t))"
by (simp only: fresh_permute_iff)
then have "b \<sharp> (Lam a ((c \<rightleftharpoons> b) \<bullet> t))" using fr1 fr2 fr5 e
by simp
then show ?thesis using a1 fr3
by (simp only: swap_fresh_fresh)
qed
lemma lam_fresh2:
assumes f: "finite (supp t)"
shows "(atom a) \<sharp> Lam a t"
sorry
lemma lam_supp:
shows "supp (Lam x t) = ((supp t) - {atom x})"
apply(default)
apply(simp_all add: supp_conv_fresh)
apply(auto)
sorry
lemma fresh_lam:
"(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)"
apply(simp add: fresh_def)
apply(simp add: lam_supp)
apply(auto)
done
lemma lam_induct_strong:
fixes a::"'a::fs"
assumes a1: "\<And>name b. P b (Var name)"
and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)"
and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
shows "P a lam"
proof -
have "\<And>pi a. P a (pi \<bullet> lam)"
proof (induct lam rule: lam_induct)
case (1 name pi)
show "P a (pi \<bullet> Var name)"
apply (simp)
apply (rule a1)
done
next
case (2 lam1 lam2 pi)
have b1: "\<And>pi a. P a (pi \<bullet> lam1)" by fact
have b2: "\<And>pi a. P a (pi \<bullet> lam2)" by fact
show "P a (pi \<bullet> App lam1 lam2)"
apply (simp)
apply (rule a2)
apply (rule b1)
apply (rule b2)
done
next
case (3 name lam pi a)
have b: "\<And>pi a. P a (pi \<bullet> lam)" by fact
obtain c::name where fr: "atom c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)"
apply(rule obtain_atom)
apply(auto)
sorry
from b fr have p: "P a (Lam c (((c \<leftrightarrow> (pi \<bullet> name)) + pi)\<bullet>lam))"
apply -
apply(rule a3)
apply(blast)
apply(simp add: fresh_Pair)
done
have eq: "(atom c \<rightleftharpoons> atom (pi\<bullet>name)) \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)"
apply(rule swap_fresh_fresh)
using fr
apply(simp add: fresh_lam fresh_Pair)
apply(simp add: fresh_lam fresh_Pair)
done
show "P a (pi \<bullet> Lam name lam)"
apply (simp)
apply(subst eq[symmetric])
using p
apply(simp only: permute_lam)
apply(simp add: flip_def)
done
qed
then have "P a (0 \<bullet> lam)" by blast
then show "P a lam" by simp
qed
lemma var_fresh:
fixes a::"name"
shows "(atom a \<sharp> (Var b)) = (atom a \<sharp> b)"
apply(simp add: fresh_def)
apply(simp add: var_supp1)
done
end