Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
qpaper / INJ
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 14 Jun 2010 12:07:55 +0200
changeset 2245 280b92df6a8b
parent 2244 e907165b953b
child 2246 8f493d371234
qpaper / INJ
Quotient-Paper/Paper.thy file | annotate | diff | comparison | revisions 
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 11:42:07 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 12:07:55 2010 +0200
@@ -714,10 +714,10 @@
   \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
   @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
   @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{equality (with same types and different types):}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
   @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
   @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{application, variable, constant:}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
   @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
   @{text "REG (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\
   @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
@@ -732,18 +732,23 @@
   the regularized theorems and the statement of the lifted theorem both as
   terms and returns the statement of the injected theorem:
 
-  \begin{itemize}
-  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
-  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
-  \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
-  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
-  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
-  \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
-  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
-  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
-  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
-  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
-  \end{itemize}
+  \begin{center}
+  \begin{tabular}{rcl}
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
+  @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) "} & $\dn$ & @{text "\<lambda>x. INJ (t, s)"}\\
+  @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}\\
+  @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
+  @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> (INJ (t, s))"}\\
+  @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
+  @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "v\<^isub>1"}\\
+  @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}\\
+  @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "c\<^isub>1"}\\
+  @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}\\
+  \end{tabular}
+  \end{center}
 
   For existential quantifiers and unique existential quantifiers it is
   defined similarly to the universal one.
nominal2