--- a/Nominal/Ex/Foo1.thy	Wed Sep 29 06:45:01 2010 -0400
+++ b/Nominal/Ex/Foo1.thy	Wed Sep 29 09:47:26 2010 -0400
@@ -42,6 +42,238 @@
 thm foo.supp
 thm foo.fresh
 
+primrec
+  permute_bn1_raw
+where
+  "permute_bn1_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
+
+primrec
+  permute_bn2_raw
+where
+  "permute_bn2_raw p (As_raw x y t) = As_raw x (p \<bullet> y) t"
+
+primrec
+  permute_bn3_raw
+where
+  "permute_bn3_raw p (As_raw x y t) = As_raw (p \<bullet> x) (p \<bullet> y) t"
+
+quotient_definition
+  "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg"
+is
+  "permute_bn1_raw"
+
+quotient_definition
+  "permute_bn2 :: perm \<Rightarrow> assg \<Rightarrow> assg"
+is
+  "permute_bn2_raw"
+
+quotient_definition
+  "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg"
+is
+  "permute_bn3_raw"
+
+lemma [quot_respect]: 
+  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_assg_raw.cases)
+  apply simp_all
+  apply (rule foo.raw_alpha)
+  apply simp_all
+  done
+
+lemma [quot_respect]: 
+  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_assg_raw.cases)
+  apply simp_all
+  apply (rule foo.raw_alpha)
+  apply simp_all
+  done
+
+lemma [quot_respect]: 
+  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_assg_raw.cases)
+  apply simp_all
+  apply (rule foo.raw_alpha)
+  apply simp_all
+  done
+
+lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
+lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]
+lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted]
+
+lemma uu1:
+  shows "alpha_bn1 as (permute_bn1 p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[6]
+apply(simp add: permute_bn1)
+apply(simp add: foo.eq_iff)
+done
+
+lemma uu2:
+  shows "alpha_bn2 as (permute_bn2 p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[6]
+apply(simp add: permute_bn2)
+apply(simp add: foo.eq_iff)
+done
+
+lemma uu3:
+  shows "alpha_bn3 as (permute_bn3 p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[6]
+apply(simp add: permute_bn3)
+apply(simp add: foo.eq_iff)
+done
+
+lemma tt1:
+  shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[6]
+apply(simp add: permute_bn1 foo.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+lemma tt2:
+  shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[6]
+apply(simp add: permute_bn2 foo.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+lemma tt3:
+  shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[6]
+apply(simp add: permute_bn3 foo.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+
+lemma strong_exhaust1:
+  fixes c::"'a::fs"
+  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>assn trm ca. \<lbrakk>set (bn1 assn) \<sharp>* ca; c = ca; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>assn trm ca. \<lbrakk>set (bn2 assn) \<sharp>* ca; c = ca; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>assn trm ca. \<lbrakk>set (bn3 assn) \<sharp>* ca; c = ca; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in foo.exhaust(1))
+apply(rule assms(1))
+apply(auto)[2]
+apply(rule assms(2))
+apply(auto)[2]
+apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(3))
+apply(perm_simp)
+apply(assumption)
+apply(rule refl)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: foo.fresh fresh_star_def)
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(4))
+apply(simp add: set_eqvt)
+apply(simp add: tt1)
+apply(rule refl)
+apply(simp)
+apply(simp add: foo.eq_iff)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+apply(simp add: tt1 uu1)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: Abs_fresh_star)
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(5))
+apply(simp add: set_eqvt)
+apply(simp add: tt2)
+apply(rule refl)
+apply(simp)
+apply(simp add: foo.eq_iff)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+apply(simp add: tt2 uu2)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: Abs_fresh_star)
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(6))
+apply(simp add: set_eqvt)
+apply(simp add: tt3)
+apply(rule refl)
+apply(simp)
+apply(simp add: foo.eq_iff)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+apply(simp add: tt3 uu3)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: Abs_fresh_star)
+done
+
+thm foo.exhaust
+
+lemma strong_exhaust2:
+  assumes "\<And>x y t ca. \<lbrakk>c = ca; as = As x y t\<rbrakk> \<Longrightarrow> P" 
+  shows "P"
+apply(rule_tac y="as" in foo.exhaust(2))
+apply(rule assms(1))
+apply(auto)[2]
+done
+
+
+lemma 
+  fixes t::trm
+  and   as::assg
+  and   c::"'a::fs"
+  assumes a1: "\<And>x c. P1 c (Var x)"
+  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
+  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
+  and     a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)"
+  and     a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)"
+  and     a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)"
+  and     a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"
+  shows "P1 c t" "P2 c as"
+using assms
+apply(induction_schema)
+apply(rule_tac y="t" in strong_exhaust1)
+apply(blast)
+apply(blast)
+apply(blast)
+apply(blast)
+apply(blast)
+apply(blast)
+apply(rule_tac as="as" in strong_exhaust2)
+apply(blast)
+apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
+apply(auto)[1]
+apply(simp_all add: foo.size)
+done
 
 end