author huffman Fri Oct 15 08:07:20 2010 -0700 (2010-10-15) changeset 40022 3a4a24b714f3 parent 40021 d888417f7deb child 40023 a868e9d73031
simplify automation of induct proof
```     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Oct 15 06:08:42 2010 -0700
1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Oct 15 08:07:20 2010 -0700
1.3 @@ -29,18 +29,11 @@
1.4  fun message s = if !quiet_mode then () else writeln s;
1.5  fun trace s = if !trace_domain then tracing s else ();
1.6
1.7 -open Domain_Library;
1.8 +open HOLCF_Library;
1.9  infixr 0 ===>;
1.10 -infixr 0 ==>;
1.11  infix 0 == ;
1.12  infix 1 ===;
1.13 -infix 1 ~= ;
1.14 -infix 1 <<;
1.15 -infix 1 ~<<;
1.16  infix 9 `   ;
1.17 -infix 9 `% ;
1.18 -infix 9 `%%;
1.19 -infixr 9 oo;
1.20
1.21  (* ----- general proof facilities ------------------------------------------- *)
1.22
1.23 @@ -95,8 +88,6 @@
1.24      (constr_infos : Domain_Constructors.constr_info list)
1.25      (thy : theory) : thm list list * theory =
1.26  let
1.27 -  open HOLCF_Library;
1.28 -
1.29    val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info;
1.30    val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
1.31
1.32 @@ -157,7 +148,7 @@
1.33  (******************************************************************************)
1.34
1.35  fun prove_induction
1.36 -    (comp_dbind : binding, eqs : eq list)
1.37 +    (comp_dbind : binding, eqs : Domain_Library.eq list)
1.38      (constr_infos : Domain_Constructors.constr_info list)
1.39      (take_info : Domain_Take_Proofs.take_induct_info)
1.40      (take_rews : thm list)
1.41 @@ -166,7 +157,6 @@
1.42    val comp_dname = Sign.full_name thy comp_dbind;
1.43    val dnames = map (fst o fst) eqs;
1.44    val conss  = map  snd        eqs;
1.45 -  val pg = pg' thy;
1.46
1.47    val iso_infos = map #iso_info constr_infos;
1.48    val axs_rep_iso = map #rep_inverse iso_infos;
1.49 @@ -190,7 +180,6 @@
1.50
1.51    fun con_assm defined p (con, args) =
1.52      let
1.53 -      open HOLCF_Library;
1.54        val Ts = map snd args;
1.55        val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts);
1.56        val vs = map Free (ns ~~ Ts);
1.57 @@ -213,16 +202,8 @@
1.58    fun quant_tac ctxt i = EVERY
1.59      (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names);
1.60
1.61 -  fun ind_prems_tac prems = EVERY
1.62 -    (maps (fn cons =>
1.63 -      (resolve_tac prems 1 ::
1.64 -        maps (fn (_,args) =>
1.65 -          resolve_tac prems 1 ::
1.66 -          map (K(atac 1)) (nonlazy args) @
1.67 -          map (K(atac 1)) (filter is_rec args))
1.68 -        cons))
1.69 -      conss);
1.70    local
1.71 +    open Domain_Library;
1.72      fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg =>
1.73            is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
1.74            ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse
1.75 @@ -263,8 +244,7 @@
1.76                val tacs =
1.77                    rewrite_goals_tac @{thms atomize_all atomize_imp} ::
1.78                    map arg_tac args @
1.79 -                  [REPEAT (rtac impI 1)] @
1.80 -                  [ALLGOALS simplify];
1.81 +                  [REPEAT (rtac impI 1), ALLGOALS simplify];
1.82              in
1.83                Goal.prove context [] [] subgoal (K (EVERY tacs))
1.84              end;
1.85 @@ -297,56 +277,22 @@
1.86
1.87    val _ = trace " Proving ind...";
1.88    val ind =
1.89 -    if is_finite
1.90 -    then (* finite case *)
1.91 -      let
1.92 -        val concls = map (op \$) (Ps ~~ xs);
1.93 -        fun tacf {prems, context} =
1.94 -          let
1.95 -            fun finite_tacs (take_induct, fin_ind) = [
1.96 -                rtac take_induct 1,
1.97 -                rtac fin_ind 1,
1.98 -                ind_prems_tac prems];
1.99 -          in
1.100 -            TRY (safe_tac HOL_cs) ::
1.101 -            maps finite_tacs (take_induct_thms ~~ atomize global_ctxt finite_ind)
1.102 -          end;
1.103 -      in pg'' thy [] (ind_term concls) tacf end
1.104 -
1.105 -    else (* infinite case *)
1.106 -      let
1.107 -        val goal =
1.108 -          let
1.110 -            val concls = map (op \$) (Ps ~~ xs);
1.111 -          in Logic.list_implies (map one_adm Ps, ind_term concls) end;
1.112 -        val cont_rules =
1.113 -            @{thms cont_id cont_const cont2cont_Rep_CFun
1.114 -                   cont2cont_fst cont2cont_snd};
1.115 -        val subgoal =
1.116 -          let
1.117 -            val goals =
1.118 -                map (fn ((P,t),x) => P \$ HOLCF_Library.mk_capply (t \$ n, x))
1.119 -                  (Ps ~~ take_consts ~~ xs);
1.120 -          in
1.121 -            HOLogic.mk_Trueprop
1.122 -            (HOLogic.mk_all ("n", HOLogic.natT, foldr1 HOLogic.mk_conj goals))
1.123 -          end;
1.124 -        fun tacf {prems, context} =
1.125 -          let
1.126 -            val subtac =
1.127 -                EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
1.128 -            val subthm = Goal.prove context [] [] subgoal (K subtac);
1.129 -          in
1.130 -            map (fn ax_reach => rtac (ax_reach RS subst) 1) reach_thms @ [
1.131 -            cut_facts_tac (subthm :: take (length dnames) prems) 1,
1.132 -            REPEAT (rtac @{thm conjI} 1 ORELSE
1.133 -                    EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
1.134 -                           resolve_tac chain_take_thms 1,
1.135 -                           asm_simp_tac HOL_basic_ss 1])
1.136 -            ]
1.137 -          end;
1.138 -      in pg'' thy [] goal tacf end;
1.139 +    let
1.140 +      val concls = map (op \$) (Ps ~~ xs);
1.141 +      val goal = mk_trp (foldr1 mk_conj concls);
1.142 +      val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps;
1.143 +      fun tacf {prems, context} =
1.144 +        let
1.145 +          fun finite_tac (take_induct, fin_ind) =
1.146 +              rtac take_induct 1 THEN
1.147 +              (if is_finite then all_tac else resolve_tac prems 1) THEN
1.148 +              (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1;
1.149 +          val fin_inds = Project_Rule.projections context finite_ind;
1.150 +        in
1.151 +          TRY (safe_tac HOL_cs) THEN
1.152 +          EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
1.153 +        end;
1.154 +    in Goal.prove_global thy [] (adms @ assms) goal tacf end
1.155
1.156  val case_ns =
1.157    let
1.158 @@ -379,11 +325,12 @@
1.159  (******************************************************************************)
1.160
1.161  fun prove_coinduction
1.162 -    (comp_dbind : binding, eqs : eq list)
1.163 +    (comp_dbind : binding, eqs : Domain_Library.eq list)
1.164      (take_rews : thm list)
1.165      (take_lemmas : thm list)
1.166      (thy : theory) : theory =
1.167  let
1.168 +open Domain_Library;
1.169
1.170  val dnames = map (fst o fst) eqs;
1.171  val comp_dname = Sign.full_name thy comp_dbind;
1.172 @@ -522,7 +469,7 @@
1.173  (******************************************************************************)
1.174
1.175  fun comp_theorems
1.176 -    (comp_dbind : binding, eqs : eq list)
1.177 +    (comp_dbind : binding, eqs : Domain_Library.eq list)
1.178      (dbinds : binding list)
1.179      (take_info : Domain_Take_Proofs.take_induct_info)
1.180      (constr_infos : Domain_Constructors.constr_info list)
1.181 @@ -537,6 +484,7 @@
1.182
1.183  (* Test for indirect recursion *)
1.184  local
1.185 +  open Domain_Library;
1.186    fun indirect_arg arg =
1.187        rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg);
1.188    fun indirect_con (_, args) = exists indirect_arg args;
```