equal
deleted
inserted
replaced
1 theory Ex2 |
1 theory Ex2 |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 text {* example 2 *} |
5 text {* example 2 *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := false *} |
9 ML {* val _ = cheat_alpha_eqvt := true *} |
10 nominal_datatype trm' = |
10 |
|
11 nominal_datatype trm = |
11 Var "name" |
12 Var "name" |
12 | App "trm'" "trm'" |
13 | App "trm" "trm" |
13 | Lam x::"name" t::"trm'" bind x in t |
14 | Lam x::"name" t::"trm" bind_set x in t |
14 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
15 | Let p::"pat" "trm" t::"trm" bind_set "f p" in t |
15 and pat' = |
16 and pat = |
16 PN |
17 PN |
17 | PS "name" |
18 | PS "name" |
18 | PD "name" "name" |
19 | PD "name" "name" |
19 binder |
20 binder |
20 f::"pat' \<Rightarrow> atom set" |
21 f::"pat \<Rightarrow> atom set" |
21 where |
22 where |
22 "f PN = {}" |
23 "f PN = {}" |
23 | "f (PD x y) = {atom x, atom y}" |
24 | "f (PD x y) = {atom x, atom y}" |
24 | "f (PS x) = {atom x}" |
25 | "f (PS x) = {atom x}" |
25 |
26 thm trm_pat.bn |
26 thm trm'_pat'.fv |
27 thm trm_pat.perm |
27 thm trm'_pat'.eq_iff |
28 thm trm_pat.induct |
28 thm trm'_pat'.bn |
29 thm trm_pat.distinct |
29 thm trm'_pat'.perm |
30 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
30 thm trm'_pat'.induct |
|
31 thm trm'_pat'.distinct |
|
32 thm trm'_pat'.fv[simplified trm'_pat'.supp] |
|
33 |
31 |
34 end |
32 end |
35 |
33 |
36 |
34 |
37 |
35 |