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 |
12 |
13 |
13 inductive |
14 inductive |
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
15 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
15 where |
16 where |
16 Var: "triv (Var x) n" |
17 Var: "triv (Var x) n" |
449 apply (simp add: fresh_at_list[symmetric]) |
450 apply (simp add: fresh_at_list[symmetric]) |
450 apply (drule_tac x="name # l" in meta_spec) |
451 apply (drule_tac x="name # l" in meta_spec) |
451 apply auto |
452 apply auto |
452 done |
453 done |
453 |
454 |
|
455 (* |
454 lemma db_trans_test: |
456 lemma db_trans_test: |
455 assumes a: "y \<noteq> x" |
457 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))))" |
458 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 |
459 using a by simp |
|
460 *) |
458 |
461 |
459 abbreviation |
462 abbreviation |
460 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
463 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
461 where |
464 where |
462 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
465 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
587 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
590 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
588 where |
591 where |
589 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
592 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
590 unfolding eqvt_def Z_graph_def |
593 unfolding eqvt_def Z_graph_def |
591 apply (rule, perm_simp, rule) |
594 apply (rule, perm_simp, rule) |
592 prefer 2 |
|
593 ML_prf {* prop_of (hd (#prems (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))))) *} |
|
594 oops |
595 oops |
595 |
596 |
596 (* function tests *) |
597 (* function tests *) |
597 |
598 |
598 (* similar problem with function package *) |
599 (* similar problem with function package *) |