equal
deleted
inserted
replaced
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" binds x in l ("Lam [_]. _" [100, 100] 100) |
11 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
12 |
12 |
13 nominal_primrec |
13 nominal_function |
14 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
14 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
15 where |
15 where |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |