author | nipkow |
Fri, 05 Jan 2018 18:41:42 +0100 | |
changeset 67341 | df79ef3b3a41 |
parent 67123 | 3fe40ff1b921 |
permissions | -rw-r--r-- |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
1 |
(* Title: HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
2 |
Author: Bernhard Haeupler, Stefan Berghofer |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
3 |
*) |
17388 | 4 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
5 |
section \<open>Some examples demonstrating the ring and field methods\<close> |
17388 | 6 |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
17508
diff
changeset
|
7 |
theory Commutative_Ring_Ex |
67123 | 8 |
imports "../Reflective_Field" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
9 |
begin |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
10 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
11 |
lemma "4 * (x::int) ^ 5 * y ^ 3 * x ^ 2 * 3 + x * z + 3 ^ 5 = 12 * x ^ 7 * y ^ 3 + z * x + 243" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
12 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
13 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
14 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
15 |
assumes "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
16 |
shows "\<guillemotleft>4\<guillemotright> \<otimes> x [^] (5::nat) \<otimes> y [^] (3::nat) \<otimes> x [^] (2::nat) \<otimes> \<guillemotleft>3\<guillemotright> \<oplus> x \<otimes> z \<oplus> \<guillemotleft>3\<guillemotright> [^] (5::nat) = |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
17 |
\<guillemotleft>12\<guillemotright> \<otimes> x [^] (7::nat) \<otimes> y [^] (3::nat) \<oplus> z \<otimes> x \<oplus> \<guillemotleft>243\<guillemotright>" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
18 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
19 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
20 |
lemma "((x::int) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
21 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
22 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
23 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
24 |
assumes "x \<in> carrier R" "y \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
25 |
shows "(x \<oplus> y) [^] (2::nat) = x [^] (2::nat) \<oplus> y [^] (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
26 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
27 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
28 |
lemma "((x::int) + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x ^ 2 * y + 3 * y ^ 2 * x" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
29 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
30 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
31 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
32 |
assumes "x \<in> carrier R" "y \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
33 |
shows "(x \<oplus> y) [^] (3::nat) = |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
34 |
x [^] (3::nat) \<oplus> y [^] (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x [^] (2::nat) \<otimes> y \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> y [^] (2::nat) \<otimes> x" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
35 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
36 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
37 |
lemma "((x::int) - y) ^ 3 = x ^ 3 + 3 * x * y ^ 2 + (- 3) * y * x ^ 2 - y ^ 3" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
38 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
39 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
40 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
41 |
assumes "x \<in> carrier R" "y \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
42 |
shows "(x \<ominus> y) [^] (3::nat) = |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
43 |
x [^] (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x \<otimes> y [^] (2::nat) \<oplus> (\<ominus> \<guillemotleft>3\<guillemotright>) \<otimes> y \<otimes> x [^] (2::nat) \<ominus> y [^] (3::nat)" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
44 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
45 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
46 |
lemma "((x::int) - y) ^ 2 = x ^ 2 + y ^ 2 - 2 * x * y" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
47 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
48 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
49 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
50 |
assumes "x \<in> carrier R" "y \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
51 |
shows "(x \<ominus> y) [^] (2::nat) = x [^] (2::nat) \<oplus> y [^] (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
52 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
53 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
54 |
lemma " ((a::int) + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * b * c + 2 * a * c" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
55 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
56 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
57 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
58 |
assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
59 |
shows " (a \<oplus> b \<oplus> c) [^] (2::nat) = |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
60 |
a [^] (2::nat) \<oplus> b [^] (2::nat) \<oplus> c [^] (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
61 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
62 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
63 |
lemma "((a::int) - b - c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 - 2 * a * b + 2 * b * c - 2 * a * c" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
64 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
65 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
66 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
67 |
assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
68 |
shows "(a \<ominus> b \<ominus> c) [^] (2::nat) = |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
69 |
a [^] (2::nat) \<oplus> b [^] (2::nat) \<oplus> c [^] (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
70 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
71 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
72 |
lemma "(a::int) * b + a * c = a * (b + c)" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
73 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
74 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
75 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
76 |
assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
77 |
shows "a \<otimes> b \<oplus> a \<otimes> c = a \<otimes> (b \<oplus> c)" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
78 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
79 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
80 |
lemma "(a::int) ^ 2 - b ^ 2 = (a - b) * (a + b)" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
81 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
82 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
83 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
84 |
assumes "a \<in> carrier R" "b \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
85 |
shows "a [^] (2::nat) \<ominus> b [^] (2::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b)" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
86 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
87 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
88 |
lemma "(a::int) ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2)" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
89 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
90 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
91 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
92 |
assumes "a \<in> carrier R" "b \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
93 |
shows "a [^] (3::nat) \<ominus> b [^] (3::nat) = (a \<ominus> b) \<otimes> (a [^] (2::nat) \<oplus> a \<otimes> b \<oplus> b [^] (2::nat))" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
94 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
95 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
96 |
lemma "(a::int) ^ 3 + b ^ 3 = (a + b) * (a ^ 2 - a * b + b ^ 2)" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
97 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
98 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
99 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
100 |
assumes "a \<in> carrier R" "b \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
101 |
shows "a [^] (3::nat) \<oplus> b [^] (3::nat) = (a \<oplus> b) \<otimes> (a [^] (2::nat) \<ominus> a \<otimes> b \<oplus> b [^] (2::nat))" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
102 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
103 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
104 |
lemma "(a::int) ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2)" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
105 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
106 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
107 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
108 |
assumes "a \<in> carrier R" "b \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
109 |
shows "a [^] (4::nat) \<ominus> b [^] (4::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b) \<otimes> (a [^] (2::nat) \<oplus> b [^] (2::nat))" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
110 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
111 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
112 |
lemma "(a::int) ^ 10 - b ^ 10 = |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
113 |
(a - b) * (a ^ 9 + a ^ 8 * b + a ^ 7 * b ^ 2 + a ^ 6 * b ^ 3 + a ^ 5 * b ^ 4 + |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
114 |
a ^ 4 * b ^ 5 + a ^ 3 * b ^ 6 + a ^ 2 * b ^ 7 + a * b ^ 8 + b ^ 9)" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
115 |
by ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
116 |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
117 |
lemma (in cring) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
118 |
assumes "a \<in> carrier R" "b \<in> carrier R" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
119 |
shows "a [^] (10::nat) \<ominus> b [^] (10::nat) = |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
120 |
(a \<ominus> b) \<otimes> (a [^] (9::nat) \<oplus> a [^] (8::nat) \<otimes> b \<oplus> a [^] (7::nat) \<otimes> b [^] (2::nat) \<oplus> |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
121 |
a [^] (6::nat) \<otimes> b [^] (3::nat) \<oplus> a [^] (5::nat) \<otimes> b [^] (4::nat) \<oplus> |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
122 |
a [^] (4::nat) \<otimes> b [^] (5::nat) \<oplus> a [^] (3::nat) \<otimes> b [^] (6::nat) \<oplus> |
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
67123
diff
changeset
|
123 |
a [^] (2::nat) \<otimes> b [^] (7::nat) \<oplus> a \<otimes> b [^] (8::nat) \<oplus> b [^] (9::nat))" |
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
124 |
by ring |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
125 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
126 |
lemma "(x::'a::field) \<noteq> 0 \<Longrightarrow> (1 - 1 / x) * x - x + 1 = 0" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
127 |
by field |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
128 |
|
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
129 |
lemma (in field) |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
130 |
assumes "x \<in> carrier R" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
131 |
shows "x \<noteq> \<zero> \<Longrightarrow> (\<one> \<ominus> \<one> \<oslash> x) \<otimes> x \<ominus> x \<oplus> \<one> = \<zero>" |
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60533
diff
changeset
|
132 |
by field |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
133 |
|
17388 | 134 |
end |