equal
deleted
inserted
replaced
23 thm trm.fresh |
23 thm trm.fresh |
24 thm trm.exhaust |
24 thm trm.exhaust |
25 thm trm.strong_exhaust |
25 thm trm.strong_exhaust |
26 thm trm.perm_bn_simps |
26 thm trm.perm_bn_simps |
27 |
27 |
28 nominal_primrec |
28 nominal_function |
29 height_trm :: "trm \<Rightarrow> nat" |
29 height_trm :: "trm \<Rightarrow> nat" |
30 where |
30 where |
31 "height_trm (Var x) = 1" |
31 "height_trm (Var x) = 1" |
32 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
32 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
33 | "height_trm (Let x t s) = max (height_trm t) (height_trm s)" |
33 | "height_trm (Let x t s) = max (height_trm t) (height_trm s)" |
49 |
49 |
50 termination |
50 termination |
51 by lexicographic_order |
51 by lexicographic_order |
52 |
52 |
53 |
53 |
54 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
54 nominal_function (invariant "\<lambda>x (y::atom set). finite y") |
55 frees_set :: "trm \<Rightarrow> atom set" |
55 frees_set :: "trm \<Rightarrow> atom set" |
56 where |
56 where |
57 "frees_set (Var x) = {atom x}" |
57 "frees_set (Var x) = {atom x}" |
58 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
58 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
59 | "frees_set (Let x t s) = (frees_set s) - {atom x} \<union> (frees_set t)" |
59 | "frees_set (Let x t s) = (frees_set s) - {atom x} \<union> (frees_set t)" |
77 |
77 |
78 termination |
78 termination |
79 by lexicographic_order |
79 by lexicographic_order |
80 |
80 |
81 |
81 |
82 nominal_primrec |
82 nominal_function |
83 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
83 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
84 where |
84 where |
85 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
85 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
86 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
86 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
87 | "atom x \<sharp> (y, s) \<Longrightarrow> (Let x t t')[y ::= s] = Let x (t[y ::= s]) (t'[y ::= s])" |
87 | "atom x \<sharp> (y, s) \<Longrightarrow> (Let x t t')[y ::= s] = Let x (t[y ::= s]) (t'[y ::= s])" |