move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
authorhuffman
Fri Oct 15 08:52:53 2010 -0700 (2010-10-15)
changeset 40023a868e9d73031
parent 40022 3a4a24b714f3
child 40024 a0f760ef6995
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Oct 15 08:07:20 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Oct 15 08:52:53 2010 -0700
     1.3 @@ -148,35 +148,26 @@
     1.4  (******************************************************************************)
     1.5  
     1.6  fun prove_induction
     1.7 -    (comp_dbind : binding, eqs : Domain_Library.eq list)
     1.8 +    (comp_dbind : binding)
     1.9      (constr_infos : Domain_Constructors.constr_info list)
    1.10      (take_info : Domain_Take_Proofs.take_induct_info)
    1.11      (take_rews : thm list)
    1.12      (thy : theory) =
    1.13  let
    1.14    val comp_dname = Sign.full_name thy comp_dbind;
    1.15 -  val dnames = map (fst o fst) eqs;
    1.16 -  val conss  = map  snd        eqs;
    1.17  
    1.18    val iso_infos = map #iso_info constr_infos;
    1.19 -  val axs_rep_iso = map #rep_inverse iso_infos;
    1.20 -  val axs_abs_iso = map #abs_inverse iso_infos;
    1.21    val exhausts = map #exhaust constr_infos;
    1.22    val con_rews = maps #con_rews constr_infos;
    1.23 -
    1.24 -  val {take_consts, ...} = take_info;
    1.25 -  val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
    1.26 -  val {lub_take_thms, finite_defs, reach_thms, ...} = take_info;
    1.27 -  val {take_induct_thms, ...} = take_info;
    1.28 +  val {take_consts, take_induct_thms, ...} = take_info;
    1.29  
    1.30    val newTs = map #absT iso_infos;
    1.31 -  val P_names = Datatype_Prop.indexify_names (map (K "P") dnames);
    1.32 -  val x_names = Datatype_Prop.indexify_names (map (K "x") dnames);
    1.33 +  val P_names = Datatype_Prop.indexify_names (map (K "P") newTs);
    1.34 +  val x_names = Datatype_Prop.indexify_names (map (K "x") newTs);
    1.35    val P_types = map (fn T => T --> HOLogic.boolT) newTs;
    1.36    val Ps = map Free (P_names ~~ P_types);
    1.37    val xs = map Free (x_names ~~ newTs);
    1.38    val n = Free ("n", HOLogic.natT);
    1.39 -  val taken = "n" :: P_names @ x_names;
    1.40  
    1.41    fun con_assm defined p (con, args) =
    1.42      let
    1.43 @@ -195,40 +186,22 @@
    1.44        mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons;
    1.45    val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos);
    1.46  
    1.47 -  fun ind_term concls =
    1.48 -    Logic.list_implies (assms, mk_trp (foldr1 mk_conj concls));
    1.49 -
    1.50    val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
    1.51    fun quant_tac ctxt i = EVERY
    1.52      (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names);
    1.53  
    1.54 -  local
    1.55 -    open Domain_Library;
    1.56 -    fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
    1.57 -          is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
    1.58 -          ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse 
    1.59 -            rec_of arg <> n andalso rec_to (rec_of arg::ns) 
    1.60 -              (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
    1.61 -          ) o snd) cons;
    1.62 -    fun warn (n,cons) =
    1.63 -      if rec_to [] false (n,cons)
    1.64 -      then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
    1.65 -      else false;
    1.66 +  (* FIXME: move this message to domain_take_proofs.ML *)
    1.67 +  val is_finite = #is_finite take_info;
    1.68 +  val _ = if is_finite
    1.69 +          then message ("Proving finiteness rule for domain "^comp_dname^" ...")
    1.70 +          else ();
    1.71  
    1.72 -  in
    1.73 -    val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
    1.74 -    val is_emptys = map warn n__eqs;
    1.75 -    val is_finite = #is_finite take_info;
    1.76 -    val _ = if is_finite
    1.77 -            then message ("Proving finiteness rule for domain "^comp_dname^" ...")
    1.78 -            else ();
    1.79 -  end;
    1.80    val _ = trace " Proving finite_ind...";
    1.81    val finite_ind =
    1.82      let
    1.83        val concls =
    1.84 -          map (fn ((P, t), x) => P $ HOLCF_Library.mk_capply (t $ n, x))
    1.85 -              (Ps ~~ #take_consts take_info ~~ xs);
    1.86 +          map (fn ((P, t), x) => P $ mk_capply (t $ n, x))
    1.87 +              (Ps ~~ take_consts ~~ xs);
    1.88        val goal = mk_trp (foldr1 mk_conj concls);
    1.89  
    1.90        fun tacf {prems, context} =
    1.91 @@ -271,10 +244,6 @@
    1.92          end;
    1.93      in Goal.prove_global thy [] assms goal tacf end;
    1.94  
    1.95 -(* ----- theorems concerning finiteness and induction ----------------------- *)
    1.96 -
    1.97 -  val global_ctxt = ProofContext.init_global thy;
    1.98 -
    1.99    val _ = trace " Proving ind...";
   1.100    val ind =
   1.101      let
   1.102 @@ -294,23 +263,26 @@
   1.103          end;
   1.104      in Goal.prove_global thy [] (adms @ assms) goal tacf end
   1.105  
   1.106 -val case_ns =
   1.107 -  let
   1.108 -    val adms =
   1.109 -        if is_finite then [] else
   1.110 -        if length dnames = 1 then ["adm"] else
   1.111 -        map (fn s => "adm_" ^ Long_Name.base_name s) dnames;
   1.112 -    val bottoms =
   1.113 -        if length dnames = 1 then ["bottom"] else
   1.114 -        map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
   1.115 -    fun one_eq bot (_,cons) =
   1.116 -          bot :: map (fn (c,_) => Long_Name.base_name c) cons;
   1.117 -  in adms @ flat (map2 one_eq bottoms eqs) end;
   1.118 +  (* case names for induction rules *)
   1.119 +  val dnames = map (fst o dest_Type) newTs;
   1.120 +  val case_ns =
   1.121 +    let
   1.122 +      val adms =
   1.123 +          if is_finite then [] else
   1.124 +          if length dnames = 1 then ["adm"] else
   1.125 +          map (fn s => "adm_" ^ Long_Name.base_name s) dnames;
   1.126 +      val bottoms =
   1.127 +          if length dnames = 1 then ["bottom"] else
   1.128 +          map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
   1.129 +      fun one_eq bot constr_info =
   1.130 +        let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c));
   1.131 +        in bot :: map name_of (#con_specs constr_info) end;
   1.132 +    in adms @ flat (map2 one_eq bottoms constr_infos) end;
   1.133  
   1.134 -val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
   1.135 -fun ind_rule (dname, rule) =
   1.136 -    ((Binding.empty, [rule]),
   1.137 -     [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
   1.138 +  val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
   1.139 +  fun ind_rule (dname, rule) =
   1.140 +      ((Binding.empty, [rule]),
   1.141 +       [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
   1.142  
   1.143  in
   1.144    thy
   1.145 @@ -475,12 +447,27 @@
   1.146      (constr_infos : Domain_Constructors.constr_info list)
   1.147      (thy : theory) =
   1.148  let
   1.149 -val map_tab = Domain_Take_Proofs.get_map_tab thy;
   1.150 -
   1.151  val dnames = map (fst o fst) eqs;
   1.152  val comp_dname = Sign.full_name thy comp_dbind;
   1.153  
   1.154 -(* ----- getting the composite axiom and definitions ------------------------ *)
   1.155 +(* Test for emptiness *)
   1.156 +local
   1.157 +  open Domain_Library;
   1.158 +  val conss = map snd eqs;
   1.159 +  fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
   1.160 +        is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
   1.161 +        ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse 
   1.162 +          rec_of arg <> n andalso rec_to (rec_of arg::ns) 
   1.163 +            (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
   1.164 +        ) o snd) cons;
   1.165 +  fun warn (n,cons) =
   1.166 +    if rec_to [] false (n,cons)
   1.167 +    then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
   1.168 +    else false;
   1.169 +in
   1.170 +  val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
   1.171 +  val is_emptys = map warn n__eqs;
   1.172 +end;
   1.173  
   1.174  (* Test for indirect recursion *)
   1.175  local
   1.176 @@ -509,7 +496,7 @@
   1.177  (* prove induction rules, unless definition is indirect recursive *)
   1.178  val thy =
   1.179      if is_indirect then thy else
   1.180 -    prove_induction (comp_dbind, eqs) constr_infos take_info take_rews thy;
   1.181 +    prove_induction comp_dbind constr_infos take_info take_rews thy;
   1.182  
   1.183  val thy =
   1.184      if is_indirect then thy else