--- a/src/HOL/Quotient_Examples/Int_Pow.thy Fri Jan 05 15:24:57 2018 +0100
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy Fri Jan 05 18:41:42 2018 +0100
@@ -20,7 +20,7 @@
(* first some additional lemmas that are missing in monoid *)
lemma Units_nat_pow_Units [intro, simp]:
- "a \<in> Units G \<Longrightarrow> a (^) (c :: nat) \<in> Units G" by (induct c) auto
+ "a \<in> Units G \<Longrightarrow> a [^] (c :: nat) \<in> Units G" by (induct c) auto
lemma Units_r_cancel [simp]:
"[| z \<in> Units G; x \<in> carrier G; y \<in> carrier G |] ==>
@@ -49,14 +49,14 @@
lemma mult_same_comm:
assumes [simp, intro]: "a \<in> Units G"
- shows "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> a (^) m"
+ shows "a [^] (m::nat) \<otimes> inv (a [^] (n::nat)) = inv (a [^] n) \<otimes> a [^] m"
proof (cases "m\<ge>n")
have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> 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) \<otimes> inv (a (^) (n::nat)) = a (^) k"
+ have "a [^] (m::nat) \<otimes> inv (a [^] (n::nat)) = a [^] k"
using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
- also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
+ also have "\<dots> = inv (a [^] n) \<otimes> a [^] m"
using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric])
finally show ?thesis .
next
@@ -64,15 +64,15 @@
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) \<otimes> inv (a (^) (n::nat)) = inv(a (^) k)"
+ have "a [^] (m::nat) \<otimes> inv (a [^] (n::nat)) = inv(a [^] k)"
using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
- also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
+ also have "\<dots> = inv (a [^] n) \<otimes> 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 \<in> Units G \<Longrightarrow> inv (a (^) (m::nat)) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> inv (a (^) m)"
+ "a \<in> Units G \<Longrightarrow> inv (a [^] (m::nat)) \<otimes> inv (a [^] (n::nat)) = inv (a [^] n) \<otimes> inv (a [^] m)"
by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed)
context
@@ -82,15 +82,15 @@
lemma int_pow_rsp:
assumes eq: "(b::nat) + e = d + c"
assumes a_in_G [simp, intro]: "a \<in> Units G"
- shows "a (^) b \<otimes> inv (a (^) c) = a (^) d \<otimes> inv (a (^) e)"
+ shows "a [^] b \<otimes> inv (a [^] c) = a [^] d \<otimes> inv (a [^] e)"
proof(cases "b\<ge>c")
have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> 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"
+ 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)"
+ 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
@@ -98,20 +98,20 @@
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)"
+ 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)"
+ 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.
+ it doesn't contain a test z < 0 when a [^] z is being defined.
*)
lift_definition int_pow :: "('a, 'm) monoid_scheme \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'a" is
- "\<lambda>G a (n1, n2). if a \<in> Units G \<and> monoid G then (a (^)\<^bsub>G\<^esub> n1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a (^)\<^bsub>G\<^esub> n2)) else \<one>\<^bsub>G\<^esub>"
+ "\<lambda>G a (n1, n2). if a \<in> Units G \<and> monoid G then (a [^]\<^bsub>G\<^esub> n1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> n2)) else \<one>\<^bsub>G\<^esub>"
unfolding intrel_def by (auto intro: monoid.int_pow_rsp)
(*
@@ -125,12 +125,12 @@
proof -
{
fix k l m :: nat
- have "a (^) l \<otimes> (inv (a (^) m) \<otimes> inv (a (^) k)) = (a (^) l \<otimes> inv (a (^) k)) \<otimes> inv (a (^) m)"
+ have "a [^] l \<otimes> (inv (a [^] m) \<otimes> inv (a [^] k)) = (a [^] l \<otimes> inv (a [^] k)) \<otimes> inv (a [^] m)"
(is "?lhs = _")
by (simp add: mult_inv_same_comm m_assoc Units_closed)
- also have "\<dots> = (inv (a (^) k) \<otimes> a (^) l) \<otimes> inv (a (^) m)"
+ also have "\<dots> = (inv (a [^] k) \<otimes> a [^] l) \<otimes> inv (a [^] m)"
by (simp add: mult_same_comm)
- also have "\<dots> = inv (a (^) k) \<otimes> (a (^) l \<otimes> inv (a (^) m))" (is "_ = ?rhs")
+ also have "\<dots> = inv (a [^] k) \<otimes> (a [^] l \<otimes> inv (a [^] m))" (is "_ = ?rhs")
by (simp add: m_assoc Units_closed)
finally have "?lhs = ?rhs" .
}