Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Commutative_Ring_Complete.thy
author haftmann
Fri, 20 Apr 2007 11:21:40 +0200
changeset 22742 06165e40e7bd
parent 17508 c84af7f39a6b
child 23266 50f0a4f12ed3
permissions -rw-r--r--
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 
     1
 
(*  ID:         $Id$
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 
     2
 
    Author:     Bernhard Haeupler
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 
     3
 







17388






495c799df31d
tuned headers etc.;



wenzelm


parents: 
17378

diff
changeset




     4


This theory is about of the relative completeness of method comm-ring













495c799df31d
tuned headers etc.;



wenzelm


parents: 
17378

diff
changeset




     5


method.  As long as the reified atomic polynomials of type 'a pol are













495c799df31d
tuned headers etc.;



wenzelm


parents: 
17378

diff
changeset




     6


in normal form, the cring method is complete.













495c799df31d
tuned headers etc.;



wenzelm


parents: 
17378

diff
changeset




     7


*)













495c799df31d
tuned headers etc.;



wenzelm


parents: 
17378

diff
changeset




     8














495c799df31d
tuned headers etc.;



wenzelm


parents: 
17378

diff
changeset




     9


header {* Proof of the relative completeness of method comm-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




    10














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




    11


theory Commutative_Ring_Complete








17508






c84af7f39a6b
tuned theory dependencies;



wenzelm


parents: 
17396

diff
changeset




    12


imports Commutative_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




    13


begin