equal
deleted
inserted
replaced
8 nominal_datatype lt = |
8 nominal_datatype lt = |
9 Var name ("_~" [150] 149) |
9 Var name ("_~" [150] 149) |
10 | App lt lt (infixl "$$" 100) |
10 | App lt lt (infixl "$$" 100) |
11 | Lam x::"name" t::"lt" binds x in t |
11 | Lam x::"name" t::"lt" binds x in t |
12 |
12 |
13 nominal_primrec |
13 nominal_function |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [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])" |
42 |
42 |
43 lemma [simp]: "supp (M[x ::= V]) <= (supp(M) - {atom x}) Un (supp V)" |
43 lemma [simp]: "supp (M[x ::= V]) <= (supp(M) - {atom x}) Un (supp V)" |
44 by (nominal_induct M avoiding: x V rule: lt.strong_induct) |
44 by (nominal_induct M avoiding: x V rule: lt.strong_induct) |
45 (auto simp add: lt.supp supp_at_base, blast, blast) |
45 (auto simp add: lt.supp supp_at_base, blast, blast) |
46 |
46 |
47 nominal_primrec |
47 nominal_function |
48 isValue:: "lt => bool" |
48 isValue:: "lt => bool" |
49 where |
49 where |
50 "isValue (Var x) = True" |
50 "isValue (Var x) = True" |
51 | "isValue (Lam y N) = True" |
51 | "isValue (Lam y N) = True" |
52 | "isValue (A $$ B) = False" |
52 | "isValue (A $$ B) = False" |