filled in gap in library offering
authorblanchet
Wed Sep 25 16:43:46 2013 +0200 (2013-09-25)
changeset 53887ee91bd2a506a
parent 53886 c83727c7a510
child 53888 7031775668e8
filled in gap in library offering
src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
src/HOL/BNF/Tools/bnf_util.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/hologic.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:29:35 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:43:46 2013 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4        (case Term.strip_comb t of
     1.5          (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
     1.6        | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
     1.7 -        fld (conds @ conjuncts cond) then_branch
     1.8 +        fld (conds @ HOLogic.conjuncts cond) then_branch
     1.9          o fld (conds @ s_not_disj cond) else_branch
    1.10        | (Const (c, _), args as _ :: _) =>
    1.11          let val n = num_binder_types (Sign.the_const_type thy c) in
    1.12 @@ -239,7 +239,7 @@
    1.13              (case dest_case ctxt s Ts t of
    1.14                NONE => f conds t
    1.15              | SOME (conds', branches) =>
    1.16 -              fold_rev (uncurry fld) (map (append conds o conjuncts) conds' ~~ branches))
    1.17 +              fold_rev (uncurry fld) (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
    1.18            | _ => f conds t)
    1.19          end
    1.20        | _ => f conds t)
     2.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 16:29:35 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 16:43:46 2013 +0200
     2.3 @@ -134,8 +134,6 @@
     2.4    val list_all_free: term list -> term -> term
     2.5    val list_exists_free: term list -> term -> term
     2.6  
     2.7 -  val conjuncts: term -> term list
     2.8 -
     2.9    (*parameterized terms*)
    2.10    val mk_nthN: int -> term -> int -> term
    2.11  
    2.12 @@ -647,12 +645,6 @@
    2.13  val list_all_free = list_quant_free HOLogic.all_const;
    2.14  val list_exists_free = list_quant_free HOLogic.exists_const;
    2.15  
    2.16 -(*Like dest_conj, but flattens conjunctions however nested*)
    2.17 -fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    2.18 - | conjuncts_aux t conjs = t::conjs;
    2.19 -
    2.20 -fun conjuncts t = conjuncts_aux t [];
    2.21 -
    2.22  fun find_indices eq xs ys = map_filter I
    2.23    (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);
    2.24  
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 25 16:29:35 2013 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 25 16:43:46 2013 +0200
     3.3 @@ -43,7 +43,6 @@
     3.4    val dest_indprem : indprem -> term
     3.5    val map_indprem : (term -> term) -> indprem -> indprem
     3.6    (* general syntactic functions *)
     3.7 -  val conjuncts : term -> term list
     3.8    val is_equationlike : thm -> bool
     3.9    val is_pred_equation : thm -> bool
    3.10    val is_intro : string -> thm -> bool
    3.11 @@ -456,12 +455,6 @@
    3.12  
    3.13  (* general syntactic functions *)
    3.14  
    3.15 -(*Like dest_conj, but flattens conjunctions however nested*)
    3.16 -fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    3.17 -  | conjuncts_aux t conjs = t::conjs;
    3.18 -
    3.19 -fun conjuncts t = conjuncts_aux t [];
    3.20 -
    3.21  fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    3.22    | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
    3.23    | is_equationlike_term _ = false
     4.1 --- a/src/HOL/Tools/hologic.ML	Wed Sep 25 16:29:35 2013 +0200
     4.2 +++ b/src/HOL/Tools/hologic.ML	Wed Sep 25 16:43:46 2013 +0200
     4.3 @@ -38,6 +38,7 @@
     4.4    val mk_imp: term * term -> term
     4.5    val mk_not: term -> term
     4.6    val dest_conj: term -> term list
     4.7 +  val conjuncts: term -> term list
     4.8    val dest_disj: term -> term list
     4.9    val disjuncts: term -> term list
    4.10    val dest_imp: term -> term * term
    4.11 @@ -244,6 +245,12 @@
    4.12  fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
    4.13    | dest_conj t = [t];
    4.14  
    4.15 +(*Like dest_conj, but flattens conjunctions however nested*)
    4.16 +fun conjuncts_aux (Const ("HOL.conj", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    4.17 +  | conjuncts_aux t conjs = t::conjs;
    4.18 +
    4.19 +fun conjuncts t = conjuncts_aux t [];
    4.20 +
    4.21  fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
    4.22    | dest_disj t = [t];
    4.23