equal
deleted
inserted
replaced
55 quotient_definition |
55 quotient_definition |
56 "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
56 "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
57 is |
57 is |
58 "permute_bn3_raw" |
58 "permute_bn3_raw" |
59 |
59 |
60 lemma [quot_respect]: |
|
61 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw" |
|
62 apply (simp add: fun_rel_def) |
|
63 apply clarify |
|
64 apply (erule alpha_assg_raw.cases) |
|
65 apply simp_all |
|
66 apply (rule foo.raw_alpha) |
|
67 apply simp_all |
|
68 done |
|
69 |
|
70 lemma [quot_respect]: |
|
71 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw" |
|
72 apply (simp add: fun_rel_def) |
|
73 apply clarify |
|
74 apply (erule alpha_assg_raw.cases) |
|
75 apply simp_all |
|
76 apply (rule foo.raw_alpha) |
|
77 apply simp_all |
|
78 done |
|
79 |
|
80 lemma [quot_respect]: |
|
81 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw" |
|
82 apply (simp add: fun_rel_def) |
|
83 apply clarify |
|
84 apply (erule alpha_assg_raw.cases) |
|
85 apply simp_all |
|
86 apply (rule foo.raw_alpha) |
|
87 apply simp_all |
|
88 done |
|
89 |
|
90 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted] |
60 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted] |
91 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted] |
61 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted] |
92 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted] |
62 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted] |
93 |
63 |
94 lemma uu1: |
64 lemma uu1: |