src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 33317 b4534348b8fd
parent 32957 675c0c7e6a37
child 33396 45c5c3c51918
equal deleted inserted replaced
33316:6a72af4e84b8 33317:b4534348b8fd
   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