1 theory Test |
1 theory Test |
2 imports "Parser" |
2 imports "Parser" |
3 begin |
3 begin |
4 |
4 |
|
5 (* This file contains only the examples that are not supposed to work yet. *) |
|
6 |
|
7 |
5 atom_decl name |
8 atom_decl name |
6 |
9 |
7 ML {* val _ = recursive := false *} |
10 ML {* val _ = recursive := false *} |
8 |
|
9 text {* example 3 from Terms.thy *} |
|
10 |
|
11 nominal_datatype trm3 = |
|
12 Vr3 "name" |
|
13 | Ap3 "trm3" "trm3" |
|
14 | Lm3 x::"name" t::"trm3" bind x in t |
|
15 | Lt3 r::"rassigns3" t::"trm3" bind "bv3 r" in t |
|
16 and rassigns3 = |
|
17 ANil |
|
18 | ACons "name" "trm3" "rassigns3" |
|
19 binder |
|
20 bv3 |
|
21 where |
|
22 "bv3 ANil = {}" |
|
23 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
|
24 |
|
25 thm trm3_rassigns3.fv |
|
26 thm trm3_rassigns3.eq_iff |
|
27 thm trm3_rassigns3.bn |
|
28 thm trm3_rassigns3.perm |
|
29 thm trm3_rassigns3.induct |
|
30 thm trm3_rassigns3.distinct |
|
31 thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp] |
|
32 |
|
33 (* example 5 from Terms.thy *) |
|
34 |
|
35 nominal_datatype trm5 = |
|
36 Vr5 "name" |
|
37 | Ap5 "trm5" "trm5" |
|
38 | Lt5 l::"lts" t::"trm5" bind "bv5 l" in t |
|
39 and lts = |
|
40 Lnil |
|
41 | Lcons "name" "trm5" "lts" |
|
42 binder |
|
43 bv5 |
|
44 where |
|
45 "bv5 Lnil = {}" |
|
46 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
|
47 |
|
48 thm trm5_lts.fv |
|
49 thm trm5_lts.eq_iff |
|
50 thm trm5_lts.bn |
|
51 thm trm5_lts.perm |
|
52 thm trm5_lts.induct |
|
53 thm trm5_lts.distinct |
|
54 thm trm5_lts.fv[simplified trm5_lts.supp] |
|
55 |
|
56 (* example 3 from Peter Sewell's bestiary *) |
|
57 |
|
58 nominal_datatype exp = |
|
59 VarP "name" |
|
60 | AppP "exp" "exp" |
|
61 | LamP x::"name" e::"exp" bind x in e |
|
62 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1 |
|
63 and pat3 = |
|
64 PVar "name" |
|
65 | PUnit |
|
66 | PPair "pat3" "pat3" |
|
67 binder |
|
68 bp'' :: "pat3 \<Rightarrow> atom set" |
|
69 where |
|
70 "bp'' (PVar x) = {atom x}" |
|
71 | "bp'' (PUnit) = {}" |
|
72 | "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2" |
|
73 |
|
74 thm exp_pat3.fv |
|
75 thm exp_pat3.eq_iff |
|
76 thm exp_pat3.bn |
|
77 thm exp_pat3.perm |
|
78 thm exp_pat3.induct |
|
79 thm exp_pat3.distinct |
|
80 thm exp_pat3.fv[simplified exp_pat3.supp] |
|
81 |
|
82 (* example 6 from Peter Sewell's bestiary *) |
|
83 nominal_datatype exp6 = |
|
84 EVar name |
|
85 | EPair exp6 exp6 |
|
86 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 |
|
87 and pat6 = |
|
88 PVar' name |
|
89 | PUnit' |
|
90 | PPair' pat6 pat6 |
|
91 binder |
|
92 bp6 :: "pat6 \<Rightarrow> atom set" |
|
93 where |
|
94 "bp6 (PVar' x) = {atom x}" |
|
95 | "bp6 (PUnit') = {}" |
|
96 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
|
97 |
|
98 thm exp6_pat6.fv |
|
99 thm exp6_pat6.eq_iff |
|
100 thm exp6_pat6.bn |
|
101 thm exp6_pat6.perm |
|
102 thm exp6_pat6.induct |
|
103 thm exp6_pat6.distinct |
|
104 |
|
105 |
|
106 (* THE REST ARE NOT SUPPOSED TO WORK YET *) |
|
107 |
11 |
108 (* example 7 from Peter Sewell's bestiary *) |
12 (* example 7 from Peter Sewell's bestiary *) |
109 (* dest_Const raised |
13 (* dest_Const raised |
110 nominal_datatype exp7 = |
14 nominal_datatype exp7 = |
111 EVar' name |
15 EVar' name |
178 | Lm4 x::"name" t::"trm4" bind x in t |
82 | Lm4 x::"name" t::"trm4" bind x in t |
179 |
83 |
180 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
84 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
181 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
85 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
182 *) |
86 *) |
183 (* core haskell *) |
|
184 atom_decl var |
|
185 atom_decl tvar |
|
186 |
|
187 (* there are types, coercion types and regular types *) |
|
188 (* list-data-structure |
|
189 nominal_datatype tkind = |
|
190 KStar |
|
191 | KFun "tkind" "tkind" |
|
192 and ckind = |
|
193 CKEq "ty" "ty" |
|
194 and ty = |
|
195 TVar "tvar" |
|
196 | TC "string" |
|
197 | TApp "ty" "ty" |
|
198 | TFun "string" "ty list" |
|
199 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
|
200 | TEq "ty" "ty" "ty" |
|
201 and co = |
|
202 CC "string" |
|
203 | CApp "co" "co" |
|
204 | CFun "string" "co list" |
|
205 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
|
206 | CEq "co" "co" "co" |
|
207 | CSym "co" |
|
208 | CCir "co" "co" |
|
209 | CLeft "co" |
|
210 | CRight "co" |
|
211 | CSim "co" |
|
212 | CRightc "co" |
|
213 | CLeftc "co" |
|
214 | CCoe "co" "co" |
|
215 |
|
216 abbreviation |
|
217 "atoms A \<equiv> atom ` A" |
|
218 |
|
219 nominal_datatype trm = |
|
220 Var "var" |
|
221 | C "string" |
|
222 | LAM tv::"tvar" "kind" t::"trm" bind tv in t |
|
223 | APP "trm" "ty" |
|
224 | Lam v::"var" "ty" t::"trm" bind v in t |
|
225 | App "trm" "trm" |
|
226 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
|
227 | Case "trm" "assoc list" |
|
228 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
|
229 and assoc = |
|
230 A p::"pat" t::"trm" bind "bv p" in t |
|
231 and pat = |
|
232 K "string" "(tvar \<times> kind) list" "(var \<times> ty) list" |
|
233 binder |
|
234 bv :: "pat \<Rightarrow> atom set" |
|
235 where |
|
236 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
|
237 *) |
|
238 |
87 |
239 (* example 8 from Terms.thy *) |
88 (* example 8 from Terms.thy *) |
240 |
89 |
241 (* Binding in a term under a bn, needs to fail *) |
90 (* Binding in a term under a bn, needs to fail *) |
242 (* |
91 (* |