1.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 03 11:54:21 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 03 11:54:21 2012 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
     1.5    val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
     1.6      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
     1.7 +  val interleave: 'a list -> 'a list -> 'a list
     1.8    val transpose: 'a list list -> 'a list list
     1.9  
    1.10    val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
    1.11 @@ -87,6 +88,9 @@
    1.12    val mk_subset: term -> term -> term
    1.13    val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
    1.14  
    1.15 +  val list_all_free: term list -> term -> term
    1.16 +  val list_exists_free: term list -> term -> term
    1.17 +
    1.18    (*parameterized terms*)
    1.19    val mk_nthN: int -> term -> int -> term
    1.20  
    1.21 @@ -94,6 +98,7 @@
    1.22    val mk_Un_upper: int -> int -> thm
    1.23    val mk_conjIN: int -> thm
    1.24    val mk_conjunctN: int -> int -> thm
    1.25 +  val mk_disjIN: int -> int -> thm
    1.26    val mk_nthI: int -> int -> thm
    1.27    val mk_nth_conv: int -> int -> thm
    1.28    val mk_ordLeq_csum: int -> int -> thm -> thm
    1.29 @@ -108,6 +113,9 @@
    1.30    val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
    1.31    val find_indices: ''a list -> ''a list -> int list
    1.32  
    1.33 +  val certifyT: Proof.context -> typ -> ctyp
    1.34 +  val certify: Proof.context -> term -> cterm
    1.35 +
    1.36    val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    1.37    val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
    1.38      tactic
    1.39 @@ -223,6 +231,10 @@
    1.40      in (x :: xs, acc'') end
    1.41    | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    1.42  
    1.43 +(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
    1.44 +fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    1.45 +fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    1.46 +
    1.47  (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
    1.48  fun WRAP gen_before gen_after xs core_tac =
    1.49    fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
    1.50 @@ -434,6 +446,16 @@
    1.51  
    1.52  fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
    1.53  
    1.54 +val list_all_free =
    1.55 +  fold_rev (fn free => fn P =>
    1.56 +    let val (x, T) = Term.dest_Free free;
    1.57 +    in HOLogic.all_const T $ Term.absfree (x, T) P end);
    1.58 +
    1.59 +val list_exists_free =
    1.60 +  fold_rev (fn free => fn P =>
    1.61 +    let val (x, T) = Term.dest_Free free;
    1.62 +    in HOLogic.exists_const T $ Term.absfree (x, T) P end);
    1.63 +
    1.64  fun find_indices xs ys = map_filter I
    1.65    (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys);
    1.66  
    1.67 @@ -471,6 +493,11 @@
    1.68  fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
    1.69    | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
    1.70  
    1.71 +fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
    1.72 +  | mk_disjIN _ 1 = disjI1
    1.73 +  | mk_disjIN 2 2 = disjI2
    1.74 +  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
    1.75 +
    1.76  fun mk_ordLeq_csum 1 1 thm = thm
    1.77    | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}]
    1.78    | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}]
    1.79 @@ -497,6 +524,8 @@
    1.80      | mk_UnN n m = mk_UnN' (n - m)
    1.81  end;
    1.82  
    1.83 +fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
    1.84 +
    1.85  fun transpose [] = []
    1.86    | transpose ([] :: xss) = transpose xss
    1.87    | transpose xss = map hd xss :: transpose (map tl xss);