theory Foo1imports "../Nominal2" begintext {* Contrived example that has more than one binding function*}atom_decl namenominal_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 tand 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_bnthm foo.perm_bn_alphathm foo.perm_bn_simpsthm foo.bn_finitethm foo.distinctthm foo.inductthm foo.inductsthm foo.exhaustthm foo.strong_inductthm foo.strong_exhaustthm foo.fv_defsthm foo.bn_defsthm foo.perm_simpsthm foo.eq_iffthm foo.fv_bn_eqvtthm foo.size_eqvtthm foo.supportsthm foo.fsuppthm foo.suppthm foo.freshthm foo.bn_finiteend