src/HOL/Quotient_Examples/Int_Pow.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 66453 cc19f7ca2ed6
child 67341 df79ef3b3a41
permissions -rw-r--r--
more fundamental definition of div and mod on int
kuncar@53653
     1
(*  Title:      HOL/Quotient_Examples/Int_Pow.thy
kuncar@53653
     2
    Author:     Ondrej Kuncar
kuncar@53653
     3
    Author:     Lars Noschinski
kuncar@53653
     4
*)
kuncar@53653
     5
kuncar@53653
     6
theory Int_Pow
wenzelm@66453
     7
imports Main "HOL-Algebra.Group"
hoelzl@62378
     8
begin
kuncar@53653
     9
kuncar@53653
    10
(*
kuncar@53653
    11
  This file demonstrates how to restore Lifting/Transfer enviromenent.
kuncar@53653
    12
hoelzl@62378
    13
  We want to define int_pow (a power with an integer exponent) by directly accessing
kuncar@53653
    14
  the representation type "nat * nat" that was used to define integers.
kuncar@53653
    15
*)
kuncar@53653
    16
kuncar@53653
    17
context monoid
kuncar@53653
    18
begin
kuncar@53653
    19
kuncar@53653
    20
(* first some additional lemmas that are missing in monoid *)
kuncar@53653
    21
hoelzl@62378
    22
lemma Units_nat_pow_Units [intro, simp]:
kuncar@53653
    23
  "a \<in> Units G \<Longrightarrow> a (^) (c :: nat) \<in> Units G" by (induct c) auto
kuncar@53653
    24
kuncar@53653
    25
lemma Units_r_cancel [simp]:
kuncar@53653
    26
  "[| z \<in> Units G; x \<in> carrier G; y \<in> carrier G |] ==>
kuncar@53653
    27
   (x \<otimes> z = y \<otimes> z) = (x = y)"
kuncar@53653
    28
proof
kuncar@53653
    29
  assume eq: "x \<otimes> z = y \<otimes> z"
kuncar@53653
    30
    and G: "z \<in> Units G"  "x \<in> carrier G"  "y \<in> carrier G"
kuncar@53653
    31
  then have "x \<otimes> (z \<otimes> inv z) = y \<otimes> (z \<otimes> inv z)"
kuncar@53653
    32
    by (simp add: m_assoc[symmetric] Units_closed del: Units_r_inv)
kuncar@53653
    33
  with G show "x = y" by simp
kuncar@53653
    34
next
kuncar@53653
    35
  assume eq: "x = y"
kuncar@53653
    36
    and G: "z \<in> Units G"  "x \<in> carrier G"  "y \<in> carrier G"
kuncar@53653
    37
  then show "x \<otimes> z = y \<otimes> z" by simp
kuncar@53653
    38
qed
kuncar@53653
    39
kuncar@53653
    40
lemma inv_mult_units:
kuncar@53653
    41
  "[| x \<in> Units G; y \<in> Units G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
kuncar@53653
    42
proof -
kuncar@53653
    43
  assume G: "x \<in> Units G"  "y \<in> Units G"
wenzelm@63540
    44
  then have "x \<in> carrier G"  "y \<in> carrier G" by auto
wenzelm@63540
    45
  with G have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
kuncar@53653
    46
    by (simp add: m_assoc) (simp add: m_assoc [symmetric])
kuncar@53653
    47
  with G show ?thesis by (simp del: Units_l_inv)
kuncar@53653
    48
qed
kuncar@53653
    49
hoelzl@62378
    50
lemma mult_same_comm:
hoelzl@62378
    51
  assumes [simp, intro]: "a \<in> Units G"
kuncar@53653
    52
  shows "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> a (^) m"
kuncar@53653
    53
proof (cases "m\<ge>n")
wenzelm@63167
    54
  have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> by (rule Units_closed)
kuncar@53653
    55
  case True
hoelzl@62378
    56
    then obtain k where *:"m = k + n" and **:"m = n + k" by (metis le_iff_add add.commute)
kuncar@53653
    57
    have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = a (^) k"
kuncar@53653
    58
      using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
kuncar@53653
    59
    also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
kuncar@53653
    60
      using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric])
kuncar@53653
    61
    finally show ?thesis .
kuncar@53653
    62
next
wenzelm@63167
    63
  have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> by (rule Units_closed)
kuncar@53653
    64
  case False
hoelzl@62378
    65
    then obtain k where *:"n = k + m" and **:"n = m + k"
hoelzl@62378
    66
      by (metis le_iff_add add.commute nat_le_linear)
kuncar@53653
    67
    have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv(a (^) k)"
kuncar@53653
    68
      using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
kuncar@53653
    69
    also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
kuncar@53653
    70
      using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc inv_mult_units)
kuncar@53653
    71
    finally show ?thesis .
kuncar@53653
    72
qed
kuncar@53653
    73
hoelzl@62378
    74
lemma mult_inv_same_comm:
kuncar@53653
    75
  "a \<in> Units G \<Longrightarrow> inv (a (^) (m::nat)) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> inv (a (^) m)"
kuncar@53653
    76
by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed)
kuncar@53653
    77
kuncar@53653
    78
context
kuncar@53653
    79
includes int.lifting (* restores Lifting/Transfer for integers *)
kuncar@53653
    80
begin
kuncar@53653
    81
kuncar@53653
    82
lemma int_pow_rsp:
kuncar@53653
    83
  assumes eq: "(b::nat) + e = d + c"
kuncar@53653
    84
  assumes a_in_G [simp, intro]: "a \<in> Units G"
kuncar@53653
    85
  shows "a (^) b \<otimes> inv (a (^) c) = a (^) d \<otimes> inv (a (^) e)"
kuncar@53653
    86
proof(cases "b\<ge>c")
wenzelm@63167
    87
  have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> by (rule Units_closed)
kuncar@53653
    88
  case True
hoelzl@62378
    89
    then obtain n where "b = n + c" by (metis le_iff_add add.commute)
kuncar@53653
    90
    then have "d = n + e" using eq by arith
wenzelm@63167
    91
    from \<open>b = _\<close> have "a (^) b \<otimes> inv (a (^) c) = a (^) n"
kuncar@53653
    92
      by (auto simp add: nat_pow_mult[symmetric] m_assoc)
wenzelm@63167
    93
    also from \<open>d = _\<close>  have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
kuncar@53653
    94
      by (auto simp add: nat_pow_mult[symmetric] m_assoc)
kuncar@53653
    95
    finally show ?thesis .
kuncar@53653
    96
next
wenzelm@63167
    97
  have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> by (rule Units_closed)
kuncar@53653
    98
  case False
hoelzl@62378
    99
    then obtain n where "c = n + b" by (metis le_iff_add add.commute nat_le_linear)
kuncar@53653
   100
    then have "e = n + d" using eq by arith
wenzelm@63167
   101
    from \<open>c = _\<close> have "a (^) b \<otimes> inv (a (^) c) = inv (a (^) n)"
kuncar@53653
   102
      by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
wenzelm@63167
   103
    also from \<open>e = _\<close> have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
kuncar@53653
   104
      by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
kuncar@53653
   105
    finally show ?thesis .
kuncar@53653
   106
qed
kuncar@53653
   107
kuncar@53653
   108
(*
kuncar@53653
   109
  This definition is more convinient than the definition in HOL/Algebra/Group because
kuncar@53653
   110
  it doesn't contain a test z < 0 when a (^) z is being defined.
kuncar@53653
   111
*)
kuncar@53653
   112
hoelzl@62378
   113
lift_definition int_pow :: "('a, 'm) monoid_scheme \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'a" is
hoelzl@62378
   114
  "\<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>"
kuncar@53653
   115
unfolding intrel_def by (auto intro: monoid.int_pow_rsp)
kuncar@53653
   116
kuncar@53653
   117
(*
hoelzl@62378
   118
  Thus, for example, the proof of distributivity of int_pow and addition
kuncar@53653
   119
  doesn't require a substantial number of case distinctions.
kuncar@53653
   120
*)
kuncar@53653
   121
kuncar@53653
   122
lemma int_pow_dist:
kuncar@53653
   123
  assumes [simp]: "a \<in> Units G"
kuncar@53653
   124
  shows "int_pow G a ((n::int) + m) = int_pow G a n \<otimes>\<^bsub>G\<^esub> int_pow G a m"
kuncar@53653
   125
proof -
kuncar@53653
   126
  {
kuncar@53653
   127
    fix k l m :: nat
hoelzl@62378
   128
    have "a (^) l \<otimes> (inv (a (^) m) \<otimes> inv (a (^) k)) = (a (^) l \<otimes> inv (a (^) k)) \<otimes> inv (a (^) m)"
kuncar@53653
   129
      (is "?lhs = _")
kuncar@53653
   130
      by (simp add: mult_inv_same_comm m_assoc Units_closed)
kuncar@53653
   131
    also have "\<dots> = (inv (a (^) k) \<otimes> a (^) l) \<otimes> inv (a (^) m)"
kuncar@53653
   132
      by (simp add: mult_same_comm)
kuncar@53653
   133
    also have "\<dots> = inv (a (^) k) \<otimes> (a (^) l \<otimes> inv (a (^) m))" (is "_ = ?rhs")
kuncar@53653
   134
      by (simp add: m_assoc Units_closed)
kuncar@53653
   135
    finally have "?lhs = ?rhs" .
kuncar@53653
   136
  }
kuncar@53653
   137
  then show ?thesis
kuncar@53653
   138
    by (transfer fixing: G) (auto simp add: nat_pow_mult[symmetric] inv_mult_units m_assoc Units_closed)
kuncar@53653
   139
qed
kuncar@53653
   140
kuncar@53653
   141
end
kuncar@53653
   142
kuncar@53653
   143
lifting_update int.lifting
kuncar@53653
   144
lifting_forget int.lifting
kuncar@53653
   145
kuncar@53653
   146
end
kuncar@53682
   147
kuncar@53682
   148
end