# HG changeset patch
# User wenzelm
# Date 1363123441 -3600
# Node ID 2aea76fe9c7335e4b712274d87216c76c1c4ae4d
# Parent  f4c82c165f589fa309c17b105837150ed15dc9e0# Parent  90a598019aeb6ad397f4b0f69559d97b1666ca19
merged

diff -r 90a598019aeb -r 2aea76fe9c73 src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 22:22:05 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 22:24:01 2013 +0100
@@ -91,6 +91,10 @@
 
 text{*
 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)"}.
 
 \subsection{Definitions}
 
diff -r 90a598019aeb -r 2aea76fe9c73 src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Tue Mar 12 22:22:05 2013 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy	Tue Mar 12 22:24:01 2013 +0100
@@ -8,12 +8,12 @@
 by simp
 
 text{* In order to display commands annotated with state sets,
-states must be translated into a printable format as lists of pairs,
+states must be translated into a printable format as sets of pairs,
 for a given set of variable names. This is what @{text show_acom} does: *}
 
 definition show_acom ::
-  "vname list \<Rightarrow> state set acom \<Rightarrow> (vname*val)list set acom" where
-"show_acom xs = map_acom (\<lambda>S. (\<lambda>s. map (\<lambda>x. (x, s x)) xs) ` S)"
+  "vname set \<Rightarrow> state set acom \<Rightarrow> (vname*val)set set acom" where
+"show_acom X = map_acom (\<lambda>S. (\<lambda>s. (\<lambda>x. (x, s x)) ` X) ` S)"
 
 
 text{* The example: *}
@@ -23,24 +23,24 @@
 
 text{* Collecting semantics: *}
 
-value "show_acom [''x''] (((step {<>}) ^^ 1) C0)"
-value "show_acom [''x''] (((step {<>}) ^^ 2) C0)"
-value "show_acom [''x''] (((step {<>}) ^^ 3) C0)"
-value "show_acom [''x''] (((step {<>}) ^^ 4) C0)"
-value "show_acom [''x''] (((step {<>}) ^^ 5) C0)"
-value "show_acom [''x''] (((step {<>}) ^^ 6) C0)"
-value "show_acom [''x''] (((step {<>}) ^^ 7) C0)"
-value "show_acom [''x''] (((step {<>}) ^^ 8) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 1) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 2) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 3) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 4) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 5) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 6) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 7) C0)"
+value "show_acom {''x''} (((step {<>}) ^^ 8) C0)"
 
 text{* Small-step semantics: *}
-value "show_acom [''x''] (((step {}) ^^ 0) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 1) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 2) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 3) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 4) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 5) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 6) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 7) (step {<>} C0))"
-value "show_acom [''x''] (((step {}) ^^ 8) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 0) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 1) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 2) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 3) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 4) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 5) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 6) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 7) (step {<>} C0))"
+value "show_acom {''x''} (((step {}) ^^ 8) (step {<>} C0))"
 
 end
diff -r 90a598019aeb -r 2aea76fe9c73 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Tue Mar 12 22:22:05 2013 +0100
+++ b/src/HOL/IMP/Live.thy	Tue Mar 12 22:24:01 2013 +0100
@@ -7,12 +7,14 @@
 
 subsection "Liveness Analysis"
 
+text_raw{*\snip{LDef}{0}{2}{% *}
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
-"L SKIP X = X" |
-"L (x ::= a) X = X-{x} \<union> vars a" |
-"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
+"L SKIP     X = X" |
+"L (x ::= a) X = (X - {x}) \<union> vars a" |
+"L (c\<^isub>1; c\<^isub>2)  X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
 "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
-"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
+"L (WHILE b DO c)          X = vars b \<union> X \<union> L c X"
+text_raw{*}%endsnip*}
 
 value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
 
diff -r 90a598019aeb -r 2aea76fe9c73 src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Tue Mar 12 22:22:05 2013 +0100
+++ b/src/HOL/IMP/Types.thy	Tue Mar 12 22:24:01 2013 +0100
@@ -11,6 +11,7 @@
 
 datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
 
+text_raw{*\snip{tavalDef}{0}{2}{% *}
 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
 "taval (Ic i) s (Iv i)" |
 "taval (Rc r) s (Rv r)" |
@@ -19,6 +20,7 @@
  \<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
  \<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
+text_raw{*}%endsnip*}
 
 inductive_cases [elim!]:
   "taval (Ic i) s v"  "taval (Rc i) s v"
@@ -29,12 +31,14 @@
 
 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
+text_raw{*\snip{tbvalDef}{0}{2}{% *}
 inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
 "tbval (Bc v) s v" |
 "tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
 "tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
 "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
+text_raw{*}%endsnip*}
 
 subsection "Syntax of Commands"
 (* a copy of Com.thy - keep in sync! *)
@@ -49,6 +53,7 @@
 
 subsection "Small-Step Semantics of Commands"
 
+text_raw{*\snip{tsmallstepDef}{0}{2}{% *}
 inductive
   small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
 where
@@ -61,6 +66,7 @@
 IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
 
 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+text_raw{*}%endsnip*}
 
 lemmas small_step_induct = small_step.induct[split_format(complete)]
 
@@ -70,6 +76,7 @@
 
 type_synonym tyenv = "vname \<Rightarrow> ty"
 
+text_raw{*\snip{atypingDef}{0}{2}{% *}
 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
 where
@@ -77,25 +84,30 @@
 Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
 V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
 Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
+text_raw{*}%endsnip*}
 
 text{* Warning: the ``:'' notation leads to syntactic ambiguities,
 i.e. multiple parse trees, because ``:'' also stands for set membership.
 In most situations Isabelle's type system will reject all but one parse tree,
 but will still inform you of the potential ambiguity. *}
 
+text_raw{*\snip{btypingDef}{0}{2}{% *}
 inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
 where
 B_ty: "\<Gamma> \<turnstile> Bc v" |
 Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
 And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
 Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
+text_raw{*}%endsnip*}
 
+text_raw{*\snip{ctypingDef}{0}{2}{% *}
 inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
 Skip_ty: "\<Gamma> \<turnstile> SKIP" |
 Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
 Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
 If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
 While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
+text_raw{*}%endsnip*}
 
 inductive_cases [elim!]:
   "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;c2"
diff -r 90a598019aeb -r 2aea76fe9c73 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Mar 12 22:22:05 2013 +0100
+++ b/src/HOL/Product_Type.thy	Tue Mar 12 22:24:01 2013 +0100
@@ -184,6 +184,8 @@
 
 translations
   "(x, y)" == "CONST Pair x y"
+  "_pattern x y" => "CONST Pair x y"
+  "_patterns x y" => "CONST Pair x y"
   "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
   "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
   "%(x, y). b" == "CONST prod_case (%x y. b)"
diff -r 90a598019aeb -r 2aea76fe9c73 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Mar 12 22:22:05 2013 +0100
+++ b/src/HOL/Set.thy	Tue Mar 12 22:24:01 2013 +0100
@@ -48,11 +48,11 @@
   "{x. P}" == "CONST Collect (%x. P)"
 
 syntax
-  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
+  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
 syntax (xsymbols)
-  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
+  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
 translations
-  "{x:A. P}" => "{x. x:A & P}"
+  "{p:A. P}" => "CONST Collect (%p. p:A & P)"
 
 lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
   by simp