--- a/src/HOL/IMP/Big_Step.thy Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/IMP/Big_Step.thy Fri Jan 12 14:08:53 2018 +0100
@@ -4,13 +4,13 @@
subsection "Big-Step Semantics of Commands"
-text {*
+text \<open>
The big-step semantics is a straight-forward inductive definition
with concrete syntax. Note that the first parameter is a tuple,
so the syntax becomes @{text "(c,s) \<Rightarrow> s'"}.
-*}
+\<close>
-text_raw{*\snip{BigStepdef}{0}{1}{% *}
+text_raw\<open>\snip{BigStepdef}{0}{1}{%\<close>
inductive
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
@@ -23,30 +23,30 @@
WhileTrue:
"\<lbrakk> bval b s\<^sub>1; (c,s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk>
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3"
-text_raw{*}%endsnip*}
+text_raw\<open>}%endsnip\<close>
-text_raw{*\snip{BigStepEx}{1}{2}{% *}
+text_raw\<open>\snip{BigStepEx}{1}{2}{%\<close>
schematic_goal ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
apply(rule Seq)
apply(rule Assign)
apply simp
apply(rule Assign)
done
-text_raw{*}%endsnip*}
+text_raw\<open>}%endsnip\<close>
thm ex[simplified]
-text{* We want to execute the big-step rules: *}
+text\<open>We want to execute the big-step rules:\<close>
code_pred big_step .
-text{* For inductive definitions we need command
- \texttt{values} instead of \texttt{value}. *}
+text\<open>For inductive definitions we need command
+ \texttt{values} instead of \texttt{value}.\<close>
values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}"
-text{* We need to translate the result state into a list
-to display it. *}
+text\<open>We need to translate the result state into a list
+to display it.\<close>
values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"
@@ -57,46 +57,46 @@
<''x'' := 0, ''y'' := 13>) \<Rightarrow> t}"
-text{* Proof automation: *}
+text\<open>Proof automation:\<close>
-text {* The introduction rules are good for automatically
+text \<open>The introduction rules are good for automatically
construction small program executions. The recursive cases
may require backtracking, so we declare the set as unsafe
-intro rules. *}
+intro rules.\<close>
declare big_step.intros [intro]
-text{* The standard induction rule
-@{thm [display] big_step.induct [no_vars]} *}
+text\<open>The standard induction rule
+@{thm [display] big_step.induct [no_vars]}\<close>
thm big_step.induct
-text{*
+text\<open>
This induction schema is almost perfect for our purposes, but
our trick for reusing the tuple syntax means that the induction
schema has two parameters instead of the @{text c}, @{text s},
and @{text s'} that we are likely to encounter. Splitting
the tuple parameter fixes this:
-*}
+\<close>
lemmas big_step_induct = big_step.induct[split_format(complete)]
thm big_step_induct
-text {*
+text \<open>
@{thm [display] big_step_induct [no_vars]}
-*}
+\<close>
subsection "Rule inversion"
-text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
-That @{prop "s = t"}. This is how we can automatically prove it: *}
+text\<open>What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
+That @{prop "s = t"}. This is how we can automatically prove it:\<close>
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
thm SkipE
-text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
+text\<open>This is an \emph{elimination rule}. The [elim] attribute tells auto,
blast and friends (but not simp!) to use it automatically; [elim!] means that
it is applied eagerly.
-Similarly for the other commands: *}
+Similarly for the other commands:\<close>
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
thm AssignE
@@ -107,20 +107,20 @@
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
thm WhileE
-text{* Only [elim]: [elim!] would not terminate. *}
+text\<open>Only [elim]: [elim!] would not terminate.\<close>
-text{* An automatic example: *}
+text\<open>An automatic example:\<close>
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
by blast
-text{* Rule inversion by hand via the ``cases'' method: *}
+text\<open>Rule inversion by hand via the ``cases'' method:\<close>
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
shows "t = s"
proof-
from assms show ?thesis
- proof cases --"inverting assms"
+ proof cases \<comment>"inverting assms"
case IfTrue thm IfTrue
thus ?thesis by blast
next
@@ -133,7 +133,7 @@
"(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
by auto
-text {* An example combining rule inversion and derivations *}
+text \<open>An example combining rule inversion and derivations\<close>
lemma Seq_assoc:
"(c1;; c2;; c3, s) \<Rightarrow> s' \<longleftrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'"
proof
@@ -147,7 +147,7 @@
with c1
show "(c1;; (c2;; c3), s) \<Rightarrow> s'" by (rule Seq)
next
- -- "The other direction is analogous"
+ \<comment> "The other direction is analogous"
assume "(c1;; (c2;; c3), s) \<Rightarrow> s'"
thus "(c1;; c2;; c3, s) \<Rightarrow> s'" by auto
qed
@@ -155,70 +155,70 @@
subsection "Command Equivalence"
-text {*
+text \<open>
We call two statements @{text c} and @{text c'} equivalent wrt.\ the
big-step semantics when \emph{@{text c} started in @{text s} terminates
in @{text s'} iff @{text c'} started in the same @{text s} also terminates
in the same @{text s'}}. Formally:
-*}
-text_raw{*\snip{BigStepEquiv}{0}{1}{% *}
+\<close>
+text_raw\<open>\snip{BigStepEquiv}{0}{1}{%\<close>
abbreviation
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
"c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"
-text_raw{*}%endsnip*}
+text_raw\<open>}%endsnip\<close>
-text {*
+text \<open>
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
As an example, we show that loop unfolding is an equivalence
transformation on programs:
-*}
+\<close>
lemma unfold_while:
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
proof -
- -- "to show the equivalence, we look at the derivation tree for"
- -- "each side and from that construct a derivation tree for the other side"
+ \<comment> "to show the equivalence, we look at the derivation tree for"
+ \<comment> "each side and from that construct a derivation tree for the other side"
have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
- proof cases --"rule inversion on \<open>(?w, s) \<Rightarrow> t\<close>"
+ proof cases \<comment>"rule inversion on \<open>(?w, s) \<Rightarrow> t\<close>"
case WhileFalse
thus ?thesis by blast
next
case WhileTrue
- from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where
+ from \<open>bval b s\<close> \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
- -- "now we can build a derivation tree for the @{text IF}"
- -- "first, the body of the True-branch:"
+ \<comment> "now we can build a derivation tree for the @{text IF}"
+ \<comment> "first, the body of the True-branch:"
hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
- -- "then the whole @{text IF}"
- with `bval b s` show ?thesis by (rule IfTrue)
+ \<comment> "then the whole @{text IF}"
+ with \<open>bval b s\<close> show ?thesis by (rule IfTrue)
qed
qed
moreover
- -- "now the other direction:"
+ \<comment> "now the other direction:"
have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
- proof cases --"rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>"
+ proof cases \<comment>"rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>"
case IfFalse
- hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
- thus ?thesis using `\<not>bval b s` by blast
+ hence "s = t" using \<open>(?iw, s) \<Rightarrow> t\<close> by blast
+ thus ?thesis using \<open>\<not>bval b s\<close> by blast
next
case IfTrue
- -- "and for this, only the Seq-rule is applicable:"
- from `(c;; ?w, s) \<Rightarrow> t` obtain s' where
+ \<comment> "and for this, only the Seq-rule is applicable:"
+ from \<open>(c;; ?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
- -- "with this information, we can build a derivation tree for @{text WHILE}"
- with `bval b s` show ?thesis by (rule WhileTrue)
+ \<comment> "with this information, we can build a derivation tree for @{text WHILE}"
+ with \<open>bval b s\<close> show ?thesis by (rule WhileTrue)
qed
qed
ultimately
show ?thesis by blast
qed
-text {* Luckily, such lengthy proofs are seldom necessary. Isabelle can
-prove many such facts automatically. *}
+text \<open>Luckily, such lengthy proofs are seldom necessary. Isabelle can
+prove many such facts automatically.\<close>
lemma while_unfold:
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)"
@@ -244,9 +244,9 @@
lemma sim_while_cong: "c \<sim> c' \<Longrightarrow> WHILE b DO c \<sim> WHILE b DO c'"
by (metis sim_while_cong_aux)
-text {* Command equivalence is an equivalence relation, i.e.\ it is
+text \<open>Command equivalence is an equivalence relation, i.e.\ it is
reflexive, symmetric, and transitive. Because we used an abbreviation
-above, Isabelle derives this automatically. *}
+above, Isabelle derives this automatically.\<close>
lemma sim_refl: "c \<sim> c" by simp
lemma sim_sym: "(c \<sim> c') = (c' \<sim> c)" by auto
@@ -254,35 +254,35 @@
subsection "Execution is deterministic"
-text {* This proof is automatic. *}
+text \<open>This proof is automatic.\<close>
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
by (induction arbitrary: u rule: big_step.induct) blast+
-text {*
+text \<open>
This is the proof as you might present it in a lecture. The remaining
cases are simple enough to be proved automatically:
-*}
-text_raw{*\snip{BigStepDetLong}{0}{2}{% *}
+\<close>
+text_raw\<open>\snip{BigStepDetLong}{0}{2}{%\<close>
theorem
"(c,s) \<Rightarrow> t \<Longrightarrow> (c,s) \<Rightarrow> t' \<Longrightarrow> t' = t"
proof (induction arbitrary: t' rule: big_step.induct)
- -- "the only interesting case, @{text WhileTrue}:"
+ \<comment> "the only interesting case, @{text WhileTrue}:"
fix b c s s\<^sub>1 t t'
- -- "The assumptions of the rule:"
+ \<comment> "The assumptions of the rule:"
assume "bval b s" and "(c,s) \<Rightarrow> s\<^sub>1" and "(WHILE b DO c,s\<^sub>1) \<Rightarrow> t"
- -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
+ \<comment> \<open>Ind.Hyp; note the @{text"\<And>"} because of arbitrary:\<close>
assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s\<^sub>1"
assume IHw: "\<And>t'. (WHILE b DO c,s\<^sub>1) \<Rightarrow> t' \<Longrightarrow> t' = t"
- -- "Premise of implication:"
+ \<comment> "Premise of implication:"
assume "(WHILE b DO c,s) \<Rightarrow> t'"
- with `bval b s` obtain s\<^sub>1' where
+ with \<open>bval b s\<close> obtain s\<^sub>1' where
c: "(c,s) \<Rightarrow> s\<^sub>1'" and
w: "(WHILE b DO c,s\<^sub>1') \<Rightarrow> t'"
by auto
from c IHc have "s\<^sub>1' = s\<^sub>1" by blast
with w IHw show "t' = t" by blast
-qed blast+ -- "prove the rest automatically"
-text_raw{*}%endsnip*}
+qed blast+ \<comment> "prove the rest automatically"
+text_raw\<open>}%endsnip\<close>
end