Theory Stuff

(* Title:  Stuff.thy
   Author: Lars Noschinski, TU München

theory Stuff


section ‹Additional theorems for base libraries›

text ‹
  This section contains lemmas unrelated to graph theory which might be
  interesting for the Isabelle distribution

lemma ereal_Inf_finite_Min:
  fixes S :: "ereal set"
  assumes "finite S" and "S  {}"
  shows "Inf S = Min S"
using assms
by (induct S rule: finite_ne_induct) (auto simp: min_absorb1)

lemma finite_INF_in:
  fixes f :: "'a  ereal"
  assumes "finite S"
  assumes "S  {}"
  shows "(INF s S. f s)  f ` S"
proof -
  from assms
  have "finite (f ` S)" "f ` S  {}" by auto
  then show "Inf (f ` S)  f ` S"
    using ereal_Inf_finite_Min [of "f ` S"]  by simp

lemma not_mem_less_INF:
  fixes f :: "'a  'b :: complete_lattice"
  assumes "f x < (INF s S. f s)"
  assumes "x  S"
  shows "False"
using assms by (metis INF_lower less_le_not_le)

lemma sym_diff:
  assumes "sym A" "sym B" shows "sym (A - B)"
using assms by (auto simp: sym_def)

subsection ‹List›

lemmas list_exhaust2 = list.exhaust[case_product list.exhaust]

lemma list_exhaust_NSC:
  obtains (Nil) "xs = []" | (Single) x where "xs = [x]" | (Cons_Cons) x y ys where "xs = x # y # ys"
by (metis list.exhaust)

lemma tl_rev:
  "tl (rev p) = rev (butlast p)"
by (induct p) auto

lemma butlast_rev:
  "butlast (rev p) = rev (tl p)"
by (induct p) auto

lemma take_drop_take:
   "take n xs @ drop n (take m xs) = take (max n m) xs"
proof cases
  assume "m < n" then show ?thesis by (auto simp: max_def)
  assume "¬m < n"
  then have "take n xs = take n (take m xs)" by (auto simp: min_def)
  then show ?thesis by (simp del: take_take add: max_def)

lemma drop_take_drop:
  "drop n (take m xs) @ drop m xs = drop (min n m) xs"
proof cases
  assume A: "¬m < n"
  then show ?thesis
    using drop_append[of n "take m xs" "drop m xs"]
  by (cases "length xs < n") (auto simp: not_less min_def)
qed (auto simp: min_def)

lemma not_distinct_decomp_min_prefix:
  assumes "¬ distinct ws"
  shows " xs ys zs y. ws = xs @ y # ys @ y # zs  distinct xs  y  set xs  y  set ys "
proof -
  obtain xs y ys where "y  set xs" "distinct xs" "ws = xs @ y # ys"
    using assms by (auto simp: not_distinct_conv_prefix)
  moreover then obtain xs' ys' where "xs = xs' @ y # ys'" by (auto simp: in_set_conv_decomp)
  ultimately show ?thesis by auto

lemma not_distinct_decomp_min_not_distinct:
  assumes "¬ distinct ws"
  shows "xs y ys zs. ws = xs @ y # ys @ y # zs  distinct (ys @ [y])"
using assms
proof (induct ws)
  case (Cons w ws)
  show ?case
  proof (cases "distinct ws")
    case True
    then obtain xs ys where "ws = xs @ w # ys" "w  set xs"
      using Cons.prems by (fastforce dest: split_list_first)
    then have "distinct (xs @ [w])" "w # ws = [] @ w # xs @ w # ys"
      using distinct ws by auto
    then show ?thesis by blast
    case False
    then obtain xs y ys zs where "ws = xs @ y # ys @ y # zs  distinct (ys @ [y])"
      using Cons by auto
    then have "w # ws = (w # xs) @ y # ys @ y # zs  distinct (ys @ [y])"
      by simp
    then show ?thesis by blast
qed simp

lemma card_Ex_subset:
  "k  card M  N. N  M  card N = k"
by (induct rule: inc_induct) (auto simp: card_Suc_eq)

lemma list_set_tl: "x  set (tl xs)  x  set xs"
by (cases xs) auto

section ‹NOMATCH simproc›

text ‹
 The simplification procedure can be used to avoid simplification of terms of a certain form

definition NOMATCH :: "'a  'a  bool" where "NOMATCH val pat  True"
lemma NOMATCH_cong[cong]: "NOMATCH val pat = NOMATCH val pat" by (rule refl)

simproc_setup NOMATCH ("NOMATCH val pat") = fn _ => fn ctxt => fn ct =>
    val thy = Proof_Context.theory_of ctxt
    val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
    val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
  in if m then NONE else SOME @{thm NOMATCH_def} end

text ‹
  This setup ensures that a rewrite rule of the form @{term "NOMATCH val pat  t"}
  is only applied, if the pattern @{term pat} does not match the value @{term val}.