nominal2: Nominal/Test.thy@88b33de74e61 (annotated)

1629 a0ca7d9f6781 some tuning; possible fix for strange paper generation Christian Urban <urbanc@in.tum.de> parents: 1600 diff changeset	1	(<)
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	theory Test
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1595 diff changeset	3	imports "Parser"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	begin
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	6	(* This file contains only the examples that are not supposed to work yet. *)
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	7
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	8
1428 4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	9	atom_decl name
4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	10
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	11	(* example 4 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	12	(* fv_eqvt does not work, we need to repaire defined permute functions
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	13	defined fv and defined alpha... *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	14	(* lists-datastructure does not work yet
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	15	nominal_datatype trm4 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	16	Vr4 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	17	\| Ap4 "trm4" "trm4 list"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	18	\| Lm4 x::"name" t::"trm4" bind x in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	19
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	20	thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	21	thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	22	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	23
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	24	(* example 8 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	25
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	26	(* Binding in a term under a bn, needs to fail *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	27	(*
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	28	nominal_datatype foo8 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	29	Foo0 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	30	\| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	31	and bar8 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	32	Bar0 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	33	\| Bar1 "name" s::"name" b::"bar8" bind s in b
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	34	binder
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	35	bv8
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	36	where
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	37	"bv8 (Bar0 x) = {}"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	38	\| "bv8 (Bar1 v x b) = {atom v}"
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	39	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	40
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	41	(* example 9 from Peter Sewell's bestiary *)
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	42	(* run out of steam at the moment *)
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	43
961 0f88e04eb486 Variable takes a 'name'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 954 diff changeset	44	end
1629 a0ca7d9f6781 some tuning; possible fix for strange paper generation Christian Urban <urbanc@in.tum.de> parents: 1600 diff changeset	45	(>)
1223 160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	46
160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	47

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 30 Mar 2010 12:31:28 +0200 (2010-03-30)
changeset 1710	88b33de74e61
parent 1655	9cec4269b7f9
permissions	-rw-r--r--