author ballarin Mon Mar 10 17:25:34 2003 +0100 (2003-03-10) changeset 13854 91c9ab25fece parent 13853 89131afa9f01 child 13855 644692eca537
First distributed version of Group and Ring theory.
 src/HOL/Algebra/CRing.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions src/HOL/Algebra/ringsimp.ML file | annotate | diff | revisions
1.1 --- a/src/HOL/Algebra/CRing.thy	Mon Mar 10 16:21:06 2003 +0100
1.2 +++ b/src/HOL/Algebra/CRing.thy	Mon Mar 10 17:25:34 2003 +0100
1.3 @@ -7,7 +7,8 @@
1.5  header {* The algebraic hierarchy of rings as axiomatic classes *}
1.7 -theory Ring = Group
1.8 +theory CRing = Group
1.9 +files ("ringsimp.ML"):
1.11  section {* The Algebraic Hierarchy of Rings *}
1.13 @@ -17,49 +18,18 @@
1.14    zero :: 'a ("\<zero>\<index>")
1.15    add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
1.16    a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
1.17 +  minus :: "['a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
1.19  locale cring = abelian_monoid R +
1.20    assumes a_abelian_group: "abelian_group (| carrier = carrier R,
1.21        mult = add R, one = zero R, m_inv = a_inv R |)"
1.22 +    and minus_def: "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
1.23      and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
1.24        ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
1.25      and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
1.26        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
1.28 -ML {*
1.29 -  thm "cring.l_distr"
1.30 -*}
1.31 -
1.32  (*
1.33 -locale cring = struct R +
1.34 -  assumes a_group: "abelian_group (| carrier = carrier R,
1.35 -      mult = add R, one = zero R, m_inv = a_inv R |)"
1.36 -    and m_monoid: "abelian_monoid (| carrier = carrier R - {zero R},
1.37 -      mult = mult R, one = one R |)"
1.38 -    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
1.39 -      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
1.40 -
1.41 -locale field = struct R +
1.42 -  assumes a_group: "abelian_group (| carrier = carrier R,
1.43 -      mult = add R, one = zero R, m_inv = a_inv R |)"
1.44 -    and m_group: "monoid (| carrier = carrier R - {zero R},
1.45 -      mult = mult R, one = one R |)"
1.46 -    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
1.47 -      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
1.48 -*)
1.49 -(*
1.50 -  a_assoc:      "(a + b) + c = a + (b + c)"
1.51 -  l_zero:       "0 + a = a"
1.52 -  l_neg:        "(-a) + a = 0"
1.53 -  a_comm:       "a + b = b + a"
1.54 -
1.55 -  m_assoc:      "(a * b) * c = a * (b * c)"
1.56 -  l_one:        "1 * a = a"
1.57 -
1.58 -  l_distr:      "(a + b) * c = a * c + b * c"
1.59 -
1.60 -  m_comm:       "a * b = b * a"
1.61 -
1.62    -- {* Definition of derived operations *}
1.64    minus_def:    "a - b = a + (-b)"
1.65 @@ -108,171 +78,154 @@
1.66       mult = add R, one = zero R, m_inv = a_inv R |)"
1.69 -lemma (in cring) a_assoc:
1.70 -  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
1.71 -  ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
1.72 -  using semigroup.m_assoc [OF a_semigroup]
1.73 -  by simp
1.74 +lemmas (in cring) a_closed [intro, simp] =
1.75 +  magma.m_closed [OF a_magma, simplified]
1.76 +
1.77 +lemmas (in cring) zero_closed [intro, simp] =
1.78 +  l_one.one_closed [OF a_l_one, simplified]
1.79 +
1.80 +lemmas (in cring) a_inv_closed [intro, simp] =
1.81 +  group.inv_closed [OF a_group, simplified]
1.82 +
1.83 +lemma (in cring) minus_closed [intro, simp]:
1.84 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
1.85 +  by (simp add: minus_def)
1.86 +
1.87 +lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified]
1.89 -lemma (in cring) l_zero:
1.90 -  "x \<in> carrier R ==> \<zero> \<oplus> x = x"
1.91 -  using l_one.l_one [OF a_l_one]
1.92 +lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified]
1.93 +
1.94 +lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified]
1.95 +
1.96 +lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified]
1.97 +
1.98 +lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified]
1.99 +
1.100 +lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup,
1.101 +  simplified]
1.103 +lemmas (in cring) a_lcomm =
1.104 +  abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified]
1.106 +lemma (in cring) r_zero [simp]:
1.107 +  "x \<in> carrier R ==> x \<oplus> \<zero> = x"
1.108 +  using group.r_one [OF a_group]
1.109    by simp
1.111 -lemma (in cring) l_neg:
1.112 -  "x \<in> carrier R ==> (\<ominus> x) \<oplus> x = \<zero>"
1.113 -  using group.l_inv [OF a_group]
1.114 +lemma (in cring) r_neg:
1.115 +  "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
1.116 +  using group.r_inv [OF a_group]
1.117 +  by simp
1.119 +lemmas (in cring) minus_zero [simp] = group.inv_one [OF a_group, simplified]
1.121 +lemma (in cring) minus_minus [simp]:
1.122 +  "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
1.123 +  using group.inv_inv [OF a_group, simplified]
1.124    by simp
1.126 -lemma (in cring) a_comm:
1.127 -  "[| x \<in> carrier R; y \<in> carrier R |]
1.128 -  ==> x \<oplus> y = y \<oplus> x"
1.129 -  using abelian_semigroup.m_comm [OF a_abelian_semigroup]
1.131 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
1.132 +  using abelian_group.inv_mult [OF a_abelian_group]
1.133    by simp
1.135 +lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
1.137 +subsection {* Normaliser for Commutative Rings *}
1.140 +lemma (in cring) r_neg2:
1.141 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
1.142 +proof -
1.143 +  assume G: "x \<in> carrier R" "y \<in> carrier R"
1.144 +  then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
1.145 +  with G show ?thesis by (simp add: a_ac)
1.146  qed
1.148 -  l_zero:       "0 + a = a"
1.149 -  l_neg:        "(-a) + a = 0"
1.150 -  a_comm:       "a + b = b + a"
1.152 -  m_assoc:      "(a * b) * c = a * (b * c)"
1.153 -  l_one:        "1 * a = a"
1.155 -  l_distr:      "(a + b) * c = a * c + b * c"
1.157 -  m_comm:       "a * b = b * a"
1.158 -text {* Normaliser for Commutative Rings *}
1.160 -use "order.ML"
1.162 -method_setup ring =
1.163 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
1.164 -  {* computes distributive normal form in rings *}
1.166 -subsection {* Rings and the summation operator *}
1.168 -(* Basic facts --- move to HOL!!! *)
1.170 -lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
1.171 -by simp
1.173 -lemma natsum_Suc [simp]:
1.174 -  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
1.177 -lemma natsum_Suc2:
1.178 -  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
1.179 -proof (induct n)
1.180 -  case 0 show ?case by simp
1.181 -next
1.182 -  case Suc thus ?case by (simp add: assoc)
1.183 +lemma (in cring) r_neg1:
1.184 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
1.185 +proof -
1.186 +  assume G: "x \<in> carrier R" "y \<in> carrier R"
1.187 +  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
1.188 +  with G show ?thesis by (simp add: a_ac)
1.189  qed
1.191 -lemma natsum_cong [cong]:
1.192 -  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
1.193 -        setsum f {..j} = setsum g {..k}"
1.194 -by (induct j) auto
1.196 -lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
1.197 -by (induct n) simp_all
1.200 -  "!!f::nat=>'a::plus_ac0.
1.201 -   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
1.202 -by (induct n) (simp_all add: plus_ac0)
1.204 -(* Facts specific to rings *)
1.206 -instance ring < plus_ac0
1.207 -proof
1.208 -  fix x y z
1.209 -  show "(x::'a::ring) + y = y + x" by (rule a_comm)
1.210 -  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
1.211 -  show "0 + (x::'a::ring) = x" by (rule l_zero)
1.212 +lemma (in cring) r_distr:
1.213 +  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
1.214 +  ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
1.215 +proof -
1.216 +  assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
1.217 +  then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
1.218 +  also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
1.219 +  also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
1.220 +  finally show ?thesis .
1.221  qed
1.223 -ML {*
1.224 -  local
1.225 -    val lhss =
1.226 -        [read_cterm (sign_of (the_context ()))
1.227 -                    ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
1.228 -	 read_cterm (sign_of (the_context ()))
1.229 -                    ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
1.230 -	 read_cterm (sign_of (the_context ()))
1.231 -                    ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
1.232 -	 read_cterm (sign_of (the_context ()))
1.233 -                    ("- ?t::'a::ring", TVar (("'z", 0), []))
1.234 -	];
1.235 -    fun proc sg _ t =
1.236 -      let val rew = Tactic.prove sg [] []
1.237 -            (HOLogic.mk_Trueprop
1.238 -              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
1.239 -                (fn _ => simp_tac ring_ss 1)
1.240 -            |> mk_meta_eq;
1.241 -          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
1.242 -      in if t' aconv u
1.243 -        then None
1.244 -        else Some rew
1.245 -    end;
1.246 -  in
1.247 -    val ring_simproc = mk_simproc "ring" lhss proc;
1.248 -  end;
1.249 +text {*
1.250 +  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
1.251  *}
1.253 -ML_setup {* Addsimprocs [ring_simproc] *}
1.255 -lemma natsum_ldistr:
1.256 -  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
1.257 -by (induct n) simp_all
1.259 -lemma natsum_rdistr:
1.260 -  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
1.261 -by (induct n) simp_all
1.263 -subsection {* Integral Domains *}
1.264 +lemma (in cring) l_null [simp]:
1.265 +  "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
1.266 +proof -
1.267 +  assume R: "x \<in> carrier R"
1.268 +  then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
1.269 +    by (simp add: l_distr del: l_zero r_zero)
1.270 +  also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
1.271 +  finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
1.272 +  with R show ?thesis by (simp del: r_zero)
1.273 +qed
1.275 -declare one_not_zero [simp]
1.277 -lemma zero_not_one [simp]:
1.278 -  "0 ~= (1::'a::domain)"
1.279 -by (rule not_sym) simp
1.280 +lemma (in cring) r_null [simp]:
1.281 +  "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
1.282 +proof -
1.283 +  assume R: "x \<in> carrier R"
1.284 +  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
1.285 +  also from R have "... = \<zero>" by simp
1.286 +  finally show ?thesis .
1.287 +qed
1.289 -lemma integral_iff: (* not by default a simp rule! *)
1.290 -  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
1.291 -proof
1.292 -  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
1.293 -next
1.294 -  assume "a = 0 | b = 0" then show "a * b = 0" by auto
1.295 +lemma (in cring) l_minus:
1.296 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
1.297 +proof -
1.298 +  assume R: "x \<in> carrier R" "y \<in> carrier R"
1.299 +  then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
1.300 +  also from R have "... = \<zero>" by (simp add: l_neg l_null)
1.301 +  finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
1.302 +  with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
1.303 +  with R show ?thesis by (simp add: a_assoc r_neg )
1.304  qed
1.306 -(*
1.307 -lemma "(a::'a::ring) - (a - b) = b" apply simp
1.308 - simproc seems to fail on this example (fixed with new term order)
1.309 -*)
1.310 -(*
1.311 -lemma bug: "(b::'a::ring) - (b - a) = a" by simp
1.312 -   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
1.313 -*)
1.314 -lemma m_lcancel:
1.315 -  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
1.316 -proof
1.317 -  assume eq: "a * b = a * c"
1.318 -  then have "a * (b - c) = 0" by simp
1.319 -  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
1.320 -  with prem have "b - c = 0" by auto
1.321 -  then have "b = b - (b - c)" by simp
1.322 -  also have "b - (b - c) = c" by simp
1.323 -  finally show "b = c" .
1.324 -next
1.325 -  assume "b = c" then show "a * b = a * c" by simp
1.326 +lemma (in cring) r_minus:
1.327 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
1.328 +proof -
1.329 +  assume R: "x \<in> carrier R" "y \<in> carrier R"
1.330 +  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
1.331 +  also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
1.332 +  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
1.333 +  finally show ?thesis .
1.334  qed
1.336 -lemma m_rcancel:
1.337 -  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
1.339 +lemmas (in cring) cring_simprules =
1.340 +  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
1.341 +  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
1.342 +  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
1.343 +  a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
1.345 +use "ringsimp.ML"
1.347 +method_setup algebra =
1.348 +  {* Method.ctxt_args cring_normalise *}
1.349 +  {* computes distributive normal form in commutative rings (locales version) *}
1.351 +lemma
1.352 +  includes cring R + cring S
1.353 +  shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
1.354 +  a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
1.355 +  by algebra
1.357 +lemma
1.358 +  includes cring
1.359 +  shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
1.360 +  by algebra
1.362  end
2.1 --- a/src/HOL/Algebra/Group.thy	Mon Mar 10 16:21:06 2003 +0100
2.2 +++ b/src/HOL/Algebra/Group.thy	Mon Mar 10 17:25:34 2003 +0100
2.3 @@ -20,14 +20,6 @@
2.5  subsection {* Definitions *}
2.7 -(* The following may be unnecessary. *)
2.8 -text {*
2.9 -  We write groups additively.  This simplifies notation for rings.
2.10 -  All rings have an additive inverse, only fields have a
2.11 -  multiplicative one.  This definitions reduces the need for
2.12 -  qualifiers.
2.13 -*}
2.14 -
2.15  record 'a semigroup =
2.16    carrier :: "'a set"
2.17    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
2.18 @@ -104,6 +96,14 @@
2.19    then show "y \<otimes> x = z \<otimes> x" by simp
2.20  qed
2.22 +lemma (in group) inv_one [simp]:
2.23 +  "inv \<one> = \<one>"
2.24 +proof -
2.25 +  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
2.26 +  moreover have "... = \<one>" by (simp add: r_inv)
2.27 +  finally show ?thesis .
2.28 +qed
2.29 +
2.30  lemma (in group) inv_inv [simp]:
2.31    "x \<in> carrier G ==> inv (inv x) = x"
2.32  proof -
2.33 @@ -112,7 +112,7 @@
2.34    with x show ?thesis by simp
2.35  qed
2.37 -lemma (in group) inv_mult:
2.38 +lemma (in group) inv_mult_group:
2.39    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
2.40  proof -
2.41    assume G: "x \<in> carrier G" "y \<in> carrier G"
2.42 @@ -245,21 +245,21 @@
2.44  constdefs
2.45    DirProdSemigroup ::
2.46 -    "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
2.47 +    "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
2.48      => ('a \<times> 'b) semigroup"
2.49      (infixr "\<times>\<^sub>s" 80)
2.50    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
2.51      mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
2.53    DirProdMonoid ::
2.54 -    "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
2.55 +    "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
2.56      (infixr "\<times>\<^sub>m" 80)
2.57    "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
2.58      mult = mult (G \<times>\<^sub>s H),
2.59      one = (one G, one H) |)"
2.61    DirProdGroup ::
2.62 -    "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
2.63 +    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
2.64      (infixr "\<times>\<^sub>g" 80)
2.65    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
2.66      mult = mult (G \<times>\<^sub>m H),
2.67 @@ -409,4 +409,8 @@
2.69  locale abelian_group = abelian_monoid + group
2.71 +lemma (in abelian_group) inv_mult:
2.72 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
2.73 +  by (simp add: ac inv_mult_group)
2.74 +
2.75  end
3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Algebra/ringsimp.ML	Mon Mar 10 17:25:34 2003 +0100
3.3 @@ -0,0 +1,87 @@
3.4 +(*
3.5 +  Title:     Normalisation method for locale cring
3.6 +  Id:        \$Id\$
3.7 +  Author:    Clemens Ballarin
3.9 +*)
3.10 +
3.11 +local
3.12 +
3.13 +(*** Lexicographic path order on terms.
3.14 +
3.15 +  See Baader & Nipkow, Term rewriting, CUP 1998.
3.16 +  Without variables.  Const, Var, Bound, Free and Abs are treated all as
3.17 +  constants.
3.18 +
3.19 +  f_ord maps strings to integers and serves two purposes:
3.20 +  - Predicate on constant symbols.  Those that are not recognised by f_ord
3.21 +    must be mapped to ~1.
3.22 +  - Order on the recognised symbols.  These must be mapped to distinct
3.23 +    integers >= 0.
3.24 +
3.25 +***)
3.26 +
3.27 +fun dest_hd f_ord (Const (a, T)) =
3.28 +      let val ord = f_ord a in
3.29 +        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
3.30 +      end
3.31 +  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
3.32 +  | dest_hd _ (Var v) = ((1, v), 1)
3.33 +  | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
3.34 +  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
3.35 +
3.36 +fun term_lpo f_ord (s, t) =
3.37 +  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
3.38 +    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
3.39 +    then case hd_ord f_ord (f, g) of
3.40 +	GREATER =>
3.41 +	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
3.42 +	  then GREATER else LESS
3.43 +      | EQUAL =>
3.44 +	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
3.45 +	  then list_ord (term_lpo f_ord) (ss, ts)
3.46 +	  else LESS
3.47 +      | LESS => LESS
3.48 +    else GREATER
3.49 +  end
3.50 +and hd_ord f_ord (f, g) = case (f, g) of
3.51 +    (Abs (_, T, t), Abs (_, U, u)) =>
3.52 +      (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
3.53 +  | (_, _) => prod_ord (prod_ord int_ord
3.54 +                  (prod_ord Term.indexname_ord Term.typ_ord)) int_ord
3.55 +                (dest_hd f_ord f, dest_hd f_ord g)
3.56 +
3.57 +in
3.58 +
3.59 +(*** Term order for commutative rings ***)
3.60 +
3.61 +fun ring_ord a =
3.62 +  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
3.63 +  "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
3.64 +
3.65 +fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
3.66 +
3.67 +val cring_ss = HOL_ss settermless termless_ring;
3.68 +
3.69 +fun cring_normalise ctxt = let
3.70 +    fun filter t = case HOLogic.dest_Trueprop t of
3.71 +        Const ("CRing.cring_axioms", _) \$ Free (s, _) => [s]
3.72 +      | _ => []
3.73 +      handle TERM _ => [];
3.74 +    val insts = flat (map (filter o #prop o rep_thm)
3.75 +      (ProofContext.prems_of ctxt));
3.76 +val _ = warning ("Rings in proof context: " ^ implode insts);
3.77 +    val simps =
3.78 +      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
3.79 +        insts);