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