812 handle ERROR "find_qt_asm: no pair" => no_tac) |
812 handle ERROR "find_qt_asm: no pair" => no_tac) |
813 | _ => no_tac) |
813 | _ => no_tac) |
814 *} |
814 *} |
815 |
815 |
816 ML {* |
816 ML {* |
|
817 fun equals_rsp_tac R ctxt = |
|
818 let |
|
819 val t = domain_type (fastype_of R); |
|
820 val thy = ProofContext.theory_of ctxt |
|
821 val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
|
822 in |
|
823 rtac thm THEN' RANGE [quotient_tac ctxt] |
|
824 end |
|
825 handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac |
|
826 *} |
|
827 |
|
828 ML {* |
817 fun rep_abs_rsp_tac ctxt = |
829 fun rep_abs_rsp_tac ctxt = |
818 SUBGOAL (fn (goal, i) => |
830 SUBGOAL (fn (goal, i) => |
819 case (bare_concl goal) of |
831 case (bare_concl goal) of |
820 (rel $ _ $ (rep $ (abs $ _))) => |
832 (rel $ _ $ (rep $ (abs $ _))) => |
821 (let |
833 (let |
831 handle _ => no_tac) |
843 handle _ => no_tac) |
832 | _ => no_tac) |
844 | _ => no_tac) |
833 *} |
845 *} |
834 |
846 |
835 ML {* |
847 ML {* |
836 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
848 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
837 (case (bare_concl goal) of |
849 (case (bare_concl goal) of |
838 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
850 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
839 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
851 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
840 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
852 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
841 |
853 |
866 | (_ $ |
878 | (_ $ |
867 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
879 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
868 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
880 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
869 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
881 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
870 |
882 |
|
883 | Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE' |
|
884 (equals_rsp_tac R ctxt THEN' RANGE [ |
|
885 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) |
|
886 |
871 (* reflexivity of operators arising from Cong_tac *) |
887 (* reflexivity of operators arising from Cong_tac *) |
872 | Const (@{const_name "op ="},_) $ _ $ _ |
888 | Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} |
873 => rtac @{thm refl} (*ORELSE' |
|
874 (resolve_tac trans2 THEN' RANGE [ |
|
875 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*) |
|
876 |
889 |
877 (* respectfulness of constants; in particular of a simple relation *) |
890 (* respectfulness of constants; in particular of a simple relation *) |
878 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
891 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
879 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
892 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
880 |
893 |
886 | _ => error "inj_repabs_tac not a relation" |
899 | _ => error "inj_repabs_tac not a relation" |
887 ) i) |
900 ) i) |
888 *} |
901 *} |
889 |
902 |
890 ML {* |
903 ML {* |
891 fun inj_repabs_step_tac ctxt rel_refl trans2 = |
904 fun inj_repabs_step_tac ctxt rel_refl = |
892 (FIRST' [ |
905 (FIRST' [ |
893 NDT ctxt "0" (inj_repabs_tac_match ctxt trans2), |
906 NDT ctxt "0" (inj_repabs_tac_match ctxt), |
894 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
907 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
895 |
908 |
896 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
909 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
897 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), |
910 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), |
898 |
|
899 (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *) |
|
900 NDT ctxt "B" (resolve_tac trans2 THEN' |
|
901 RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
|
902 |
911 |
903 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
912 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
904 (* merge with previous tactic *) |
913 (* merge with previous tactic *) |
905 NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN' |
914 NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN' |
906 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
915 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
919 |
928 |
920 ML {* |
929 ML {* |
921 fun inj_repabs_tac ctxt = |
930 fun inj_repabs_tac ctxt = |
922 let |
931 let |
923 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
932 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
924 val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt) |
|
925 in |
933 in |
926 inj_repabs_step_tac ctxt rel_refl trans2 |
934 inj_repabs_step_tac ctxt rel_refl |
927 end |
935 end |
928 |
936 |
929 fun all_inj_repabs_tac ctxt = |
937 fun all_inj_repabs_tac ctxt = |
930 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
938 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
931 *} |
939 *} |