equal
deleted
inserted
replaced
1 theory Ex3 |
1 theory Ex3 |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* Example 3, identical to example 1 from Terms.thy *) |
5 (* Example 3, identical to example 1 from Terms.thy *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := false *} |
9 nominal_datatype trm = |
10 nominal_datatype trm0 = |
10 Var "name" |
11 Var0 "name" |
11 | App "trm" "trm" |
12 | App0 "trm0" "trm0" |
12 | Lam x::"name" t::"trm" bind_set x in t |
13 | Lam0 x::"name" t::"trm0" bind x in t |
13 | Let p::"pat" "trm" t::"trm" bind_set "f p" in t |
14 | Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t |
14 and pat = |
15 and pat0 = |
15 PN |
16 PN0 |
16 | PS "name" |
17 | PS0 "name" |
17 | PD "pat" "pat" |
18 | PD0 "pat0" "pat0" |
|
19 binder |
18 binder |
20 f0::"pat0 \<Rightarrow> atom set" |
19 f::"pat \<Rightarrow> atom set" |
21 where |
20 where |
22 "f0 PN0 = {}" |
21 "f PN = {}" |
23 | "f0 (PS0 x) = {atom x}" |
22 | "f (PS x) = {atom x}" |
24 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
23 | "f (PD p1 p2) = (f p1) \<union> (f p2)" |
25 |
24 |
26 thm trm0_pat0.fv |
25 thm trm_pat.fv |
27 thm trm0_pat0.eq_iff |
26 thm trm_pat.eq_iff |
28 thm trm0_pat0.bn |
27 thm trm_pat.bn |
29 thm trm0_pat0.perm |
28 thm trm_pat.perm |
30 thm trm0_pat0.induct |
29 thm trm_pat.induct |
31 thm trm0_pat0.distinct |
30 thm trm_pat.distinct |
32 thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars] |
31 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
33 |
32 |
34 end |
33 end |
35 |
34 |
36 |
35 |
37 |
36 |