equal
deleted
inserted
replaced
14 |
14 |
15 notation |
15 notation |
16 App (infixl "\<cdot>" 98) and |
16 App (infixl "\<cdot>" 98) and |
17 Lam ("\<integral> _. _" [97, 97] 99) |
17 Lam ("\<integral> _. _" [97, 97] 99) |
18 |
18 |
19 nominal_primrec |
19 nominal_function |
20 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
20 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
21 where |
21 where |
22 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
22 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
23 | "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])" |
23 | "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])" |
24 | "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])" |
24 | "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])" |