equal
deleted
inserted
replaced
43 apply(all_trivials) |
43 apply(all_trivials) |
44 done |
44 done |
45 |
45 |
46 termination (eqvt) by lexicographic_order |
46 termination (eqvt) by lexicographic_order |
47 |
47 |
48 ML {* |
|
49 Item_Net.content (Nominal_Function_Common.get_function @{context}) |
|
50 *} |
|
51 |
|
52 thm is_app_def |
48 thm is_app_def |
53 |
49 thm is_app.eqvt |
54 |
50 |
55 lemma [eqvt]: |
51 thm eqvts |
56 shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)" |
|
57 apply(induct t rule: lam.induct) |
|
58 apply(simp_all add: permute_bool_def) |
|
59 done |
|
60 |
52 |
61 nominal_primrec |
53 nominal_primrec |
62 rator :: "lam \<Rightarrow> lam option" |
54 rator :: "lam \<Rightarrow> lam option" |
63 where |
55 where |
64 "rator (Var x) = None" |
56 "rator (Var x) = None" |
72 apply(simp_all) |
64 apply(simp_all) |
73 done |
65 done |
74 |
66 |
75 termination (eqvt) by lexicographic_order |
67 termination (eqvt) by lexicographic_order |
76 |
68 |
77 lemma [eqvt]: |
|
78 shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)" |
|
79 apply(induct t rule: lam.induct) |
|
80 apply(simp_all) |
|
81 done |
|
82 |
|
83 nominal_primrec |
69 nominal_primrec |
84 rand :: "lam \<Rightarrow> lam option" |
70 rand :: "lam \<Rightarrow> lam option" |
85 where |
71 where |
86 "rand (Var x) = None" |
72 "rand (Var x) = None" |
87 | "rand (App t1 t2) = Some t2" |
73 | "rand (App t1 t2) = Some t2" |
93 apply(auto)[3] |
79 apply(auto)[3] |
94 apply(simp_all) |
80 apply(simp_all) |
95 done |
81 done |
96 |
82 |
97 termination (eqvt) by lexicographic_order |
83 termination (eqvt) by lexicographic_order |
98 |
|
99 lemma [eqvt]: |
|
100 shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)" |
|
101 apply(induct t rule: lam.induct) |
|
102 apply(simp_all) |
|
103 done |
|
104 |
84 |
105 nominal_primrec |
85 nominal_primrec |
106 is_eta_nf :: "lam \<Rightarrow> bool" |
86 is_eta_nf :: "lam \<Rightarrow> bool" |
107 where |
87 where |
108 "is_eta_nf (Var x) = True" |
88 "is_eta_nf (Var x) = True" |
160 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
140 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
161 apply(perm_simp) |
141 apply(perm_simp) |
162 apply(rule refl) |
142 apply(rule refl) |
163 done |
143 done |
164 |
144 |
165 thm inl_eqvt |
|
166 thm var_pos_def |
|
167 |
|
168 thm fun_eq_iff |
|
169 |
|
170 termination (eqvt) by lexicographic_order |
145 termination (eqvt) by lexicographic_order |
171 |
146 |
172 lemma var_pos1: |
147 lemma var_pos1: |
173 assumes "atom y \<notin> supp t" |
148 assumes "atom y \<notin> supp t" |
174 shows "var_pos y t = {}" |
149 shows "var_pos y t = {}" |
313 done |
288 done |
314 |
289 |
315 termination (eqvt) |
290 termination (eqvt) |
316 by lexicographic_order |
291 by lexicographic_order |
317 |
292 |
318 lemma subst_eqvt[eqvt]: |
293 thm subst.eqvt |
319 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
|
320 by (induct t x s rule: subst.induct) (simp_all) |
|
321 |
294 |
322 lemma forget: |
295 lemma forget: |
323 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
296 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
324 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
297 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
325 (auto simp add: lam.fresh fresh_at_base) |
298 (auto simp add: lam.fresh fresh_at_base) |