|
2494
|
1 |
theory Foo1
|
|
|
2 |
imports "../Nominal2"
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
(*
|
|
|
6 |
Contrived example that has more than one
|
|
|
7 |
binding function for a datatype
|
|
|
8 |
*)
|
|
|
9 |
|
|
|
10 |
atom_decl name
|
|
|
11 |
|
|
|
12 |
nominal_datatype foo: trm =
|
|
|
13 |
Var "name"
|
|
|
14 |
| App "trm" "trm"
|
|
|
15 |
| Lam x::"name" t::"trm" bind x in t
|
|
|
16 |
| Let1 a::"assg" t::"trm" bind "bn1 a" in t
|
|
|
17 |
| Let2 a::"assg" t::"trm" bind "bn2 a" in t
|
|
|
18 |
| Let3 a::"assg" t::"trm" bind "bn3 a" in t
|
|
|
19 |
and assg =
|
|
|
20 |
As "name" "name" "trm"
|
|
|
21 |
binder
|
|
|
22 |
bn1::"assg \<Rightarrow> atom list" and
|
|
|
23 |
bn2::"assg \<Rightarrow> atom list" and
|
|
|
24 |
bn3::"assg \<Rightarrow> atom list"
|
|
|
25 |
where
|
|
|
26 |
"bn1 (As x y t) = [atom x]"
|
|
|
27 |
| "bn2 (As x y t) = [atom y]"
|
|
|
28 |
| "bn3 (As x y t) = [atom x, atom y]"
|
|
|
29 |
|
|
|
30 |
thm foo.distinct
|
|
|
31 |
thm foo.induct
|
|
|
32 |
thm foo.inducts
|
|
|
33 |
thm foo.exhaust
|
|
|
34 |
thm foo.fv_defs
|
|
|
35 |
thm foo.bn_defs
|
|
|
36 |
thm foo.perm_simps
|
|
|
37 |
thm foo.eq_iff
|
|
|
38 |
thm foo.fv_bn_eqvt
|
|
|
39 |
thm foo.size_eqvt
|
|
|
40 |
thm foo.supports
|
|
|
41 |
thm foo.fsupp
|
|
|
42 |
thm foo.supp
|
|
|
43 |
thm foo.fresh
|
|
|
44 |
|
|
|
45 |
|
|
|
46 |
end
|
|
|
47 |
|
|
|
48 |
|
|
|
49 |
|