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.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

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} \<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 foo.strong_exhaust(1))
  apply(simp_all)[5]
  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)
  done

end