| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 16 Jul 2010 05:09:45 +0100 | |
| changeset 2364 | 2bf351f09317 |
| parent 2288 | 3b83960f9544 |
| permissions | -rw-r--r-- |
|
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 |
*) |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
2163
diff
changeset
|
16 |
|
| 1600 | 17 |
(* This file contains only the examples that are not supposed to work yet. *) |
18 |
||
19 |
||
|
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
|
20 |
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
|
21 |
|
|
1428
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
22 |
|
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
23 |
(* example 4 from Terms.thy *) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
24 |
(* 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
|
25 |
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
|
26 |
(* lists-datastructure does not work yet *) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
27 |
|
|
2103
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2062
diff
changeset
|
28 |
nominal_datatype trm = |
|
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2062
diff
changeset
|
29 |
Vr "name" |
|
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2062
diff
changeset
|
30 |
| Ap "trm" "trm list" |
|
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2062
diff
changeset
|
31 |
| 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
|
32 |
|
|
2103
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 |