Theory Stuff

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

theory Stuff
imports
  Main
  "HOL-Library.Extended_Real"

begin

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
qed

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)
next
  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)
qed

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
qed

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
  next
    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
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 =>
  let
    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}.
›


end