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