src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 33396 45c5c3c51918
parent 33317 b4534348b8fd
child 33427 3182812d33ed
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Nov 02 19:56:06 2009 +0100
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Nov 02 12:26:23 2009 -0800
     1.3 @@ -33,6 +33,8 @@
     1.4  val antisym_less_inverse = @{thm below_antisym_inverse};
     1.5  val beta_cfun = @{thm beta_cfun};
     1.6  val cfun_arg_cong = @{thm cfun_arg_cong};
     1.7 +val ch2ch_fst = @{thm ch2ch_fst};
     1.8 +val ch2ch_snd = @{thm ch2ch_snd};
     1.9  val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
    1.10  val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
    1.11  val chain_iterate = @{thm chain_iterate};
    1.12 @@ -43,6 +45,14 @@
    1.13  val compact_up = @{thm compact_up};
    1.14  val contlub_cfun_arg = @{thm contlub_cfun_arg};
    1.15  val contlub_cfun_fun = @{thm contlub_cfun_fun};
    1.16 +val contlub_fst = @{thm contlub_fst};
    1.17 +val contlub_snd = @{thm contlub_snd};
    1.18 +val contlubE = @{thm contlubE};
    1.19 +val cont_const = @{thm cont_const};
    1.20 +val cont_id = @{thm cont_id};
    1.21 +val cont2cont_fst = @{thm cont2cont_fst};
    1.22 +val cont2cont_snd = @{thm cont2cont_snd};
    1.23 +val cont2cont_Rep_CFun = @{thm cont2cont_Rep_CFun};
    1.24  val fix_def2 = @{thm fix_def2};
    1.25  val injection_eq = @{thm injection_eq};
    1.26  val injection_less = @{thm injection_below};
    1.27 @@ -116,7 +126,7 @@
    1.28  
    1.29  val chain_tac =
    1.30    REPEAT_DETERM o resolve_tac 
    1.31 -    [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
    1.32 +    [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL, ch2ch_fst, ch2ch_snd];
    1.33  
    1.34  (* ----- general proofs ----------------------------------------------------- *)
    1.35  
    1.36 @@ -589,7 +599,7 @@
    1.37        val lhs = dc_copy`%"f"`(con_app con args);
    1.38        fun one_rhs arg =
    1.39            if DatatypeAux.is_rec_type (dtyp_of arg)
    1.40 -          then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
    1.41 +          then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
    1.42            else (%# arg);
    1.43        val rhs = con_app2 con one_rhs args;
    1.44        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
    1.45 @@ -836,12 +846,14 @@
    1.46            val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
    1.47            val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
    1.48            val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
    1.49 +          val rules = [contlub_fst RS contlubE RS ssubst,
    1.50 +                       contlub_snd RS contlubE RS ssubst];
    1.51            fun tacf {prems, context} = [
    1.52              res_inst_tac context [(("t", 0), x_name n    )] (ax_reach RS subst) 1,
    1.53              res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
    1.54              stac fix_def2 1,
    1.55              REPEAT (CHANGED
    1.56 -              (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
    1.57 +              (resolve_tac rules 1 THEN chain_tac 1)),
    1.58              stac contlub_cfun_fun 1,
    1.59              stac contlub_cfun_fun 2,
    1.60              rtac lub_equal 3,
    1.61 @@ -955,6 +967,9 @@
    1.62              fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
    1.63              fun concf n dn = %:(P_name n) $ %:(x_name n);
    1.64            in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
    1.65 +        val cont_rules =
    1.66 +            [cont_id, cont_const, cont2cont_Rep_CFun,
    1.67 +             cont2cont_fst, cont2cont_snd];
    1.68          fun tacf {prems, context} =
    1.69            map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
    1.70            quant_tac context 1,
    1.71 @@ -963,13 +978,14 @@
    1.72            REPEAT_DETERM (
    1.73              TRY (rtac adm_conj 1) THEN 
    1.74              rtac adm_subst 1 THEN 
    1.75 -            cont_tacR 1 THEN resolve_tac prems 1),
    1.76 +            REPEAT (resolve_tac cont_rules 1) THEN
    1.77 +            resolve_tac prems 1),
    1.78            strip_tac 1,
    1.79            rtac (rewrite_rule axs_take_def finite_ind) 1,
    1.80            ind_prems_tac prems];
    1.81          val ind = (pg'' thy [] goal tacf
    1.82            handle ERROR _ =>
    1.83 -            (warning "Cannot prove infinite induction rule"; refl));
    1.84 +            (warning "Cannot prove infinite induction rule"; TrueI));
    1.85        in (finites, ind) end
    1.86    )
    1.87        handle THM _ =>