nominal2: Nominal/Ex/Test.thy@5dc48e1af733 (annotated)

954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Test
2062 65bdcc42badd "isabelle make" compiles all examples with newparser/newfv/newalpha only. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2045 diff changeset	2	imports "../NewParser"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
2163 5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	5	declare [[STEPS = 4]]
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	6
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	7	atom_decl name
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	8
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	9	(*
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	10	nominal_datatype trm =
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	11	Vr "name"
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	12	\| Ap "trm" "trm"
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	13
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	14	thm fv_trm_raw.simps[no_vars]
5dc48e1af733 added comments about pottiers work Christian Urban <urbanc@in.tum.de> parents: 2143 diff changeset	15	*)
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	16	(* 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	17
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	18
2143 871d8a5e0c67 somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms Christian Urban <urbanc@in.tum.de> parents: 2103 diff changeset	19	declare [[STEPS = 2]]
871d8a5e0c67 somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms Christian Urban <urbanc@in.tum.de> parents: 2103 diff changeset	20
1428 4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	21
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	22	(* example 4 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	23	(* 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	24	defined fv and defined alpha... *)
2103 e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	25	(* lists-datastructure does not work yet *)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	26
2103 e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	27	nominal_datatype trm =
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	28	Vr "name"
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	29	\| Ap "trm" "trm list"
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	30	\| Lm x::"name" t::"trm" bind x in t
2143 871d8a5e0c67 somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms Christian Urban <urbanc@in.tum.de> parents: 2103 diff changeset	31
2103 e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	32
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	33	(*
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	34	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	35	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	36	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	37
961 0f88e04eb486 Variable takes a 'name'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 954 diff changeset	38	end
1223 160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	39
160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	40

author	Christian Urban <urbanc@in.tum.de>
	Wed, 19 May 2010 12:43:38 +0100
changeset 2163	5dc48e1af733
parent 2143	871d8a5e0c67
child 2288	3b83960f9544
permissions	-rw-r--r--