equal
deleted
inserted
replaced
46 is |
46 is |
47 "permute_bn_raw" |
47 "permute_bn_raw" |
48 |
48 |
49 lemma [quot_respect]: |
49 lemma [quot_respect]: |
50 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw" |
50 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw" |
51 apply simp |
51 apply (simp add: fun_rel_def) |
52 apply clarify |
52 apply clarify |
53 apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
53 apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
54 apply (rule TrueI)+ |
54 apply (rule TrueI)+ |
55 apply simp_all |
55 apply simp_all |
56 apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
56 apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |