Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Set_Algebras.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Set_Algebras.thy
    Author:     Jeremy Avigad
    Author:     Kevin Donnelly
    Author:     Florian Haftmann, TUM
*)

section \<open>Algebraic operations on sets\<close>

theory Set_Algebras
  imports Main
begin

text \<open>
  This library lifts operations like addition and multiplication to sets. It
  was designed to support asymptotic calculations. See the comments at the top
  of \<^file>\<open>BigO.thy\<close>.
\<close>

instantiation set :: (plus) plus
begin

definition plus_set :: "'a::plus set \ 'a set \ 'a set"
  where set_plus_def: "A + B = {c. \a\A. \b\B. c = a + b}"

instance ..

end

instantiation set :: (times) times
begin

definition times_set :: "'a::times set \ 'a set \ 'a set"
  where set_times_def: "A * B = {c. \a\A. \b\B. c = a * b}"

instance ..

end

instantiation set :: (zero) zero
begin

definition set_zero[simp]: "(0::'a::zero set) = {0}"

instance ..

end

instantiation set :: (one) one
begin

definition set_one[simp]: "(1::'a::one set) = {1}"

instance ..

end

definition elt_set_plus :: "'a::plus \ 'a set \ 'a set" (infixl "+o" 70)
  where "a +o B = {c. \b\B. c = a + b}"

definition elt_set_times :: "'a::times \ 'a set \ 'a set" (infixl "*o" 80)
  where "a *o B = {c. \b\B. c = a * b}"

abbreviation (input) elt_set_eq :: "'a \ 'a set \ bool" (infix "=o" 50)
  where "x =o A \ x \ A"

instance set :: (semigroup_add) semigroup_add
  by standard (force simp add: set_plus_def add.assoc)

instance set :: (ab_semigroup_add) ab_semigroup_add
  by standard (force simp add: set_plus_def add.commute)

instance set :: (monoid_add) monoid_add
  by standard (simp_all add: set_plus_def)

instance set :: (comm_monoid_add) comm_monoid_add
  by standard (simp_all add: set_plus_def)

instance set :: (semigroup_mult) semigroup_mult
  by standard (force simp add: set_times_def mult.assoc)

instance set :: (ab_semigroup_mult) ab_semigroup_mult
  by standard (force simp add: set_times_def mult.commute)

instance set :: (monoid_mult) monoid_mult
  by standard (simp_all add: set_times_def)

instance set :: (comm_monoid_mult) comm_monoid_mult
  by standard (simp_all add: set_times_def)

lemma set_plus_intro [intro]: "a \ C \ b \ D \ a + b \ C + D"
  by (auto simp add: set_plus_def)

lemma set_plus_elim:
  assumes "x \ A + B"
  obtains a b where "x = a + b" and "a \ A" and "b \ B"
  using assms unfolding set_plus_def by fast

lemma set_plus_intro2 [intro]: "b \ C \ a + b \ a +o C"
  by (auto simp add: elt_set_plus_def)

lemma set_plus_rearrange: "(a +o C) + (b +o D) = (a + b) +o (C + D)"
  for a b :: "'a::comm_monoid_add"
  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
   apply (rule_tac x = "ba + bb" in exI)
   apply (auto simp add: ac_simps)
  apply (rule_tac x = "aa + a" in exI)
  apply (auto simp add: ac_simps)
  done

lemma set_plus_rearrange2: "a +o (b +o C) = (a + b) +o C"
  for a b :: "'a::semigroup_add"
  by (auto simp add: elt_set_plus_def add.assoc)

lemma set_plus_rearrange3: "(a +o B) + C = a +o (B + C)"
  for a :: "'a::semigroup_add"
  apply (auto simp add: elt_set_plus_def set_plus_def)
   apply (blast intro: ac_simps)
  apply (rule_tac x = "a + aa" in exI)
  apply (rule conjI)
   apply (rule_tac x = "aa" in bexI)
    apply auto
  apply (rule_tac x = "ba" in bexI)
   apply (auto simp add: ac_simps)
  done

theorem set_plus_rearrange4: "C + (a +o D) = a +o (C + D)"
  for a :: "'a::comm_monoid_add"
  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
   apply (rule_tac x = "aa + ba" in exI)
   apply (auto simp add: ac_simps)
  done

lemmas set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
  set_plus_rearrange3 set_plus_rearrange4

lemma set_plus_mono [intro!]: "C \ D \ a +o C \ a +o D"
  by (auto simp add: elt_set_plus_def)

lemma set_plus_mono2 [intro]: "C \ D \ E \ F \ C + E \ D + F"
  for C D E F :: "'a::plus set"
  by (auto simp add: set_plus_def)

lemma set_plus_mono3 [intro]: "a \ C \ a +o D \ C + D"
  by (auto simp add: elt_set_plus_def set_plus_def)

lemma set_plus_mono4 [intro]: "a \ C \ a +o D \ D + C"
  for a :: "'a::comm_monoid_add"
  by (auto simp add: elt_set_plus_def set_plus_def ac_simps)

lemma set_plus_mono5: "a \ C \ B \ D \ a +o B \ C + D"
  apply (subgoal_tac "a +o B \ a +o D")
   apply (erule order_trans)
   apply (erule set_plus_mono3)
  apply (erule set_plus_mono)
  done

lemma set_plus_mono_b: "C \ D \ x \ a +o C \ x \ a +o D"
  apply (frule set_plus_mono)
  apply auto
  done

lemma set_plus_mono2_b: "C \ D \ E \ F \ x \ C + E \ x \ D + F"
  apply (frule set_plus_mono2)
   prefer 2
   apply force
  apply assumption
  done

lemma set_plus_mono3_b: "a \ C \ x \ a +o D \ x \ C + D"
  apply (frule set_plus_mono3)
  apply auto
  done

lemma set_plus_mono4_b: "a \ C \ x \ a +o D \ x \ D + C"
  for a x :: "'a::comm_monoid_add"
  apply (frule set_plus_mono4)
  apply auto
  done

lemma set_zero_plus [simp]: "0 +o C = C"
  for C :: "'a::comm_monoid_add set"
  by (auto simp add: elt_set_plus_def)

lemma set_zero_plus2: "0 \ A \ B \ A + B"
  for A B :: "'a::comm_monoid_add set"
  apply (auto simp add: set_plus_def)
  apply (rule_tac x = 0 in bexI)
   apply (rule_tac x = x in bexI)
    apply (auto simp add: ac_simps)
  done

lemma set_plus_imp_minus: "a \ b +o C \ a - b \ C"
  for a b :: "'a::ab_group_add"
  by (auto simp add: elt_set_plus_def ac_simps)

lemma set_minus_imp_plus: "a - b \ C \ a \ b +o C"
  for a b :: "'a::ab_group_add"
  apply (auto simp add: elt_set_plus_def ac_simps)
  apply (subgoal_tac "a = (a + - b) + b")
   apply (rule bexI)
    apply assumption
   apply (auto simp add: ac_simps)
  done

lemma set_minus_plus: "a - b \ C \ a \ b +o C"
  for a b :: "'a::ab_group_add"
  apply (rule iffI)
   apply (rule set_minus_imp_plus)
   apply assumption
  apply (rule set_plus_imp_minus)
  apply assumption
  done

lemma set_times_intro [intro]: "a \ C \ b \ D \ a * b \ C * D"
  by (auto simp add: set_times_def)

lemma set_times_elim:
  assumes "x \ A * B"
  obtains a b where "x = a * b" and "a \ A" and "b \ B"
  using assms unfolding set_times_def by fast

lemma set_times_intro2 [intro!]: "b \ C \ a * b \ a *o C"
  by (auto simp add: elt_set_times_def)

lemma set_times_rearrange: "(a *o C) * (b *o D) = (a * b) *o (C * D)"
  for a b :: "'a::comm_monoid_mult"
  apply (auto simp add: elt_set_times_def set_times_def)
   apply (rule_tac x = "ba * bb" in exI)
   apply (auto simp add: ac_simps)
  apply (rule_tac x = "aa * a" in exI)
  apply (auto simp add: ac_simps)
  done

lemma set_times_rearrange2: "a *o (b *o C) = (a * b) *o C"
  for a b :: "'a::semigroup_mult"
  by (auto simp add: elt_set_times_def mult.assoc)

lemma set_times_rearrange3: "(a *o B) * C = a *o (B * C)"
  for a :: "'a::semigroup_mult"
  apply (auto simp add: elt_set_times_def set_times_def)
   apply (blast intro: ac_simps)
  apply (rule_tac x = "a * aa" in exI)
  apply (rule conjI)
   apply (rule_tac x = "aa" in bexI)
    apply auto
  apply (rule_tac x = "ba" in bexI)
   apply (auto simp add: ac_simps)
  done

theorem set_times_rearrange4: "C * (a *o D) = a *o (C * D)"
  for a :: "'a::comm_monoid_mult"
  apply (auto simp add: elt_set_times_def set_times_def ac_simps)
   apply (rule_tac x = "aa * ba" in exI)
   apply (auto simp add: ac_simps)
  done

lemmas set_times_rearranges = set_times_rearrange set_times_rearrange2
  set_times_rearrange3 set_times_rearrange4

lemma set_times_mono [intro]: "C \ D \ a *o C \ a *o D"
  by (auto simp add: elt_set_times_def)

lemma set_times_mono2 [intro]: "C \ D \ E \ F \ C * E \ D * F"
  for C D E F :: "'a::times set"
  by (auto simp add: set_times_def)

lemma set_times_mono3 [intro]: "a \ C \ a *o D \ C * D"
  by (auto simp add: elt_set_times_def set_times_def)

lemma set_times_mono4 [intro]: "a \ C \ a *o D \ D * C"
  for a :: "'a::comm_monoid_mult"
  by (auto simp add: elt_set_times_def set_times_def ac_simps)

lemma set_times_mono5: "a \ C \ B \ D \ a *o B \ C * D"
  apply (subgoal_tac "a *o B \ a *o D")
   apply (erule order_trans)
   apply (erule set_times_mono3)
  apply (erule set_times_mono)
  done

lemma set_times_mono_b: "C \ D \ x \ a *o C \ x \ a *o D"
  apply (frule set_times_mono)
  apply auto
  done

lemma set_times_mono2_b: "C \ D \ E \ F \ x \ C * E \ x \ D * F"
  apply (frule set_times_mono2)
   prefer 2
   apply force
  apply assumption
  done

lemma set_times_mono3_b: "a \ C \ x \ a *o D \ x \ C * D"
  apply (frule set_times_mono3)
  apply auto
  done

lemma set_times_mono4_b: "a \ C \ x \ a *o D \ x \ D * C"
  for a x :: "'a::comm_monoid_mult"
  apply (frule set_times_mono4)
  apply auto
  done

lemma set_one_times [simp]: "1 *o C = C"
  for C :: "'a::comm_monoid_mult set"
  by (auto simp add: elt_set_times_def)

lemma set_times_plus_distrib: "a *o (b +o C) = (a * b) +o (a *o C)"
  for a b :: "'a::semiring"
  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)

lemma set_times_plus_distrib2: "a *o (B + C) = (a *o B) + (a *o C)"
  for a :: "'a::semiring"
  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
   apply blast
  apply (rule_tac x = "b + bb" in exI)
  apply (auto simp add: ring_distribs)
  done

lemma set_times_plus_distrib3: "(a +o C) * D \ a *o D + C * D"
  for a :: "'a::semiring"
  apply (auto simp: elt_set_plus_def elt_set_times_def set_times_def set_plus_def ring_distribs)
  apply auto
  done

lemmas set_times_plus_distribs =
  set_times_plus_distrib
  set_times_plus_distrib2

lemma set_neg_intro: "a \ (- 1) *o C \ - a \ C"
  for a :: "'a::ring_1"
  by (auto simp add: elt_set_times_def)

lemma set_neg_intro2: "a \ C \ - a \ (- 1) *o C"
  for a :: "'a::ring_1"
  by (auto simp add: elt_set_times_def)

lemma set_plus_image: "S + T = (\(x, y). x + y) ` (S \ T)"
  by (fastforce simp: set_plus_def image_iff)

lemma set_times_image: "S * T = (\(x, y). x * y) ` (S \ T)"
  by (fastforce simp: set_times_def image_iff)

lemma finite_set_plus: "finite s \ finite t \ finite (s + t)"
  by (simp add: set_plus_image)

lemma finite_set_times: "finite s \ finite t \ finite (s * t)"
  by (simp add: set_times_image)

lemma set_sum_alt:
  assumes fin: "finite I"
  shows "sum S I = {sum s I |s. \i\I. s i \ S i}"
    (is "_ = ?sum I")
  using fin
proof induct
  case empty
  then show ?case by simp
next
  case (insert x F)
  have "sum S (insert x F) = S x + ?sum F"
    using insert.hyps by auto
  also have "\ = {s x + sum s F |s. \ i\insert x F. s i \ S i}"
    unfolding set_plus_def
  proof safe
    fix y s
    assume "y \ S x" "\i\F. s i \ S i"
    then show "\s'. y + sum s F = s' x + sum s' F \ (\i\insert x F. s' i \ S i)"
      using insert.hyps
      by (intro exI[of _ "\i. if i \ F then s i else y"]) (auto simp add: set_plus_def)
  qed auto
  finally show ?case
    using insert.hyps by auto
qed

lemma sum_set_cond_linear:
  fixes f :: "'a::comm_monoid_add set \ 'b::comm_monoid_add set"
  assumes [intro!]: "\A B. P A \ P B \ P (A + B)" "P {0}"
    and f: "\A B. P A \ P B \ f (A + B) = f A + f B" "f {0} = {0}"
  assumes all: "\i. i \ I \ P (S i)"
  shows "f (sum S I) = sum (f \ S) I"
proof (cases "finite I")
  case True
  from this all show ?thesis
  proof induct
    case empty
    then show ?case by (auto intro!: f)
  next
    case (insert x F)
    from \<open>finite F\<close> \<open>\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)\<close> have "P (sum S F)"
      by induct auto
    with insert show ?case
      by (simp, subst f) auto
  qed
next
  case False
  then show ?thesis by (auto intro!: f)
qed

lemma sum_set_linear:
  fixes f :: "'a::comm_monoid_add set \ 'b::comm_monoid_add set"
  assumes "\A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
  shows "f (sum S I) = sum (f \ S) I"
  using sum_set_cond_linear[of "\x. True" f I S] assms by auto

lemma set_times_Un_distrib:
  "A * (B \ C) = A * B \ A * C"
  "(A \ B) * C = A * C \ B * C"
  by (auto simp: set_times_def)

lemma set_times_UNION_distrib:
  "A * \(M ` I) = (\i\I. A * M i)"
  "\(M ` I) * A = (\i\I. M i * A)"
  by (auto simp: set_times_def)

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.