Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Small_Step.thy Sprache: Isabelle

Original von: Isabelle^©

section "Small-Step Semantics of Commands"

theory Small_Step imports Star Big_Step begin

subsection "The transition relation"

inductive
  small_step :: "com * state \ com * state \ bool" (infix "\" 55)
where
Assign:  "(x ::= a, s) \ (SKIP, s(x := aval a s))" |

Seq1:    "(SKIP;;c\<^sub>2,s) \ (c\<^sub>2,s)" |
Seq2:    "(c\<^sub>1,s) \ (c\<^sub>1',s') \ (c\<^sub>1;;c\<^sub>2,s) \ (c\<^sub>1';;c\<^sub>2,s')" |

IfTrue:  "bval b s \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>1,s)" |
IfFalse: "\bval b s \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>2,s)" |

While:   "(WHILE b DO c,s) \
            (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"

abbreviation
  small_steps :: "com * state \ com * state \ bool" (infix "\*" 55)
where "x \* y == star small_step x y"

subsection\<open>Executability\<close>

code_pred small_step .

values "{(c',map t [''x'',''y'',''z'']) |c' t.
   (''x'' ::= V ''z'';; ''y'' ::= V ''x'',
    <''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"

subsection\<open>Proof infrastructure\<close>

subsubsection\<open>Induction rules\<close>

text\<open>The default induction rule @{thm[source] small_step.induct} only works
for lemmas of the form \<open>a \<rightarrow> b \<Longrightarrow> \<dots>\<close> where \<open>a\<close> and \<open>b\<close> are
not already pairs \<open>(DUMMY,DUMMY)\<close>. We can generate a suitable variant
of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments
\<open>\<rightarrow>\<close> into pairs:\<close>
lemmas small_step_induct = small_step.induct[split_format(complete)]

subsubsection\<open>Proof automation\<close>

declare small_step.intros[simp,intro]

text\<open>Rule inversion:\<close>

inductive_cases SkipE[elim!]: "(SKIP,s) \ ct"
thm SkipE
inductive_cases AssignE[elim!]: "(x::=a,s) \ ct"
thm AssignE
inductive_cases SeqE[elim]: "(c1;;c2,s) \ ct"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ ct"
inductive_cases WhileE[elim]: "(WHILE b DO c, s) \ ct"

text\<open>A simple property:\<close>
lemma deterministic:
  "cs \ cs' \ cs \ cs'' \ cs'' = cs'"
apply(induction arbitrary: cs'' rule: small_step.induct)
apply blast+
done

subsection "Equivalence with big-step semantics"

lemma star_seq2: "(c1,s) \* (c1',s') \ (c1;;c2,s) \* (c1';;c2,s')"
proof(induction rule: star_induct)
  case refl thus ?case by simp
next
  case step
  thus ?case by (metis Seq2 star.step)
qed

lemma seq_comp:
  "\ (c1,s1) \* (SKIP,s2); (c2,s2) \* (SKIP,s3) \
   \<Longrightarrow> (c1;;c2, s1) \<rightarrow>* (SKIP,s3)"
by(blast intro: star.step star_seq2 star_trans)

text\<open>The following proof corresponds to one on the board where one would
show chains of \<open>\<rightarrow>\<close> and \<open>\<rightarrow>*\<close> steps.\<close>

lemma big_to_small:
  "cs \ t \ cs \* (SKIP,t)"
proof (induction rule: big_step.induct)
  fix s show "(SKIP,s) \* (SKIP,s)" by simp
next
  fix x a s show "(x ::= a,s) \* (SKIP, s(x := aval a s))" by auto
next
  fix c1 c2 s1 s2 s3
  assume "(c1,s1) \* (SKIP,s2)" and "(c2,s2) \* (SKIP,s3)"
  thus "(c1;;c2, s1) \* (SKIP,s3)" by (rule seq_comp)
next
  fix s::state and b c0 c1 t
  assume "bval b s"
  hence "(IF b THEN c0 ELSE c1,s) \ (c0,s)" by simp
  moreover assume "(c0,s) \* (SKIP,t)"
  ultimately
  show "(IF b THEN c0 ELSE c1,s) \* (SKIP,t)" by (metis star.simps)
next
  fix s::state and b c0 c1 t
  assume "\bval b s"
  hence "(IF b THEN c0 ELSE c1,s) \ (c1,s)" by simp
  moreover assume "(c1,s) \* (SKIP,t)"
  ultimately
  show "(IF b THEN c0 ELSE c1,s) \* (SKIP,t)" by (metis star.simps)
next
  fix b c and s::state
  assume b: "\bval b s"
  let ?if = "IF b THEN c;; WHILE b DO c ELSE SKIP"
  have "(WHILE b DO c,s) \ (?if, s)" by blast
  moreover have "(?if,s) \ (SKIP, s)" by (simp add: b)
  ultimately show "(WHILE b DO c,s) \* (SKIP,s)" by(metis star.refl star.step)
next
  fix b c s s' t
  let ?w  = "WHILE b DO c"
  let ?if = "IF b THEN c;; ?w ELSE SKIP"
  assume w: "(?w,s') \* (SKIP,t)"
  assume c: "(c,s) \* (SKIP,s')"
  assume b: "bval b s"
  have "(?w,s) \ (?if, s)" by blast
  moreover have "(?if, s) \ (c;; ?w, s)" by (simp add: b)
  moreover have "(c;; ?w,s) \* (SKIP,t)" by(rule seq_comp[OF c w])
  ultimately show "(WHILE b DO c,s) \* (SKIP,t)" by (metis star.simps)
qed

text\<open>Each case of the induction can be proved automatically:\<close>
lemma  "cs \ t \ cs \* (SKIP,t)"
proof (induction rule: big_step.induct)
  case Skip show ?case by blast
next
  case Assign show ?case by blast
next
  case Seq thus ?case by (blast intro: seq_comp)
next
  case IfTrue thus ?case by (blast intro: star.step)
next
  case IfFalse thus ?case by (blast intro: star.step)
next
  case WhileFalse thus ?case
    by (metis star.step star_step1 small_step.IfFalse small_step.While)
next
  case WhileTrue
  thus ?case
    by(metis While seq_comp small_step.IfTrue star.step[of small_step])
qed

lemma small1_big_continue:
  "cs \ cs' \ cs' \ t \ cs \ t"
apply (induction arbitrary: t rule: small_step.induct)
apply auto
done

lemma small_to_big:
  "cs \* (SKIP,t) \ cs \ t"
apply (induction cs "(SKIP,t)" rule: star.induct)
apply (auto intro: small1_big_continue)
done

text \<open>
  Finally, the equivalence theorem:
\<close>
theorem big_iff_small:
  "cs \ t = cs \* (SKIP,t)"
by(metis big_to_small small_to_big)

subsection "Final configurations and infinite reductions"

definition "final cs \ \(\cs'. cs \ cs')"

lemma finalD: "final (c,s) \ c = SKIP"
apply(simp add: final_def)
apply(induction c)
apply blast+
done

lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
by (metis SkipE finalD final_def)

text\<open>Now we can show that \<open>\<Rightarrow>\<close> yields a final state iff \<open>\<rightarrow>\<close>
terminates:\<close>

lemma big_iff_small_termination:
  "(\t. cs \ t) \ (\cs'. cs \* cs' \ final cs')"
by(simp add: big_iff_small final_iff_SKIP)

text\<open>This is the same as saying that the absence of a big step result is
equivalent with absence of a terminating small step sequence, i.e.\ with
nontermination.  Since \<open>\<rightarrow>\<close> is determininistic, there is no difference
between may and must terminate.\<close>

end

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.