src/HOL/Decision_Procs/Algebra_Aux.thy
author wenzelm
Sat, 10 Jun 2017 21:48:02 +0200
changeset 66061 880db47fed30
parent 64998 d51478d6aae4
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Decision_Procs/Algebra_Aux.thy
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     3
*)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     4
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     5
section \<open>Things that can be added to the Algebra library\<close>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     6
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     7
theory Algebra_Aux
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     8
imports "~~/src/HOL/Algebra/Ring"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
     9
begin
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    10
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    11
definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    12
  "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> = (op \<oplus>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub> ^^ n) \<zero>\<^bsub>R\<^esub>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    13
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    14
definition of_integer :: "('a, 'm) ring_scheme \<Rightarrow> int \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<index>") where
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    15
  "\<guillemotleft>i\<guillemotright>\<^bsub>R\<^esub> = (if 0 \<le> i then \<guillemotleft>nat i\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> else \<ominus>\<^bsub>R\<^esub> \<guillemotleft>nat (- i)\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub>)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    16
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    17
context ring begin
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    18
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    19
lemma of_nat_0 [simp]: "\<guillemotleft>0\<guillemotright>\<^sub>\<nat> = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    20
  by (simp add: of_natural_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    21
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    22
lemma of_nat_Suc [simp]: "\<guillemotleft>Suc n\<guillemotright>\<^sub>\<nat> = \<one> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    23
  by (simp add: of_natural_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    24
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    25
lemma of_int_0 [simp]: "\<guillemotleft>0\<guillemotright> = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    26
  by (simp add: of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    27
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    28
lemma of_nat_closed [simp]: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat> \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    29
  by (induct n) simp_all
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    30
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    31
lemma of_int_closed [simp]: "\<guillemotleft>i\<guillemotright> \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    32
  by (simp add: of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    33
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    34
lemma of_int_minus [simp]: "\<guillemotleft>- i\<guillemotright> = \<ominus> \<guillemotleft>i\<guillemotright>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    35
  by (simp add: of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    36
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    37
lemma of_nat_add [simp]: "\<guillemotleft>m + n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    38
  by (induct m) (simp_all add: a_ac)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    39
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    40
lemma of_nat_diff [simp]: "n \<le> m \<Longrightarrow> \<guillemotleft>m - n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    41
proof (induct m arbitrary: n)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    42
  case (Suc m)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    43
  note Suc' = this
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    44
  show ?case
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    45
  proof (cases n)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    46
    case (Suc k)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    47
    with Suc' have "\<guillemotleft>Suc m - Suc k\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    48
    also have "\<dots> = \<one> \<oplus> \<ominus> \<one> \<oplus> (\<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    49
      by (simp add: r_neg)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    50
    also have "\<dots> = \<guillemotleft>Suc m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>Suc k\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    51
      by (simp add: minus_eq minus_add a_ac)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    52
    finally show ?thesis using Suc by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    53
  qed (simp add: minus_eq)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    54
qed (simp add: minus_eq)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    55
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    56
lemma of_int_add [simp]: "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<oplus> \<guillemotleft>j\<guillemotright>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    57
proof (cases "0 \<le> i")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    58
  case True
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    59
  show ?thesis
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    60
  proof (cases "0 \<le> j")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    61
    case True
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
    62
    with \<open>0 \<le> i\<close> show ?thesis by (simp add: of_integer_def nat_add_distrib)
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    63
  next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    64
    case False
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    65
    show ?thesis
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    66
    proof (cases "0 \<le> i + j")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    67
      case True
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    68
      then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (i - (- j))\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    69
        by (simp add: of_integer_def)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
    70
      also from True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    71
      have "nat (i - (- j)) = nat i - nat (- j)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    72
        by (simp add: nat_diff_distrib)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
    73
      finally show ?thesis using True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    74
        by (simp add: minus_eq of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    75
    next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    76
      case False
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    77
      then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- j - i)\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    78
        by (simp add: of_integer_def) (simp only: diff_conv_add_uminus add_ac)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
    79
      also from False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    80
      have "nat (- j - i) = nat (- j) - nat i"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    81
        by (simp add: nat_diff_distrib)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
    82
      finally show ?thesis using False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    83
        by (simp add: minus_eq minus_add a_ac of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    84
    qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    85
  qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    86
next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    87
  case False
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    88
  show ?thesis
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    89
  proof (cases "0 \<le> j")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    90
    case True
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    91
    show ?thesis
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    92
    proof (cases "0 \<le> i + j")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    93
      case True
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    94
      then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (j - (- i))\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    95
        by (simp add: of_integer_def add_ac)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
    96
      also from True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    97
      have "nat (j - (- i)) = nat j - nat (- i)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
    98
        by (simp add: nat_diff_distrib)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
    99
      finally show ?thesis using True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   100
        by (simp add: minus_eq minus_add a_ac of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   101
    next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   102
      case False
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   103
      then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- i - j)\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   104
        by (simp add: of_integer_def)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
   105
      also from False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   106
      have "nat (- i - j) = nat (- i) - nat j"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   107
        by (simp add: nat_diff_distrib)
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
   108
      finally show ?thesis using False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   109
        by (simp add: minus_eq minus_add of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   110
    qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   111
  next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   112
    case False
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
   113
    with \<open>\<not> 0 \<le> i\<close> show ?thesis
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   114
      by (simp add: of_integer_def nat_add_distrib minus_add diff_conv_add_uminus
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   115
        del: add_uminus_conv_diff uminus_add_conv_diff)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   116
  qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   117
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   118
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   119
lemma of_int_diff [simp]: "\<guillemotleft>i - j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<ominus> \<guillemotleft>j\<guillemotright>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   120
  by (simp only: diff_conv_add_uminus of_int_add) (simp add: minus_eq)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   121
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   122
lemma of_nat_mult [simp]: "\<guillemotleft>i * j\<guillemotright>\<^sub>\<nat> = \<guillemotleft>i\<guillemotright>\<^sub>\<nat> \<otimes> \<guillemotleft>j\<guillemotright>\<^sub>\<nat>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   123
  by (induct i) (simp_all add: l_distr)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   124
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   125
lemma of_int_mult [simp]: "\<guillemotleft>i * j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<otimes> \<guillemotleft>j\<guillemotright>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   126
proof (cases "0 \<le> i")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   127
  case True
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   128
  show ?thesis
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   129
  proof (cases "0 \<le> j")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   130
    case True
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
   131
    with \<open>0 \<le> i\<close> show ?thesis
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   132
      by (simp add: of_integer_def nat_mult_distrib zero_le_mult_iff)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   133
  next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   134
    case False
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
   135
    with \<open>0 \<le> i\<close> show ?thesis
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   136
      by (simp add: of_integer_def zero_le_mult_iff
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   137
        minus_mult_right nat_mult_distrib r_minus
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   138
        del: minus_mult_right [symmetric])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   139
  qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   140
next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   141
  case False
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   142
  show ?thesis
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   143
  proof (cases "0 \<le> j")
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   144
    case True
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
   145
    with \<open>\<not> 0 \<le> i\<close> show ?thesis
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   146
      by (simp add: of_integer_def zero_le_mult_iff
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   147
        minus_mult_left nat_mult_distrib l_minus
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   148
        del: minus_mult_left [symmetric])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   149
  next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   150
    case False
64998
d51478d6aae4 isabelle update_cartouches
haftmann
parents: 64962
diff changeset
   151
    with \<open>\<not> 0 \<le> i\<close> show ?thesis
64962
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   152
      by (simp add: of_integer_def zero_le_mult_iff
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   153
        minus_mult_minus [of i j, symmetric] nat_mult_distrib
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   154
        l_minus r_minus
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   155
        del: minus_mult_minus
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   156
        minus_mult_left [symmetric] minus_mult_right [symmetric])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   157
  qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   158
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   159
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   160
lemma of_int_1 [simp]: "\<guillemotleft>1\<guillemotright> = \<one>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   161
  by (simp add: of_integer_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   162
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   163
lemma of_int_2: "\<guillemotleft>2\<guillemotright> = \<one> \<oplus> \<one>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   164
  by (simp add: of_integer_def numeral_2_eq_2)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   165
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   166
lemma minus_0_r [simp]: "x \<in> carrier R \<Longrightarrow> x \<ominus> \<zero> = x"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   167
  by (simp add: minus_eq)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   168
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   169
lemma minus_0_l [simp]: "x \<in> carrier R \<Longrightarrow> \<zero> \<ominus> x = \<ominus> x"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   170
  by (simp add: minus_eq)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   171
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   172
lemma eq_diff0:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   173
  assumes "x \<in> carrier R" "y \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   174
  shows "(x \<ominus> y = \<zero>) = (x = y)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   175
proof
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   176
  assume "x \<ominus> y = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   177
  with assms have "x \<oplus> (\<ominus> y \<oplus> y) = y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   178
    by (simp add: minus_eq a_assoc [symmetric])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   179
  with assms show "x = y" by (simp add: l_neg)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   180
next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   181
  assume "x = y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   182
  with assms show "x \<ominus> y = \<zero>" by (simp add: minus_eq r_neg)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   183
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   184
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   185
lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x (^) (2::nat) = x \<otimes> x"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   186
  by (simp add: numeral_eq_Suc)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   187
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   188
lemma eq_neg_iff_add_eq_0:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   189
  assumes "x \<in> carrier R" "y \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   190
  shows "(x = \<ominus> y) = (x \<oplus> y = \<zero>)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   191
proof
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   192
  assume "x = \<ominus> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   193
  with assms show "x \<oplus> y = \<zero>" by (simp add: l_neg)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   194
next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   195
  assume "x \<oplus> y = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   196
  with assms have "x \<oplus> (y \<oplus> \<ominus> y) = \<zero> \<oplus> \<ominus> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   197
    by (simp add: a_assoc [symmetric])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   198
  with assms show "x = \<ominus> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   199
    by (simp add: r_neg)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   200
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   201
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   202
lemma neg_equal_iff_equal:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   203
  assumes x: "x \<in> carrier R" and y: "y \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   204
  shows "(\<ominus> x = \<ominus> y) = (x = y)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   205
proof
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   206
  assume "\<ominus> x = \<ominus> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   207
  then have "\<ominus> (\<ominus> x) = \<ominus> (\<ominus> y)" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   208
  with x y show "x = y" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   209
next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   210
  assume "x = y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   211
  then show "\<ominus> x = \<ominus> y" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   212
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   213
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   214
lemma neg_equal_swap:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   215
  assumes x: "x \<in> carrier R" and y: "y \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   216
  shows "(\<ominus> x = y) = (x = \<ominus> y)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   217
  using assms neg_equal_iff_equal [of x "\<ominus> y"]
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   218
  by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   219
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   220
lemma mult2: "x \<in> carrier R \<Longrightarrow> x \<oplus> x = \<guillemotleft>2\<guillemotright> \<otimes> x"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   221
  by (simp add: of_int_2 l_distr)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   222
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   223
end
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   224
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   225
lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> (^) n"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   226
  by (induct n) (simp_all add: m_ac)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   227
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   228
definition cring_class_ops :: "'a::comm_ring_1 ring" where
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   229
  "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   230
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   231
lemma cring_class: "cring cring_class_ops"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   232
  apply unfold_locales
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   233
  apply (auto simp add: cring_class_ops_def ring_distribs Units_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   234
  apply (rule_tac x="- x" in exI)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   235
  apply simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   236
  done
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   237
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   238
lemma carrier_class: "x \<in> carrier cring_class_ops"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   239
  by (simp add: cring_class_ops_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   240
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   241
lemma zero_class: "\<zero>\<^bsub>cring_class_ops\<^esub> = 0"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   242
  by (simp add: cring_class_ops_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   243
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   244
lemma one_class: "\<one>\<^bsub>cring_class_ops\<^esub> = 1"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   245
  by (simp add: cring_class_ops_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   246
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   247
lemma plus_class: "x \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   248
  by (simp add: cring_class_ops_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   249
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   250
lemma times_class: "x \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   251
  by (simp add: cring_class_ops_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   252
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   253
lemma uminus_class: "\<ominus>\<^bsub>cring_class_ops\<^esub> x = - x"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   254
  apply (simp add: a_inv_def m_inv_def cring_class_ops_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   255
  apply (rule the_equality)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   256
  apply (simp_all add: eq_neg_iff_add_eq_0)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   257
  done
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   258
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   259
lemma minus_class: "x \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   260
  by (simp add: a_minus_def carrier_class plus_class uminus_class)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   261
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   262
lemma power_class: "x (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   263
  by (induct n) (simp_all add: one_class times_class
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   264
    monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   265
    monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   266
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   267
lemma of_nat_class: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   268
  by (induct n) (simp_all add: cring_class_ops_def of_natural_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   269
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   270
lemma of_int_class: "\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub> = of_int i"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   271
  by (simp add: of_integer_def of_nat_class uminus_class)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   272
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   273
lemmas class_simps = zero_class one_class plus_class minus_class uminus_class
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   274
  times_class power_class of_nat_class of_int_class carrier_class
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   275
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   276
interpretation cring_class: cring "cring_class_ops::'a::comm_ring_1 ring"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   277
  rewrites
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   278
    "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   279
    "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   280
    "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   281
    "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   282
    "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   283
    "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   284
    "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   285
    "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   286
    "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   287
    "(Int.of_int (numeral m)::'a) = numeral m"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   288
  by (simp_all add: cring_class class_simps)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   289
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   290
lemma (in domain) nat_pow_eq_0_iff [simp]:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   291
  "a \<in> carrier R \<Longrightarrow> (a (^) (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   292
  by (induct n) (auto simp add: integral_iff)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   293
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   294
lemma (in domain) square_eq_iff:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   295
  assumes "x \<in> carrier R" "y \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   296
  shows "(x \<otimes> x = y \<otimes> y) = (x = y \<or> x = \<ominus> y)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   297
proof
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   298
  assume "x \<otimes> x = y \<otimes> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   299
  with assms have "(x \<ominus> y) \<otimes> (x \<oplus> y) = x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) \<oplus> (y \<otimes> y \<oplus> \<ominus> (y \<otimes> y))"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   300
    by (simp add: r_distr l_distr minus_eq r_minus m_comm a_ac)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   301
  with assms show "x = y \<or> x = \<ominus> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   302
    by (simp add: integral_iff eq_neg_iff_add_eq_0 eq_diff0 r_neg)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   303
next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   304
  assume "x = y \<or> x = \<ominus> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   305
  with assms show "x \<otimes> x = y \<otimes> y" by (auto simp add: l_minus r_minus)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   306
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   307
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   308
definition
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   309
  m_div :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oslash>\<index>" 70) where
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   310
  "x \<oslash>\<^bsub>G\<^esub> y = (if y = \<zero>\<^bsub>G\<^esub> then \<zero>\<^bsub>G\<^esub> else x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   311
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   312
context field
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   313
begin
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   314
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   315
lemma inv_closed [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   316
  by (simp add: field_Units)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   317
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   318
lemma l_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<otimes> x = \<one>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   319
  by (simp add: field_Units)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   320
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   321
lemma r_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> x \<otimes> inv x = \<one>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   322
  by (simp add: field_Units)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   323
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   324
lemma inverse_unique:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   325
  assumes a: "a \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   326
  and b: "b \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   327
  and ab: "a \<otimes> b = \<one>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   328
  shows "inv a = b"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   329
proof -
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   330
  have "a \<noteq> \<zero>" using ab b by (cases "a = \<zero>") simp_all
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   331
  moreover with a have "inv a \<otimes> (a \<otimes> b) = inv a" by (simp add: ab)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   332
  ultimately show ?thesis using a b by (simp add: m_assoc [symmetric])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   333
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   334
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   335
lemma nonzero_inverse_inverse_eq:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   336
  "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> inv (inv a) = a"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   337
  by (rule inverse_unique) simp_all
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   338
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   339
lemma inv_1 [simp]: "inv \<one> = \<one>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   340
  by (rule inverse_unique) simp_all
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   341
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   342
lemma nonzero_inverse_mult_distrib:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   343
  assumes "a \<in> carrier R" and "b \<in> carrier R" and "a \<noteq> \<zero>" and "b \<noteq> \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   344
  shows "inv (a \<otimes> b) = inv b \<otimes> inv a"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   345
proof -
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   346
  have "a \<otimes> (b \<otimes> inv b) \<otimes> inv a = \<one>" using assms by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   347
  hence eq: "a \<otimes> b \<otimes> (inv b \<otimes> inv a) = \<one>" using assms
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   348
    by (simp only: m_assoc m_closed inv_closed assms)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   349
  from inverse_unique [OF _ _ eq] assms
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   350
  show ?thesis by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   351
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   352
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   353
lemma nonzero_imp_inverse_nonzero:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   354
  assumes "a \<in> carrier R" and "a \<noteq> \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   355
  shows "inv a \<noteq> \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   356
proof
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   357
  assume ianz: "inv a = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   358
  from assms
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   359
  have "\<one> = a \<otimes> inv a" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   360
  also with assms have "... = \<zero>" by (simp add: ianz)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   361
  finally have "\<one> = \<zero>" .
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   362
  thus False by (simp add: eq_commute)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   363
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   364
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   365
lemma nonzero_divide_divide_eq_left:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   366
  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   367
   a \<oslash> b \<oslash> c = a \<oslash> (b \<otimes> c)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   368
  by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   369
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   370
lemma nonzero_times_divide_eq:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   371
  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   372
   b \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<otimes> (c \<oslash> d) = (a \<otimes> c) \<oslash> (b \<otimes> d)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   373
  by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   374
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   375
lemma nonzero_divide_divide_eq:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   376
  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   377
   b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<oslash> (c \<oslash> d) = (a \<otimes> d) \<oslash> (b \<otimes> c)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   378
  by (simp add: m_div_def nonzero_inverse_mult_distrib
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   379
    nonzero_imp_inverse_nonzero nonzero_inverse_inverse_eq m_ac integral_iff)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   380
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   381
lemma divide_1 [simp]: "x \<in> carrier R \<Longrightarrow> x \<oslash> \<one> = x"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   382
  by (simp add: m_div_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   383
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   384
lemma add_frac_eq:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   385
  assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   386
  and "y \<noteq> \<zero>" and "z \<noteq> \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   387
  shows "x \<oslash> y \<oplus> w \<oslash> z = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   388
proof -
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   389
  from assms
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   390
  have "x \<oslash> y \<oplus> w \<oslash> z = x \<otimes> inv y \<otimes> (z \<otimes> inv z) \<oplus> w \<otimes> inv z \<otimes> (y \<otimes> inv y)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   391
    by (simp add: m_div_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   392
  also from assms have "\<dots> = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   393
    by (simp add: m_div_def nonzero_inverse_mult_distrib r_distr m_ac integral_iff del: r_inv)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   394
  finally show ?thesis .
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   395
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   396
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   397
lemma div_closed [simp]:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   398
  "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> y \<noteq> \<zero> \<Longrightarrow> x \<oslash> y \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   399
  by (simp add: m_div_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   400
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   401
lemma minus_divide_left [simp]:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   402
  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> \<ominus> (a \<oslash> b) = \<ominus> a \<oslash> b"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   403
  by (simp add: m_div_def l_minus)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   404
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   405
lemma diff_frac_eq:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   406
  assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   407
  and "y \<noteq> \<zero>" and "z \<noteq> \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   408
  shows "x \<oslash> y \<ominus> w \<oslash> z = (x \<otimes> z \<ominus> w \<otimes> y) \<oslash> (y \<otimes> z)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   409
  using assms
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   410
  by (simp add: minus_eq l_minus add_frac_eq)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   411
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   412
lemma nonzero_mult_divide_mult_cancel_left [simp]:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   413
  assumes "a \<in> carrier R" and "b \<in> carrier R" and "c \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   414
  and "b \<noteq> \<zero>" and "c \<noteq> \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   415
  shows "(c \<otimes> a) \<oslash> (c \<otimes> b) = a \<oslash> b"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   416
proof -
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   417
  from assms have "(c \<otimes> a) \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   418
    by (simp add: m_div_def nonzero_inverse_mult_distrib integral_iff)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   419
  also from assms have "\<dots> =  a \<otimes> inv b \<otimes> (inv c \<otimes> c)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   420
    by (simp add: m_ac)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   421
  also from assms have "\<dots> =  a \<otimes> inv b" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   422
  finally show ?thesis using assms by (simp add: m_div_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   423
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   424
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   425
lemma times_divide_eq_left [simp]:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   426
  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   427
   (b \<oslash> c) \<otimes> a = b \<otimes> a \<oslash> c"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   428
  by (simp add: m_div_def m_ac)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   429
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   430
lemma times_divide_eq_right [simp]:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   431
  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   432
   a \<otimes> (b \<oslash> c) = a \<otimes> b \<oslash> c"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   433
  by (simp add: m_div_def m_ac)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   434
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   435
lemma nonzero_power_divide:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   436
  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   437
   (a \<oslash> b) (^) (n::nat) = a (^) n \<oslash> b (^) n"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   438
  by (induct n) (simp_all add: nonzero_divide_divide_eq_left)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   439
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   440
lemma r_diff_distr:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   441
  "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow>
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   442
   z \<otimes> (x \<ominus> y) = z \<otimes> x \<ominus> z \<otimes> y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   443
  by (simp add: minus_eq r_distr r_minus)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   444
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   445
lemma divide_zero_left [simp]:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   446
  "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> \<zero> \<oslash> a = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   447
  by (simp add: m_div_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   448
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   449
lemma divide_self: "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> a \<oslash> a = \<one>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   450
  by (simp add: m_div_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   451
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   452
lemma divide_eq_0_iff:
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   453
  assumes "a \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   454
  and "b \<in> carrier R"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   455
  and "b \<noteq> \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   456
  shows "(a \<oslash> b = \<zero>) = (a = \<zero>)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   457
proof
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   458
  assume "a = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   459
  with assms show "a \<oslash> b = \<zero>" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   460
next
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   461
  assume "a \<oslash> b = \<zero>"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   462
  with assms have "b \<otimes> (a \<oslash> b) = b \<otimes> \<zero>" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   463
  also from assms have "b \<otimes> (a \<oslash> b) = b \<otimes> a \<oslash> b" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   464
  also from assms have "b \<otimes> a = a \<otimes> b" by (simp add: m_comm)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   465
  also from assms have "a \<otimes> b \<oslash> b = a \<otimes> (b \<oslash> b)" by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   466
  also from assms have "b \<oslash> b = \<one>" by (simp add: divide_self)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   467
  finally show "a = \<zero>" using assms by simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   468
qed
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   469
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   470
end
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   471
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   472
lemma field_class: "field (cring_class_ops::'a::field ring)"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   473
  apply unfold_locales
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   474
  apply (simp_all add: cring_class_ops_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   475
  apply (auto simp add: Units_def)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   476
  apply (rule_tac x="1 / x" in exI)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   477
  apply simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   478
  done
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   479
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   480
lemma div_class: "(x::'a::field) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   481
  apply (simp add: m_div_def m_inv_def class_simps)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   482
  apply (rule impI)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   483
  apply (rule ssubst [OF the_equality, of _ "1 / y"])
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   484
  apply simp_all
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   485
  apply (drule conjunct2)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   486
  apply (drule_tac f="\<lambda>x. x / y" in arg_cong)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   487
  apply simp
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   488
  done
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   489
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   490
interpretation field_class: field "cring_class_ops::'a::field ring"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   491
  rewrites
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   492
    "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   493
    "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   494
    "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   495
    "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   496
    "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   497
    "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   498
    "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   499
    "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   500
    "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   501
    "(x::'a) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y" and
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   502
    "(Int.of_int (numeral m)::'a) = numeral m"
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   503
  by (simp_all add: field_class class_simps div_class)
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   504
bf41e1109db3 Added new / improved tactics for fields and rings
berghofe
parents:
diff changeset
   505
end