Quelle Int_Pow.thy Sprache: Isabelle

(*  Title:      HOL/Quotient_Examples/Int_Pow.thy
    Author:     Ondrej Kuncar
    Author:     Lars Noschinski
*)

theory Int_Pow
imports Main "HOL-Algebra.Group"
begin

(*
  This file demonstrates how to restore Lifting/Transfer enviromenent.

  We want to define int_pow (a power with an integer exponent) by directly accessing
  the representation type "nat * nat" that was used to define integers.
*)

context monoid
begin

(* first some additional lemmas that are missing in monoid *)

lemma Units_nat_pow_Units [intro, simp]:
  "a \ Units G \ a [^] (c :: nat) \ Units G" by (induct c) auto

lemma Units_r_cancel [simp]:
  "[| z \ Units G; x \ carrier G; y \ carrier G |] ==>
   (x \<otimes> z = y \<otimes> z) = (x = y)"
proof
  assume eq: "x \ z = y \ z"
    and G: "z \ Units G" "x \ carrier G" "y \ carrier G"
  then have "x \ (z \ inv z) = y \ (z \ inv z)"
    by (simp add: m_assoc[symmetric] Units_closed del: Units_r_inv)
  with G show "x = y" by simp
next
  assume eq: "x = y"
    and G: "z \ Units G" "x \ carrier G" "y \ carrier G"
  then show "x \ z = y \ z" by simp
qed

lemma inv_mult_units:
  "[| x \ Units G; y \ Units G |] ==> inv (x \ y) = inv y \ inv x"
proof -
  assume G: "x \ Units G" "y \ Units G"
  then have "x \ carrier G" "y \ carrier G" by auto
  with G have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)"
    by (simp add: m_assoc) (simp add: m_assoc [symmetric])
  with G show ?thesis by (simp del: Units_l_inv)
qed

lemma mult_same_comm:
  assumes [simp, intro]: "a \ Units G"
  shows "a [^] (m::nat) \ inv (a [^] (n::nat)) = inv (a [^] n) \ a [^] m"
proof (cases "m\n")
  have [simp]: "a \ carrier G" using \a \ _\ by (rule Units_closed)
  case True
    then obtain k where *:"m = k + n" and **:"m = n + k" by (metis le_iff_add add.commute)
    have "a [^] (m::nat) \ inv (a [^] (n::nat)) = a [^] k"
      using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
    also have "\ = inv (a [^] n) \ a [^] m"
      using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric])
    finally show ?thesis .
next
  have [simp]: "a \ carrier G" using \a \ _\ by (rule Units_closed)
  case False
    then obtain k where *:"n = k + m" and **:"n = m + k"
      by (metis le_iff_add add.commute nat_le_linear)
    have "a [^] (m::nat) \ inv (a [^] (n::nat)) = inv(a [^] k)"
      using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
    also have "\ = inv (a [^] n) \ a [^] m"
      using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc inv_mult_units)
    finally show ?thesis .
qed

lemma mult_inv_same_comm:
  "a \ Units G \ inv (a [^] (m::nat)) \ inv (a [^] (n::nat)) = inv (a [^] n) \ inv (a [^] m)"
by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed)

context
includes int.lifting (* restores Lifting/Transfer for integers *)
begin

lemma int_pow_rsp:
  assumes eq: "(b::nat) + e = d + c"
  assumes a_in_G [simp, intro]: "a \ Units G"
  shows "a [^] b \ inv (a [^] c) = a [^] d \ inv (a [^] e)"
proof(cases "b\c")
  have [simp]: "a \ carrier G" using \a \ _\ by (rule Units_closed)
  case True
    then obtain n where "b = n + c" by (metis le_iff_add add.commute)
    then have "d = n + e" using eq by arith
    from \<open>b = _\<close> have "a [^] b \<otimes> inv (a [^] c) = a [^] n"
      by (auto simp add: nat_pow_mult[symmetric] m_assoc)
    also from \<open>d = _\<close>  have "\<dots> = a [^] d \<otimes> inv (a [^] e)"
      by (auto simp add: nat_pow_mult[symmetric] m_assoc)
    finally show ?thesis .
next
  have [simp]: "a \ carrier G" using \a \ _\ by (rule Units_closed)
  case False
    then obtain n where "c = n + b" by (metis le_iff_add add.commute nat_le_linear)
    then have "e = n + d" using eq by arith
    from \<open>c = _\<close> have "a [^] b \<otimes> inv (a [^] c) = inv (a [^] n)"
      by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
    also from \<open>e = _\<close> have "\<dots> = a [^] d \<otimes> inv (a [^] e)"
      by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
    finally show ?thesis .
qed

(*
  This definition is more convinient than the definition in HOL/Algebra/Group because
  it doesn't contain a test z < 0 when a [^] z is being defined.
*)

lift_definition int_pow :: "('a, 'm) monoid_scheme \ 'a \ int \ 'a" is
  "\G a (n1, n2). if a \ Units G \ monoid G then (a [^]\<^bsub>G\<^esub> n1) \\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> n2)) else \\<^bsub>G\<^esub>"
unfolding intrel_def by (auto intro: monoid.int_pow_rsp)

(*
  Thus, for example, the proof of distributivity of int_pow and addition
  doesn't require a substantial number of case distinctions.
*)

lemma int_pow_dist:
  assumes [simp]: "a \ Units G"
  shows "int_pow G a ((n::int) + m) = int_pow G a n \\<^bsub>G\<^esub> int_pow G a m"
proof -
  {
    fix k l m :: nat
    have "a [^] l \ (inv (a [^] m) \ inv (a [^] k)) = (a [^] l \ inv (a [^] k)) \ inv (a [^] m)"
      (is "?lhs = _")
      by (simp add: mult_inv_same_comm m_assoc Units_closed)
    also have "\ = (inv (a [^] k) \ a [^] l) \ inv (a [^] m)"
      by (simp add: mult_same_comm)
    also have "\ = inv (a [^] k) \ (a [^] l \ inv (a [^] m))" (is "_ = ?rhs")
      by (simp add: m_assoc Units_closed)
    finally have "?lhs = ?rhs" .
  }
  then show ?thesis
    by (transfer fixing: G) (auto simp add: nat_pow_mult[symmetric] inv_mult_units m_assoc Units_closed)
qed

end

lifting_update int.lifting
lifting_forget int.lifting

end

end

quality99%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.