author | ballarin |
Thu, 27 Feb 2003 15:12:29 +0100 | |
changeset 13835 | 12b2ffbe543a |
child 13854 | 91c9ab25fece |
permissions | -rw-r--r-- |
13835
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
1 |
(* |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
2 |
Title: The algebraic hierarchy of rings |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
3 |
Id: $Id$ |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
4 |
Author: Clemens Ballarin, started 9 December 1996 |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
5 |
Copyright: Clemens Ballarin |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
6 |
*) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
7 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
8 |
header {* The algebraic hierarchy of rings as axiomatic classes *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
9 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
10 |
theory Ring = Group |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
11 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
12 |
section {* The Algebraic Hierarchy of Rings *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
13 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
14 |
subsection {* Basic Definitions *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
15 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
16 |
record 'a ring = "'a group" + |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
17 |
zero :: 'a ("\<zero>\<index>") |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
18 |
add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
19 |
a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
20 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
21 |
locale cring = abelian_monoid R + |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
22 |
assumes a_abelian_group: "abelian_group (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
23 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
24 |
and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
25 |
==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
26 |
and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
27 |
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
28 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
29 |
ML {* |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
30 |
thm "cring.l_distr" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
31 |
*} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
32 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
33 |
(* |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
34 |
locale cring = struct R + |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
35 |
assumes a_group: "abelian_group (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
36 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
37 |
and m_monoid: "abelian_monoid (| carrier = carrier R - {zero R}, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
38 |
mult = mult R, one = one R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
39 |
and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
40 |
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
41 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
42 |
locale field = struct R + |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
43 |
assumes a_group: "abelian_group (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
44 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
45 |
and m_group: "monoid (| carrier = carrier R - {zero R}, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
46 |
mult = mult R, one = one R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
47 |
and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
48 |
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
49 |
*) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
50 |
(* |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
51 |
a_assoc: "(a + b) + c = a + (b + c)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
52 |
l_zero: "0 + a = a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
53 |
l_neg: "(-a) + a = 0" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
54 |
a_comm: "a + b = b + a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
55 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
56 |
m_assoc: "(a * b) * c = a * (b * c)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
57 |
l_one: "1 * a = a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
58 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
59 |
l_distr: "(a + b) * c = a * c + b * c" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
60 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
61 |
m_comm: "a * b = b * a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
62 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
63 |
-- {* Definition of derived operations *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
64 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
65 |
minus_def: "a - b = a + (-b)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
66 |
inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
67 |
divide_def: "a / b = a * inverse b" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
68 |
power_def: "a ^ n = nat_rec 1 (%u b. b * a) n" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
69 |
*) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
70 |
subsection {* Basic Facts *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
71 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
72 |
lemma (in cring) a_magma [simp, intro]: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
73 |
"magma (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
74 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
75 |
using a_abelian_group by (simp only: abelian_group_def) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
76 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
77 |
lemma (in cring) a_l_one [simp, intro]: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
78 |
"l_one (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
79 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
80 |
using a_abelian_group by (simp only: abelian_group_def) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
81 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
82 |
lemma (in cring) a_abelian_group_parts [simp, intro]: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
83 |
"semigroup_axioms (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
84 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
85 |
"group_axioms (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
86 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
87 |
"abelian_semigroup_axioms (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
88 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
89 |
using a_abelian_group by (simp_all only: abelian_group_def) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
90 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
91 |
lemma (in cring) a_semigroup: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
92 |
"semigroup (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
93 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
94 |
by (simp add: semigroup_def) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
95 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
96 |
lemma (in cring) a_group: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
97 |
"group (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
98 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
99 |
by (simp add: group_def) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
100 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
101 |
lemma (in cring) a_abelian_semigroup: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
102 |
"abelian_semigroup (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
103 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
104 |
by (simp add: abelian_semigroup_def) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
105 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
106 |
lemma (in cring) a_abelian_group: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
107 |
"abelian_group (| carrier = carrier R, |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
108 |
mult = add R, one = zero R, m_inv = a_inv R |)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
109 |
by (simp add: abelian_group_def) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
110 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
111 |
lemma (in cring) a_assoc: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
112 |
"[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
113 |
==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
114 |
using semigroup.m_assoc [OF a_semigroup] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
115 |
by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
116 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
117 |
lemma (in cring) l_zero: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
118 |
"x \<in> carrier R ==> \<zero> \<oplus> x = x" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
119 |
using l_one.l_one [OF a_l_one] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
120 |
by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
121 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
122 |
lemma (in cring) l_neg: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
123 |
"x \<in> carrier R ==> (\<ominus> x) \<oplus> x = \<zero>" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
124 |
using group.l_inv [OF a_group] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
125 |
by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
126 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
127 |
lemma (in cring) a_comm: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
128 |
"[| x \<in> carrier R; y \<in> carrier R |] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
129 |
==> x \<oplus> y = y \<oplus> x" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
130 |
using abelian_semigroup.m_comm [OF a_abelian_semigroup] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
131 |
by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
132 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
133 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
134 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
135 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
136 |
qed |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
137 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
138 |
l_zero: "0 + a = a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
139 |
l_neg: "(-a) + a = 0" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
140 |
a_comm: "a + b = b + a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
141 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
142 |
m_assoc: "(a * b) * c = a * (b * c)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
143 |
l_one: "1 * a = a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
144 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
145 |
l_distr: "(a + b) * c = a * c + b * c" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
146 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
147 |
m_comm: "a * b = b * a" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
148 |
text {* Normaliser for Commutative Rings *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
149 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
150 |
use "order.ML" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
151 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
152 |
method_setup ring = |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
153 |
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
154 |
{* computes distributive normal form in rings *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
155 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
156 |
subsection {* Rings and the summation operator *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
157 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
158 |
(* Basic facts --- move to HOL!!! *) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
159 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
160 |
lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
161 |
by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
162 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
163 |
lemma natsum_Suc [simp]: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
164 |
"setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
165 |
by (simp add: atMost_Suc) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
166 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
167 |
lemma natsum_Suc2: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
168 |
"setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
169 |
proof (induct n) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
170 |
case 0 show ?case by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
171 |
next |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
172 |
case Suc thus ?case by (simp add: assoc) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
173 |
qed |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
174 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
175 |
lemma natsum_cong [cong]: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
176 |
"!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==> |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
177 |
setsum f {..j} = setsum g {..k}" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
178 |
by (induct j) auto |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
179 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
180 |
lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
181 |
by (induct n) simp_all |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
182 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
183 |
lemma natsum_add [simp]: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
184 |
"!!f::nat=>'a::plus_ac0. |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
185 |
setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
186 |
by (induct n) (simp_all add: plus_ac0) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
187 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
188 |
(* Facts specific to rings *) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
189 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
190 |
instance ring < plus_ac0 |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
191 |
proof |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
192 |
fix x y z |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
193 |
show "(x::'a::ring) + y = y + x" by (rule a_comm) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
194 |
show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
195 |
show "0 + (x::'a::ring) = x" by (rule l_zero) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
196 |
qed |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
197 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
198 |
ML {* |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
199 |
local |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
200 |
val lhss = |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
201 |
[read_cterm (sign_of (the_context ())) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
202 |
("?t + ?u::'a::ring", TVar (("'z", 0), [])), |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
203 |
read_cterm (sign_of (the_context ())) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
204 |
("?t - ?u::'a::ring", TVar (("'z", 0), [])), |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
205 |
read_cterm (sign_of (the_context ())) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
206 |
("?t * ?u::'a::ring", TVar (("'z", 0), [])), |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
207 |
read_cterm (sign_of (the_context ())) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
208 |
("- ?t::'a::ring", TVar (("'z", 0), [])) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
209 |
]; |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
210 |
fun proc sg _ t = |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
211 |
let val rew = Tactic.prove sg [] [] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
212 |
(HOLogic.mk_Trueprop |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
213 |
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
214 |
(fn _ => simp_tac ring_ss 1) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
215 |
|> mk_meta_eq; |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
216 |
val (t', u) = Logic.dest_equals (Thm.prop_of rew); |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
217 |
in if t' aconv u |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
218 |
then None |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
219 |
else Some rew |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
220 |
end; |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
221 |
in |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
222 |
val ring_simproc = mk_simproc "ring" lhss proc; |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
223 |
end; |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
224 |
*} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
225 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
226 |
ML_setup {* Addsimprocs [ring_simproc] *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
227 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
228 |
lemma natsum_ldistr: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
229 |
"!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
230 |
by (induct n) simp_all |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
231 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
232 |
lemma natsum_rdistr: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
233 |
"!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
234 |
by (induct n) simp_all |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
235 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
236 |
subsection {* Integral Domains *} |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
237 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
238 |
declare one_not_zero [simp] |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
239 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
240 |
lemma zero_not_one [simp]: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
241 |
"0 ~= (1::'a::domain)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
242 |
by (rule not_sym) simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
243 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
244 |
lemma integral_iff: (* not by default a simp rule! *) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
245 |
"(a * b = (0::'a::domain)) = (a = 0 | b = 0)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
246 |
proof |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
247 |
assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
248 |
next |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
249 |
assume "a = 0 | b = 0" then show "a * b = 0" by auto |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
250 |
qed |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
251 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
252 |
(* |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
253 |
lemma "(a::'a::ring) - (a - b) = b" apply simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
254 |
simproc seems to fail on this example (fixed with new term order) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
255 |
*) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
256 |
(* |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
257 |
lemma bug: "(b::'a::ring) - (b - a) = a" by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
258 |
simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
259 |
*) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
260 |
lemma m_lcancel: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
261 |
assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
262 |
proof |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
263 |
assume eq: "a * b = a * c" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
264 |
then have "a * (b - c) = 0" by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
265 |
then have "a = 0 | (b - c) = 0" by (simp only: integral_iff) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
266 |
with prem have "b - c = 0" by auto |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
267 |
then have "b = b - (b - c)" by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
268 |
also have "b - (b - c) = c" by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
269 |
finally show "b = c" . |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
270 |
next |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
271 |
assume "b = c" then show "a * b = a * c" by simp |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
272 |
qed |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
273 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
274 |
lemma m_rcancel: |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
275 |
"(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
276 |
by (simp add: m_lcancel) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
277 |
|
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff
changeset
|
278 |
end |