Nominal/Ex/Ex1.thy
author Christian Urban <urbanc@in.tum.de>
Fri, 10 Sep 2010 09:17:40 +0800
changeset 2475 486d4647bb37
parent 2454 9ffee4eb1ae1
child 2561 7926f1cb45eb
permissions -rw-r--r--
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)

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.distinct
thm foo_bar.induct
thm foo_bar.inducts
thm foo_bar.exhaust
thm foo_bar.fv_defs
thm foo_bar.bn_defs
thm foo_bar.perm_simps
thm foo_bar.eq_iff
thm foo_bar.fv_bn_eqvt
thm foo_bar.size_eqvt
thm foo_bar.supports
thm foo_bar.fsupp
thm foo_bar.supp

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