# HG changeset patch
# User kleing
# Date 1375978392 -7200
# Node ID c10bd1f49ff5b4dc5b72a1aeadd116dad8a8597d
# Parent  7a1537b54f1614233f84815a843c46f293e2f17d
avoid re-inventing transitive closure

diff -r 7a1537b54f16 -r c10bd1f49ff5 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Aug 08 16:38:50 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Aug 08 18:13:12 2013 +0200
@@ -2,7 +2,7 @@
 
 header "Compiler for IMP"
 
-theory Compiler imports Big_Step 
+theory Compiler imports Big_Step Star
 begin
 
 subsection "List setup"
@@ -63,24 +63,25 @@
   "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
+by (simp add: exec1_def)
 
-inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
-   ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
+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''"
+  "exec P \<equiv> star (exec1 P)"
+
+declare star.step[intro]
 
-declare refl[intro] step[intro]
+lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
 
-lemmas exec_induct = exec.induct[split_format(complete)]
-
-code_pred exec by fastforce
+code_pred exec1 by (metis exec1_def)
 
 values
   "{(i,map t [''x'',''y''],stk) | i t stk.
@@ -90,9 +91,6 @@
 
 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. *}
@@ -102,16 +100,17 @@
 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:
@@ -154,7 +153,7 @@
  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]
@@ -237,7 +236,7 @@
   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"
@@ -253,7 +252,7 @@
     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
diff -r 7a1537b54f16 -r c10bd1f49ff5 src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Thu Aug 08 16:38:50 2013 +0200
+++ b/src/HOL/IMP/Compiler2.thy	Thu Aug 08 18:13:12 2013 +0200
@@ -50,7 +50,7 @@
 
 lemma exec_exec_n:
   "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
-  by (induct rule: exec.induct) (auto simp del: exec1_def intro: exec_Suc)
+  by (induct rule: star.induct) (auto intro: exec_Suc)
     
 lemma exec_eq_exec_n:
   "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')"
@@ -58,7 +58,7 @@
 
 lemma exec_n_Nil [simp]:
   "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
-  by (induct k) auto
+  by (induct k) (auto simp: exec1_def)
 
 lemma exec1_exec_n [intro!]:
   "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
@@ -75,7 +75,7 @@
 
 lemma exec1_end:
   "size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
-  by auto
+  by (auto simp: exec1_def)
 
 lemma exec_n_end:
   "size P <= (n::int) \<Longrightarrow> 
@@ -262,7 +262,7 @@
   shows
   "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow> 
   c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
-  by (auto split: instr.splits)
+  by (auto split: instr.splits simp: exec1_def)
 
 lemma exec_n_split:
   fixes i j :: int
@@ -304,7 +304,7 @@
     assume "j0 \<notin> {0 ..< size c}"
     moreover
     from c j0 have "j0 \<in> succs c 0"
-      by (auto dest: succs_iexec1 simp del: iexec.simps)
+      by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
     ultimately
     have "j0 \<in> exits c" by (simp add: exits_def)
     with c j0 rest
@@ -343,7 +343,8 @@
   have "n = size P1 + (n - size P1)" by simp 
   then obtain n' :: int where "n = size P1 + n'" ..
   ultimately 
-  show ?thesis using assms by (clarsimp simp del: iexec.simps)
+  show ?thesis using assms 
+    by (clarsimp simp: exec1_def simp del: iexec.simps)
 qed
 
 lemma exec_n_drop_left:
@@ -365,7 +366,7 @@
     by (rule exec1_drop_left)
   moreover
   then have "i' - size P \<in> succs P' 0"
-    by (fastforce dest!: succs_iexec1 simp del: iexec.simps)
+    by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
   with `exits P' \<subseteq> {0..}`
   have "size P \<le> i'" by (auto simp: exits_def)
   from rest this `exits P' \<subseteq> {0..}`     
@@ -438,8 +439,8 @@
        "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
     by (auto dest!: exec_n_split_full)
 
-  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
-qed (auto simp: exec_n_simps)
+  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def)
+qed (auto simp: exec_n_simps exec1_def)
 
 lemma bcomp_split:
   fixes i j :: int
@@ -460,7 +461,7 @@
          s' = s \<and> stk' = stk"
 using assms proof (induction b arbitrary: c j i n s' stk')
   case Bc thus ?case 
-    by (simp split: split_if_asm add: exec_n_simps)
+    by (simp split: split_if_asm add: exec_n_simps exec1_def)
 next
   case (Not b) 
   from Not.prems show ?case
@@ -488,7 +489,7 @@
     by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
 next
   case Less
-  thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) 
+  thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *) 
 qed
 
 lemma ccomp_empty [elim!]:
@@ -506,7 +507,7 @@
 next
   case (Assign x a)
   thus ?case
-    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
+    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps exec1_def)
 next
   case (Seq c1 c2)
   thus ?case by (fastforce dest!: exec_n_split_full)
@@ -542,7 +543,8 @@
     show ?thesis
       by simp
          (fastforce dest: exec_n_drop_right 
-                   split: split_if_asm simp: exec_n_simps)
+                   split: split_if_asm
+                   simp: exec_n_simps exec1_def)
   next
     case False with cs'
     show ?thesis
@@ -583,7 +585,7 @@
         obtain m where
           "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')"
           "m < n"
-          by (auto simp: exec_n_step [where k=k])
+          by (auto simp: exec_n_step [where k=k] exec1_def)
         with "1.IH"
         show ?case by blast
       next
@@ -603,7 +605,7 @@
         obtain k' where
           "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')"
           "k' < n"
-          by (auto simp: exec_n_step [where k=m])
+          by (auto simp: exec_n_step [where k=m] exec1_def)
         with "1.IH"
         have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
         ultimately