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