theory Foo1+
−
imports "../Nominal2" +
−
begin+
−
+
−
(* +
−
  Contrived example that has more than one+
−
  binding function for a datatype+
−
*)+
−
+
−
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+
−
and assg =+
−
  As "name" "name" "trm"+
−
binder+
−
  bn1::"assg \<Rightarrow> atom list" and+
−
  bn2::"assg \<Rightarrow> atom list" and+
−
  bn3::"assg \<Rightarrow> atom list"+
−
where+
−
  "bn1 (As x y t) = [atom x]"+
−
| "bn2 (As x y t) = [atom y]"+
−
| "bn3 (As x y t) = [atom x, atom y]"+
−
+
−
thm foo.distinct+
−
thm foo.induct+
−
thm foo.inducts+
−
thm foo.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+
−
+
−
+
−
end+
−
+
−
+
−
+
−