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" bind x in l ("Lam [_]. _" [100, 100] 100) |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
12 |
12 |
13 text {* free name function *} |
13 |
|
14 section {* free name function *} |
14 |
15 |
15 text {* first returns an atom list *} |
16 text {* first returns an atom list *} |
16 |
17 |
17 nominal_primrec |
18 nominal_primrec |
18 frees_lst :: "lam \<Rightarrow> atom list" |
19 frees_lst :: "lam \<Rightarrow> atom list" |
19 where |
20 where |
20 "frees_lst (Var x) = [atom x]" |
21 "frees_lst (Var x) = [atom x]" |
21 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
22 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
22 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
23 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
23 unfolding eqvt_def frees_lst_graph_def |
24 unfolding eqvt_def |
|
25 unfolding frees_lst_graph_def |
24 apply (rule, perm_simp, rule) |
26 apply (rule, perm_simp, rule) |
25 apply(rule TrueI) |
27 apply(rule TrueI) |
26 apply(rule_tac y="x" in lam.exhaust) |
28 apply(rule_tac y="x" in lam.exhaust) |
27 apply(auto) |
29 apply(auto) |
28 apply (erule Abs_lst1_fcb) |
30 apply (erule Abs_lst1_fcb) |
72 shows "a \<sharp> f x y z" |
74 shows "a \<sharp> f x y z" |
73 using fresh_fun_eqvt_app[OF a b(1)] a b |
75 using fresh_fun_eqvt_app[OF a b(1)] a b |
74 by (metis fresh_fun_app) |
76 by (metis fresh_fun_app) |
75 |
77 |
76 |
78 |
77 text {* A test with a locale and an interpretation. *} |
79 section {* A test with a locale and an interpretation. *} |
|
80 |
|
81 text {* conclusion: it is no necessary *} |
78 |
82 |
79 locale test = |
83 locale test = |
80 fixes f1::"name \<Rightarrow> ('a::pt)" |
84 fixes f1::"name \<Rightarrow> ('a::pt)" |
81 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
85 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
82 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
86 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
124 apply (auto simp add: pure_fresh supp_Pair) |
128 apply (auto simp add: pure_fresh supp_Pair) |
125 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3] |
129 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3] |
126 apply (simp_all add: eqvt_def permute_fun_def permute_pure) |
130 apply (simp_all add: eqvt_def permute_fun_def permute_pure) |
127 done |
131 done |
128 |
132 |
129 text {* height function *} |
133 section {* height function *} |
130 |
134 |
131 nominal_primrec |
135 nominal_primrec |
132 height :: "lam \<Rightarrow> int" |
136 height :: "lam \<Rightarrow> int" |
133 where |
137 where |
134 "height (Var x) = 1" |
138 "height (Var x) = 1" |
147 by lexicographic_order |
151 by lexicographic_order |
148 |
152 |
149 thm height.simps |
153 thm height.simps |
150 |
154 |
151 |
155 |
152 text {* capture - avoiding substitution *} |
156 section {* capture-avoiding substitution *} |
153 |
157 |
154 nominal_primrec |
158 nominal_primrec |
155 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
159 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
156 where |
160 where |
157 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
161 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |