equal
deleted
inserted
replaced
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 thm single_let.supp |
36 thm single_let.supp |
37 thm single_let.fresh |
37 thm single_let.fresh |
38 |
|
39 quotient_definition |
|
40 "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg" |
|
41 is |
|
42 "permute_bn_raw" |
|
43 |
|
44 lemma [quot_respect]: |
|
45 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw" |
|
46 apply (simp add: fun_rel_def) |
|
47 apply clarify |
|
48 apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
|
49 apply (rule TrueI)+ |
|
50 apply simp_all |
|
51 apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
52 apply simp_all |
|
53 done |
|
54 |
38 |
55 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
39 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
56 |
40 |
57 lemma uu: |
41 lemma uu: |
58 shows "alpha_bn as (permute_bn p as)" |
42 shows "alpha_bn as (permute_bn p as)" |