equal
deleted
inserted
replaced
31 thm single_let.eq_iff |
31 thm single_let.eq_iff |
32 thm single_let.fv_bn_eqvt |
32 thm single_let.fv_bn_eqvt |
33 thm single_let.size_eqvt |
33 thm single_let.size_eqvt |
34 thm single_let.supports |
34 thm single_let.supports |
35 thm single_let.fsupp |
35 thm single_let.fsupp |
36 |
|
37 lemma Abs_eq_iff: |
|
38 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
|
39 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
|
40 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
|
41 by (lifting alphas_abs) |
|
42 |
36 |
43 lemma test2: |
37 lemma test2: |
44 assumes "fv_trm t = supp t" |
38 assumes "fv_trm t = supp t" |
45 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
39 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
46 apply(rule allI) |
40 apply(rule allI) |