321 (case (bare_concl goal) of |
321 (case (bare_concl goal) of |
322 (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) |
322 (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) |
323 (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
323 (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
324 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
324 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
325 |
325 |
326 | Const (@{const_name "op ="},_) $ |
|
327 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
328 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
329 rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1} |
|
330 |
|
331 (* TODO: Check why less _ are needed then in EX/ALL cases *) |
|
332 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
333 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $ |
|
334 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) |
|
335 rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
336 |
|
337 (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) |
326 (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) |
338 | (Const (@{const_name "op ="},_) $ |
327 | (Const (@{const_name "op ="},_) $ |
339 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
328 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
340 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
329 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
341 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
330 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
354 |
343 |
355 (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) |
344 (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) |
356 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
345 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
357 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
346 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
358 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
347 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
348 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
349 |
|
350 | Const (@{const_name "op ="},_) $ |
|
351 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
352 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
353 => rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1} |
|
354 |
|
355 (* TODO: Check why less _ are needed then in EX/ALL cases *) |
|
356 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
357 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $ |
|
358 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) |
359 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
359 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
360 |
360 |
361 | (_ $ |
361 | (_ $ |
362 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
362 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
363 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
363 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |