1.1 --- a/src/HOL/BNF/Tools/ctr_sugar_util.ML Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,192 +0,0 @@
1.4 -(* Title: HOL/BNF/Tools/ctr_sugar_util.ML
1.5 - Author: Jasmin Blanchette, TU Muenchen
1.6 - Copyright 2012
1.7 -
1.8 -Library for wrapping existing freely generated type's constructors.
1.9 -*)
1.10 -
1.11 -signature CTR_SUGAR_UTIL =
1.12 -sig
1.13 - val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
1.14 - val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
1.15 - val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
1.16 - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
1.17 - val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
1.18 - val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
1.19 - 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
1.20 - val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
1.21 - val transpose: 'a list list -> 'a list list
1.22 - val pad_list: 'a -> int -> 'a list -> 'a list
1.23 - val splice: 'a list -> 'a list -> 'a list
1.24 - val permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list
1.25 -
1.26 - val mk_names: int -> string -> string list
1.27 - val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
1.28 - val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context
1.29 - val mk_TFrees: int -> Proof.context -> typ list * Proof.context
1.30 - val mk_Frees': string -> typ list -> Proof.context ->
1.31 - (term list * (string * typ) list) * Proof.context
1.32 - val mk_Freess': string -> typ list list -> Proof.context ->
1.33 - (term list list * (string * typ) list list) * Proof.context
1.34 - val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
1.35 - val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
1.36 - val resort_tfree: sort -> typ -> typ
1.37 - val variant_types: string list -> sort list -> Proof.context ->
1.38 - (string * sort) list * Proof.context
1.39 - val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
1.40 -
1.41 - val mk_predT: typ list -> typ
1.42 - val mk_pred1T: typ -> typ
1.43 -
1.44 - val mk_disjIN: int -> int -> thm
1.45 -
1.46 - val mk_unabs_def: int -> thm -> thm
1.47 -
1.48 - val mk_IfN: typ -> term list -> term list -> term
1.49 - val mk_Trueprop_eq: term * term -> term
1.50 -
1.51 - val rapp: term -> term -> term
1.52 -
1.53 - val list_all_free: term list -> term -> term
1.54 - val list_exists_free: term list -> term -> term
1.55 -
1.56 - val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
1.57 -
1.58 - val unfold_thms: Proof.context -> thm list -> thm -> thm
1.59 -
1.60 - val certifyT: Proof.context -> typ -> ctyp
1.61 - val certify: Proof.context -> term -> cterm
1.62 -
1.63 - val standard_binding: binding
1.64 - val equal_binding: binding
1.65 - val parse_binding: binding parser
1.66 -
1.67 - val ss_only: thm list -> Proof.context -> Proof.context
1.68 -end;
1.69 -
1.70 -structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
1.71 -struct
1.72 -
1.73 -fun map3 _ [] [] [] = []
1.74 - | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
1.75 - | map3 _ _ _ _ = raise ListPair.UnequalLengths;
1.76 -
1.77 -fun map4 _ [] [] [] [] = []
1.78 - | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
1.79 - | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
1.80 -
1.81 -fun map5 _ [] [] [] [] [] = []
1.82 - | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
1.83 - f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
1.84 - | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
1.85 -
1.86 -fun fold_map2 _ [] [] acc = ([], acc)
1.87 - | fold_map2 f (x1::x1s) (x2::x2s) acc =
1.88 - let
1.89 - val (x, acc') = f x1 x2 acc;
1.90 - val (xs, acc'') = fold_map2 f x1s x2s acc';
1.91 - in (x :: xs, acc'') end
1.92 - | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
1.93 -
1.94 -fun fold_map3 _ [] [] [] acc = ([], acc)
1.95 - | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
1.96 - let
1.97 - val (x, acc') = f x1 x2 x3 acc;
1.98 - val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
1.99 - in (x :: xs, acc'') end
1.100 - | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
1.101 -
1.102 -fun seq_conds f n k xs =
1.103 - if k = n then
1.104 - map (f false) (take (k - 1) xs)
1.105 - else
1.106 - let val (negs, pos) = split_last (take k xs) in
1.107 - map (f false) negs @ [f true pos]
1.108 - end;
1.109 -
1.110 -fun transpose [] = []
1.111 - | transpose ([] :: xss) = transpose xss
1.112 - | transpose xss = map hd xss :: transpose (map tl xss);
1.113 -
1.114 -fun pad_list x n xs = xs @ replicate (n - length xs) x;
1.115 -
1.116 -fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
1.117 -
1.118 -fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
1.119 -
1.120 -fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
1.121 -fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
1.122 -
1.123 -val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
1.124 -
1.125 -fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
1.126 -
1.127 -fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
1.128 -fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
1.129 -
1.130 -fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
1.131 -fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
1.132 -
1.133 -fun resort_tfree S (TFree (s, _)) = TFree (s, S);
1.134 -
1.135 -fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
1.136 -
1.137 -fun variant_types ss Ss ctxt =
1.138 - let
1.139 - val (tfrees, _) =
1.140 - fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
1.141 - val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
1.142 - in (tfrees, ctxt') end;
1.143 -
1.144 -fun variant_tfrees ss =
1.145 - apfst (map TFree) o
1.146 - variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
1.147 -
1.148 -fun mk_predT Ts = Ts ---> HOLogic.boolT;
1.149 -fun mk_pred1T T = mk_predT [T];
1.150 -
1.151 -fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
1.152 - | mk_disjIN _ 1 = disjI1
1.153 - | mk_disjIN 2 2 = disjI2
1.154 - | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
1.155 -
1.156 -fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
1.157 -
1.158 -fun mk_IfN _ _ [t] = t
1.159 - | mk_IfN T (c :: cs) (t :: ts) =
1.160 - Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
1.161 -
1.162 -val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
1.163 -
1.164 -fun rapp u t = betapply (t, u);
1.165 -
1.166 -fun list_quant_free quant_const =
1.167 - fold_rev (fn free => fn P =>
1.168 - let val (x, T) = Term.dest_Free free;
1.169 - in quant_const T $ Term.absfree (x, T) P end);
1.170 -
1.171 -val list_all_free = list_quant_free HOLogic.all_const;
1.172 -val list_exists_free = list_quant_free HOLogic.exists_const;
1.173 -
1.174 -fun fo_match ctxt t pat =
1.175 - let val thy = Proof_Context.theory_of ctxt in
1.176 - Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
1.177 - end;
1.178 -
1.179 -fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
1.180 -
1.181 -(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
1.182 -fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
1.183 -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
1.184 -
1.185 -(* The standard binding stands for a name generated following the canonical convention (e.g.,
1.186 - "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
1.187 - binding at all, depending on the context. *)
1.188 -val standard_binding = @{binding _};
1.189 -val equal_binding = @{binding "="};
1.190 -
1.191 -val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
1.192 -
1.193 -fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
1.194 -
1.195 -end;