src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 55535 10194808430d
child 57090 0224caba67ca
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012, 2013
     5 
     6 Library for wrapping existing freely generated type's constructors.
     7 *)
     8 
     9 signature CTR_SUGAR_UTIL =
    10 sig
    11   val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    12   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
    13   val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
    14     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
    15   val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
    16   val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
    17     'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
    18   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
    19   val transpose: 'a list list -> 'a list list
    20   val pad_list: 'a -> int -> 'a list -> 'a list
    21   val splice: 'a list -> 'a list -> 'a list
    22   val permute_like_unique: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list
    23   val permute_like: ('a * 'a -> bool) -> 'a list -> 'a list -> 'b list -> 'b list
    24 
    25   val mk_names: int -> string -> string list
    26   val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
    27   val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context
    28   val mk_TFrees: int -> Proof.context -> typ list * Proof.context
    29   val mk_Frees': string -> typ list -> Proof.context ->
    30     (term list * (string * typ) list) * Proof.context
    31   val mk_Freess': string -> typ list list -> Proof.context ->
    32     (term list list * (string * typ) list list) * Proof.context
    33   val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
    34   val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
    35   val resort_tfree: sort -> typ -> typ
    36   val variant_types: string list -> sort list -> Proof.context ->
    37     (string * sort) list * Proof.context
    38   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
    39 
    40   val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
    41   val subst_nonatomic_types: (typ * typ) list -> term -> term
    42 
    43   val lhs_head_of : thm -> term
    44 
    45   val mk_predT: typ list -> typ
    46   val mk_pred1T: typ -> typ
    47 
    48   val mk_disjIN: int -> int -> thm
    49 
    50   val mk_unabs_def: int -> thm -> thm
    51 
    52   val mk_IfN: typ -> term list -> term list -> term
    53   val mk_Trueprop_eq: term * term -> term
    54 
    55   val rapp: term -> term -> term
    56 
    57   val list_all_free: term list -> term -> term
    58   val list_exists_free: term list -> term -> term
    59 
    60   val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
    61 
    62   val cterm_instantiate_pos: cterm option list -> thm -> thm
    63   val unfold_thms: Proof.context -> thm list -> thm -> thm
    64 
    65   val certifyT: Proof.context -> typ -> ctyp
    66   val certify: Proof.context -> term -> cterm
    67 
    68   val standard_binding: binding
    69   val equal_binding: binding
    70   val parse_binding: binding parser
    71   val parse_binding_colon: binding parser
    72   val parse_opt_binding_colon: binding parser
    73 
    74   val ss_only: thm list -> Proof.context -> Proof.context
    75 
    76   val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    77   val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
    78     tactic
    79   val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
    80   val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
    81   val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
    82   val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
    83 end;
    84 
    85 structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
    86 struct
    87 
    88 fun map3 _ [] [] [] = []
    89   | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
    90   | map3 _ _ _ _ = raise ListPair.UnequalLengths;
    91 
    92 fun map4 _ [] [] [] [] = []
    93   | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
    94   | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
    95 
    96 fun map5 _ [] [] [] [] [] = []
    97   | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
    98     f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
    99   | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   100 
   101 fun fold_map2 _ [] [] acc = ([], acc)
   102   | fold_map2 f (x1::x1s) (x2::x2s) acc =
   103     let
   104       val (x, acc') = f x1 x2 acc;
   105       val (xs, acc'') = fold_map2 f x1s x2s acc';
   106     in (x :: xs, acc'') end
   107   | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
   108 
   109 fun fold_map3 _ [] [] [] acc = ([], acc)
   110   | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
   111     let
   112       val (x, acc') = f x1 x2 x3 acc;
   113       val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
   114     in (x :: xs, acc'') end
   115   | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
   116 
   117 fun seq_conds f n k xs =
   118   if k = n then
   119     map (f false) (take (k - 1) xs)
   120   else
   121     let val (negs, pos) = split_last (take k xs) in
   122       map (f false) negs @ [f true pos]
   123     end;
   124 
   125 fun transpose [] = []
   126   | transpose ([] :: xss) = transpose xss
   127   | transpose xss = map hd xss :: transpose (map tl xss);
   128 
   129 fun pad_list x n xs = xs @ replicate (n - length xs) x;
   130 
   131 fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
   132 
   133 fun permute_like_unique eq xs xs' ys =
   134   map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
   135 
   136 fun fresh eq x names =
   137   (case AList.lookup eq names x of
   138     NONE => ((x, 0), (x, 0) :: names)
   139   | SOME n => ((x, n + 1), AList.update eq (x, n + 1) names));
   140 
   141 fun deambiguate eq xs = fst (fold_map (fresh eq) xs []);
   142 
   143 fun permute_like eq xs xs' =
   144   permute_like_unique (eq_pair eq (op =)) (deambiguate eq xs) (deambiguate eq xs');
   145 
   146 fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
   147 fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
   148 
   149 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
   150 
   151 fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
   152 
   153 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
   154 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
   155 
   156 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
   157 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
   158 
   159 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
   160 
   161 fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
   162 
   163 fun variant_types ss Ss ctxt =
   164   let
   165     val (tfrees, _) =
   166       fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
   167     val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   168   in (tfrees, ctxt') end;
   169 
   170 fun variant_tfrees ss =
   171   apfst (map TFree) o
   172     variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
   173 
   174 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
   175 fun typ_subst_nonatomic [] = I
   176   | typ_subst_nonatomic inst =
   177     let
   178       fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts))
   179         | subst T = perhaps (AList.lookup (op =) inst) T;
   180     in subst end;
   181 
   182 fun subst_nonatomic_types [] = I
   183   | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst);
   184 
   185 fun lhs_head_of thm = Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))));
   186 
   187 fun mk_predT Ts = Ts ---> HOLogic.boolT;
   188 fun mk_pred1T T = mk_predT [T];
   189 
   190 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
   191   | mk_disjIN _ 1 = disjI1
   192   | mk_disjIN 2 2 = disjI2
   193   | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
   194 
   195 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
   196 
   197 fun mk_IfN _ _ [t] = t
   198   | mk_IfN T (c :: cs) (t :: ts) =
   199     Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
   200 
   201 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   202 
   203 fun rapp u t = betapply (t, u);
   204 
   205 fun list_quant_free quant_const =
   206   fold_rev (fn Free (xT as (_, T)) => fn P => quant_const T $ Term.absfree xT P);
   207 
   208 val list_all_free = list_quant_free HOLogic.all_const;
   209 val list_exists_free = list_quant_free HOLogic.exists_const;
   210 
   211 fun fo_match ctxt t pat =
   212   let val thy = Proof_Context.theory_of ctxt in
   213     Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
   214   end;
   215 
   216 fun cterm_instantiate_pos cts thm =
   217   let
   218     val cert = Thm.cterm_of (Thm.theory_of_thm thm);
   219     val vars = Term.add_vars (prop_of thm) [];
   220     val vars' = rev (drop (length vars - length cts) vars);
   221     val ps = map_filter (fn (_, NONE) => NONE
   222       | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
   223   in
   224     Drule.cterm_instantiate ps thm
   225   end;
   226 
   227 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
   228 
   229 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
   230 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
   231 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
   232 
   233 (* The standard binding stands for a name generated following the canonical convention (e.g.,
   234    "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
   235    binding at all, depending on the context. *)
   236 val standard_binding = @{binding _};
   237 val equal_binding = @{binding "="};
   238 
   239 val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
   240 val parse_binding_colon = parse_binding --| @{keyword ":"};
   241 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
   242 
   243 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
   244 
   245 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
   246 fun WRAP gen_before gen_after xs core_tac =
   247   fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
   248 
   249 fun WRAP' gen_before gen_after xs core_tac =
   250   fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
   251 
   252 fun CONJ_WRAP_GEN conj_tac gen_tac xs =
   253   let val (butlast, last) = split_last xs;
   254   in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
   255 
   256 fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
   257   let val (butlast, last) = split_last xs;
   258   in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
   259 
   260 (*not eta-converted because of monotype restriction*)
   261 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
   262 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
   263 
   264 end;