equal
deleted
inserted
replaced
1 (* ID: $Id$ |
1 (* Author: Bernhard Haeupler |
2 Author: Bernhard Haeupler |
|
3 |
2 |
4 This theory is about of the relative completeness of method comm-ring |
3 This theory is about of the relative completeness of method comm-ring |
5 method. As long as the reified atomic polynomials of type 'a pol are |
4 method. As long as the reified atomic polynomials of type 'a pol are |
6 in normal form, the cring method is complete. |
5 in normal form, the cring method is complete. |
7 *) |
6 *) |
12 imports Commutative_Ring |
11 imports Commutative_Ring |
13 begin |
12 begin |
14 |
13 |
15 text {* Formalization of normal form *} |
14 text {* Formalization of normal form *} |
16 fun |
15 fun |
17 isnorm :: "('a::{comm_ring,recpower}) pol \<Rightarrow> bool" |
16 isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool" |
18 where |
17 where |
19 "isnorm (Pc c) \<longleftrightarrow> True" |
18 "isnorm (Pc c) \<longleftrightarrow> True" |
20 | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False" |
19 | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False" |
21 | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False" |
20 | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False" |
22 | "isnorm (Pinj 0 P) \<longleftrightarrow> False" |
21 | "isnorm (Pinj 0 P) \<longleftrightarrow> False" |