theory ex05_tmpl_reduced imports "~~/src/HOL/IMP/BExp" "~~/src/HOL/IMP/Star" begin (****************************************) (** Com.thy **) (****************************************) datatype com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;;/ _" [60, 61] 60) | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) | Or com com | Assume bexp (****************************************) (** Big_Step.thy **) (****************************************) subsection "Big-Step Semantics of Commands" text {* The big-step semantics is a straight-forward inductive definition with concrete syntax. Note that the first paramenter is a tuple, so the syntax becomes @{text "(c,s) \ s'"}. *} inductive big_step :: "com \ state \ state \ bool" (infix "\" 55) where Skip: "(SKIP,s) \ s" | Assign: "(x ::= a,s) \ s(x := aval a s)" | Seq: "\ (c\<^sub>1,s\<^sub>1) \ s\<^sub>2; (c\<^sub>2,s\<^sub>2) \ s\<^sub>3 \ \ (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \ s\<^sub>3" | IfTrue: "\ bval b s; (c\<^sub>1,s) \ t \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ t" | IfFalse: "\ \bval b s; (c\<^sub>2,s) \ t \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ t" | WhileFalse: "\bval b s \ (WHILE b DO c,s) \ s" | WhileTrue: "\ bval b s\<^sub>1; (c,s\<^sub>1) \ s\<^sub>2; (WHILE b DO c, s\<^sub>2) \ s\<^sub>3 \ \ (WHILE b DO c, s\<^sub>1) \ s\<^sub>3" | Or1: "\ (c1,s) \ s' \ \ (Or c1 c2, s) \ s'" | Or2: "\ (c2,s) \ s' \ \ (Or c1 c2, s) \ s'" | Assume: "\ bval b s \ \ (Assume b,s) \ s" text{* Proof automation: *} text {* 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. *} declare big_step.intros [intro] text{* The standard induction rule @{thm [display] big_step.induct [no_vars]} *} thm big_step.induct text{* 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: *} lemmas big_step_induct = big_step.induct[split_format(complete)] thm big_step_induct text {* @{thm [display] big_step_induct [no_vars]} *} subsection "Rule inversion" text{* What can we deduce from @{prop "(SKIP,s) \ t"} ? That @{prop "s = t"}. This is how we can automatically prove it: *} inductive_cases SkipE[elim!]: "(SKIP,s) \ t" thm SkipE text{* 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: *} inductive_cases AssignE[elim!]: "(x ::= a,s) \ t" thm AssignE inductive_cases SeqE[elim!]: "(c1;;c2,s1) \ s3" thm SeqE inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ t" thm IfE inductive_cases WhileE[elim]: "(WHILE b DO c,s) \ t" thm WhileE text{* Only [elim]: [elim!] would not terminate. *} inductive_cases OrE[elim!]: "(Or b1 b2,s) \ t" inductive_cases AssumeE[elim!]: "(Assume b,s) \ t" (****************************************) (** Small_Step.thy **) (****************************************) subsection "The transition relation" text_raw{*\snip{SmallStepDef}{0}{2}{% *} 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)" | Or1: "(Or c1 c2,s) \ (c1,s)" | Or2: "(Or c1 c2,s) \ (c2,s)" | Assume: "bval b s \ (Assume b,s) \ (SKIP,s)" text_raw{*}%endsnip*} abbreviation small_steps :: "com * state \ com * state \ bool" (infix "\*" 55) where "x \* y == star small_step x y" subsection{* Proof infrastructure *} subsubsection{* Induction rules *} text{* The default induction rule @{thm[source] small_step.induct} only works for lemmas of the form @{text"a \ b \ \"} where @{text a} and @{text b} are not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments @{text"\"} into pairs: *} lemmas small_step_induct = small_step.induct[split_format(complete)] subsubsection{* Proof automation *} declare small_step.intros[simp,intro] text{* Rule inversion: *} inductive_cases ssSkipE[elim!]: "(SKIP,s) \ ct" thm ssSkipE inductive_cases ssAssignE[elim!]: "(x::=a,s) \ ct" thm ssAssignE inductive_cases ssSeqE[elim]: "(c1;;c2,s) \ ct" thm ssSeqE inductive_cases ssIfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ ct" inductive_cases ssWhileE[elim]: "(WHILE b DO c, s) \ ct" inductive_cases ssOrE[elim!]: "(Or c1 c2,s) \ ct" inductive_cases ssAssumeE[elim!]: "(Assume b,s) \ ct" 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) \ \ (c1;;c2, s1) \* (SKIP,s3)" by(blast intro: star.step star_seq2 star_trans) text{* The following proof corresponds to one on the board where one would show chains of @{text "\"} and @{text "\*"} steps. *} text{* Each case of the induction can be proved automatically: *} lemma big_to_small: "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]) next case Or1 thus ?case by (metis small_step.Or1 star.simps) next case Or2 thus ?case by (metis small_step.Or2 star.simps) next case Assume thus ?case by fast qed lemma small1_big_continue: "cs \ cs' \ cs' \ t \ cs \ t" apply (induction arbitrary: t rule: small_step.induct) apply auto done lemma small_big_continue: "cs \* cs' \ cs' \ t \ cs \ t" apply (induction rule: star.induct) apply (auto intro: small1_big_continue) done lemma small_to_big: "cs \* (SKIP,t) \ cs \ t" by (metis small_big_continue Skip) text {* Finally, the equivalence theorem: *} 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 \ \(EX cs'. cs \ cs')" lemma finalD: "final (c,s) \ c = SKIP \ (\b. c=Assume b \ \ bval b s)" apply(simp add: final_def) apply(induction c) apply blast+ try done lemma final_iff_SKIP: "final (c,s) = (c = SKIP)" by (metis ssSkipE finalD final_def) text{* Now we can show that @{text"\"} yields a final state iff @{text"\"} terminates: *} lemma big_iff_small_termination: "(EX t. cs \ t) \ (EX cs'. cs \* cs' \ final cs')" by(simp add: big_iff_small final_iff_SKIP) text{* 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 @{text"\"} is determininistic, there is no difference between may and must terminate. *} end