equal
deleted
inserted
replaced
40 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
40 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
41 is |
41 is |
42 "permute_bn_raw" |
42 "permute_bn_raw" |
43 |
43 |
44 lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw" |
44 lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw" |
45 apply simp |
45 apply (simp add: fun_rel_def) |
46 apply clarify |
46 apply clarify |
47 apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts) |
47 apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts) |
48 apply (rule TrueI)+ |
48 apply (rule TrueI)+ |
49 apply simp_all |
49 apply simp_all |
50 apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros) |
50 apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros) |