1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
|
5 |
|
6 (* inductive_cases do not simplify with simple equations *) |
|
7 atom_decl var |
|
8 nominal_datatype expr = |
|
9 eCnst nat |
|
10 | eVar nat |
|
11 |
|
12 inductive |
|
13 eval :: "expr \<Rightarrow> nat list \<Rightarrow> bool" |
|
14 where |
|
15 evCnst1: "eval (eCnst c) [2,1]" |
|
16 | evCnst2: "eval (eCnst b) [1,2]" |
|
17 | evVar: "eval (eVar n) [1]" |
|
18 |
|
19 inductive_cases |
|
20 evInv_Cnst: "eval (eCnst c) [1,2]" |
|
21 |
|
22 thm evInv_Cnst |
|
23 |
|
24 |
4 |
25 |
5 |
26 atom_decl name |
6 atom_decl name |
27 |
7 |
28 nominal_datatype lam = |
8 nominal_datatype lam = |
513 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
493 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
514 apply(induct xs arbitrary: n) |
494 apply(induct xs arbitrary: n) |
515 apply(simp_all add: permute_pure) |
495 apply(simp_all add: permute_pure) |
516 done |
496 done |
517 |
497 |
518 (* |
498 |
|
499 text {* tests of functions containing if and case *} |
|
500 |
|
501 consts P :: "lam \<Rightarrow> bool" |
|
502 |
|
503 nominal_primrec |
|
504 A :: "lam => lam" |
|
505 where |
|
506 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
|
507 | "A (Var x) = (Var x)" |
|
508 | "A (App M N) = (if True then M else A N)" |
|
509 oops |
|
510 |
|
511 nominal_primrec |
|
512 C :: "lam => lam" |
|
513 where |
|
514 "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" |
|
515 | "C (Var x) = (Var x)" |
|
516 | "C (App M N) = (if True then M else C N)" |
|
517 oops |
|
518 |
|
519 nominal_primrec |
|
520 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
|
521 where |
|
522 "map_term f (Var x) = f (Var x)" |
|
523 | "map_term f (App t1 t2) = App (f t1) (f t2)" |
|
524 | "map_term f (Lam [x].t) = Lam [x].(f t)" |
|
525 oops |
|
526 |
|
527 nominal_primrec |
|
528 A :: "lam => lam" |
|
529 where |
|
530 "A (Lam [x].M) = (Lam [x].M)" |
|
531 | "A (Var x) = (Var x)" |
|
532 | "A (App M N) = (if True then M else A N)" |
|
533 oops |
|
534 |
|
535 nominal_primrec |
|
536 B :: "lam => lam" |
|
537 where |
|
538 "B (Lam [x].M) = (Lam [x].M)" |
|
539 | "B (Var x) = (Var x)" |
|
540 | "B (App M N) = (if True then M else (B N))" |
|
541 unfolding eqvt_def |
|
542 unfolding B_graph_def |
|
543 apply(perm_simp) |
|
544 apply(rule allI) |
|
545 apply(rule refl) |
|
546 oops |
|
547 |
|
548 text {* not working yet *} |
|
549 |
|
550 (* not working yet |
519 nominal_primrec |
551 nominal_primrec |
520 trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
552 trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
521 where |
553 where |
522 "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
554 "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
523 | "trans (App t1 t2) xs = ((trans t1 xs) \<guillemotright>= (\<lambda>db1. (trans t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
555 | "trans (App t1 t2) xs = ((trans t1 xs) \<guillemotright>= (\<lambda>db1. (trans t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
524 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
556 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
525 *) |
557 *) |
526 |
558 |
|
559 (* not working yet |
|
560 nominal_primrec |
|
561 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
562 where |
|
563 "CPS (Var x) k = Var x" |
|
564 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))" |
|
565 *) |
|
566 |
|
567 |
|
568 (* function tests *) |
|
569 |
|
570 (* similar problem with function package *) |
|
571 function |
|
572 f :: "int list \<Rightarrow> int" |
|
573 where |
|
574 "f [] = 0" |
|
575 | "f [e] = e" |
|
576 | "f (l @ m) = f l + f m" |
|
577 apply(simp_all) |
|
578 oops |
|
579 |
|
580 |
|
581 |
|
582 |
527 |
583 |
528 |
584 |
529 end |
585 end |
530 |
586 |
531 |
587 |