equal
deleted
inserted
replaced
72 is |
72 is |
73 "permute_bn3_raw" |
73 "permute_bn3_raw" |
74 |
74 |
75 lemma [quot_respect]: |
75 lemma [quot_respect]: |
76 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw" |
76 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw" |
77 apply simp |
77 apply (simp add: fun_rel_def) |
78 apply clarify |
78 apply clarify |
79 apply (erule alpha_assg_raw.cases) |
79 apply (erule alpha_assg_raw.cases) |
80 apply simp_all |
80 apply simp_all |
81 apply (rule foo.raw_alpha) |
81 apply (rule foo.raw_alpha) |
82 apply simp_all |
82 apply simp_all |
83 done |
83 done |
84 |
84 |
85 lemma [quot_respect]: |
85 lemma [quot_respect]: |
86 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw" |
86 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw" |
87 apply simp |
87 apply (simp add: fun_rel_def) |
88 apply clarify |
88 apply clarify |
89 apply (erule alpha_assg_raw.cases) |
89 apply (erule alpha_assg_raw.cases) |
90 apply simp_all |
90 apply simp_all |
91 apply (rule foo.raw_alpha) |
91 apply (rule foo.raw_alpha) |
92 apply simp_all |
92 apply simp_all |
93 done |
93 done |
94 |
94 |
95 lemma [quot_respect]: |
95 lemma [quot_respect]: |
96 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw" |
96 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw" |
97 apply simp |
97 apply (simp add: fun_rel_def) |
98 apply clarify |
98 apply clarify |
99 apply (erule alpha_assg_raw.cases) |
99 apply (erule alpha_assg_raw.cases) |
100 apply simp_all |
100 apply simp_all |
101 apply (rule foo.raw_alpha) |
101 apply (rule foo.raw_alpha) |
102 apply simp_all |
102 apply simp_all |