equal
deleted
inserted
replaced
34 |
34 |
35 quotient_definition |
35 quotient_definition |
36 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
36 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
37 is |
37 is |
38 "permute_bn_raw" |
38 "permute_bn_raw" |
39 |
|
40 lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw" |
|
41 apply (simp add: fun_rel_def) |
|
42 apply clarify |
|
43 apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts) |
|
44 apply (rule TrueI)+ |
|
45 apply simp_all |
|
46 apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros) |
|
47 apply simp_all |
|
48 done |
|
49 |
39 |
50 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
40 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
51 |
41 |
52 lemma uu: |
42 lemma uu: |
53 shows "alpha_bn as (permute_bn p as)" |
43 shows "alpha_bn as (permute_bn p as)" |