1596
|
1 |
theory Ex1rec
|
2056
|
2 |
imports "../NewParser"
|
1596
|
3 |
begin
|
|
4 |
|
|
5 |
atom_decl name
|
|
6 |
|
2056
|
7 |
ML {* val _ = cheat_supp_eq := true *}
|
|
8 |
|
1946
|
9 |
nominal_datatype lam =
|
2056
|
10 |
Var "name"
|
|
11 |
| App "lam" "lam"
|
|
12 |
| Lam x::"name" t::"lam" bind_set x in t
|
|
13 |
| Let bp::"bp" t::"lam" bind_set "bi bp" in bp t
|
1946
|
14 |
and bp =
|
2056
|
15 |
Bp "name" "lam"
|
1596
|
16 |
binder
|
1946
|
17 |
bi::"bp \<Rightarrow> atom set"
|
1596
|
18 |
where
|
2056
|
19 |
"bi (Bp x t) = {atom x}"
|
1596
|
20 |
|
1946
|
21 |
thm lam_bp.fv
|
|
22 |
thm lam_bp.eq_iff[no_vars]
|
|
23 |
thm lam_bp.bn
|
|
24 |
thm lam_bp.perm
|
|
25 |
thm lam_bp.induct
|
|
26 |
thm lam_bp.inducts
|
|
27 |
thm lam_bp.distinct
|
2056
|
28 |
thm lam_bp.supp
|
1946
|
29 |
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
|
2056
|
30 |
thm lam_bp.fv[simplified lam_bp.supp(1-2)]
|
1596
|
31 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
declare permute_lam_raw_permute_bp_raw.simps[eqvt]
|
2067
|
33 |
declare alpha_gen_eqvt[eqvt]
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
|
2067
|
35 |
equivariance alpha_lam_raw
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
|
2067
|
37 |
|
1596
|
38 |
end
|
|
39 |
|
|
40 |
|
|
41 |
|