Theory Previous

theory Previous
imports Main
begin

section{*Previous general results*}

text{*We present here some result and theorems which will be used in our
developement. There are general properties, not centered in any section of
our implementation.*}

lemma less_than_Suc_union:
  shows "{i. i < Suc (n::nat)} = {i. i < n} ∪ {n}"
  unfolding lessThan_def [symmetric]
  unfolding lessThan_Suc_atMost 
  using atMost_Suc by (cases n, auto)


text{*Next two lemmas is a non-elegant trick which makes possible work with 
premisses that contains multiples @{term "op ∧"}*}
lemma conjI3: "[|A; B; C|] ==> A ∧ B ∧ C"
  by fast

lemma conjI4: "[|A; B; C; D|] ==> A ∧ B ∧ C ∧ D"
  by fast

lemma conjI5: "[|A; B; C; D; E|] ==> A ∧ B ∧ C ∧ D ∧ E"
  by fast

lemma conjI6:
  shows "[|A; B; C; D; E; F|] ==> A ∧ B ∧ C ∧ D ∧ E ∧ F"
  by fast

text{*Next lemmas prove some properties of the bijections between
  subsets of a given set.*}
lemma bij_betw_subset:
  assumes b: "bij_betw f A B" and sb: "C ⊆ A"
  shows "bij_betw f C (f ` C)"
  using b sb
  unfolding bij_betw_def
  unfolding image_def inj_on_def by auto

lemma
  bij_betw_image_minus:
  assumes b: "bij_betw f A B" and a: "a ∈ A"
  shows "f ` (A - {a}) = B - {f a}"
proof
  show "f ` (A - {a}) ⊆ B - {f a}"
    using b
    unfolding bij_betw_def
    using a unfolding image_def unfolding inj_on_def by auto
  show "B - {f a} ⊆ f ` (A - {a})"
    using b
    unfolding bij_betw_def
    using a unfolding image_def unfolding inj_on_def by auto
qed

end