2083
|
1 |
theory NoneExamples
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2 |
imports "../NewParser"
|
1589
|
3 |
begin
|
|
4 |
|
|
5 |
atom_decl name
|
|
6 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
7 |
(* this example binds bound names and
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
so is not respectful *)
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
9 |
(*
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
nominal_datatype trm =
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
Vr "name"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
| Lm x::"name" t::"trm" bind x in t
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
| Lt left::"trm" right::"trm" bind "bv left" in right
|
1589
|
14 |
binder
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
bv
|
1589
|
16 |
where
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
"bv (Vr n) = {}"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
| "bv (Lm n t) = {atom n} \<union> bv t"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
| "bv (Lt l r) = bv l \<union> bv r"
|
1589
|
20 |
*)
|
|
21 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
(* this example uses "-" in the binding function;
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
at the moment this is unsupported *)
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
(*
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
nominal_datatype trm' =
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
Vr' "name"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
| Lm' l::"name" r::"trm'" bind l in r
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
| Lt' l::"trm'" r::"trm'" bind "bv' l" in r
|
1589
|
29 |
binder
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
bv'
|
1589
|
31 |
where
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
"bv' (Vr' n) = {atom n}"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
| "bv' (Lm' n t) = bv' t - {atom n}"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
| "bv' (Lt' l r) = bv' l \<union> bv' r"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
*)
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
(* this example again binds bound names *)
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
(*
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
nominal_datatype trm'' =
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
Va'' "name"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
| Lm'' n::"name" l::"trm''" bind n in l
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
and bla'' =
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
binder
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
bv''
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
where
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
"bv'' (Vm'' x) = {}"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
| "bv'' (Lm'' x b) = {atom x}"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
*)
|
1589
|
50 |
|
|
51 |
end
|
|
52 |
|
|
53 |
|
|
54 |
|