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" binds x in t+ −
| Let1 a::"assg" t::"trm" binds "bn1 a" in t+ −
| Let2 a::"assg" t::"trm" binds "bn2 a" in t+ −
| Let3 a::"assg" t::"trm" binds "bn3 a" in t+ −
| Let4 a::"assg'" t::"trm" binds (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_induct+ −
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+ −
+ −
+ −
end+ −
+ −
+ −
+ −