src/HOL/Algebra/Divisibility.thy
author ballarin
Wed, 30 Jul 2008 19:03:33 +0200
changeset 27713 95b36bfe7fc4
parent 27701 ed7a2e0fab59
child 27717 21bbd410ba04
permissions -rw-r--r--
New locales for orders and lattices where the equivalence relation is not restricted to equality.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
     1
(*
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
     2
  Title:     Divisibility in monoids and rings
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
     3
  Id:        $Id$
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
     4
  Author:    Clemens Ballarin, started 18 July 2008
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
     5
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
     6
Based on work by Stefan Hohe.
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
     7
*)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
     8
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
     9
theory Divisibility
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
    10
imports Permutation Coset Group
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    11
begin
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    12
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    13
subsection {* Monoid with cancelation law *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    14
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    15
locale monoid_cancel = monoid +
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    16
  assumes l_cancel: 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    17
          "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    18
      and r_cancel: 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    19
          "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    20
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    21
lemma (in monoid) monoid_cancelI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    22
  assumes l_cancel: 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    23
          "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    24
      and r_cancel: 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    25
          "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    26
  shows "monoid_cancel G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    27
by unfold_locales fact+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    28
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    29
lemma (in monoid_cancel) is_monoid_cancel:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    30
  "monoid_cancel G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    31
by intro_locales
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    32
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    33
interpretation group \<subseteq> monoid_cancel
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    34
by unfold_locales simp+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    35
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    36
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    37
locale comm_monoid_cancel = monoid_cancel + comm_monoid
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    38
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    39
lemma comm_monoid_cancelI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    40
  includes comm_monoid
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    41
  assumes cancel: 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    42
          "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    43
  shows "comm_monoid_cancel G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    44
apply unfold_locales
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    45
 apply (subgoal_tac "a \<otimes> c = b \<otimes> c")
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    46
  apply (iprover intro: cancel)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    47
 apply (simp add: m_comm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    48
apply (iprover intro: cancel)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    49
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    50
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    51
lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    52
  "comm_monoid_cancel G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    53
by intro_locales
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    54
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    55
interpretation comm_group \<subseteq> comm_monoid_cancel
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    56
by unfold_locales
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    57
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    58
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    59
subsection {* Products of units in monoids *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    60
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    61
lemma (in monoid) Units_m_closed[simp, intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    62
  assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    63
  shows "h1 \<otimes> h2 \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    64
unfolding Units_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    65
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    66
apply safe
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    67
apply fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    68
apply (intro bexI[of _ "inv h2 \<otimes> inv h1"], safe)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    69
  apply (simp add: m_assoc Units_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    70
  apply (simp add: m_assoc[symmetric] Units_closed Units_l_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    71
 apply (simp add: m_assoc Units_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    72
 apply (simp add: m_assoc[symmetric] Units_closed Units_r_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    73
apply fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    74
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    75
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    76
lemma (in monoid) prod_unit_l:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    77
  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    78
    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    79
  shows "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    80
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    81
  have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    82
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    83
  have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    84
  also have "\<dots> = \<one>" by (simp add: Units_l_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    85
  finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    86
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    87
  have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    88
  also have "\<dots> = inv a \<otimes> \<one> \<otimes> a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    89
  also have "\<dots> = inv a \<otimes> ((a \<otimes> b) \<otimes> inv (a \<otimes> b)) \<otimes> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    90
       by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    91
  also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    92
    by (simp add: m_assoc del: Units_l_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    93
  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    94
  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    95
  finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    96
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    97
  from c li ri
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    98
      show "b \<in> Units G" by (simp add: Units_def, fast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
    99
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   100
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   101
lemma (in monoid) prod_unit_r:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   102
  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and bunit[simp]: "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   103
    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   104
  shows "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   105
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   106
  have c: "b \<otimes> inv (a \<otimes> b) \<in> carrier G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   107
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   108
  have "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = (a \<otimes> b) \<otimes> inv (a \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   109
    by (simp add: m_assoc del: Units_r_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   110
  also have "\<dots> = \<one>" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   111
  finally have li: "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = \<one>" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   112
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   113
  have "\<one> = b \<otimes> inv b" by (simp add: Units_r_inv[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   114
  also have "\<dots> = b \<otimes> \<one> \<otimes> inv b" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   115
  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b" 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   116
       by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   117
  also have "\<dots> = (b \<otimes> inv (a \<otimes> b) \<otimes> a) \<otimes> (b \<otimes> inv b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   118
    by (simp add: m_assoc del: Units_l_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   119
  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   120
  finally have ri: "(b \<otimes> inv (a \<otimes> b)) \<otimes> a = \<one> " by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   121
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   122
  from c li ri
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   123
      show "a \<in> Units G" by (simp add: Units_def, fast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   124
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   125
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   126
lemma (in comm_monoid) unit_factor:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   127
  assumes abunit: "a \<otimes> b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   128
    and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   129
  shows "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   130
using abunit[simplified Units_def]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   131
proof clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   132
  fix i
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   133
  assume [simp]: "i \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   134
    and li: "i \<otimes> (a \<otimes> b) = \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   135
    and ri: "a \<otimes> b \<otimes> i = \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   136
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   137
  have carr': "b \<otimes> i \<in> carrier G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   138
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   139
  have "(b \<otimes> i) \<otimes> a = (i \<otimes> b) \<otimes> a" by (simp add: m_comm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   140
  also have "\<dots> = i \<otimes> (b \<otimes> a)" by (simp add: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   141
  also have "\<dots> = i \<otimes> (a \<otimes> b)" by (simp add: m_comm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   142
  also note li
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   143
  finally have li': "(b \<otimes> i) \<otimes> a = \<one>" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   144
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   145
  have "a \<otimes> (b \<otimes> i) = a \<otimes> b \<otimes> i" by (simp add: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   146
  also note ri
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   147
  finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   148
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   149
  from carr' li' ri'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   150
      show "a \<in> Units G" by (simp add: Units_def, fast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   151
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   152
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   153
subsection {* Divisibility and association *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   154
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   155
subsubsection {* Function definitions *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   156
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   157
constdefs (structure G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   158
  factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   159
  "a divides b == \<exists>c\<in>carrier G. b = a \<otimes> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   160
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   161
constdefs (structure G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   162
  associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   163
  "a \<sim> b == a divides b \<and> b divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   164
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   165
abbreviation
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   166
  "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   167
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   168
constdefs (structure G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   169
  properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   170
  "properfactor G a b == a divides b \<and> \<not>(b divides a)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   171
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   172
constdefs (structure G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   173
  irreducible :: "[_, 'a] \<Rightarrow> bool"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   174
  "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   175
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   176
constdefs (structure G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   177
  prime :: "[_, 'a] \<Rightarrow> bool"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   178
  "prime G p == p \<notin> Units G \<and> 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   179
                (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides (a \<otimes> b) \<longrightarrow> p divides a \<or> p divides b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   180
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   181
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   182
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   183
subsubsection {* Divisibility *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   184
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   185
lemma dividesI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   186
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   187
  assumes carr: "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   188
    and p: "b = a \<otimes> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   189
  shows "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   190
unfolding factor_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   191
using assms by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   192
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   193
lemma dividesI' [intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   194
   fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   195
  assumes p: "b = a \<otimes> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   196
    and carr: "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   197
  shows "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   198
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   199
by (fast intro: dividesI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   200
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   201
lemma dividesD:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   202
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   203
  assumes "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   204
  shows "\<exists>c\<in>carrier G. b = a \<otimes> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   205
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   206
unfolding factor_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   207
by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   208
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   209
lemma dividesE [elim]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   210
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   211
  assumes d: "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   212
    and elim: "\<And>c. \<lbrakk>b = a \<otimes> c; c \<in> carrier G\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   213
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   214
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   215
  from dividesD[OF d]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   216
      obtain c
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   217
      where "c\<in>carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   218
      and "b = a \<otimes> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   219
      by auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   220
  thus "P" by (elim elim)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   221
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   222
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   223
lemma (in monoid) divides_refl[simp, intro!]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   224
  assumes carr: "a \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   225
  shows "a divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   226
apply (intro dividesI[of "\<one>"])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   227
apply (simp, simp add: carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   228
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   229
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   230
lemma (in monoid) divides_trans [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   231
  assumes dvds: "a divides b"  "b divides c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   232
    and acarr: "a \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   233
  shows "a divides c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   234
using dvds[THEN dividesD]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   235
by (blast intro: dividesI m_assoc acarr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   236
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   237
lemma (in monoid) divides_mult_lI [intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   238
  assumes ab: "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   239
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   240
  shows "(c \<otimes> a) divides (c \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   241
using ab
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   242
apply (elim dividesE, simp add: m_assoc[symmetric] carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   243
apply (fast intro: dividesI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   244
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   245
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   246
lemma (in monoid_cancel) divides_mult_l [simp]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   247
  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   248
  shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   249
apply safe
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   250
 apply (elim dividesE, intro dividesI, assumption)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   251
 apply (rule l_cancel[of c])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   252
    apply (simp add: m_assoc carr)+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   253
apply (fast intro: divides_mult_lI carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   254
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   255
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   256
lemma (in comm_monoid) divides_mult_rI [intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   257
  assumes ab: "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   258
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   259
  shows "(a \<otimes> c) divides (b \<otimes> c)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   260
using carr ab
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   261
apply (simp add: m_comm[of a c] m_comm[of b c])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   262
apply (rule divides_mult_lI, assumption+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   263
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   264
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   265
lemma (in comm_monoid_cancel) divides_mult_r [simp]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   266
  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   267
  shows "(a \<otimes> c) divides (b \<otimes> c) = a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   268
using carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   269
by (simp add: m_comm[of a c] m_comm[of b c])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   270
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   271
lemma (in monoid) divides_prod_r:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   272
  assumes ab: "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   273
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   274
  shows "a divides (b \<otimes> c)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   275
using ab carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   276
by (fast intro: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   277
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   278
lemma (in comm_monoid) divides_prod_l:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   279
  assumes carr[intro]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   280
    and ab: "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   281
  shows "a divides (c \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   282
using ab carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   283
apply (simp add: m_comm[of c b])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   284
apply (fast intro: divides_prod_r)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   285
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   286
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   287
lemma (in monoid) unit_divides:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   288
  assumes uunit: "u \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   289
      and acarr: "a \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   290
  shows "u divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   291
proof (intro dividesI[of "(inv u) \<otimes> a"], fast intro: uunit acarr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   292
  from uunit acarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   293
      have xcarr: "inv u \<otimes> a \<in> carrier G" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   294
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   295
  from uunit acarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   296
       have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a" by (fast intro: m_assoc[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   297
  also have "\<dots> = \<one> \<otimes> a" by (simp add: Units_r_inv[OF uunit])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   298
  also from acarr 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   299
       have "\<dots> = a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   300
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   301
       show "a = u \<otimes> (inv u \<otimes> a)" ..
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   302
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   303
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   304
lemma (in comm_monoid) divides_unit:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   305
  assumes udvd: "a divides u"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   306
      and  carr: "a \<in> carrier G"  "u \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   307
  shows "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   308
using udvd carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   309
by (blast intro: unit_factor)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   310
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   311
lemma (in comm_monoid) Unit_eq_dividesone:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   312
  assumes ucarr: "u \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   313
  shows "u \<in> Units G = u divides \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   314
using ucarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   315
by (fast dest: divides_unit intro: unit_divides)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   316
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   317
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   318
subsubsection {* Association *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   319
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   320
lemma associatedI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   321
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   322
  assumes "a divides b"  "b divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   323
  shows "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   324
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   325
by (simp add: associated_def)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   326
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   327
lemma (in monoid) associatedI2:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   328
  assumes uunit[simp]: "u \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   329
    and a: "a = b \<otimes> u"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   330
    and bcarr[simp]: "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   331
  shows "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   332
using uunit bcarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   333
unfolding a
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   334
apply (intro associatedI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   335
 apply (rule dividesI[of "inv u"], simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   336
 apply (simp add: m_assoc Units_closed Units_r_inv)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   337
apply fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   338
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   339
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   340
lemma (in monoid) associatedI2':
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   341
  assumes a: "a = b \<otimes> u"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   342
    and uunit: "u \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   343
    and bcarr: "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   344
  shows "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   345
using assms by (intro associatedI2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   346
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   347
lemma associatedD:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   348
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   349
  assumes "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   350
  shows "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   351
using assms by (simp add: associated_def)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   352
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   353
lemma (in monoid_cancel) associatedD2:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   354
  assumes assoc: "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   355
    and carr: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   356
  shows "\<exists>u\<in>Units G. a = b \<otimes> u"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   357
using assoc
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   358
unfolding associated_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   359
proof clarify
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   360
  assume "b divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   361
  hence "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   362
  from this obtain u
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   363
      where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   364
      by auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   365
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   366
  assume "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   367
  hence "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   368
  from this obtain u'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   369
      where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   370
      by auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   371
  note carr = carr ucarr u'carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   372
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   373
  from carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   374
       have "a \<otimes> \<one> = a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   375
  also have "\<dots> = b \<otimes> u" by (simp add: a)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   376
  also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   377
  also from carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   378
       have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   379
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   380
       have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   381
  with carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   382
      have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   383
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   384
  from carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   385
       have "b \<otimes> \<one> = b" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   386
  also have "\<dots> = a \<otimes> u'" by (simp add: b)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   387
  also have "\<dots> = b \<otimes> u \<otimes> u'" by (simp add: a)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   388
  also from carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   389
       have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   390
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   391
       have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   392
  with carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   393
      have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   394
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   395
  from u'carr u1[symmetric] u2[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   396
      have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   397
  hence "u \<in> Units G" by (simp add: Units_def ucarr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   398
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   399
  from ucarr this a
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   400
      show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   401
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   402
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   403
lemma associatedE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   404
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   405
  assumes assoc: "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   406
    and e: "\<lbrakk>a divides b; b divides a\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   407
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   408
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   409
  from assoc
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   410
      have "a divides b"  "b divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   411
      by (simp add: associated_def)+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   412
  thus "P" by (elim e)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   413
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   414
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   415
lemma (in monoid_cancel) associatedE2:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   416
  assumes assoc: "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   417
    and e: "\<And>u. \<lbrakk>a = b \<otimes> u; u \<in> Units G\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   418
    and carr: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   419
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   420
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   421
  from assoc and carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   422
      have "\<exists>u\<in>Units G. a = b \<otimes> u" by (rule associatedD2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   423
  from this obtain u
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   424
      where "u \<in> Units G"  "a = b \<otimes> u"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   425
      by auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   426
  thus "P" by (elim e)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   427
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   428
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   429
lemma (in monoid) associated_refl [simp, intro!]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   430
  assumes "a \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   431
  shows "a \<sim> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   432
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   433
by (fast intro: associatedI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   434
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   435
lemma (in monoid) associated_sym [sym]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   436
  assumes "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   437
    and "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   438
  shows "b \<sim> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   439
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   440
by (iprover intro: associatedI elim: associatedE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   441
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   442
lemma (in monoid) associated_trans [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   443
  assumes "a \<sim> b"  "b \<sim> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   444
    and "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   445
  shows "a \<sim> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   446
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   447
by (iprover intro: associatedI divides_trans elim: associatedE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   448
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   449
lemma (in monoid) division_equiv [intro, simp]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   450
  "equivalence (division_rel G)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   451
  apply unfold_locales
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   452
  apply simp_all
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   453
  apply (rule associated_sym, assumption+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   454
  apply (iprover intro: associated_trans)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   455
  done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   456
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   457
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   458
subsubsection {* Division and associativity *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   459
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   460
lemma divides_antisym:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   461
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   462
  assumes "a divides b"  "b divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   463
    and "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   464
  shows "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   465
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   466
by (fast intro: associatedI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   467
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   468
lemma (in monoid) divides_cong_l [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   469
  assumes xx': "x \<sim> x'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   470
    and xdvdy: "x' divides y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   471
    and carr [simp]: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   472
  shows "x divides y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   473
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   474
  from xx'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   475
       have "x divides x'" by (simp add: associatedD)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   476
  also note xdvdy
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   477
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   478
       show "x divides y" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   479
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   480
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   481
lemma (in monoid) divides_cong_r [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   482
  assumes xdvdy: "x divides y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   483
    and yy': "y \<sim> y'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   484
    and carr[simp]: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   485
  shows "x divides y'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   486
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   487
  note xdvdy
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   488
  also from yy'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   489
       have "y divides y'" by (simp add: associatedD)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   490
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   491
       show "x divides y'" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   492
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   493
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   494
lemma (in monoid) division_weak_partial_order [simp, intro!]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   495
  "weak_partial_order (division_rel G)"
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   496
  apply unfold_locales
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   497
  apply simp_all
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   498
  apply (simp add: associated_sym)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   499
  apply (blast intro: associated_trans)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   500
  apply (simp add: divides_antisym)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   501
  apply (blast intro: divides_trans)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   502
  apply (blast intro: divides_cong_l divides_cong_r associated_sym)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   503
  done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   504
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   505
    
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   506
subsubsection {* Multiplication and associativity *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   507
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   508
lemma (in monoid_cancel) mult_cong_r:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   509
  assumes "b \<sim> b'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   510
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   511
  shows "a \<otimes> b \<sim> a \<otimes> b'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   512
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   513
apply (elim associatedE2, intro associatedI2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   514
apply (auto intro: m_assoc[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   515
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   516
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   517
lemma (in comm_monoid_cancel) mult_cong_l:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   518
  assumes "a \<sim> a'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   519
    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   520
  shows "a \<otimes> b \<sim> a' \<otimes> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   521
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   522
apply (elim associatedE2, intro associatedI2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   523
    apply assumption
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   524
   apply (simp add: m_assoc Units_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   525
   apply (simp add: m_comm Units_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   526
  apply simp+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   527
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   528
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   529
lemma (in monoid_cancel) assoc_l_cancel:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   530
  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   531
    and "a \<otimes> b \<sim> a \<otimes> b'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   532
  shows "b \<sim> b'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   533
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   534
apply (elim associatedE2, intro associatedI2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   535
    apply assumption
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   536
   apply (rule l_cancel[of a])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   537
      apply (simp add: m_assoc Units_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   538
     apply fast+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   539
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   540
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   541
lemma (in comm_monoid_cancel) assoc_r_cancel:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   542
  assumes "a \<otimes> b \<sim> a' \<otimes> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   543
    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   544
  shows "a \<sim> a'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   545
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   546
apply (elim associatedE2, intro associatedI2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   547
    apply assumption
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   548
   apply (rule r_cancel[of a b])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   549
      apply (simp add: m_assoc Units_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   550
      apply (simp add: m_comm Units_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   551
     apply fast+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   552
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   553
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   554
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   555
subsubsection {* Units *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   556
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   557
lemma (in monoid_cancel) assoc_unit_l [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   558
  assumes asc: "a \<sim> b" and bunit: "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   559
    and carr: "a \<in> carrier G" 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   560
  shows "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   561
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   562
by (fast elim: associatedE2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   563
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   564
lemma (in monoid_cancel) assoc_unit_r [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   565
  assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   566
    and bcarr: "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   567
  shows "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   568
using aunit bcarr associated_sym[OF asc]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   569
by (blast intro: assoc_unit_l)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   570
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   571
lemma (in comm_monoid) Units_cong:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   572
  assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   573
    and bcarr: "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   574
  shows "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   575
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   576
by (blast intro: divides_unit elim: associatedE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   577
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   578
lemma (in monoid) Units_assoc:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   579
  assumes units: "a \<in> Units G"  "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   580
  shows "a \<sim> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   581
using units
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   582
by (fast intro: associatedI unit_divides)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   583
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   584
lemma (in monoid) Units_are_ones:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   585
  "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   586
apply (simp add: set_eq_def elem_def, rule, simp_all)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   587
proof clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   588
  fix a
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   589
  assume aunit: "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   590
  show "a \<sim> \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   591
  apply (rule associatedI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   592
   apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   593
  apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   594
  done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   595
next
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   596
  have "\<one> \<in> Units G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   597
  moreover have "\<one> \<sim> \<one>" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   598
  ultimately show "\<exists>a \<in> Units G. \<one> \<sim> a" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   599
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   600
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   601
lemma (in comm_monoid) Units_Lower:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   602
  "Units G = Lower (division_rel G) (carrier G)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   603
apply (simp add: Units_def Lower_def)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   604
apply (rule, rule)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   605
 apply clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   606
  apply (rule unit_divides)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   607
   apply (unfold Units_def, fast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   608
  apply assumption
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   609
apply clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   610
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   611
  fix x
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   612
  assume xcarr: "x \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   613
  assume r[rule_format]: "\<forall>y. y \<in> carrier G \<longrightarrow> x divides y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   614
  have "\<one> \<in> carrier G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   615
  hence "x divides \<one>" by (rule r)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   616
  hence "\<exists>x'\<in>carrier G. \<one> = x \<otimes> x'" by (rule dividesE, fast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   617
  from this obtain x'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   618
      where x'carr: "x' \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   619
      and xx': "\<one> = x \<otimes> x'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   620
      by auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   621
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   622
  note xx'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   623
  also with xcarr x'carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   624
       have "\<dots> = x' \<otimes> x" by (simp add: m_comm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   625
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   626
       have "\<one> = x' \<otimes> x" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   627
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   628
  from x'carr xx'[symmetric] this[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   629
      show "\<exists>y\<in>carrier G. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   630
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   631
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   632
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   633
subsubsection {* Proper factors *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   634
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   635
lemma properfactorI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   636
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   637
  assumes "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   638
    and "\<not>(b divides a)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   639
  shows "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   640
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   641
unfolding properfactor_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   642
by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   643
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   644
lemma properfactorI2:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   645
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   646
  assumes advdb: "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   647
    and neq: "\<not>(a \<sim> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   648
  shows "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   649
apply (rule properfactorI, rule advdb)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   650
proof (rule ccontr, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   651
  assume "b divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   652
  with advdb have "a \<sim> b" by (rule associatedI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   653
  with neq show "False" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   654
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   655
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   656
lemma (in comm_monoid_cancel) properfactorI3:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   657
  assumes p: "p = a \<otimes> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   658
    and nunit: "b \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   659
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "p \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   660
  shows "properfactor G a p"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   661
unfolding p
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   662
using carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   663
apply (intro properfactorI, fast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   664
proof (clarsimp, elim dividesE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   665
  fix c
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   666
  assume ccarr: "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   667
  note [simp] = carr ccarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   668
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   669
  have "a \<otimes> \<one> = a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   670
  also assume "a = a \<otimes> b \<otimes> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   671
  also have "\<dots> = a \<otimes> (b \<otimes> c)" by (simp add: m_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   672
  finally have "a \<otimes> \<one> = a \<otimes> (b \<otimes> c)" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   673
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   674
  hence rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   675
  also have "\<dots> = c \<otimes> b" by (simp add: m_comm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   676
  finally have linv: "\<one> = c \<otimes> b" .
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   677
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   678
  from ccarr linv[symmetric] rinv[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   679
  have "b \<in> Units G" unfolding Units_def by fastsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   680
  with nunit
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   681
      show "False" ..
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   682
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   683
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   684
lemma properfactorE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   685
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   686
  assumes pf: "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   687
    and r: "\<lbrakk>a divides b; \<not>(b divides a)\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   688
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   689
using pf
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   690
unfolding properfactor_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   691
by (fast intro: r)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   692
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   693
lemma properfactorE2:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   694
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   695
  assumes pf: "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   696
    and elim: "\<lbrakk>a divides b; \<not>(a \<sim> b)\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   697
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   698
using pf
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   699
unfolding properfactor_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   700
by (fast elim: elim associatedE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   702
lemma (in monoid) properfactor_unitE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   703
  assumes uunit: "u \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   704
    and pf: "properfactor G a u"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   705
    and acarr: "a \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   706
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   707
using pf unit_divides[OF uunit acarr]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   708
by (fast elim: properfactorE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   709
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   710
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   711
lemma (in monoid) properfactor_divides:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   712
  assumes pf: "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   713
  shows "a divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   714
using pf
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   715
by (elim properfactorE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   716
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   717
lemma (in monoid) properfactor_trans1 [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   718
  assumes dvds: "a divides b"  "properfactor G b c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   719
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   720
  shows "properfactor G a c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   721
using dvds carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   722
apply (elim properfactorE, intro properfactorI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   723
 apply (iprover intro: divides_trans)+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   724
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   725
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   726
lemma (in monoid) properfactor_trans2 [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   727
  assumes dvds: "properfactor G a b"  "b divides c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   728
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   729
  shows "properfactor G a c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   730
using dvds carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   731
apply (elim properfactorE, intro properfactorI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   732
 apply (iprover intro: divides_trans)+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   733
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   734
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   735
lemma properfactor_lless:
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   736
  fixes G (structure)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   737
  shows "properfactor G = lless (division_rel G)"
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   738
apply (rule ext) apply (rule ext) apply rule
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   739
 apply (fastsimp elim: properfactorE2 intro: weak_llessI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   740
apply (fastsimp elim: weak_llessE intro: properfactorI2)
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   741
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   742
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   743
lemma (in monoid) properfactor_cong_l [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   744
  assumes x'x: "x' \<sim> x"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   745
    and pf: "properfactor G x y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   746
    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   747
  shows "properfactor G x' y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   748
using pf
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   749
unfolding properfactor_lless
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   750
proof -
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   751
  interpret weak_partial_order ["division_rel G"] ..
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   752
  from x'x
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   753
       have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   754
  also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   755
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   756
       show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   757
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   758
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   759
lemma (in monoid) properfactor_cong_r [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   760
  assumes pf: "properfactor G x y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   761
    and yy': "y \<sim> y'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   762
    and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   763
  shows "properfactor G x y'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   764
using pf
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   765
unfolding properfactor_lless
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   766
proof -
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27701
diff changeset
   767
  interpret weak_partial_order ["division_rel G"] ..
27701
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   768
  assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   769
  also from yy'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   770
       have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   771
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   772
       show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   773
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   774
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   775
lemma (in monoid_cancel) properfactor_mult_lI [intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   776
  assumes ab: "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   777
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   778
  shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   779
using ab carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   780
by (fastsimp elim: properfactorE intro: properfactorI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   781
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   782
lemma (in monoid_cancel) properfactor_mult_l [simp]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   783
  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   784
  shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   785
using carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   786
by (fastsimp elim: properfactorE intro: properfactorI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   787
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   788
lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   789
  assumes ab: "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   790
    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   791
  shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   792
using ab carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   793
by (fastsimp elim: properfactorE intro: properfactorI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   794
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   795
lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   796
  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   797
  shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   798
using carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   799
by (fastsimp elim: properfactorE intro: properfactorI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   800
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   801
lemma (in monoid) properfactor_prod_r:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   802
  assumes ab: "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   803
    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   804
  shows "properfactor G a (b \<otimes> c)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   805
by (intro properfactor_trans2[OF ab] divides_prod_r, simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   806
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   807
lemma (in comm_monoid) properfactor_prod_l:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   808
  assumes ab: "properfactor G a b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   809
    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   810
  shows "properfactor G a (c \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   811
by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   812
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   813
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   814
subsection {* Irreducible elements and primes *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   815
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   816
subsubsection {* Irreducible elements *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   817
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   818
lemma irreducibleI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   819
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   820
  assumes "a \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   821
    and "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b a\<rbrakk> \<Longrightarrow> b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   822
  shows "irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   823
using assms 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   824
unfolding irreducible_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   825
by blast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   826
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   827
lemma irreducibleE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   828
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   829
  assumes irr: "irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   830
     and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   831
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   832
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   833
unfolding irreducible_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   834
by blast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   835
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   836
lemma irreducibleD:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   837
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   838
  assumes irr: "irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   839
     and pf: "properfactor G b a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   840
     and bcarr: "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   841
  shows "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   842
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   843
by (fast elim: irreducibleE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   844
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   845
lemma (in monoid_cancel) irreducible_cong [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   846
  assumes irred: "irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   847
    and aa': "a \<sim> a'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   848
    and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   849
  shows "irreducible G a'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   850
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   851
apply (elim irreducibleE, intro irreducibleI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   852
apply simp_all
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   853
proof clarify
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   854
  assume "a' \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   855
  also note aa'[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   856
  finally have aunit: "a \<in> Units G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   857
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   858
  assume "a \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   859
  with aunit
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   860
      show "False" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   861
next
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   862
  fix b
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   863
  assume r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   864
    and bcarr[simp]: "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   865
  assume "properfactor G b a'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   866
  also note aa'[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   867
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   868
       have "properfactor G b a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   869
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   870
  with bcarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   871
     show "b \<in> Units G" by (fast intro: r)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   872
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   873
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   874
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   875
lemma (in monoid) irreducible_prod_rI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   876
  assumes airr: "irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   877
    and bunit: "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   878
    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   879
  shows "irreducible G (a \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   880
using airr carr bunit
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   881
apply (elim irreducibleE, intro irreducibleI, clarify)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   882
 apply (subgoal_tac "a \<in> Units G", simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   883
 apply (intro prod_unit_r[of a b] carr bunit, assumption)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   884
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   885
  fix c
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   886
  assume [simp]: "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   887
    and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   888
  assume "properfactor G c (a \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   889
  also have "a \<otimes> b \<sim> a" by (intro associatedI2[OF bunit], simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   890
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   891
       have pfa: "properfactor G c a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   892
  show "c \<in> Units G" by (rule r, simp add: pfa)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   893
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   894
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   895
lemma (in comm_monoid) irreducible_prod_lI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   896
  assumes birr: "irreducible G b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   897
    and aunit: "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   898
    and carr [simp]: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   899
  shows "irreducible G (a \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   900
apply (subst m_comm, simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   901
apply (intro irreducible_prod_rI assms)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   902
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   903
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   904
lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   905
  assumes irr: "irreducible G (a \<otimes> b)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   906
    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   907
    and e1: "\<lbrakk>irreducible G a; b \<in> Units G\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   908
    and e2: "\<lbrakk>a \<in> Units G; irreducible G b\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   909
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   910
using irr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   911
proof (elim irreducibleE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   912
  assume abnunit: "a \<otimes> b \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   913
    and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   914
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   915
  show "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   916
  proof (cases "a \<in> Units G")
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   917
    assume aunit: "a \<in>  Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   918
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   919
    have "irreducible G b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   920
    apply (rule irreducibleI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   921
    proof (rule ccontr, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   922
      assume "b \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   923
      with aunit have "(a \<otimes> b) \<in> Units G" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   924
      with abnunit show "False" ..
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   925
    next
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   926
      fix c
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   927
      assume ccarr: "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   928
        and "properfactor G c b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   929
      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   930
      from ccarr this show "c \<in> Units G" by (fast intro: isunit)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   931
    qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   932
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   933
    from aunit this show "P" by (rule e2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   934
  next
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   935
    assume anunit: "a \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   936
    with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   937
    hence bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   938
    hence bunit: "b \<in> Units G" by (intro isunit, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   939
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   940
    have "irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   941
    apply (rule irreducibleI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   942
    proof (rule ccontr, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   943
      assume "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   944
      with bunit have "(a \<otimes> b) \<in> Units G" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   945
      with abnunit show "False" ..
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   946
    next
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   947
      fix c
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   948
      assume ccarr: "c \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   949
        and "properfactor G c a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   950
      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_r[of c a b])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   951
      from ccarr this show "c \<in> Units G" by (fast intro: isunit)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   952
    qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   953
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   954
    from this bunit show "P" by (rule e1)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   955
  qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   956
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   957
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   958
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   959
subsubsection {* Prime elements *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   960
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   961
lemma primeI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   962
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   963
  assumes "p \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   964
    and "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G; p divides (a \<otimes> b)\<rbrakk> \<Longrightarrow> p divides a \<or> p divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   965
  shows "prime G p"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   966
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   967
unfolding prime_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   968
by blast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   969
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   970
lemma primeE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   971
  fixes G (structure)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   972
  assumes pprime: "prime G p"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   973
    and e: "\<lbrakk>p \<notin> Units G; \<forall>a\<in>carrier G. \<forall>b\<in>carrier G.
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   974
                          p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   975
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   976
using pprime
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   977
unfolding prime_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   978
by (blast dest: e)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   979
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   980
lemma (in comm_monoid_cancel) prime_divides:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   981
  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   982
    and pprime: "prime G p"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   983
    and pdvd: "p divides a \<otimes> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   984
  shows "p divides a \<or> p divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   985
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   986
by (blast elim: primeE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   987
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   988
lemma (in monoid_cancel) prime_cong [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   989
  assumes pprime: "prime G p"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   990
    and pp': "p \<sim> p'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   991
    and carr[simp]: "p \<in> carrier G"  "p' \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   992
  shows "prime G p'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   993
using pprime
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   994
apply (elim primeE, intro primeI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   995
proof clarify
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   996
  assume pnunit: "p \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   997
  assume "p' \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   998
  also note pp'[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
   999
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1000
       have "p \<in> Units G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1001
  with pnunit
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1002
       show False ..
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1003
next
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1004
  fix a b
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1005
  assume r[rule_format]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1006
         "\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1007
  assume p'dvd: "p' divides a \<otimes> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1008
    and carr'[simp]: "a \<in> carrier G"  "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1009
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1010
  note pp'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1011
  also note p'dvd
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1012
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1013
       have "p divides a \<otimes> b" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1014
  hence "p divides a \<or> p divides b" by (intro r, simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1015
  moreover {
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1016
    note pp'[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1017
    also assume "p divides a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1018
    finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1019
         have "p' divides a" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1020
    hence "p' divides a \<or> p' divides b" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1021
  }
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1022
  moreover {
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1023
    note pp'[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1024
    also assume "p divides b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1025
    finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1026
         have "p' divides b" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1027
    hence "p' divides a \<or> p' divides b" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1028
  }
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1029
  ultimately
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1030
    show "p' divides a \<or> p' divides b" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1031
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1032
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1033
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1034
subsection {* Factorization and factorial monoids *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1035
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1036
(*
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1037
hide (open) const mult     (* Multiset.mult, conflicting with monoid.mult *)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1038
*)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1039
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1040
subsubsection {* Function definitions *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1041
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1042
constdefs (structure G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1043
  factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1044
  "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> = a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1045
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1046
  wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1047
  "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> \<sim> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1048
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1049
abbreviation
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1050
  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) where
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1051
  "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1052
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1053
constdefs (structure G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1054
  essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1055
  "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>] fs2)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1056
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1057
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1058
locale factorial_monoid = comm_monoid_cancel +
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1059
  assumes factors_exist: 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1060
          "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1061
      and factors_unique: 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1062
          "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G; 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1063
            set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1064
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1065
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1066
subsubsection {* Comparing lists of elements *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1067
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1068
text {* Association on lists *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1069
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1070
lemma (in monoid) listassoc_refl [simp, intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1071
  assumes "set as \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1072
  shows "as [\<sim>] as"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1073
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1074
by (induct as) simp+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1075
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1076
lemma (in monoid) listassoc_sym [sym]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1077
  assumes "as [\<sim>] bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1078
    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1079
  shows "bs [\<sim>] as"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1080
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1081
proof (induct as arbitrary: bs, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1082
  case Cons
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1083
  thus ?case
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1084
    apply (induct bs, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1085
    apply clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1086
    apply (iprover intro: associated_sym)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1087
  done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1088
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1089
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1090
lemma (in monoid) listassoc_trans [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1091
  assumes "as [\<sim>] bs" and "bs [\<sim>] cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1092
    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" and "set cs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1093
  shows "as [\<sim>] cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1094
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1095
apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1096
apply (rule associated_trans)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1097
    apply (subgoal_tac "as ! i \<sim> bs ! i", assumption)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1098
    apply (simp, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1099
  apply blast+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1100
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1101
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1102
lemma (in monoid_cancel) irrlist_listassoc_cong:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1103
  assumes "\<forall>a\<in>set as. irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1104
    and "as [\<sim>] bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1105
    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1106
  shows "\<forall>a\<in>set bs. irreducible G a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1107
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1108
apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1109
apply (blast intro: irreducible_cong)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1110
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1111
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1112
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1113
text {* Permutations *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1114
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1115
lemma perm_map [intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1116
  assumes p: "a <~~> b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1117
  shows "map f a <~~> map f b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1118
using p
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1119
by induct auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1120
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1121
lemma perm_map_switch:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1122
  assumes m: "map f a = map f b" and p: "b <~~> c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1123
  shows "\<exists>d. a <~~> d \<and> map f d = map f c"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1124
using p m
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1125
by (induct arbitrary: a) (simp, force, force, blast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1126
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1127
lemma (in monoid) perm_assoc_switch:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1128
   assumes a:"as [\<sim>] bs" and p: "bs <~~> cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1129
   shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1130
using p a
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1131
apply (induct bs cs arbitrary: as, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1132
  apply (clarsimp simp add: list_all2_Cons2, blast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1133
 apply (clarsimp simp add: list_all2_Cons2)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1134
 apply blast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1135
apply blast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1136
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1137
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1138
lemma (in monoid) perm_assoc_switch_r:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1139
   assumes p: "as <~~> bs" and a:"bs [\<sim>] cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1140
   shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1141
using p a
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1142
apply (induct as bs arbitrary: cs, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1143
  apply (clarsimp simp add: list_all2_Cons1, blast)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1144
 apply (clarsimp simp add: list_all2_Cons1)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1145
 apply blast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1146
apply blast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1147
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1148
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1149
declare perm_sym [sym]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1150
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1151
lemma perm_setP:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1152
  assumes perm: "as <~~> bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1153
    and as: "P (set as)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1154
  shows "P (set bs)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1155
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1156
  from perm
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1157
      have "multiset_of as = multiset_of bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1158
      by (simp add: multiset_of_eq_perm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1159
  hence "set as = set bs" by (rule multiset_of_eq_setD)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1160
  with as
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1161
      show "P (set bs)" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1162
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1163
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1164
lemmas (in monoid) perm_closed =
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1165
    perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1166
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1167
lemmas (in monoid) irrlist_perm_cong =
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1168
    perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1169
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1170
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1171
text {* Essentially equal factorizations *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1172
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1173
lemma (in monoid) essentially_equalI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1174
  assumes ex: "fs1 <~~> fs1'"  "fs1' [\<sim>] fs2"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1175
  shows "essentially_equal G fs1 fs2"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1176
using ex
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1177
unfolding essentially_equal_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1178
by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1179
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1180
lemma (in monoid) essentially_equalE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1181
  assumes ee: "essentially_equal G fs1 fs2"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1182
    and e: "\<And>fs1'. \<lbrakk>fs1 <~~> fs1'; fs1' [\<sim>] fs2\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1183
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1184
using ee
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1185
unfolding essentially_equal_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1186
by (fast intro: e)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1187
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1188
lemma (in monoid) ee_refl [simp,intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1189
  assumes carr: "set as \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1190
  shows "essentially_equal G as as"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1191
using carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1192
by (fast intro: essentially_equalI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1193
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1194
lemma (in monoid) ee_sym [sym]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1195
  assumes ee: "essentially_equal G as bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1196
    and carr: "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1197
  shows "essentially_equal G bs as"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1198
using ee
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1199
proof (elim essentially_equalE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1200
  fix fs
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1201
  assume "as <~~> fs"  "fs [\<sim>] bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1202
  hence "\<exists>fs'. as [\<sim>] fs' \<and> fs' <~~> bs" by (rule perm_assoc_switch_r)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1203
  from this obtain fs'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1204
      where a: "as [\<sim>] fs'" and p: "fs' <~~> bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1205
      by auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1206
  from p have "bs <~~> fs'" by (rule perm_sym)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1207
  with a[symmetric] carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1208
      show ?thesis
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1209
      by (iprover intro: essentially_equalI perm_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1210
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1211
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1212
lemma (in monoid) ee_trans [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1213
  assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1214
    and ascarr: "set as \<subseteq> carrier G" 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1215
    and bscarr: "set bs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1216
    and cscarr: "set cs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1217
  shows "essentially_equal G as cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1218
using ab bc
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1219
proof (elim essentially_equalE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1220
  fix abs bcs
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1221
  assume  "abs [\<sim>] bs" and pb: "bs <~~> bcs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1222
  hence "\<exists>bs'. abs <~~> bs' \<and> bs' [\<sim>] bcs" by (rule perm_assoc_switch)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1223
  from this obtain bs'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1224
      where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1225
      by auto
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1226
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1227
  assume "as <~~> abs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1228
  with p
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1229
      have pp: "as <~~> bs'" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1230
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1231
  from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1232
  from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1233
  note a
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1234
  also assume "bcs [\<sim>] cs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1235
  finally (listassoc_trans) have"bs' [\<sim>] cs" by (simp add: c1 c2 cscarr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1236
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1237
  with pp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1238
      show ?thesis
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1239
      by (rule essentially_equalI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1240
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1241
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1242
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1243
subsubsection {* Properties of lists of elements *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1244
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1245
text {* Multiplication of factors in a list *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1246
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1247
lemma (in monoid) multlist_closed [simp, intro]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1248
  assumes ascarr: "set fs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1249
  shows "foldr (op \<otimes>) fs \<one> \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1250
by (insert ascarr, induct fs, simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1251
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1252
lemma  (in comm_monoid) multlist_dividesI (*[intro]*):
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1253
  assumes "f \<in> set fs" and "f \<in> carrier G" and "set fs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1254
  shows "f divides (foldr (op \<otimes>) fs \<one>)"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1255
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1256
apply (induct fs)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1257
 apply simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1258
apply (case_tac "f = a", simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1259
 apply (fast intro: dividesI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1260
apply clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1261
apply (elim dividesE, intro dividesI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1262
 defer 1
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1263
 apply (simp add: m_comm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1264
 apply (simp add: m_assoc[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1265
 apply (simp add: m_comm)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1266
apply simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1267
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1268
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1269
lemma (in comm_monoid_cancel) multlist_listassoc_cong:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1270
  assumes "fs [\<sim>] fs'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1271
    and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1272
  shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1273
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1274
proof (induct fs arbitrary: fs', simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1275
  case (Cons a as fs')
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1276
  thus ?case
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1277
  apply (induct fs', simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1278
  proof clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1279
    fix b bs
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1280
    assume "a \<sim> b" 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1281
      and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1282
      and ascarr: "set as \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1283
    hence p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1284
        by (fast intro: mult_cong_l)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1285
    also
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1286
      assume "as [\<sim>] bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1287
         and bscarr: "set bs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1288
         and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1289
      hence "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1290
      with ascarr bscarr bcarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1291
          have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1292
          by (fast intro: mult_cong_r)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1293
   finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1294
       show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1295
       by (simp add: ascarr bscarr acarr bcarr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1296
  qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1297
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1298
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1299
lemma (in comm_monoid) multlist_perm_cong:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1300
  assumes prm: "as <~~> bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1301
    and ascarr: "set as \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1302
  shows "foldr (op \<otimes>) as \<one> = foldr (op \<otimes>) bs \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1303
using prm ascarr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1304
apply (induct, simp, clarsimp simp add: m_ac, clarsimp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1305
proof clarsimp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1306
  fix xs ys zs
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1307
  assume "xs <~~> ys"  "set xs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1308
  hence "set ys \<subseteq> carrier G" by (rule perm_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1309
  moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1310
  ultimately show "foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1311
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1312
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1313
lemma (in comm_monoid_cancel) multlist_ee_cong:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1314
  assumes "essentially_equal G fs fs'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1315
    and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1316
  shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1317
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1318
apply (elim essentially_equalE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1319
apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1320
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1321
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1322
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1323
subsubsection {* Factorization in irreducible elements *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1324
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1325
lemma wfactorsI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1326
  includes (struct G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1327
  assumes "\<forall>f\<in>set fs. irreducible G f"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1328
    and "foldr (op \<otimes>) fs \<one> \<sim> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1329
  shows "wfactors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1330
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1331
unfolding wfactors_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1332
by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1333
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1334
lemma wfactorsE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1335
  includes (struct G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1336
  assumes wf: "wfactors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1337
    and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1338
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1339
using wf
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1340
unfolding wfactors_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1341
by (fast dest: e)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1342
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1343
lemma (in monoid) factorsI:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1344
  includes (struct G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1345
  assumes "\<forall>f\<in>set fs. irreducible G f"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1346
    and "foldr (op \<otimes>) fs \<one> = a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1347
  shows "factors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1348
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1349
unfolding factors_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1350
by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1351
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1352
lemma factorsE:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1353
  includes (struct G)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1354
  assumes f: "factors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1355
    and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1356
  shows "P"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1357
using f
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1358
unfolding factors_def
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1359
by (simp add: e)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1360
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1361
lemma (in monoid) factors_wfactors:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1362
  assumes "factors G as a" and "set as \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1363
  shows "wfactors G as a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1364
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1365
by (blast elim: factorsE intro: wfactorsI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1366
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1367
lemma (in monoid) wfactors_factors:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1368
  assumes "wfactors G as a" and "set as \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1369
  shows "\<exists>a'. factors G as a' \<and> a' \<sim> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1370
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1371
by (blast elim: wfactorsE intro: factorsI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1372
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1373
lemma (in monoid) factors_closed [dest]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1374
  assumes "factors G fs a" and "set fs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1375
  shows "a \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1376
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1377
by (elim factorsE, clarsimp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1378
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1379
lemma (in monoid) nunit_factors:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1380
  assumes anunit: "a \<notin> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1381
    and fs: "factors G as a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1382
  shows "length as > 0"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1383
apply (insert fs, elim factorsE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1384
proof (cases "length as = 0")
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1385
  assume "length as = 0"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1386
  hence fold: "foldr op \<otimes> as \<one> = \<one>" by force
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1387
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1388
  assume "foldr op \<otimes> as \<one> = a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1389
  with fold
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1390
       have "a = \<one>" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1391
  then have "a \<in> Units G" by fast
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1392
  with anunit
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1393
       have "False" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1394
  thus ?thesis ..
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1395
qed simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1396
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1397
lemma (in monoid) unit_wfactors [simp]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1398
  assumes aunit: "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1399
  shows "wfactors G [] a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1400
using aunit
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1401
by (intro wfactorsI) (simp, simp add: Units_assoc)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1402
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1403
lemma (in comm_monoid_cancel) unit_wfactors_empty:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1404
  assumes aunit: "a \<in> Units G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1405
    and wf: "wfactors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1406
    and carr[simp]: "set fs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1407
  shows "fs = []"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1408
proof (rule ccontr, cases fs, simp)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1409
  fix f fs'
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1410
  assume fs: "fs = f # fs'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1411
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1412
  from carr
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1413
      have fcarr[simp]: "f \<in> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1414
      and carr'[simp]: "set fs' \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1415
      by (simp add: fs)+
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1416
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1417
  from fs wf
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1418
      have "irreducible G f" by (simp add: wfactors_def)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1419
  hence fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1420
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1421
  from fs wf
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1422
      have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1423
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1424
  note aunit
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1425
  also from fs wf
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1426
       have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1427
       have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>" 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1428
       by (simp add: Units_closed[OF aunit] a[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1429
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1430
       have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1431
  hence "f \<in> Units G" by (intro unit_factor[of f], simp+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1432
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1433
  with fnunit show "False" by simp
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1434
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1435
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1436
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1437
text {* Comparing wfactors *}
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1438
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1439
lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1440
  assumes fact: "wfactors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1441
    and asc: "fs [\<sim>] fs'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1442
    and carr: "a \<in> carrier G"  "set fs \<subseteq> carrier G"  "set fs' \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1443
  shows "wfactors G fs' a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1444
using fact
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1445
apply (elim wfactorsE, intro wfactorsI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1446
proof -
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1447
  assume "\<forall>f\<in>set fs. irreducible G f"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1448
  also note asc
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1449
  finally (irrlist_listassoc_cong)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1450
       show "\<forall>f\<in>set fs'. irreducible G f" by (simp add: carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1451
next
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1452
  from asc[symmetric]
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1453
       have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" 
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1454
       by (simp add: multlist_listassoc_cong carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1455
  also assume "foldr op \<otimes> fs \<one> \<sim> a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1456
  finally
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1457
       show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1458
qed
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1459
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1460
lemma (in comm_monoid) wfactors_perm_cong_l:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1461
  assumes "wfactors G fs a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1462
    and "fs <~~> fs'"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1463
    and "set fs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1464
  shows "wfactors G fs' a"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1465
using assms
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1466
apply (elim wfactorsE, intro wfactorsI)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1467
 apply (rule irrlist_perm_cong, assumption+)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1468
apply (simp add: multlist_perm_cong[symmetric])
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1469
done
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1470
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1471
lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1472
  assumes ee: "essentially_equal G as bs"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1473
    and bfs: "wfactors G bs b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1474
    and carr: "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1475
  shows "wfactors G as b"
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1476
using ee
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1477
proof (elim essentially_equalE)
ed7a2e0fab59 New theory on divisibility.
ballarin
parents:
diff changeset
  1478
  fix fs