diff -r 582916f289ea -r 99a180fd4194 thys/Abacus.thy
--- a/thys/Abacus.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/Abacus.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -227,7 +227,6 @@
   @{text "start_of layout n"} looks out the starting state of @{text "n"}-th
   TM in the finall TM.
 *}
-thm listsum_def
 
 fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
   where
@@ -877,7 +876,6 @@
   from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp = (s'' + off, l'', r'')"
     by(erule_tac ind, simp)
   from c b h a k assms show "?case"
-    thm tm_append_second_step_eq
     apply(simp add: step_red) by(rule tm_append_second_step_eq, simp_all)
 qed
 
@@ -902,7 +900,6 @@
   and even: "length A mod 2 = 0"
   shows "steps (Suc off, l, r) (A @ shift B off, 0) stp = (0, l', r')"
 proof -
-  thm before_final
   have "\<exists>n. \<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')"
     using exec by(rule_tac before_final, simp)
  then obtain n where a: 
@@ -1508,7 +1505,6 @@
   and P: "P = (\<lambda> ((s, l, r), n). s = Suc (2 * n))"
   and Q: "Q = (\<lambda> ((s, l, r), n). findnth_inv ly n (as, lm) (s, l, r) ires)"
   shows "\<exists> stp. P (f stp) \<and> Q (f stp)"
-thm halt_lemma2
 proof(rule_tac LE = findnth_LE in halt_lemma2)
   show "wf findnth_LE"  by(intro wf_findnth_LE)
 next
@@ -2101,7 +2097,6 @@
   shows "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp 
         = (2*n + 10, Bk # Bk # ires, <lma> @ Bk\<up>k) \<and> stp > 0"
 proof -
-  thm tm_append_steps
   have "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r')
     \<and> inv_locate_a (as, lm) (n, l', r') ires"
     using assms
@@ -2349,7 +2344,6 @@
 
 lemma start_of_less_2: 
   "start_of ly e \<le> start_of ly (Suc e)"
-thm take_Suc
 apply(case_tac "e < length ly")
 apply(auto simp: start_of.simps take_Suc take_Suc_conv_app_nth)
 done
@@ -3234,7 +3228,6 @@
   from this obtain stpa la ra where a:
     "steps (start_of ly as + 2 * n, l, r) (?P, ?off) stpa = (Suc (start_of ly as) + 2*n, la, ra)
              \<and>  inv_locate_b (as, lm) (n, la, ra) ires" by blast
-  term dec_inv_1
   have "\<exists> stp lb rb. steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stp = (start_of ly e, lb, rb)
              \<and>  dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires"
     using assms a
@@ -3714,7 +3707,6 @@
 
 text{*The tp @ [(Nop, 0), (Nop, 0)] is nomoral turing machines, so we can use Hoare_plus when composing with Mop machine*}
 
-thm layout_of.simps
 lemma layout_id_cons: "layout_of (ap @ [p]) = layout_of ap @ [length_of p]"
 apply(simp add: layout_of.simps)
 done
@@ -3722,11 +3714,6 @@
 lemma [simp]: "length (layout_of xs) = length xs"
 by(simp add: layout_of.simps)
 
-thm tms_of.simps
-term ci
-thm tms_of.simps
-thm tpairs_of.simps
-
 lemma [simp]:  
   "map (start_of (layout_of xs @ [length_of x])) [0..<length xs] =  (map (start_of (layout_of xs)) [0..<length xs])"
 apply(auto)
@@ -4495,7 +4482,6 @@
 done
 
 declare mopup_inv.simps[simp del]
-term mopup_inv
 
 lemma [simp]: 
   "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> 
@@ -4534,7 +4520,6 @@
         apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)
         done
       then have "mopup_inv (a, b, c) lm n ires"
-        thm mopup_inv_steps
         using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]
         apply(simp)
         done
@@ -4641,7 +4626,6 @@
   then have b: "steps (Suc 0 + off, Bk # Bk # ires, <am> @ Bk \<up> k) (tp @ shift (mopup n) off, 0) stpb
     = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"
     using assms wf_mopup
-   thm tm_append_second_halt_eq
     apply(drule_tac tm_append_second_halt_eq, auto)
     done
   from a b show "?thesis"