(* 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