| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 03 Apr 2010 22:31:11 +0200 | |
| changeset 1773 | c0eac04ae3b4 |
| parent 1598 | Nominal/Ex3.thy@2406350c358f |
| child 2028 | 15c5a2926622 |
| permissions | -rw-r--r-- |
| 1597 | 1 |
theory Ex3 |
|
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
1598
diff
changeset
|
2 |
imports "../Parser" |
| 1597 | 3 |
begin |
4 |
||
|
1598
2406350c358f
Term1 is identical to Example 3
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1597
diff
changeset
|
5 |
(* Example 3, identical to example 1 from Terms.thy *) |
|
2406350c358f
Term1 is identical to Example 3
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1597
diff
changeset
|
6 |
|
| 1597 | 7 |
atom_decl name |
8 |
||
9 |
ML {* val _ = recursive := false *}
|
|
10 |
nominal_datatype trm0 = |
|
11 |
Var0 "name" |
|
12 |
| App0 "trm0" "trm0" |
|
13 |
| Lam0 x::"name" t::"trm0" bind x in t |
|
14 |
| Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t |
|
15 |
and pat0 = |
|
16 |
PN0 |
|
17 |
| PS0 "name" |
|
18 |
| PD0 "pat0" "pat0" |
|
19 |
binder |
|
20 |
f0::"pat0 \<Rightarrow> atom set" |
|
21 |
where |
|
22 |
"f0 PN0 = {}"
|
|
23 |
| "f0 (PS0 x) = {atom x}"
|
|
24 |
| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
|
25 |
||
26 |
thm trm0_pat0.fv |
|
27 |
thm trm0_pat0.eq_iff |
|
28 |
thm trm0_pat0.bn |
|
29 |
thm trm0_pat0.perm |
|
30 |
thm trm0_pat0.induct |
|
31 |
thm trm0_pat0.distinct |
|
32 |
thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars] |
|
33 |
||
34 |
end |
|
35 |
||
36 |
||
37 |