# HG changeset patch
# User nipkow
# Date 1020791711 -7200
# Node ID 7275750553b7a22a42ce67bc5b792b3392d98ac6
# Parent  2d6782e717024bcdd0d0fdb65005671339de2ff0
a bit of conversion to structured proofs

diff -r 2d6782e71702 -r 7275750553b7 src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Tue May 07 15:03:50 2002 +0200
+++ b/src/HOL/IMP/Compiler0.thy	Tue May 07 19:15:11 2002 +0200
@@ -215,18 +215,24 @@
   Second proof; statement is generalized to cater for prefixes and suffixes;
   needs none of the lifting lemmas, but instantiations of pre/suffix.
   *}
-theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> 
-  !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
-apply(erule evalc.induct)
-      apply simp
-     apply(force intro!: ASIN)
-    apply(intro strip)
-    apply(erule_tac x = a in allE)
-    apply(erule_tac x = "a@compile c0" in allE)
-    apply(erule_tac x = "compile c1@z" in allE)
-    apply(erule_tac x = z in allE)
-    apply(simp add:add_assoc[THEN sym])
-    apply(blast intro:rtrancl_trans)
+
+theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+shows "\<And>a z. a@compile c@z \<turnstile> \<langle>s,size a\<rangle> -*\<rightarrow> \<langle>t,size a + size(compile c)\<rangle>"
+      (is "\<And>a z. ?P c s t a z")
+proof -
+  from A show "\<And>a z. ?thesis a z"
+  proof induct
+    case Skip thus ?case by simp
+  next
+    case Assign thus ?case by (force intro!: ASIN)
+  next
+    fix c1 c2 s s' s'' a z
+    assume IH1: "\<And>a z. ?P c1 s s' a z" and IH2: "\<And>a z. ?P c2 s' s'' a z"
+    from IH1 IH2[of "a@compile c1"]
+    show "?P (c1;c2) s s'' a z"
+      by(simp add:add_assoc[THEN sym])(blast intro:rtrancl_trans)
+  next
+(* at this point I gave up converting to structured proofs *)
 (* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
    apply(intro strip)
    (* instantiate assumption sufficiently for later: *)