Theory Prelim

chapter ‹Preliminaries›

(*<*)
theory Prelim
  imports Main "HOL-Eisbach.Eisbach"
begin
(*>*)

section ‹Trivia›

abbreviation (input) any where "any ≡ undefined"

lemma Un_Diff2: "B ∩ C = {} ⟹ A ∪ B - C = A - C ∪ B" by auto

lemma Diff_Diff_Un: "A - B - C = A - (B ∪ C)" by auto

fun first :: "nat ⇒ nat list" where
  "first 0 = []"
| "first (Suc n) = n # first n"


text ‹Facts about zipping lists:›

lemma fst_set_zip_map_fst:
  "length xs = length ys ⟹ fst ` (set (zip (map fst xs) ys)) = fst ` (set xs)"
  by (induct xs ys rule: list_induct2) auto

lemma snd_set_zip_map_snd:
  "length xs = length ys ⟹ snd ` (set (zip xs (map snd ys))) = snd ` (set ys)"
  by (induct xs ys rule: list_induct2) auto

lemma snd_set_zip:
  "length xs = length ys ⟹ snd ` (set (zip xs ys)) = set ys"
  by (induct xs ys rule: list_induct2) auto

lemma set_zip_D: "(x, y) ∈ set (zip xs ys) ⟹ x ∈ set xs ∧ y ∈ set ys"
  using set_zip_leftD set_zip_rightD by auto

lemma inj_on_set_zip_map:
  assumes i: "inj_on f X"
    and a: "(f x1, y1) ∈ set (zip (map f xs) ys)" "set xs ⊆ X" "x1 ∈ X" "length xs = length ys"
  shows "(x1, y1) ∈ set (zip xs ys)"
using a proof (induct xs arbitrary: ys x1 y1)
  case (Cons x xs yys)
  thus ?case using i unfolding inj_on_def by (cases yys) auto
qed (insert i, auto)

lemma set_zip_map_fst_snd:
  assumes "(u,x) ∈ set (zip us (map snd txs))"
    and "(t,u) ∈ set (zip (map fst txs) us)"
    and "distinct (map snd txs)"
    and "distinct us" and "length us = length txs"
  shows "(t, x) ∈ set txs"
  using assms(5,1-4)
  by (induct us txs arbitrary: u x t rule: list_induct2)
    (auto dest: set_zip_leftD set_zip_rightD)

lemma set_zip_map_fst_snd2:
  assumes "(u, x) ∈ set (zip us (map snd txs))"
    and "(t, x) ∈ set txs"
    and "distinct (map snd txs)"
    and "distinct us" and "length us = length txs"
  shows "(t, u) ∈ set (zip (map fst txs) us)"
  using assms(5,1-4)
  by (induct us txs arbitrary: u x t rule: list_induct2)
    (auto dest: set_zip_rightD simp: image_iff)

lemma set_zip_length_map:
  assumes "(x1, y1) ∈ set (zip xs ys)" and "length xs = length ys"
  shows "(f x1, y1) ∈ set (zip (map f xs) ys)"
  using assms(2,1) by (induct xs ys arbitrary: x1 y1 rule: list_induct2) auto

definition asList :: "'a set ⇒ 'a list" where
  "asList A ≡ SOME as. set as = A"

lemma asList[simp,intro!]: "finite A ⟹ set (asList A) = A"
  unfolding asList_def by (meson finite_list tfl_some)

lemma triv_Un_imp_aux:
  "(⋀a. φ ⟹ a ∉ A ⟹ a ∈ B ⟷ a ∈ C) ⟹ φ ⟶ A ∪ B = A ∪ C"
  by auto

definition toN where "toN n ≡ [0..<(Suc n)]"

lemma set_toN[simp]: "set (toN n) = {0..n}"
  unfolding toN_def by auto

declare list.map_cong[cong]


section ‹Some Proof Infrastructure›

ML ‹
exception TAC of term

val simped = Thm.rule_attribute [] (fn context => fn thm =>
  let
    val ctxt = Context.proof_of context;
    val (thm', ctxt') = yield_singleton (apfst snd oo Variable.import false) thm ctxt;
    val full_goal = Thm.prop_of thm';
    val goal = Goal.prove ctxt' [] [] full_goal (fn {context = ctxt, prems = _} =>
      HEADGOAL (asm_full_simp_tac ctxt THEN' TRY o SUBGOAL (fn (goal, _) => raise (TAC goal))))
      |> K (HOLogic.mk_Trueprop @{term True})
      handle TAC goal => goal;
    val thm = Goal.prove ctxt' [] [] goal (fn {context = ctxt, prems = _} =>
      HEADGOAL (Method.insert_tac ctxt [thm'] THEN' asm_full_simp_tac ctxt))
      |> singleton (Variable.export ctxt' ctxt);
  in thm end)

val _ = Theory.setup
  (Attrib.setup \<^binding>‹simped› (pair simped) "simped rule");
›

method RULE methods meth uses rule =
  (rule rule; (solves meth)?)

text ‹TryUntilFail:›
(* This is non-hazardous, since it does not touch the goal on which it fails. *)
method TUF methods meth =
  ((meth;fail)+)?

text ‹Helping a method, usually simp or auto, with specific substitutions inserted.
For auto, this is a bit like a "simp!" analogue of "intro!" and "dest!": It forces
the application of an indicated simplification rule, if this is possible.›

method variousSubsts1 methods meth uses s1 =
  (meth?,(subst s1)?, meth?)
method variousSubsts2 methods meth uses s1 s2 =
  (meth?,(subst s1)?, meth?, subst s2, meth?)
method variousSubsts3 methods meth uses s1 s2 s3 =
  (meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?)
method variousSubsts4 methods meth uses s1 s2 s3 s4 =
  (meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?, (subst s4)?, meth?)
method variousSubsts5 methods meth uses s1 s2 s3 s4 s5 =
  (meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?, (subst s4)?, meth?, (subst s5)?, meth?)
method variousSubsts6 methods meth uses s1 s2 s3 s4 s5 s6 =
  (meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?,
         (subst s4)?, meth?, (subst s5)?, meth?, (subst s6)?, meth?)

(*<*)
end
(*>*)