equal
deleted
inserted
replaced
148 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
148 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
149 |
149 |
150 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
150 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
151 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
151 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
152 |
152 |
153 instantiation trm1 and bp :: pt |
153 setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
154 begin |
154 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} |
155 |
|
156 quotient_definition |
|
157 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
158 is |
|
159 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
|
160 |
|
161 instance by default |
|
162 (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted]) |
|
163 |
|
164 end |
|
165 |
155 |
166 lemmas |
156 lemmas |
167 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
157 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
168 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
158 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
169 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
159 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |