Paper/Paper.thy
changeset 1718 0d057e57e9a8
parent 1717 a3ef7fba983f
child 1720 a5def8fe0714
equal deleted inserted replaced
1717:a3ef7fba983f 1718:0d057e57e9a8
  1270 *}
  1270 *}
  1271 
  1271 
  1272 section {* The Lifting of Definitions and Properties *}
  1272 section {* The Lifting of Definitions and Properties *}
  1273 
  1273 
  1274 text {*
  1274 text {*
  1275   To define quotient types of the raw types we first show that the defined relation
  1275   To define quotient types of the raw types we first show that the defined relations
  1276   in an equivalence relation.
  1276   are equivalence relations.
  1277 
  1277 
  1278   \begin{lemma} The relations $\approx_1,\ldots,\approx_n,\approx_{bn1},\ldots,\approx_{bnm}$
  1278   \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}
  1279   defined as above are equivalence relations.
  1279   defined as above are equivalence relations and are equivariant.
  1280   \end{lemma}
  1280   \end{lemma}
  1281   \begin{proof}
  1281   \begin{proof} Reflexivity by induction on the raw datatype. Symmetry,
  1282   Reflexivity by induction on the raw datatype, symmetry and transitivity by
  1282   transitivity and equivariance by induction on the alpha equivalence
  1283   induction on the alpha equivalence relation. Using lemma \ref{alphaeq}, the
  1283   relation. Using lemma \ref{alphaeq}, the conditions follow by simple
  1284   conditions follow by simple calculations.
  1284   calculations.  \end{proof}
  1285   \end{proof}
  1285 
  1286 
  1286   \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
  1287   \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift the raw
  1287   the raw definitions to the quotient type, we need to prove that they
  1288   definitions to the quotient type, we need to prove that they \emph{respect} the
  1288   \emph{respect} the relation. We follow the definition of respectfullness given
  1289   relation. We follow the definition of respectfullness given by
  1289   by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition
  1290   Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition is that
  1290   is that when a function (or constructor) is given arguments that are
  1291   when a function (or constructor) is given arguments that are alpha-equivalent the
  1291   alpha-equivalent the results are also alpha equivalent. For arguments that are
  1292   results are also alpha equivalent. For arguments that are not of any of the relations
  1292   not of any of the relations taken into account, equivalence is replaced by
  1293   taken into account, equvalence is replaced by equality.
  1293   equality. In particular the respectfullness condition for a @{text "bn"}
  1294 
  1294   function means that for alpha equivalent raw terms it returns the same bound
  1295 % Could be written as a \{lemma}
  1295   names. Thanks to the restrictions on the binding functions introduced in
  1296   In particular the respectfullness condition for a @{text "bn"} function means that for
  1296   Section~\ref{sec:alpha} we can show that are respectful.
  1297   alpha equivalent raw terms it returns the same bound names. Thanks to the
  1297 
  1298   restrictions on the binding functions introduced in Section~\ref{sec:alpha}, we can
  1298   \begin{lemma} The functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"}, @{text "fv_ty\<^isub>1 \<dots> fv_ty\<^isub>n"},
  1299   show that are respectful. With this we can show the respectfullness of @{text "fv_ty"}
  1299   the raw constructors, the raw permutations and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are
  1300   functions by induction. Respectfullness of permutations is a direct consequence
  1300   respectful w.r.t. the relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>n"}.
  1301   of equivariance. Respectfullness of type constructors and of @{text "alpha_bn"} follows
  1301   \end{lemma}
  1302   by induction from type definitions.
  1302   \begin{proof} Respectfullness of permutations is a direct consequence of
  1303 
  1303   equivariance.  All other properties by induction on the alpha-equivalence
       
  1304   relation.  For @{text "bn"} the thesis follows by simple calculations thanks
       
  1305   to the restrictions on the binding functions. For @{text "fv"} functions it
       
  1306   follows using respectfullness of @{text "bn"}. For type constructors it is a
       
  1307   simple calculation thanks to the way alpha-equivalence was defined. For @{text
       
  1308   "alpha_bn"} after a second induction on the second relation by simple
       
  1309   calculations.  \end{proof}
       
  1310 
       
  1311   With these respectfullness properties we can use the quotient package
       
  1312   to define the above constants on the quotient level. We can then automatically
       
  1313   lift the theorems that talk about the raw constants to theorems on the quotient
       
  1314   level. The following lifted properties are proved:
       
  1315 
       
  1316   \begin{center}
       
  1317   \begin{tabular}{cp{7cm}}
       
  1318   $\bullet$ & permutation defining equations \\
       
  1319   $\bullet$ & @{term "bn"} defining equations \\
       
  1320   $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\
       
  1321   $\bullet$ & induction (weak induction, just on the term structure) \\
       
  1322   $\bullet$ & quasi-injectivity, the equations that specify when two
       
  1323      constructors are equal\\
       
  1324   $\bullet$ & distinctness\\
       
  1325   $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\
       
  1326   \end{tabular}
       
  1327   \end{center}
  1304 
  1328 
  1305 *}
  1329 *}
  1306 
  1330 
  1307 text {*
  1331 text {*
  1308   Restrictions
  1332   Restrictions