|
2494
|
1 |
theory Foo1
|
|
|
2 |
imports "../Nominal2"
|
|
|
3 |
begin
|
|
|
4 |
|
|
2564
|
5 |
text {*
|
|
2494
|
6 |
Contrived example that has more than one
|
|
2564
|
7 |
binding function
|
|
|
8 |
*}
|
|
2494
|
9 |
|
|
2571
|
10 |
|
|
2494
|
11 |
atom_decl name
|
|
|
12 |
|
|
|
13 |
nominal_datatype foo: trm =
|
|
|
14 |
Var "name"
|
|
|
15 |
| App "trm" "trm"
|
|
|
16 |
| Lam x::"name" t::"trm" bind x in t
|
|
|
17 |
| Let1 a::"assg" t::"trm" bind "bn1 a" in t
|
|
|
18 |
| Let2 a::"assg" t::"trm" bind "bn2 a" in t
|
|
|
19 |
| Let3 a::"assg" t::"trm" bind "bn3 a" in t
|
|
2564
|
20 |
| Let4 a::"assg'" t::"trm" bind (set) "bn4 a" in t
|
|
2494
|
21 |
and assg =
|
|
|
22 |
As "name" "name" "trm"
|
|
2564
|
23 |
and assg' =
|
|
|
24 |
BNil
|
|
|
25 |
| BAs "name" "assg'"
|
|
2494
|
26 |
binder
|
|
|
27 |
bn1::"assg \<Rightarrow> atom list" and
|
|
|
28 |
bn2::"assg \<Rightarrow> atom list" and
|
|
2564
|
29 |
bn3::"assg \<Rightarrow> atom list" and
|
|
|
30 |
bn4::"assg' \<Rightarrow> atom set"
|
|
2494
|
31 |
where
|
|
|
32 |
"bn1 (As x y t) = [atom x]"
|
|
|
33 |
| "bn2 (As x y t) = [atom y]"
|
|
|
34 |
| "bn3 (As x y t) = [atom x, atom y]"
|
|
2564
|
35 |
| "bn4 (BNil) = {}"
|
|
|
36 |
| "bn4 (BAs a as) = {atom a} \<union> bn4 as"
|
|
|
37 |
|
|
2598
|
38 |
thm foo.permute_bn
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
thm foo.perm_bn_alpha
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
thm foo.perm_bn_simps
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
thm foo.bn_finite
|
|
2494
|
42 |
|
|
|
43 |
thm foo.distinct
|
|
|
44 |
thm foo.induct
|
|
|
45 |
thm foo.inducts
|
|
|
46 |
thm foo.exhaust
|
|
2630
|
47 |
thm foo.strong_induct
|
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
thm foo.strong_exhaust
|
|
2494
|
49 |
thm foo.fv_defs
|
|
|
50 |
thm foo.bn_defs
|
|
|
51 |
thm foo.perm_simps
|
|
|
52 |
thm foo.eq_iff
|
|
|
53 |
thm foo.fv_bn_eqvt
|
|
|
54 |
thm foo.size_eqvt
|
|
|
55 |
thm foo.supports
|
|
|
56 |
thm foo.fsupp
|
|
|
57 |
thm foo.supp
|
|
|
58 |
thm foo.fresh
|
|
2571
|
59 |
thm foo.bn_finite
|
|
2494
|
60 |
|
|
|
61 |
|
|
|
62 |
end
|
|
|
63 |
|
|
|
64 |
|
|
|
65 |
|