--- 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}
--- 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
--- 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''})"
--- 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"
--- 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)"
--- 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