theory Ex1+
−
imports "../Nominal2"+
−
begin+
−
+
−
(* free names in bar are bound in foo *)+
−
+
−
atom_decl name+
−
+
−
nominal_datatype foo =+
−
  Foo0 "name"+
−
| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f+
−
and bar =+
−
  Bar0 "name"+
−
| Bar1 "name" s::"name" b::"bar" bind (set) s in b+
−
binder+
−
  bv+
−
where+
−
  "bv (Bar0 x) = {}"+
−
| "bv (Bar1 v x b) = {atom v}"+
−
+
−
+
−
thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars]+
−
+
−
lemma+
−
  "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"+
−
apply(simp only: foo_bar.fv_defs)+
−
apply(simp only: foo_bar.bn_defs)+
−
apply(simp only: supp_at_base)+
−
apply(simp)+
−
done+
−
+
−
end+
−
+
−
+
−