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