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