808 handle ERROR "find_qt_asm: no pair" => no_tac) |
808 handle ERROR "find_qt_asm: no pair" => no_tac) |
809 | _ => no_tac) |
809 | _ => no_tac) |
810 *} |
810 *} |
811 |
811 |
812 ML {* |
812 ML {* |
|
813 fun equals_rsp_tac R ctxt = |
|
814 let |
|
815 val t = domain_type (fastype_of R); |
|
816 val thy = ProofContext.theory_of ctxt |
|
817 val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
|
818 in |
|
819 rtac thm THEN' RANGE [quotient_tac ctxt] |
|
820 end |
|
821 handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac |
|
822 *} |
|
823 |
|
824 ML {* |
813 fun rep_abs_rsp_tac ctxt = |
825 fun rep_abs_rsp_tac ctxt = |
814 SUBGOAL (fn (goal, i) => |
826 SUBGOAL (fn (goal, i) => |
815 case (bare_concl goal) of |
827 case (bare_concl goal) of |
816 (rel $ _ $ (rep $ (abs $ _))) => |
828 (rel $ _ $ (rep $ (abs $ _))) => |
817 (let |
829 (let |
827 handle _ => no_tac) |
839 handle _ => no_tac) |
828 | _ => no_tac) |
840 | _ => no_tac) |
829 *} |
841 *} |
830 |
842 |
831 ML {* |
843 ML {* |
832 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
844 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
833 (case (bare_concl goal) of |
845 (case (bare_concl goal) of |
834 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
846 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
835 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
847 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
836 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
848 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
837 |
849 |
862 | (_ $ |
874 | (_ $ |
863 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
875 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
864 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
876 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
865 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
877 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
866 |
878 |
|
879 | Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE' |
|
880 (equals_rsp_tac R ctxt THEN' RANGE [ |
|
881 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) |
|
882 |
867 (* reflexivity of operators arising from Cong_tac *) |
883 (* reflexivity of operators arising from Cong_tac *) |
868 | Const (@{const_name "op ="},_) $ _ $ _ |
884 | Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} |
869 => rtac @{thm refl} (*ORELSE' |
|
870 (resolve_tac trans2 THEN' RANGE [ |
|
871 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*) |
|
872 |
885 |
873 (* respectfulness of constants; in particular of a simple relation *) |
886 (* respectfulness of constants; in particular of a simple relation *) |
874 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
887 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
875 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
888 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
876 |
889 |
882 | _ => error "inj_repabs_tac not a relation" |
895 | _ => error "inj_repabs_tac not a relation" |
883 ) i) |
896 ) i) |
884 *} |
897 *} |
885 |
898 |
886 ML {* |
899 ML {* |
887 fun inj_repabs_step_tac ctxt rel_refl trans2 = |
900 fun inj_repabs_step_tac ctxt rel_refl = |
888 (FIRST' [ |
901 (FIRST' [ |
889 NDT ctxt "0" (inj_repabs_tac_match ctxt trans2), |
902 NDT ctxt "0" (inj_repabs_tac_match ctxt), |
890 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
903 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
891 |
904 |
892 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
905 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
893 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), |
906 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), |
894 |
|
895 (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *) |
|
896 NDT ctxt "B" (resolve_tac trans2 THEN' |
|
897 RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
|
898 |
907 |
899 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
908 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
900 (* merge with previous tactic *) |
909 (* merge with previous tactic *) |
901 NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN' |
910 NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN' |
902 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
911 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
915 |
924 |
916 ML {* |
925 ML {* |
917 fun inj_repabs_tac ctxt = |
926 fun inj_repabs_tac ctxt = |
918 let |
927 let |
919 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
928 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
920 val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt) |
|
921 in |
929 in |
922 inj_repabs_step_tac ctxt rel_refl trans2 |
930 inj_repabs_step_tac ctxt rel_refl |
923 end |
931 end |
924 |
932 |
925 fun all_inj_repabs_tac ctxt = |
933 fun all_inj_repabs_tac ctxt = |
926 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
934 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
927 *} |
935 *} |
928 |
936 |
929 section {* Cleaning of the Theorem *} |
937 section {* Cleaning of the Theorem *} |
930 |
938 |
|
939 (* Since the patterns for the lhs are different; there are 3 different make-insts *) |
|
940 (* 1: does ? \<rightarrow> id *) |
|
941 (* 2: does id \<rightarrow> ? *) |
|
942 (* 3: does ? \<rightarrow> ? *) |
931 ML {* |
943 ML {* |
932 fun make_inst lhs t = |
944 fun make_inst lhs t = |
933 let |
945 let |
934 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
946 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
935 val _ $ (Abs (_, _, g)) = t; |
947 val _ $ (Abs (_, _, g)) = t; |
941 | Bound j => if i = j then error "make_inst" else t |
953 | Bound j => if i = j then error "make_inst" else t |
942 | _ => t); |
954 | _ => t); |
943 in (f, Abs ("x", T, mk_abs 0 g)) end; |
955 in (f, Abs ("x", T, mk_abs 0 g)) end; |
944 *} |
956 *} |
945 |
957 |
946 (* Since the patterns for the lhs are different; there are 2 different make-insts *) |
|
947 ML {* |
958 ML {* |
948 fun make_inst2 lhs t = |
959 fun make_inst2 lhs t = |
949 let |
960 let |
950 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
961 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
951 val _ = tracing "a"; |
962 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
963 fun mk_abs i t = |
|
964 if incr_boundvars i u aconv t then Bound i |
|
965 else (case t of |
|
966 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
967 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
|
968 | Bound j => if i = j then error "make_inst" else t |
|
969 | _ => t); |
|
970 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
971 *} |
|
972 |
|
973 ML {* |
|
974 fun make_inst3 lhs t = |
|
975 let |
|
976 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
952 val _ $ (Abs (_, _, (_ $ g))) = t; |
977 val _ $ (Abs (_, _, (_ $ g))) = t; |
953 fun mk_abs i t = |
978 fun mk_abs i t = |
954 if incr_boundvars i u aconv t then Bound i |
979 if incr_boundvars i u aconv t then Bound i |
955 else (case t of |
980 else (case t of |
956 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
981 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
970 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
995 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
971 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
996 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
972 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
997 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
973 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
998 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
974 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
999 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
975 val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
|
976 val ti = |
1000 val ti = |
977 (let |
1001 (let |
978 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
1002 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
979 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1003 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
980 in |
1004 in |
981 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1005 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
982 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1006 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
983 let |
1007 let |
984 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1008 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
|
1009 val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); |
|
1010 val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
|
1011 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm) |
|
1012 in |
|
1013 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
|
1014 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
|
1015 let |
|
1016 val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm) |
985 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1017 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
986 in |
1018 in |
987 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1019 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
988 end); |
1020 end); |
989 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1021 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
991 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
1023 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
992 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
1024 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
993 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
1025 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
994 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
1026 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
995 else () |
1027 else () |
|
1028 |
996 in |
1029 in |
997 Conv.rewr_conv ti ctrm |
1030 Conv.rewr_conv ti ctrm |
998 end |
1031 end |
999 handle _ => Conv.all_conv ctrm) |
1032 handle _ => Conv.all_conv ctrm) |
1000 | _ => Conv.all_conv ctrm |
1033 | _ => Conv.all_conv ctrm |