| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Tue, 18 May 2010 17:56:41 +0200 | |
| changeset 2160 | 8c24ee88b8e8 |
| parent 2147 | e83493622e6f |
| child 2436 | 3885dc2669f9 |
| permissions | -rw-r--r-- |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Term8 |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../NewParser" |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2045
diff
changeset
|
5 |
(* example 8 *) |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
atom_decl name |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
|
|
2147
e83493622e6f
alpha_alphabn for bindings in a type under bn.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2097
diff
changeset
|
9 |
ML {* val _ = cheat_alpha_bn_rsp := true *}
|
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2045
diff
changeset
|
10 |
|
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
nominal_datatype foo = |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
Foo0 "name" |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
| Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
and bar = |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
Bar0 "name" |
| 2097 | 16 |
| Bar1 "name" s::"name" b::"bar" bind_set s in b |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
binder |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
bv |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
where |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
"bv (Bar0 x) = {}"
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
| "bv (Bar1 v x b) = {atom v}"
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
|
|
2147
e83493622e6f
alpha_alphabn for bindings in a type under bn.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2097
diff
changeset
|
23 |
thm foo_bar.supp |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2045
diff
changeset
|
24 |
|
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
end |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |