1596
|
1 |
theory Ex1rec
|
|
2 |
imports "Parser" "../Attic/Prove"
|
|
3 |
begin
|
|
4 |
|
|
5 |
atom_decl name
|
|
6 |
|
|
7 |
ML {* val _ = recursive := true *}
|
|
8 |
nominal_datatype lam' =
|
|
9 |
VAR' "name"
|
|
10 |
| APP' "lam'" "lam'"
|
|
11 |
| LAM' x::"name" t::"lam'" bind x in t
|
|
12 |
| LET' bp::"bp'" t::"lam'" bind "bi' bp" in t
|
|
13 |
and bp' =
|
|
14 |
BP' "name" "lam'"
|
|
15 |
binder
|
|
16 |
bi'::"bp' \<Rightarrow> atom set"
|
|
17 |
where
|
|
18 |
"bi' (BP' x t) = {atom x}"
|
|
19 |
|
|
20 |
thm lam'_bp'.fv
|
|
21 |
thm lam'_bp'.eq_iff[no_vars]
|
|
22 |
thm lam'_bp'.bn
|
|
23 |
thm lam'_bp'.perm
|
|
24 |
thm lam'_bp'.induct
|
|
25 |
thm lam'_bp'.inducts
|
|
26 |
thm lam'_bp'.distinct
|
|
27 |
ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
|
|
28 |
thm lam'_bp'.fv[simplified lam'_bp'.supp]
|
|
29 |
|
|
30 |
end
|
|
31 |
|
|
32 |
|
|
33 |
|