equal
deleted
inserted
replaced
106 thm trm0_pat0.perm |
106 thm trm0_pat0.perm |
107 thm trm0_pat0.induct |
107 thm trm0_pat0.induct |
108 thm trm0_pat0.distinct |
108 thm trm0_pat0.distinct |
109 thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars] |
109 thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars] |
110 |
110 |
111 text {* example type schemes *} |
|
112 |
|
113 nominal_datatype t = |
|
114 VarTS "name" |
|
115 | FunTS "t" "t" |
|
116 and tyS = |
|
117 All xs::"name fset" ty::"t" bind xs in ty |
|
118 |
|
119 thm t_tyS.fv |
|
120 thm t_tyS.eq_iff |
|
121 thm t_tyS.bn |
|
122 thm t_tyS.perm |
|
123 thm t_tyS.induct |
|
124 thm t_tyS.distinct |
|
125 thm t_tyS.fv[simplified t_tyS.supp] |
|
126 |
|
127 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
|
128 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
|
129 |
|
130 |
|
131 |
|
132 (* example 1 from Terms.thy *) |
111 (* example 1 from Terms.thy *) |
133 |
|
134 |
112 |
135 nominal_datatype trm1 = |
113 nominal_datatype trm1 = |
136 Vr1 "name" |
114 Vr1 "name" |
137 | Ap1 "trm1" "trm1" |
115 | Ap1 "trm1" "trm1" |
138 | Lm1 x::"name" t::"trm1" bind x in t |
116 | Lm1 x::"name" t::"trm1" bind x in t |
264 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
242 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
265 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
243 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
266 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp |
244 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp |
267 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp] |
245 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp] |
268 |
246 |
269 |
|
270 (* example from my PHD *) |
|
271 |
|
272 atom_decl coname |
|
273 |
|
274 nominal_datatype phd = |
|
275 Ax "name" "coname" |
|
276 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
|
277 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
|
278 | AndL1 n::"name" t::"phd" "name" bind n in t |
|
279 | AndL2 n::"name" t::"phd" "name" bind n in t |
|
280 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
|
281 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
|
282 |
|
283 thm phd.fv |
|
284 thm phd.eq_iff |
|
285 thm phd.bn |
|
286 thm phd.perm |
|
287 thm phd.induct |
|
288 thm phd.distinct |
|
289 thm phd.fv[simplified phd.supp] |
|
290 |
|
291 (* example 3 from Peter Sewell's bestiary *) |
247 (* example 3 from Peter Sewell's bestiary *) |
292 |
248 |
293 nominal_datatype exp = |
249 nominal_datatype exp = |
294 VarP "name" |
250 VarP "name" |
295 | AppP "exp" "exp" |
251 | AppP "exp" "exp" |
469 bv :: "pat \<Rightarrow> atom set" |
425 bv :: "pat \<Rightarrow> atom set" |
470 where |
426 where |
471 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
427 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
472 *) |
428 *) |
473 |
429 |
474 text {* weirdo example from Peter Sewell's bestiary *} |
|
475 |
|
476 nominal_datatype weird = |
|
477 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
|
478 bind x in p1, bind x in p2, bind y in p2, bind y in p3 |
|
479 | WV "name" |
|
480 | WP "weird" "weird" |
|
481 |
|
482 thm permute_weird_raw.simps[no_vars] |
|
483 thm alpha_weird_raw.intros[no_vars] |
|
484 thm fv_weird_raw.simps[no_vars] |
|
485 |
|
486 (* example 8 from Terms.thy *) |
430 (* example 8 from Terms.thy *) |
487 |
431 |
488 (* Binding in a term under a bn, needs to fail *) |
432 (* Binding in a term under a bn, needs to fail *) |
489 (* |
433 (* |
490 nominal_datatype foo8 = |
434 nominal_datatype foo8 = |