theory Foo2+ −
imports "../Nominal2" + −
begin+ −
+ −
(* + −
Contrived example that has more than one+ −
binding clause+ −
*)+ −
+ −
atom_decl name+ −
+ −
nominal_datatype foo: trm =+ −
Var "name"+ −
| App "trm" "trm"+ −
| Lam x::"name" t::"trm" bind x in t+ −
| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2+ −
| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2+ −
and assg =+ −
As_Nil+ −
| As "name" x::"name" t::"trm" "assg" + −
binder+ −
bn::"assg \<Rightarrow> atom list"+ −
where+ −
"bn (As x y t a) = [atom x] @ bn a"+ −
| "bn (As_Nil) = []"+ −
+ −
thm foo.bn_defs+ −
thm foo.permute_bn+ −
thm foo.perm_bn_alpha+ −
thm foo.perm_bn_simps+ −
thm foo.bn_finite+ −
+ −
thm foo.distinct+ −
thm foo.induct+ −
thm foo.inducts+ −
thm foo.exhaust+ −
thm foo.fv_defs+ −
thm foo.bn_defs+ −
thm foo.perm_simps+ −
thm foo.eq_iff(5)+ −
thm foo.fv_bn_eqvt+ −
thm foo.size_eqvt+ −
thm foo.supports+ −
thm foo.fsupp+ −
thm foo.supp+ −
thm foo.fresh+ −
+ −
text {*+ −
tests by cu+ −
*}+ −
+ −
lemma set_renaming_perm:+ −
assumes a: "p \<bullet> bs \<inter> bs = {}" + −
and b: "finite bs"+ −
shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"+ −
using b a+ −
proof (induct)+ −
case empty+ −
have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"+ −
by (simp add: permute_set_eq supp_perm)+ −
then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast+ −
next+ −
case (insert a bs)+ −
then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" + −
by (perm_simp) (auto)+ −
then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast + −
{ assume 1: "q \<bullet> a = p \<bullet> a"+ −
have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)+ −
moreover + −
have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" + −
using ** by (auto simp add: insert_eqvt)+ −
ultimately + −
have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast+ −
}+ −
moreover+ −
{ assume 2: "q \<bullet> a \<noteq> p \<bullet> a"+ −
def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"+ −
{ have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)+ −
moreover + −
have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)+ −
ultimately + −
have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def + −
by (simp add: insert_eqvt swap_set_not_in) + −
}+ −
moreover + −
{ have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"+ −
using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`+ −
by (auto simp add: supp_perm insert_eqvt)+ −
then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)+ −
moreover+ −
have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" + −
using ** by (auto simp add: insert_eqvt)+ −
ultimately + −
have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" + −
unfolding q'_def using supp_plus_perm by blast+ −
}+ −
ultimately + −
have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast+ −
}+ −
ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"+ −
by blast+ −
qed+ −
+ −
+ −
lemma Abs_rename_set:+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" + −
and b: "finite bs"+ −
shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"+ −
proof -+ −
from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) + −
with set_renaming_perm + −
obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis+ −
have "[bs]set. x = q \<bullet> ([bs]set. x)"+ −
apply(rule perm_supp_eq[symmetric])+ −
using a **+ −
unfolding fresh_star_Pair+ −
unfolding Abs_fresh_star_iff+ −
unfolding fresh_star_def+ −
by auto+ −
also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp+ −
also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp+ −
finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" .+ −
then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast+ −
qed+ −
+ −
lemma Abs_rename_res:+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" + −
and b: "finite bs"+ −
shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"+ −
proof -+ −
from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) + −
with set_renaming_perm + −
obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis+ −
have "[bs]res. x = q \<bullet> ([bs]res. x)"+ −
apply(rule perm_supp_eq[symmetric])+ −
using a **+ −
unfolding fresh_star_Pair+ −
unfolding Abs_fresh_star_iff+ −
unfolding fresh_star_def+ −
by auto+ −
also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp+ −
also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp+ −
finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" .+ −
then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast+ −
qed+ −
+ −
lemma list_renaming_perm:+ −
fixes bs::"atom list"+ −
assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}"+ −
shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"+ −
using a+ −
proof (induct bs)+ −
case Nil+ −
have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"+ −
by (simp add: permute_set_eq supp_perm)+ −
then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast+ −
next+ −
case (Cons a bs)+ −
then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" + −
by (perm_simp) (auto)+ −
then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast + −
{ assume 1: "a \<in> set bs"+ −
have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)+ −
then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp + −
moreover + −
have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)+ −
ultimately + −
have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast+ −
}+ −
moreover+ −
{ assume 2: "a \<notin> set bs"+ −
def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"+ −
{ have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] + −
by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)+ −
moreover + −
have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` + −
by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)+ −
ultimately + −
have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def + −
by (simp add: swap_fresh_fresh) + −
}+ −
moreover + −
{ have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"+ −
using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`+ −
by (auto simp add: supp_perm insert_eqvt)+ −
then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)+ −
moreover+ −
have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" + −
using ** by (auto simp add: insert_eqvt)+ −
ultimately + −
have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" + −
unfolding q'_def using supp_plus_perm by blast+ −
}+ −
ultimately + −
have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast+ −
}+ −
ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"+ −
by blast+ −
qed+ −
+ −
+ −
lemma Abs_rename_list:+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" + −
shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"+ −
proof -+ −
from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter + −
by (simp add: fresh_star_Pair fresh_star_set)+ −
with list_renaming_perm + −
obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis + −
have "[bs]lst. x = q \<bullet> ([bs]lst. x)"+ −
apply(rule perm_supp_eq[symmetric])+ −
using a **+ −
unfolding fresh_star_Pair+ −
unfolding Abs_fresh_star_iff+ −
unfolding fresh_star_def+ −
by auto+ −
also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp+ −
also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp+ −
finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .+ −
then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast+ −
qed+ −
+ −
(*+ −
thm at_set_avoiding1[THEN exE]+ −
+ −
+ −
lemma Let1_rename:+ −
fixes c::"'a::fs"+ −
shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and> Lam name trm = Lam name' trm'"+ −
apply(simp only: foo.eq_iff)+ −
apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE])+ −
apply(simp)+ −
apply(simp add: finite_supp)+ −
apply(perm_simp)+ −
apply(rule Abs_rename_list[THEN exE])+ −
apply(simp only: set_eqvt)+ −
apply+ −
sorry + −
*)+ −
+ −
lemma test6:+ −
fixes c::"'a::fs"+ −
assumes "\<exists>name. y = Var name \<Longrightarrow> P" + −
and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"+ −
and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" + −
and "\<exists>a1 trm1 a2 trm2. ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"+ −
and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"+ −
shows "P"+ −
apply(rule_tac y="y" in foo.exhaust(1))+ −
apply(rule assms(1))+ −
apply(rule exI)++ −
apply(assumption)+ −
apply(rule assms(2))+ −
apply(rule exI)++ −
apply(assumption)+ −
(* lam case *)+ −
(*+ −
apply(rule Let1_rename)+ −
apply(rule assms(3))+ −
apply(assumption)+ −
apply(simp)+ −
*)+ −
+ −
apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")+ −
apply(erule exE)+ −
apply(insert Abs_rename_list)[1]+ −
apply(drule_tac x="p" in meta_spec)+ −
apply(drule_tac x="[atom name]" in meta_spec)+ −
apply(drule_tac x="trm" in meta_spec)+ −
apply(simp only: fresh_star_Pair set.simps)+ −
apply(drule meta_mp)+ −
apply(simp)+ −
apply(erule exE)+ −
apply(rule assms(3))+ −
apply(perm_simp)+ −
apply(erule conjE)++ −
apply(assumption)+ −
apply(clarify)+ −
apply(simp (no_asm) add: foo.eq_iff)+ −
apply(perm_simp)+ −
apply(assumption)+ −
apply(rule at_set_avoiding1)+ −
apply(simp)+ −
apply(simp add: finite_supp)+ −
(* let1 case *)+ −
apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")+ −
apply(erule exE)+ −
apply(rule assms(4))+ −
apply(simp only: foo.eq_iff)+ −
apply(insert Abs_rename_list)[1]+ −
apply(drule_tac x="p" in meta_spec)+ −
apply(drule_tac x="bn assg1" in meta_spec)+ −
apply(drule_tac x="trm1" in meta_spec)+ −
apply(insert Abs_rename_list)[1]+ −
apply(drule_tac x="p" in meta_spec)+ −
apply(drule_tac x="bn assg2" in meta_spec)+ −
apply(drule_tac x="trm2" in meta_spec)+ −
apply(drule meta_mp)+ −
apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)+ −
apply(drule meta_mp)+ −
apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)+ −
apply(erule exE)++ −
apply(rule exI)++ −
apply(perm_simp add: foo.permute_bn)+ −
apply(rule conjI)+ −
apply(simp add: fresh_star_Pair fresh_star_Un)+ −
apply(erule conjE)++ −
apply(rule conjI)+ −
apply(assumption)+ −
apply(rotate_tac 4)+ −
apply(assumption)+ −
apply(rule conjI)+ −
apply(assumption)+ −
apply(rule conjI)+ −
apply(rule foo.perm_bn_alpha)+ −
apply(rule conjI)+ −
apply(assumption)+ −
apply(rule foo.perm_bn_alpha)+ −
apply(rule at_set_avoiding1)+ −
apply(simp)+ −
apply(simp add: finite_supp)+ −
(* let2 case *)+ −
apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")+ −
apply(erule exE)+ −
apply(rule assms(5))+ −
apply(simp only:)+ −
apply(simp only: foo.eq_iff)+ −
apply(insert Abs_rename_list)[1]+ −
apply(drule_tac x="p" in meta_spec)+ −
apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec)+ −
apply(drule_tac x="trm1" in meta_spec)+ −
apply(insert Abs_rename_list)[1]+ −
apply(drule_tac x="p" in meta_spec)+ −
apply(drule_tac x="[atom name2]" in meta_spec)+ −
apply(drule_tac x="trm2" in meta_spec)+ −
apply(drule meta_mp)+ −
apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp)+ −
apply(auto)[1]+ −
apply(perm_simp)+ −
apply(auto simp add: fresh_star_def)[1]+ −
apply(perm_simp)+ −
apply(auto simp add: fresh_star_def)[1]+ −
apply(perm_simp)+ −
apply(auto simp add: fresh_star_def)[1]+ −
apply(drule meta_mp)+ −
apply(perm_simp)+ −
apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]+ −
apply(erule exE)++ −
apply(rule exI)++ −
apply(perm_simp add: foo.permute_bn)+ −
apply(rule conjI)+ −
prefer 2+ −
apply(rule conjI)+ −
apply(assumption)+ −
apply(assumption)+ −
apply(simp add: fresh_star_Pair)+ −
apply(simp add: fresh_star_def)+ −
apply(rule at_set_avoiding1)+ −
apply(simp)+ −
apply(simp add: finite_supp)+ −
done+ −
+ −
lemma test5:+ −
fixes c::"'a::fs"+ −
assumes "\<And>name. y = Var name \<Longrightarrow> P" + −
and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"+ −
and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" + −
and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P"+ −
and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"+ −
shows "P"+ −
apply(rule_tac y="y" in test6)+ −
apply(erule exE)++ −
apply(rule assms(1))+ −
apply(assumption)+ −
apply(erule exE)++ −
apply(rule assms(2))+ −
apply(assumption)+ −
apply(rule assms(3))+ −
apply(auto)[2]+ −
apply(erule exE)++ −
apply(rule assms(4))+ −
apply(auto)[2]+ −
apply(erule exE)++ −
apply(rule assms(5))+ −
apply(auto)[2]+ −
done+ −
+ −
+ −
lemma strong_induct:+ −
fixes c :: "'a :: fs"+ −
and assg :: assg and trm :: trm+ −
assumes a0: "\<And>name c. P1 c (Var name)"+ −
and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"+ −
and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"+ −
and a3: "\<And>a1 t1 a2 t2 c. + −
\<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk> + −
\<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)"+ −
and a4: "\<And>n1 n2 t1 t2 c. + −
\<lbrakk>{atom n1, atom n2} \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)"+ −
and a5: "\<And>c. P2 c As_Nil"+ −
and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"+ −
shows "P1 c trm" "P2 c assg"+ −
using assms+ −
apply(induction_schema)+ −
apply(rule_tac y="trm" and c="c" in test5)+ −
apply(simp_all)[5]+ −
apply(rule_tac y="assg" in foo.exhaust(2))+ −
apply(simp_all)[2]+ −
apply(relation "measure (sum_case (size o snd) (size o snd))")+ −
apply(simp_all add: foo.size)+ −
done+ −
+ −
end+ −
+ −
+ −
+ −