# 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"

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

```