--- a/Nominal/Ex/Foo2.thy Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/Ex/Foo2.thy Thu Dec 23 00:46:06 2010 +0000
@@ -24,10 +24,6 @@
"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
@@ -39,6 +35,7 @@
thm foo.induct
thm foo.inducts
thm foo.exhaust
+thm foo.strong_exhaust
thm foo.fv_defs
thm foo.bn_defs
thm foo.perm_simps
@@ -50,308 +47,6 @@
thm foo.supp
thm foo.fresh
-lemma at_set_avoiding5:
- assumes "finite xs"
- and "finite (supp c)"
- shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
-using assms
-apply(erule_tac c="c" in at_set_avoiding)
-apply(auto)
-done
-
-
-lemma Abs_rename_lst3:
- fixes x::"'a::fs"
- assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)"
- shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
-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>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
- using * ** by metis
-qed
-
-
-lemma
- fixes c::"'a::fs"
- assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
- shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
- supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-thm Abs_rename_lst
-apply(insert Abs_rename_lst)[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_lst)[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(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(rule a)
-apply(assumption)
-apply(simp only: foo.eq_iff)
-apply(perm_simp add: foo.permute_bn)
-apply(rule conjI)
-apply(rule refl)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule foo.perm_bn_alpha)
-done
-
-lemma
- fixes c::"'a::fs"
- assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
- shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
- supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(insert Abs_rename_lst3)[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_lst3)[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(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(erule conjE)+
-apply(simp add: foo.permute_bn)
-apply(rule a)
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) only: foo.eq_iff)
-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)
-done
-
-
-lemma
- fixes c::"'a::fs"
- assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
- shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
- supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt)
-apply(rule a)
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) only: foo.eq_iff)
-apply(rule conjI)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(simp (no_asm_use) add: fresh_star_def)
-apply(simp (no_asm_use) add: Abs_fresh_iff)[1]
-apply(rule ballI)
-apply(auto simp add: fresh_Pair)[1]
-apply(simp (no_asm_use) only: permute_Abs)
-apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt)
-apply(simp)
-apply(rule at_set_avoiding5)
-apply(simp add: multi_recs.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(rule finite_sets_supp)
-apply(simp add: multi_recs.bn_finite)
-done
-
-
-
-lemma test6:
- 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 "\<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(assumption)
-apply(rule assms(2))
-apply(assumption)
-(* lam case *)
-apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
-apply(erule exE)
-apply(insert Abs_rename_lst)[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 add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base)
-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(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(insert Abs_rename_lst)[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_lst)[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(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(rule assms(4))
-apply(assumption)
-apply(simp add: foo.eq_iff refl)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-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
@@ -362,15 +57,15 @@
\<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)"
+ \<lbrakk>({atom n1} \<union> {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(rule_tac y="trm" and c="c" in foo.strong_exhaust(1))
apply(simp_all)[5]
- apply(rule_tac y="assg" in foo.exhaust(2))
+ apply(rule_tac ya="assg" in foo.strong_exhaust(2))
apply(simp_all)[2]
apply(relation "measure (sum_case (size o snd) (size o snd))")
apply(simp_all add: foo.size)