417 by (simp_all add: branch_def ONE_pat_def) |
417 by (simp_all add: branch_def ONE_pat_def) |
418 |
418 |
419 |
419 |
420 subsection {* Wildcards, as-patterns, and lazy patterns *} |
420 subsection {* Wildcards, as-patterns, and lazy patterns *} |
421 |
421 |
422 syntax |
|
423 "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10) |
|
424 "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000) |
|
425 |
|
426 definition |
422 definition |
427 wild_pat :: "'a \<rightarrow> unit maybe" where |
423 wild_pat :: "'a \<rightarrow> unit maybe" where |
428 "wild_pat = (\<Lambda> x. return\<cdot>())" |
424 "wild_pat = (\<Lambda> x. return\<cdot>())" |
429 |
425 |
430 definition |
426 definition |
436 "lazy_pat p = (\<Lambda> x. return\<cdot>(cases\<cdot>(p\<cdot>x)))" |
432 "lazy_pat p = (\<Lambda> x. return\<cdot>(cases\<cdot>(p\<cdot>x)))" |
437 |
433 |
438 text {* Parse translations (patterns) *} |
434 text {* Parse translations (patterns) *} |
439 translations |
435 translations |
440 "_pat _" => "CONST wild_pat" |
436 "_pat _" => "CONST wild_pat" |
441 "_pat (_as_pat x y)" => "CONST as_pat (_pat y)" |
|
442 "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)" |
|
443 |
437 |
444 text {* Parse translations (variables) *} |
438 text {* Parse translations (variables) *} |
445 translations |
439 translations |
446 "_variable _ r" => "_variable _noargs r" |
440 "_variable _ r" => "_variable _noargs r" |
447 "_variable (_as_pat x y) r" => "_variable (_args x y) r" |
|
448 "_variable (_lazy_pat x) r" => "_variable x r" |
|
449 |
441 |
450 text {* Print translations *} |
442 text {* Print translations *} |
451 translations |
443 translations |
452 "_" <= "_match (CONST wild_pat) _noargs" |
444 "_" <= "_match (CONST wild_pat) _noargs" |
453 "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_variable x) v)" |
|
454 "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v" |
|
455 |
|
456 text {* Lazy patterns in lambda abstractions *} |
|
457 translations |
|
458 "_cabs (_lazy_pat p) r" == "CONST Fixrec.cases oo (_Case1 (_lazy_pat p) r)" |
|
459 |
445 |
460 lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r" |
446 lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r" |
461 by (simp add: branch_def wild_pat_def) |
447 by (simp add: branch_def wild_pat_def) |
462 |
448 |
463 lemma as_pat [simp]: |
449 lemma as_pat [simp]: |