added pairs
Tue, 12 Mar 2013 11:31:31 +0100
changeset 51393 df0f306f030f
parent 51392 635562bc14ef
child 51395 bbb7639554dc
added pairs
--- a/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 07:51:10 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 11:31:31 2013 +0100
@@ -91,6 +91,10 @@
 Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
+Pairs can be taken apart either by pattern matching (as above) or with the
+projection functions @{const fst} and @{const snd}: @{thm fst_conv} and @{thm snd_conv}. Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}
+abbreviates @{text"(a, (b, c))"} and @{text "\<tau>\<^isub>1 \<times> \<tau>\<^isub>2 \<times> \<tau>\<^isub>3"} abbreviates
+@{text "\<tau>\<^isub>1 \<times> (\<tau>\<^isub>2 \<times> \<tau>\<^isub>3)"}.