# Quotients revisited for Isabelle/HOL

Quotients revisited for Isabelle/HOL Quotients Revisited for Isabelle/HOL Cezary Kaliszyk University of Tsukuba, Japan Christian Urban Technical University of Munich, Germany kaliszyk@cs.tsukuba.ac.jp urbanc@in.tum.de ABSTRACT Higher-Order Logic (HOL) is based on a small logic kernel, whose only mechanism for extension is the introduction of safe de nitions and of non-empty types. Both extensions are often performed in quotient constructions. To ease the work involved with such quotient constructions, we re-implemented in the Isabelle/HOL theorem prover the quotient package by Homeier. In doing so we extended his work in order to deal with compositions of quotients and also speci ed completely the procedure of lifting theorems from the raw level to the quotient level. The importance for theorem proving is that many formal veri cations, in order to be feasible, require a convenient reasoning infrastructure for quotient constructions. numbers (namely add_pair (n1 , m1 ) (n2 , m2 ) (n1 + n2 , m1 + m2 )). Similarly one can construct nite sets, written fset, by quotienting the type list according to the equivalence relation xs ˆ ys ( € x. memb x xs  ’ memb x ys) (2) Keywords Quotients, Isabelle theorem prover, Higher-Order Logic 1. INTRODUCTION One might think quotients have http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png

# Quotients revisited for Isabelle/HOL

Association for Computing Machinery — Mar 21, 2011
6 pages

/lp/association-for-computing-machinery/quotients-revisited-for-isabelle-hol-2NQzGaUA5h

# References (12)

Datasource
Association for Computing Machinery
ISBN
978-1-4503-0113-8
doi
10.1145/1982185.1982529
Publisher site
See Article on Publisher Site

### Abstract

Quotients Revisited for Isabelle/HOL Cezary Kaliszyk University of Tsukuba, Japan Christian Urban Technical University of Munich, Germany kaliszyk@cs.tsukuba.ac.jp urbanc@in.tum.de ABSTRACT Higher-Order Logic (HOL) is based on a small logic kernel, whose only mechanism for extension is the introduction of safe de nitions and of non-empty types. Both extensions are often performed in quotient constructions. To ease the work involved with such quotient constructions, we re-implemented in the Isabelle/HOL theorem prover the quotient package by Homeier. In doing so we extended his work in order to deal with compositions of quotients and also speci ed completely the procedure of lifting theorems from the raw level to the quotient level. The importance for theorem proving is that many formal veri cations, in order to be feasible, require a convenient reasoning infrastructure for quotient constructions. numbers (namely add_pair (n1 , m1 ) (n2 , m2 ) (n1 + n2 , m1 + m2 )). Similarly one can construct nite sets, written fset, by quotienting the type list according to the equivalence relation xs ˆ ys ( € x. memb x xs  ’ memb x ys) (2) Keywords Quotients, Isabelle theorem prover, Higher-Order Logic 1. INTRODUCTION One might think quotients have