Mercurial Mercurial > hg > nominal2 / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Ex1rec.thy
author Christian Urban <urbanc@in.tum.de>
Sun, 16 May 2010 12:41:27 +0100 (2010-05-16)
changeset 2142 c39d4fe31100
parent 2120 2786ff1df475
child 2311 4da5c5c29009
permissions -rw-r--r--
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
theory Ex1rec
imports "../NewParser"
begin

atom_decl name

ML {* val _ = cheat_supp_eq := true *}
ML {* val _ = cheat_equivp := true *}

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" t::"lam"  bind_set x in t
| Let bp::"bp" t::"lam"   bind_set "bi bp" in bp t
and bp =
  Bp "name" "lam"
binder
  bi::"bp \<Rightarrow> atom set"
where
  "bi (Bp x t) = {atom x}"

thm lam_bp.fv
thm lam_bp.eq_iff[no_vars]
thm lam_bp.bn
thm lam_bp.perm
thm lam_bp.induct
thm lam_bp.inducts
thm lam_bp.distinct
thm lam_bp.supp
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
thm lam_bp.fv[simplified lam_bp.supp(1-2)]



end
nominal2