equal
deleted
inserted
replaced
104 \noindent |
104 \noindent |
105 One might think quotients have been studied to death, but in the context of |
105 One might think quotients have been studied to death, but in the context of |
106 theorem provers many questions concerning them are far from settled. In |
106 theorem provers many questions concerning them are far from settled. In |
107 this paper we address the question of how to establish a convenient reasoning |
107 this paper we address the question of how to establish a convenient reasoning |
108 infrastructure |
108 infrastructure |
109 for quotient constructions in the Isabelle/HOL, |
109 for quotient constructions in the Isabelle/HOL |
110 theorem prover. Higher-Order Logic (HOL) consists |
110 theorem prover. Higher-Order Logic (HOL) consists |
111 of a small number of axioms and inference rules over a simply-typed |
111 of a small number of axioms and inference rules over a simply-typed |
112 term-language. Safe reasoning in HOL is ensured by two very restricted |
112 term-language. Safe reasoning in HOL is ensured by two very restricted |
113 mechanisms for extending the logic: one is the definition of new constants |
113 mechanisms for extending the logic: one is the definition of new constants |
114 in terms of existing ones; the other is the introduction of new types by |
114 in terms of existing ones; the other is the introduction of new types by |
529 \noindent |
529 \noindent |
530 which introduce the type of integers and of finite sets using the |
530 which introduce the type of integers and of finite sets using the |
531 equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text |
531 equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text |
532 "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and |
532 "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and |
533 \eqref{listequiv}, respectively (the proofs about being equivalence |
533 \eqref{listequiv}, respectively (the proofs about being equivalence |
534 relations is omitted). Given this data, we define for declarations shown in |
534 relations are omitted). Given this data, we define for declarations shown in |
535 \eqref{typedecl} the quotient types internally as |
535 \eqref{typedecl} the quotient types internally as |
536 |
536 |
537 \begin{isabelle}\ \ \ \ \ %%% |
537 \begin{isabelle}\ \ \ \ \ %%% |
538 \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"} |
538 \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"} |
539 \end{isabelle} |
539 \end{isabelle} |