1596
|
1 |
theory Ex1rec
|
2056
|
2 |
imports "../NewParser"
|
1596
|
3 |
begin
|
|
4 |
|
2311
|
5 |
declare [[STEPS = 9]]
|
1596
|
6 |
|
2311
|
7 |
atom_decl name
|
2056
|
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 |
|
2311
|
21 |
|
|
22 |
thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros
|
|
23 |
|
1946
|
24 |
thm lam_bp.fv
|
|
25 |
thm lam_bp.eq_iff[no_vars]
|
|
26 |
thm lam_bp.bn
|
|
27 |
thm lam_bp.perm
|
|
28 |
thm lam_bp.induct
|
|
29 |
thm lam_bp.inducts
|
|
30 |
thm lam_bp.distinct
|
2056
|
31 |
thm lam_bp.supp
|
1946
|
32 |
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
|
2056
|
33 |
thm lam_bp.fv[simplified lam_bp.supp(1-2)]
|
1596
|
34 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
|
2067
|
36 |
|
1596
|
37 |
end
|
|
38 |
|
|
39 |
|
|
40 |
|