Theory ML_Utils

theory ML_Utils
imports
  "HOL-Library.FSet"
  "Dict_Construction.Dict_Construction"
begin

ML_file "utils.ML"

MLfun econtr_tac neg_thms ctxt =
  let
    val neg_thms = map (fn thm => @{thm notE} OF [thm]) neg_thms
  in SOLVED' (eresolve_tac ctxt neg_thms) end

(* from HOL.thy *)
fun eval_tac ctxt =
  let val conv = Code_Runtime.dynamic_holds_conv ctxt
  in
    CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
    resolve_tac ctxt [TrueI]
  end

lemma norm_all_conjunction:
  "P Q. ((x. PROP P x) &&& PROP Q)  (x. PROP P x &&& PROP Q)"
  "P Q. (PROP P &&& (x. PROP Q x))  (x. PROP P &&& PROP Q x)"
proof -
  show "((x. PROP P x) &&& PROP Q)  (x. PROP P x &&& PROP Q)" for P Q
    proof
      fix x
      assume "(x. PROP P x) &&& PROP Q"
      note Pure.conjunctionD1[OF this, rule_format] Pure.conjunctionD2[OF this]
      thus "PROP P x &&& PROP Q" .
    next
      assume "(x. PROP P x &&& PROP Q)"
      note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this]
      thus "(x. PROP P x) &&& PROP Q" .
    qed
next
  show "(PROP P &&& (x. PROP Q x))  (x. PROP P &&& PROP Q x)" for P Q
    proof
      fix x
      assume "PROP P &&& (x. PROP Q x)"
      note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this, rule_format]
      thus "PROP P &&& PROP Q x" .
    next
      assume "(x. PROP P &&& PROP Q x)"
      note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this]
      thus "PROP P &&& (x. PROP Q x)" .
    qed
qed

MLfun norm_all_conjunction_tac ctxt =
  CONVERSION (repeat1_conv (Dict_Construction_Util.changed_conv (Conv.top_sweep_conv
    (K (Conv.rewrs_conv @{thms norm_all_conjunction})) ctxt)))

end