1 theory Test |
1 theory Test |
2 imports "Parser" "../Attic/Prove" |
2 imports "Parser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = recursive := false *} |
|
8 |
|
9 text {* example 1, equivalent to example 2 from Terms *} |
|
10 |
|
11 nominal_datatype lam = |
|
12 VAR "name" |
|
13 | APP "lam" "lam" |
|
14 | LAM x::"name" t::"lam" bind x in t |
|
15 | LET bp::"bp" t::"lam" bind "bi bp" in t |
|
16 and bp = |
|
17 BP "name" "lam" |
|
18 binder |
|
19 bi::"bp \<Rightarrow> atom set" |
|
20 where |
|
21 "bi (BP x t) = {atom x}" |
|
22 |
|
23 thm lam_bp.fv |
|
24 thm lam_bp.supp |
|
25 thm lam_bp.eq_iff |
|
26 thm lam_bp.bn |
|
27 thm lam_bp.perm |
|
28 thm lam_bp.induct |
|
29 thm lam_bp.inducts |
|
30 thm lam_bp.distinct |
|
31 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
|
32 thm lam_bp.fv[simplified lam_bp.supp] |
|
33 |
|
34 ML {* val _ = recursive := true *} |
|
35 |
|
36 nominal_datatype lam' = |
|
37 VAR' "name" |
|
38 | APP' "lam'" "lam'" |
|
39 | LAM' x::"name" t::"lam'" bind x in t |
|
40 | LET' bp::"bp'" t::"lam'" bind "bi' bp" in t |
|
41 and bp' = |
|
42 BP' "name" "lam'" |
|
43 binder |
|
44 bi'::"bp' \<Rightarrow> atom set" |
|
45 where |
|
46 "bi' (BP' x t) = {atom x}" |
|
47 |
|
48 thm lam'_bp'.fv |
|
49 thm lam'_bp'.eq_iff[no_vars] |
|
50 thm lam'_bp'.bn |
|
51 thm lam'_bp'.perm |
|
52 thm lam'_bp'.induct |
|
53 thm lam'_bp'.inducts |
|
54 thm lam'_bp'.distinct |
|
55 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
|
56 |
|
57 thm lam'_bp'.fv[simplified lam'_bp'.supp] |
|
58 |
|
59 |
|
60 text {* example 2 *} |
|
61 |
|
62 ML {* val _ = recursive := false *} |
7 ML {* val _ = recursive := false *} |
63 nominal_datatype trm' = |
|
64 Var "name" |
|
65 | App "trm'" "trm'" |
|
66 | Lam x::"name" t::"trm'" bind x in t |
|
67 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
|
68 and pat' = |
|
69 PN |
|
70 | PS "name" |
|
71 | PD "name" "name" |
|
72 binder |
|
73 f::"pat' \<Rightarrow> atom set" |
|
74 where |
|
75 "f PN = {}" |
|
76 | "f (PD x y) = {atom x, atom y}" |
|
77 | "f (PS x) = {atom x}" |
|
78 |
|
79 thm trm'_pat'.fv |
|
80 thm trm'_pat'.eq_iff |
|
81 thm trm'_pat'.bn |
|
82 thm trm'_pat'.perm |
|
83 thm trm'_pat'.induct |
|
84 thm trm'_pat'.distinct |
|
85 thm trm'_pat'.fv[simplified trm'_pat'.supp] |
|
86 |
8 |
87 nominal_datatype trm0 = |
9 nominal_datatype trm0 = |
88 Var0 "name" |
10 Var0 "name" |
89 | App0 "trm0" "trm0" |
11 | App0 "trm0" "trm0" |
90 | Lam0 x::"name" t::"trm0" bind x in t |
12 | Lam0 x::"name" t::"trm0" bind x in t |
442 where |
364 where |
443 "bv8 (Bar0 x) = {}" |
365 "bv8 (Bar0 x) = {}" |
444 | "bv8 (Bar1 v x b) = {atom v}" |
366 | "bv8 (Bar1 v x b) = {atom v}" |
445 *) |
367 *) |
446 |
368 |
447 (* Type schemes with separate datatypes *) |
|
448 nominal_datatype T = |
|
449 TVar "name" |
|
450 | TFun "T" "T" |
|
451 |
|
452 (* PROBLEM: |
|
453 *** exception Datatype raised |
|
454 *** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML") |
|
455 *** At command "nominal_datatype". |
|
456 nominal_datatype TyS = |
|
457 TAll xs::"name list" ty::"T" bind xs in ty |
|
458 *) |
|
459 |
|
460 (* example 9 from Peter Sewell's bestiary *) |
369 (* example 9 from Peter Sewell's bestiary *) |
461 (* run out of steam at the moment *) |
370 (* run out of steam at the moment *) |
462 |
371 |
463 end |
372 end |
464 |
373 |