equal
deleted
inserted
replaced
7 |
7 |
8 nominal_datatype lam = |
8 nominal_datatype lam = |
9 Var "name" |
9 Var "name" |
10 | App "lam" "lam" |
10 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
|
12 |
|
13 nominal_primrec |
|
14 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
15 where |
|
16 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
|
17 unfolding eqvt_def Z_graph_def |
|
18 apply (rule, perm_simp, rule) |
|
19 oops |
|
20 |
12 |
21 |
13 inductive |
22 inductive |
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
23 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
15 where |
24 where |
16 Var: "triv (Var x) n" |
25 Var: "triv (Var x) n" |
449 apply (simp add: fresh_at_list[symmetric]) |
458 apply (simp add: fresh_at_list[symmetric]) |
450 apply (drule_tac x="name # l" in meta_spec) |
459 apply (drule_tac x="name # l" in meta_spec) |
451 apply auto |
460 apply auto |
452 done |
461 done |
453 |
462 |
|
463 (* |
454 lemma db_trans_test: |
464 lemma db_trans_test: |
455 assumes a: "y \<noteq> x" |
465 assumes a: "y \<noteq> x" |
456 shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
466 shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
457 using a by simp |
467 using a by simp |
|
468 *) |
458 |
469 |
459 abbreviation |
470 abbreviation |
460 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
471 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
461 where |
472 where |
462 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
473 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
564 apply(rule refl) |
575 apply(rule refl) |
565 oops |
576 oops |
566 |
577 |
567 text {* "HO" functions *} |
578 text {* "HO" functions *} |
568 |
579 |
|
580 |
569 nominal_primrec |
581 nominal_primrec |
570 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
582 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
571 where |
583 where |
572 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
584 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
573 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
585 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |