equal
deleted
inserted
replaced
444 fun sel_app_same c n sel (con, args) = |
444 fun sel_app_same c n sel (con, args) = |
445 let |
445 let |
446 val nlas = nonlazy args; |
446 val nlas = nonlazy args; |
447 val vns = map vname args; |
447 val vns = map vname args; |
448 val vnn = List.nth (vns, n); |
448 val vnn = List.nth (vns, n); |
449 val nlas' = List.filter (fn v => v <> vnn) nlas; |
449 val nlas' = filter (fn v => v <> vnn) nlas; |
450 val lhs = (%%:sel)`(con_app con args); |
450 val lhs = (%%:sel)`(con_app con args); |
451 val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); |
451 val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); |
452 fun tacs1 ctxt = |
452 fun tacs1 ctxt = |
453 if vnn mem nlas |
453 if vnn mem nlas |
454 then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn] |
454 then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn] |
553 foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)); |
553 foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)); |
554 val prem = rel (con_app con largs, con_app con rargs); |
554 val prem = rel (con_app con largs, con_app con rargs); |
555 val sargs = case largs of [_] => [] | _ => nonlazy args; |
555 val sargs = case largs of [_] => [] | _ => nonlazy args; |
556 val prop = lift_defined %: (sargs, mk_trp (prem === concl)); |
556 val prop = lift_defined %: (sargs, mk_trp (prem === concl)); |
557 in pg con_appls prop end; |
557 in pg con_appls prop end; |
558 val cons' = List.filter (fn (_,args) => args<>[]) cons; |
558 val cons' = filter (fn (_,args) => args<>[]) cons; |
559 in |
559 in |
560 val _ = trace " Proving inverts..."; |
560 val _ = trace " Proving inverts..."; |
561 val inverts = |
561 val inverts = |
562 let |
562 let |
563 val abs_less = ax_abs_iso RS (allI RS injection_less); |
563 val abs_less = ax_abs_iso RS (allI RS injection_less); |
591 if DatatypeAux.is_rec_type (dtyp_of arg) |
591 if DatatypeAux.is_rec_type (dtyp_of arg) |
592 then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg) |
592 then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg) |
593 else (%# arg); |
593 else (%# arg); |
594 val rhs = con_app2 con one_rhs args; |
594 val rhs = con_app2 con one_rhs args; |
595 val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); |
595 val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); |
596 val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args; |
596 val args' = filter_out (fn a => is_rec a orelse is_lazy a) args; |
597 val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts}; |
597 val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts}; |
598 fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; |
598 fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; |
599 val rules = [ax_abs_iso] @ @{thms domain_fun_simps}; |
599 val rules = [ax_abs_iso] @ @{thms domain_fun_simps}; |
600 val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; |
600 val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; |
601 in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; |
601 in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; |
614 in pg [] goal tacs end; |
614 in pg [] goal tacs end; |
615 |
615 |
616 fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; |
616 fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; |
617 in |
617 in |
618 val _ = trace " Proving copy_stricts..."; |
618 val _ = trace " Proving copy_stricts..."; |
619 val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons); |
619 val copy_stricts = map one_strict (filter has_nonlazy_rec cons); |
620 end; |
620 end; |
621 |
621 |
622 val copy_rews = copy_strict :: copy_apps @ copy_stricts; |
622 val copy_rews = copy_strict :: copy_apps @ copy_stricts; |
623 |
623 |
624 in |
624 in |
720 val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); |
720 val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); |
721 val rhs = con_app2 con one_rhs args; |
721 val rhs = con_app2 con one_rhs args; |
722 in Library.foldr mk_all (map vname args, lhs === rhs) end; |
722 in Library.foldr mk_all (map vname args, lhs === rhs) end; |
723 fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; |
723 fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; |
724 val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs)); |
724 val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs)); |
725 val simps = List.filter (has_fewer_prems 1) copy_rews; |
725 val simps = filter (has_fewer_prems 1) copy_rews; |
726 fun con_tac ctxt (con, args) = |
726 fun con_tac ctxt (con, args) = |
727 if nonlazy_rec args = [] |
727 if nonlazy_rec args = [] |
728 then all_tac |
728 then all_tac |
729 else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN |
729 else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN |
730 asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; |
730 asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; |
745 local |
745 local |
746 fun one_con p (con,args) = |
746 fun one_con p (con,args) = |
747 let |
747 let |
748 fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; |
748 fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; |
749 val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); |
749 val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); |
750 val t2 = lift ind_hyp (List.filter is_rec args, t1); |
750 val t2 = lift ind_hyp (filter is_rec args, t1); |
751 val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); |
751 val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); |
752 in Library.foldr mk_All (map vname args, t3) end; |
752 in Library.foldr mk_All (map vname args, t3) end; |
753 |
753 |
754 fun one_eq ((p, cons), concl) = |
754 fun one_eq ((p, cons), concl) = |
755 mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); |
755 mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); |
765 (maps (fn cons => |
765 (maps (fn cons => |
766 (resolve_tac prems 1 :: |
766 (resolve_tac prems 1 :: |
767 maps (fn (_,args) => |
767 maps (fn (_,args) => |
768 resolve_tac prems 1 :: |
768 resolve_tac prems 1 :: |
769 map (K(atac 1)) (nonlazy args) @ |
769 map (K(atac 1)) (nonlazy args) @ |
770 map (K(atac 1)) (List.filter is_rec args)) |
770 map (K(atac 1)) (filter is_rec args)) |
771 cons)) |
771 cons)) |
772 conss); |
772 conss); |
773 local |
773 local |
774 (* check whether every/exists constructor of the n-th part of the equation: |
774 (* check whether every/exists constructor of the n-th part of the equation: |
775 it has a possibly indirectly recursive argument that isn't/is possibly |
775 it has a possibly indirectly recursive argument that isn't/is possibly |
810 fun arg_tac arg = |
810 fun arg_tac arg = |
811 case_UU_tac context (prems @ con_rews) 1 |
811 case_UU_tac context (prems @ con_rews) 1 |
812 (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); |
812 (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); |
813 fun con_tacs (con, args) = |
813 fun con_tacs (con, args) = |
814 asm_simp_tac take_ss 1 :: |
814 asm_simp_tac take_ss 1 :: |
815 map arg_tac (List.filter is_nonlazy_rec args) @ |
815 map arg_tac (filter is_nonlazy_rec args) @ |
816 [resolve_tac prems 1] @ |
816 [resolve_tac prems 1] @ |
817 map (K (atac 1)) (nonlazy args) @ |
817 map (K (atac 1)) (nonlazy args) @ |
818 map (K (etac spec 1)) (List.filter is_rec args); |
818 map (K (etac spec 1)) (filter is_rec args); |
819 fun cases_tacs (cons, cases) = |
819 fun cases_tacs (cons, cases) = |
820 res_inst_tac context [(("x", 0), "x")] cases 1 :: |
820 res_inst_tac context [(("x", 0), "x")] cases 1 :: |
821 asm_simp_tac (take_ss addsimps prems) 1 :: |
821 asm_simp_tac (take_ss addsimps prems) 1 :: |
822 maps con_tacs cons; |
822 maps con_tacs cons; |
823 in |
823 in |