Skip to content

Instantly share code, notes, and snippets.

@tangentstorm

tangentstorm/exponents.thy

Created December 23, 2014 05:45
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save tangentstorm/e692f1cf6991782aa596 to your computer and use it in GitHub Desktop.
Save tangentstorm/e692f1cf6991782aa596 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
exponents.thy
theory Exponents
imports Main
begin
lemma rMulComm: "(a*b ::int) = (b*a ::int)"
by (rule Groups.ab_semigroup_mult_class.mult.commute)
lemma rExpMul: "((a^b)^c ::int) = (a^(b*c) ::int)"
by (rule Int.zpower_zpower)
theorem "((a^b)^c ::int) = ((a^c)^b :: int)"
(* 0. (a^b)^c
1. a^(b*c) by rExpMul
2. a^(c*b) by rMulComm
3. (a^c)^b by rExpMul
*)
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment