equal
deleted
inserted
replaced
12 | App "lam" "lam" |
12 | App "lam" "lam" |
13 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
13 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
14 |
14 |
15 section {* capture-avoiding substitution *} |
15 section {* capture-avoiding substitution *} |
16 |
16 |
17 nominal_primrec |
17 nominal_function |
18 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
18 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
19 where |
19 where |
20 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
20 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
21 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
21 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
22 | "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
22 | "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |