952 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
953 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
953 (case (bare_concl goal) of |
954 (case (bare_concl goal) of |
954 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
955 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
955 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
956 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
956 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
957 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
958 |
957 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
959 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
958 | (Const (@{const_name "op ="},_) $ |
960 | (Const (@{const_name "op ="},_) $ |
959 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
961 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
960 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
962 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
961 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
963 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
|
964 |
962 (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *) |
965 (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *) |
963 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
966 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
964 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
967 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
965 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
968 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
966 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
969 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
970 |
967 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
971 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
968 | Const (@{const_name "op ="},_) $ |
972 | Const (@{const_name "op ="},_) $ |
969 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
973 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
970 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
974 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
971 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
975 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
|
976 |
972 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
977 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
973 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
978 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
974 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
979 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
975 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
980 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
976 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
981 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
977 | Const (@{const_name "op ="},_) $ _ $ _ => |
982 |
978 (* reflexivity of operators arising from Cong_tac *) |
983 (* reflexivity of operators arising from Cong_tac *) |
979 rtac @{thm refl} ORELSE' |
984 | Const (@{const_name "op ="},_) $ _ $ _ |
980 (resolve_tac trans2 THEN' RANGE [ |
985 => rtac @{thm refl} ORELSE' |
981 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
986 (resolve_tac trans2 THEN' RANGE [ |
|
987 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
|
988 |
982 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
989 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
983 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
990 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
984 (Const (@{const_name fun_rel}, _) $ _ $ _) |
991 (Const (@{const_name fun_rel}, _) $ _ $ _) |
985 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
992 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
986 | _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *) |
993 |
987 (* respectfulness of constants; in particular of a simple relation *) |
994 (* respectfulness of constants; in particular of a simple relation *) |
988 resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
995 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
989 | _ $ _ $ _ => |
996 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
|
997 |
990 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
998 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
991 (* observe ---> *) |
999 (* observe ---> *) |
992 rep_abs_rsp_tac ctxt |
1000 | _ $ _ $ _ |
|
1001 => rep_abs_rsp_tac ctxt |
|
1002 |
993 | _ => error "inj_repabs_tac not a relation" |
1003 | _ => error "inj_repabs_tac not a relation" |
994 ) i) |
1004 ) i) |
995 *} |
1005 *} |
996 |
1006 |
997 ML {* |
1007 ML {* |