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