(*<*)

theory Test

imports "Parser"

begin

(* This file contains only the examples that are not supposed to work yet. *)

atom_decl name

(* example 4 from Terms.thy *)

(* fv_eqvt does not work, we need to repaire defined permute functions

   defined fv and defined alpha... *)

(* lists-datastructure does not work yet

nominal_datatype trm4 =

  Vr4 "name"

| Ap4 "trm4" "trm4 list"

| Lm4 x::"name" t::"trm4"  bind x in t

thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]

thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]

*)

(* example 8 from Terms.thy *)

(* Binding in a term under a bn, needs to fail *)

(*

nominal_datatype foo8 =

  Foo0 "name"

| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"

and bar8 =

  Bar0 "name"

| Bar1 "name" s::"name" b::"bar8" bind s in b

binder

  bv8

where

  "bv8 (Bar0 x) = {}"

| "bv8 (Bar1 v x b) = {atom v}"

*)

(* example 9 from Peter Sewell's bestiary *)

(* run out of steam at the moment *)

end

(*>*)