133 quotient_definition |
133 quotient_definition |
134 "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm" |
134 "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm" |
135 is |
135 is |
136 "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm" |
136 "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm" |
137 |
137 |
138 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] |
138 instance by default (simp_all add: |
139 |
139 permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted] |
140 lemma perm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z" |
140 permute_rkind_permute_rty_permute_rtrm_append[quot_lifted]) |
141 apply (induct rule: kind_ty_trm_induct) |
|
142 apply (simp_all) |
|
143 done |
|
144 |
|
145 lemma perm_add_ok: |
|
146 "((p + q) \<bullet> (x1 :: kind) = (p \<bullet> q \<bullet> x1))" |
|
147 "((p + q) \<bullet> (x2 :: ty) = p \<bullet> q \<bullet> x2)" |
|
148 "((p + q) \<bullet> (x3 :: trm) = p \<bullet> q \<bullet> x3)" |
|
149 apply (induct x1 and x2 and x3 rule: kind_ty_trm_inducts) |
|
150 apply (simp_all) |
|
151 done |
|
152 |
|
153 instance |
|
154 apply default |
|
155 apply (simp_all add: perm_zero_ok perm_add_ok) |
|
156 done |
|
157 |
141 |
158 end |
142 end |
159 |
143 |
160 (* |
144 (* |
161 Lifts, but slow and not needed?. |
145 Lifts, but slow and not needed?. |
162 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
146 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
163 *) |
147 *) |
|
148 |
|
149 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] |
164 |
150 |
165 lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
151 lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
166 |
152 |
167 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
153 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
168 |
154 |