Theory Transition_Systems_and_Automata.Basic

section ‹Basics›

theory Basic
imports Main
begin

  subsection ‹Miscellaneous›

  abbreviation (input) "const x ≡ λ _. x"

  lemmas [simp] = map_prod.id map_prod.comp[symmetric]
  lemma prod_UNIV[iff]: "A × B = UNIV ⟷ A = UNIV ∧ B = UNIV" by auto
  lemma prod_singleton:
    "fst ` A = {x} ⟹ A = fst ` A × snd ` A"
    "snd ` A = {y} ⟹ A = fst ` A × snd ` A"
    by force+

  lemma infinite_subset[trans]: "infinite A ⟹ A ⊆ B ⟹ infinite B" using infinite_super by this
  lemma finite_subset[trans]: "A ⊆ B ⟹ finite B ⟹ finite A" using finite_subset by this

  declare infinite_coinduct[case_names infinite, coinduct pred: infinite]
  lemma infinite_psubset_coinduct[case_names infinite, consumes 1]:
    assumes "R A"
    assumes "⋀ A. R A ⟹ ∃ B ⊂ A. R B"
    shows "infinite A"
  proof
    show "False" if "finite A" using that assms by (induct rule: finite_psubset_induct) (auto)
  qed

  (* TODO: why are there two copies of this theorem? *)
  thm inj_on_subset subset_inj_on

  lemma inj_inj_on[dest]: "inj f ⟹ inj_on f S" using inj_on_subset by auto

end