equal
deleted
inserted
replaced
44 done |
44 done |
45 |
45 |
46 termination (eqvt) by lexicographic_order |
46 termination (eqvt) by lexicographic_order |
47 |
47 |
48 ML {* |
48 ML {* |
49 Item_Net.content; |
|
50 Nominal_Function_Common.get_function |
|
51 *} |
|
52 |
|
53 ML {* |
|
54 Item_Net.content (Nominal_Function_Common.get_function @{context}) |
49 Item_Net.content (Nominal_Function_Common.get_function @{context}) |
55 *} |
50 *} |
|
51 |
|
52 thm is_app_def |
56 |
53 |
57 |
54 |
58 lemma [eqvt]: |
55 lemma [eqvt]: |
59 shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)" |
56 shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)" |
60 apply(induct t rule: lam.induct) |
57 apply(induct t rule: lam.induct) |
162 apply(rule refl) |
159 apply(rule refl) |
163 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
160 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
164 apply(perm_simp) |
161 apply(perm_simp) |
165 apply(rule refl) |
162 apply(rule refl) |
166 done |
163 done |
|
164 |
|
165 thm inl_eqvt |
|
166 thm var_pos_def |
|
167 |
|
168 thm fun_eq_iff |
167 |
169 |
168 termination (eqvt) by lexicographic_order |
170 termination (eqvt) by lexicographic_order |
169 |
171 |
170 lemma var_pos1: |
172 lemma var_pos1: |
171 assumes "atom y \<notin> supp t" |
173 assumes "atom y \<notin> supp t" |