equal
deleted
inserted
replaced
1 theory Test |
1 theory Test |
2 imports "Parser" |
2 imports "Parser" |
3 begin |
3 begin |
|
4 |
|
5 text {* weirdo example from Peter Sewell's bestiary *} |
|
6 |
|
7 nominal_datatype weird = |
|
8 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
|
9 bind x in p1, bind x in p2, bind y in p2, bind y in p3 |
|
10 | WVar "name" |
|
11 | WPair "weird" "weird" |
|
12 |
|
13 thm alpha_weird_raw.intros[no_vars] |
|
14 thm fv_weird_raw.simps[no_vars] |
|
15 (* Potential problem: Is it correct that in the fv-function |
|
16 the first two terms are created? Should be ommitted. Also |
|
17 something wrong with the permutations. *) |
4 |
18 |
5 text {* example 1 *} |
19 text {* example 1 *} |
6 |
20 |
7 nominal_datatype lam = |
21 nominal_datatype lam = |
8 VAR "name" |
22 VAR "name" |
44 where |
58 where |
45 "f PN = {}" |
59 "f PN = {}" |
46 | "f (PS x) = {atom x}" |
60 | "f (PS x) = {atom x}" |
47 | "f (PD x y) = {atom x, atom y}" |
61 | "f (PD x y) = {atom x, atom y}" |
48 |
62 |
|
63 |
|
64 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
|
65 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
49 thm f_raw.simps |
66 thm f_raw.simps |
50 |
67 |
51 nominal_datatype trm0 = |
68 nominal_datatype trm0 = |
52 Var0 "name" |
69 Var0 "name" |
53 | App0 "trm0" "trm0" |
70 | App0 "trm0" "trm0" |