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.strong_induct+ −
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.size+ −
+ −
+ −
end+ −
+ −
+ −
+ −