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