theory NoneExamplesimports "../Nominal2"begintext {* These examples are not covered by our binding specification.*}atom_decl nametext {* "Weirdo" example from Peter Sewell's bestiary. p2 occurs in two bodies*}(*nominal_datatype weird = Foo_var "name"| Foo_pair "weird" "weird" | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" binds x in p1 p2, binds y in p2 p3*)text {* This example binds bound names and therefore the fv-function is not respectful - the proof just fails.*}(*nominal_datatype trm = Var "name"| Lam x::"name" t::"trm" binds x in t| Let left::"trm" right::"trm" binds (set) "bv left" in rightbinder bvwhere "bv (Var n) = {}"| "bv (Lam n t) = {atom n} \<union> bv t"| "bv (Let l r) = bv l \<union> bv r"*)text {* This example uses "-" in the binding function; at the moment this is unsupported *}(*nominal_datatype trm' = Var "name"| Lam l::"name" r::"trm'" binds l in r| Let l::"trm'" r::"trm'" binds (set) "bv' l" in rbinder bv'where "bv' (Var n) = {atom n}"| "bv' (Lam n t) = bv' t - {atom n}"| "bv' (Let l r) = bv' l \<union> bv' r"*)text {* Again this example binds bound names - so is not respectful*}(*nominal_datatype trm = Var "name"| Lam n::"name" l::"trm" binds n in land bla = Bla f::"trm" s::"trm" binds (set) "bv f" in sbinder bv :: "trm \<Rightarrow> atom set"where "bv (Var x) = {}"| "bv (Lam x b) = {atom x}"*)text {* This example has mal-formed deep recursive binders. - Bla1: recursive deep binder used twice - Bla2: deep binder used recursively and non-recursively - Bla3: x used in recursive deep binder and somewhere else*}(*nominal_datatype trm = Var "name"and bla = App "trm" "trm"| Bla1 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1 f, binds "bv f" in s2 f| Bla2 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1, binds "bv f" in s2 f| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" binds "bv f" x in s1 f, binds y x in s2 binder bv :: "trm \<Rightarrow> atom list"where "bv (Var a) = [atom a]"*)end