159 prove {* reg_artm *} |
159 prove {* reg_artm *} |
160 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
160 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
161 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
161 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
162 done |
162 done |
163 |
163 |
164 (* rep-abs injection *) |
|
165 |
|
166 ML {* |
|
167 (* FIXME: is this the right get_fun function for rep-abs injection *) |
|
168 fun mk_repabs lthy (T, T') trm = |
|
169 Quotient_Def.get_fun repF lthy (T, T') |
|
170 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
|
171 *} |
|
172 |
|
173 ML {* |
|
174 (* replaces a term for the bound variable, *) |
|
175 (* possible capture *) |
|
176 fun replace_bnd0 (trm, Abs (x, T, t)) = |
|
177 Abs (x, T, subst_bound (trm, t)) |
|
178 *} |
|
179 |
|
180 |
|
181 ML {* |
|
182 (* bound variables need to be treated properly, *) |
|
183 (* as the type of subterms need to be calculated *) |
|
184 |
|
185 fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh) |
|
186 |
|
187 fun inj_REPABS lthy (rtrm, qtrm) = |
|
188 let |
|
189 val rty = fastype_of rtrm |
|
190 val qty = fastype_of qtrm |
|
191 in |
|
192 case (rtrm, qtrm) of |
|
193 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
|
194 Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
195 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
|
196 Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
197 | (Const (@{const_name "Babs"}, T) $ r $ t, t') => |
|
198 Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
199 | (Abs (x, T, t), Abs (x', T', t')) => |
|
200 let |
|
201 val (y, s) = Term.dest_abs (x, T, t) |
|
202 val (_, s') = Term.dest_abs (x', T', t') |
|
203 val yvar = Free (y, T) |
|
204 val res = lambda yvar (inj_REPABS lthy (s, s')) |
|
205 in |
|
206 if rty = qty |
|
207 then res |
|
208 else if T = T' |
|
209 then mk_repabs lthy (rty, qty) res |
|
210 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
|
211 end |
|
212 | _ => |
|
213 let |
|
214 val (rhead, rargs) = strip_comb rtrm |
|
215 val (qhead, qargs) = strip_comb qtrm |
|
216 (* TODO: val rhead' = inj_REPABS lthy (rhead, qhead) *) |
|
217 val rhead' = rhead; |
|
218 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs); |
|
219 val result = list_comb (rhead', rargs'); |
|
220 in |
|
221 if rty = qty then result else |
|
222 if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else |
|
223 if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else |
|
224 if rargs' = [] then rhead' else result |
|
225 end |
|
226 end |
|
227 *} |
|
228 |
|
229 ML {* |
|
230 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = |
|
231 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
|
232 *} |
|
233 |
164 |
234 lemma plus_assoc_pre: |
165 lemma plus_assoc_pre: |
235 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
166 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
236 apply (cases i) |
167 apply (cases i) |
237 apply (cases j) |
168 apply (cases j) |
276 DT ctxt "C" (atac), |
208 DT ctxt "C" (atac), |
277 DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
209 DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
278 DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), |
210 DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), |
279 DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] |
211 DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] |
280 *} |
212 *} |
|
213 *) |
281 |
214 |
282 ML {* |
215 ML {* |
283 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
216 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
284 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
217 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
285 val consts = lookup_quot_consts defs |
218 val consts = lookup_quot_consts defs |
296 ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *} |
229 ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *} |
297 ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *} |
230 ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *} |
298 |
231 |
299 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} |
232 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} |
300 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
233 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
301 (* does not work *) |
234 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
302 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms *}) |
235 done |
303 |
|
304 |
236 |
305 ML {* |
237 ML {* |
306 inj_REPABS @{context} (reg_atrm, aqtrm) |
238 inj_REPABS @{context} (reg_atrm, aqtrm) |
307 |> Syntax.string_of_term @{context} |
239 |> Syntax.string_of_term @{context} |
308 |> writeln |
240 |> writeln |