simplify automation of induct proof
authorhuffman
Fri Oct 15 08:07:20 2010 -0700 (2010-10-15)
changeset 400223a4a24b714f3
parent 40021 d888417f7deb
child 40023 a868e9d73031
simplify automation of induct proof
src/HOLCF/Tools/Domain/domain_theorems.ML
     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.109 -            fun one_adm P = mk_trp (mk_adm P);
   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;