theory Foo1
imports "../Nominal2" 
begin

text {* 
  Contrived example that has more than one
  binding function
*}


atom_decl name

nominal_datatype foo: trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"  bind x in t
| Let1 a::"assg" t::"trm"  bind "bn1 a" in t
| Let2 a::"assg" t::"trm"  bind "bn2 a" in t
| Let3 a::"assg" t::"trm"  bind "bn3 a" in t
| Let4 a::"assg'" t::"trm"  bind (set) "bn4 a" in t
and assg =
  As "name" "name" "trm"
and assg' =
  BNil
| BAs "name" "assg'"
binder
  bn1::"assg \<Rightarrow> atom list" and
  bn2::"assg \<Rightarrow> atom list" and
  bn3::"assg \<Rightarrow> atom list" and
  bn4::"assg' \<Rightarrow> atom set"
where
  "bn1 (As x y t) = [atom x]"
| "bn2 (As x y t) = [atom y]"
| "bn3 (As x y t) = [atom x, atom y]"
| "bn4 (BNil) = {}"
| "bn4 (BAs a as) = {atom a} \<union> bn4 as"

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.strong_exhaust
thm foo.fv_defs
thm foo.bn_defs
thm foo.perm_simps
thm foo.eq_iff
thm foo.fv_bn_eqvt
thm foo.size_eqvt
thm foo.supports
thm foo.fsupp
thm foo.supp
thm foo.fresh
thm foo.bn_finite

lemma 
  fixes t::trm
  and   as::assg
  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>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" 
  and     a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"
  and     a9: "\<And>c. P3 c (BNil)"
  and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"
  shows "P1 c t" "P2 c as" "P3 c as'"
apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1))
apply(simp_all)[7]
apply(rule_tac ya="as"in foo.strong_exhaust(2))
apply(simp_all)[1]
apply(rule_tac yb="as'" in foo.strong_exhaust(3))
apply(simp_all)[2]
apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))")
apply(simp_all add: foo.size)
done

end