equal
deleted
inserted
replaced
30 thm lam.strong_induct |
30 thm lam.strong_induct |
31 |
31 |
32 |
32 |
33 subsection {* Height Function *} |
33 subsection {* Height Function *} |
34 |
34 |
35 nominal_primrec |
35 nominal_function |
36 height :: "lam \<Rightarrow> int" |
36 height :: "lam \<Rightarrow> int" |
37 where |
37 where |
38 "height (Var x) = 1" |
38 "height (Var x) = 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
40 | "height (Lam [x].t) = height t + 1" |
40 | "height (Lam [x].t) = height t + 1" |
51 by lexicographic_order |
51 by lexicographic_order |
52 |
52 |
53 |
53 |
54 subsection {* Capture-Avoiding Substitution *} |
54 subsection {* Capture-Avoiding Substitution *} |
55 |
55 |
56 nominal_primrec |
56 nominal_function |
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
58 where |
58 where |
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |