872 | Const (@{const_name "op ="},_) $ _ $ _ |
872 | Const (@{const_name "op ="},_) $ _ $ _ |
873 => rtac @{thm refl} (*ORELSE' |
873 => rtac @{thm refl} (*ORELSE' |
874 (resolve_tac trans2 THEN' RANGE [ |
874 (resolve_tac trans2 THEN' RANGE [ |
875 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*) |
875 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*) |
876 |
876 |
877 (* TODO: These patterns should should be somehow combined and generalized... *) |
|
878 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
879 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
880 (Const (@{const_name fun_rel}, _) $ _ $ _) |
|
881 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
|
882 |
|
883 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
884 (Const (@{const_name prod_rel}, _) $ _ $ _) $ |
|
885 (Const (@{const_name prod_rel}, _) $ _ $ _) |
|
886 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
|
887 |
|
888 (* respectfulness of constants; in particular of a simple relation *) |
877 (* respectfulness of constants; in particular of a simple relation *) |
889 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
878 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
890 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
879 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
891 |
880 |
892 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
881 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
893 (* observe ---> *) |
882 (* observe ---> *) |
894 | _ $ _ $ _ |
883 | _ $ _ $ _ |
895 => rep_abs_rsp_tac ctxt |
884 => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt |
896 |
885 |
897 | _ => error "inj_repabs_tac not a relation" |
886 | _ => error "inj_repabs_tac not a relation" |
898 ) i) |
887 ) i) |
899 *} |
888 *} |
900 |
889 |