equal
deleted
inserted
replaced
1 theory Lambda_add |
1 theory Lambda_add |
2 imports "Lambda" |
2 imports "Lambda" |
3 begin |
3 begin |
|
4 |
|
5 nominal_primrec |
|
6 addlam :: "lam \<Rightarrow> lam" |
|
7 where |
|
8 "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)" |
|
9 | "addlam (App t1 t2) = App t1 t2" |
|
10 | "addlam (Lam [x]. t) = Lam [x].t" |
|
11 oops |
|
12 |
4 |
13 |
5 nominal_primrec |
14 nominal_primrec |
6 addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
15 addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
7 where |
16 where |
8 "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)" |
17 "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)" |