equal
deleted
inserted
replaced
145 context of HOL, there have been a few quotient packages already |
145 context of HOL, there have been a few quotient packages already |
146 \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier |
146 \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier |
147 \cite{Homeier05} implemented in HOL4. The fundamental construction these |
147 \cite{Homeier05} implemented in HOL4. The fundamental construction these |
148 quotient packages perform can be illustrated by the following picture: |
148 quotient packages perform can be illustrated by the following picture: |
149 |
149 |
|
150 %%% FIXME: Referee 1 says: |
|
151 %%% Diagram is unclear. Firstly, isn't an existing type a "set (not sets) of raw elements"? |
|
152 %%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type? |
|
153 %%% Thirdly, what do the words "non-empty subset" refer to ? |
|
154 |
150 \begin{center} |
155 \begin{center} |
151 \mbox{}\hspace{20mm}\begin{tikzpicture} |
156 \mbox{}\hspace{20mm}\begin{tikzpicture} |
152 %%\draw[step=2mm] (-4,-1) grid (4,1); |
157 %%\draw[step=2mm] (-4,-1) grid (4,1); |
153 |
158 |
154 \draw[very thick] (0.7,0.3) circle (4.85mm); |
159 \draw[very thick] (0.7,0.3) circle (4.85mm); |
401 As a result, Homeier is able to build an automatic prover that can nearly |
406 As a result, Homeier is able to build an automatic prover that can nearly |
402 always discharge a proof obligation involving @{text "Quotient"}. Our quotient |
407 always discharge a proof obligation involving @{text "Quotient"}. Our quotient |
403 package makes heavy |
408 package makes heavy |
404 use of this part of Homeier's work including an extension |
409 use of this part of Homeier's work including an extension |
405 for dealing with compositions of equivalence relations defined as follows: |
410 for dealing with compositions of equivalence relations defined as follows: |
|
411 |
|
412 %%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also |
|
413 %%% what wikipedia says. Any idea for a different name? Conjugation of Relations? |
406 |
414 |
407 \begin{definition}[Composition of Relations] |
415 \begin{definition}[Composition of Relations] |
408 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate |
416 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate |
409 composition defined by |
417 composition defined by |
410 @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
418 @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |