author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Tue, 04 May 2010 14:21:18 +0200 | |
changeset 2045 | 6800fcaafa2a |
parent 1795 | e39453c8b186 |
child 2062 | 65bdcc42badd |
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 |
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
1655
diff
changeset
|
2 |
imports "../Parser" |
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 |
|
1600 | 5 |
(* This file contains only the examples that are not supposed to work yet. *) |
6 |
||
7 |
||
1428
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
8 |
atom_decl name |
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
9 |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
10 |
(* example 4 from Terms.thy *) |
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
11 |
(* 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
|
12 |
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
|
13 |
(* lists-datastructure does not work yet |
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
14 |
nominal_datatype trm4 = |
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
15 |
Vr4 "name" |
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
16 |
| Ap4 "trm4" "trm4 list" |
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
17 |
| Lm4 x::"name" t::"trm4" bind x in t |
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
18 |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
*) |
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
22 |
|
961
0f88e04eb486
Variable takes a 'name'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
954
diff
changeset
|
23 |
end |
1223
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents:
1194
diff
changeset
|
24 |
|
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents:
1194
diff
changeset
|
25 |