src/HOL/IMP/Compiler.thy

 (* Author: Tobias Nipkow and Gerwin Klein *)
 
 header "Compiler for IMP"
 
-theory Compiler imports Big_Step 
+theory Compiler imports Big_Step Star
 begin
 
 subsection "List setup"
 
 text {* 

      ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
 where
   "P \<turnstile> c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"
 
+(*
 declare exec1_def [simp]
+*)
 
 lemma exec1I [intro, code_pred_intro]:
   "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
   \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
-by simp
-
-inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
-   ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
+by (simp add: exec1_def)
+
+abbreviation 
+  exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
 where
-refl: "P \<turnstile> c \<rightarrow>* c" |
-step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
-
-declare refl[intro] step[intro]
-
-lemmas exec_induct = exec.induct[split_format(complete)]
-
-code_pred exec by fastforce
+  "exec P \<equiv> star (exec1 P)"
+
+declare star.step[intro]
+
+lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
+
+code_pred exec1 by (metis exec1_def)
 
 values
   "{(i,map t [''x'',''y''],stk) | i t stk.
     [LOAD ''y'', STORE ''x''] \<turnstile>
     (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
 
 
 subsection{* Verification infrastructure *}
 
-lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
-by (induction rule: exec.induct) fastforce+
-
 text{* Below we need to argue about the execution of code that is embedded in
 larger programs. For this purpose we show that execution is preserved by
 appending code to the left or right of a program. *}
 
 lemma iexec_shift [simp]: 
   "((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))"
 by(auto split:instr.split)
 
 lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
-by auto
+by (auto simp: exec1_def)
 
 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
-by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+
+by (induction rule: star.induct) (fastforce intro: exec1_appendR)+
 
 lemma exec1_appendL:
   fixes i i' :: int 
   shows
   "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
    P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
+  unfolding exec1_def
   by (auto split: instr.split)
 
 lemma exec_appendL:
   fixes i i' :: int 
   shows

  size P \<le> i' \<Longrightarrow>
  P' \<turnstile>  (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
  j'' = size P + i''
  \<Longrightarrow>
  P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
-by(metis exec_trans[OF exec_appendR exec_appendL_if])
+by(metis star_trans[OF exec_appendR exec_appendL_if])
 
 
 declare Let_def[simp]
 
 

   have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
     using Seq.IH(1) by fastforce
   moreover
   have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
     using Seq.IH(2) by fastforce
-  ultimately show ?case by simp (blast intro: exec_trans)
+  ultimately show ?case by simp (blast intro: star_trans)
 next
   case (WhileTrue b s1 c s2 s3)
   let ?cc = "ccomp c"
   let ?cb = "bcomp b False (size ?cc + 1)"
   let ?cw = "ccomp(WHILE b DO c)"

   moreover
   have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
     by fastforce
   moreover
   have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
-  ultimately show ?case by(blast intro: exec_trans)
+  ultimately show ?case by(blast intro: star_trans)
 qed fastforce+
 
 end