HOLogic.dest_conj;
authorwenzelm
Sun Feb 27 15:26:47 2000 +0100 (2000-02-27)
changeset 830593aa21ec5494
parent 8304 e132d147374b
child 8306 9855f1801d2b
HOLogic.dest_conj;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 27 15:25:31 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 27 15:26:47 2000 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4      val recTs = get_rec_types descr' sorts;
     1.5      val newTs = take (length (hd descr), recTs);
     1.6  
     1.7 -    val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
     1.8 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
     1.9  
    1.10      fun prove_casedist_thm ((i, t), T) =
    1.11        let
    1.12 @@ -109,7 +109,7 @@
    1.13      val used = foldr add_typ_tfree_names (recTs, []);
    1.14      val newTs = take (length (hd descr), recTs);
    1.15  
    1.16 -    val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.17 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.18  
    1.19      val big_rec_name' = big_name ^ "_rec_set";
    1.20      val rec_set_names = map (Sign.full_name (Theory.sign_of thy0))
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Sun Feb 27 15:25:31 2000 +0100
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sun Feb 27 15:26:47 2000 +0100
     2.3 @@ -46,7 +46,6 @@
     2.4    val dest_DtTFree : dtyp -> string
     2.5    val dest_DtRec : dtyp -> int
     2.6    val dest_TFree : typ -> string
     2.7 -  val dest_conj : term -> term list
     2.8    val get_nonrec_types : (int * (string * dtyp list *
     2.9      (string * dtyp list) list)) list -> (string * sort) list -> typ list
    2.10    val get_branching_types : (int * (string * dtyp list *
    2.11 @@ -99,15 +98,13 @@
    2.12  val mk_conj = foldr1 (HOLogic.mk_binop "op &");
    2.13  val mk_disj = foldr1 (HOLogic.mk_binop "op |");
    2.14  
    2.15 -fun dest_conj (Const ("op &", _) $ t $ t') = t::(dest_conj t')
    2.16 -  | dest_conj t = [t];
    2.17  
    2.18  (* instantiate induction rule *)
    2.19  
    2.20  fun indtac indrule i st =
    2.21    let
    2.22 -    val ts = dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
    2.23 -    val ts' = dest_conj (HOLogic.dest_Trueprop
    2.24 +    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
    2.25 +    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
    2.26        (Logic.strip_imp_concl (nth_elem (i - 1, prems_of st))));
    2.27      val getP = if can HOLogic.dest_imp (hd ts) then
    2.28        (apfst Some) o HOLogic.dest_imp else pair None;
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Feb 27 15:25:31 2000 +0100
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Feb 27 15:26:47 2000 +0100
     3.3 @@ -623,7 +623,7 @@
     3.4                [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
     3.5                 etac mp 1, resolve_tac iso_elem_thms 1])]);
     3.6  
     3.7 -    val Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
     3.8 +    val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
     3.9      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
    3.10        map (Free o apfst fst o dest_Var) Ps;
    3.11      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;