296 end |
296 end |
297 handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *) |
297 handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *) |
298 | _ => no_tac) |
298 | _ => no_tac) |
299 |
299 |
300 |
300 |
301 (* FIXME / TODO needs to be adapted *) |
|
302 (* |
301 (* |
303 To prove that the regularised theorem implies the abs/rep injected, |
302 To prove that the regularised theorem implies the abs/rep injected, |
304 we try: |
303 we try: |
305 |
304 |
306 1) theorems 'trans2' from the appropriate Quot_Type |
305 The deterministic part: |
307 2) remove lambdas from both sides: lambda_rsp_tac |
306 -) remove lambdas from both sides |
308 3) remove Ball/Bex from the right hand side |
307 -) prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp |
309 4) use user-supplied RSP theorems |
308 -) prove Ball/Bex relations unfolding fun_rel_id |
310 5) remove rep_abs from the right side |
309 -) reflexivity of equality |
311 6) reflexivity of equality |
310 -) prove equality of relations using equals_rsp |
312 7) split applications of lifted type (apply_rsp) |
311 -) use user-supplied RSP theorems |
313 8) split applications of non-lifted type (cong_tac) |
312 -) solve 'relation of relations' goals using quot_rel_rsp |
314 9) apply extentionality |
313 -) remove rep_abs from the right side |
315 A) reflexivity of the relation |
|
316 B) assumption |
|
317 (Lambdas under respects may have left us some assumptions) |
314 (Lambdas under respects may have left us some assumptions) |
318 C) proving obvious higher order equalities by simplifying fun_rel |
315 Then in order: |
319 (not sure if it is still needed?) |
316 -) split applications of lifted type (apply_rsp) |
320 D) unfolding lambda on one side |
317 -) split applications of non-lifted type (cong_tac) |
321 E) simplifying (= ===> =) for simpler respectfulness |
318 -) apply extentionality |
|
319 -) assumption |
|
320 -) reflexivity of the relation |
322 *) |
321 *) |
323 |
322 |
324 |
323 |
325 fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) => |
324 fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) => |
326 (case (bare_concl goal) of |
325 (case (bare_concl goal) of |