# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360571508 0
# Node ID 99a180fd4194b1a7959e2b36995ccac9402b6b43
# Parent  582916f289ea2b6c81a124fde5966ab44d6fdf69
removed some dead code

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"
diff -r 582916f289ea -r 99a180fd4194 thys/Rec_Def.thy
--- a/thys/Rec_Def.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/Rec_Def.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -2,42 +2,26 @@
 imports Main
 begin
 
-section {*
-  Recursive functions
-*}
-
-text {*
-  Datatype of recursive operators.
-*}
+section {* Recursive functions *}
 
 datatype recf = 
- -- {* The zero function, which always resturns @{text "0"} as result. *}
-  z | 
- -- {* The successor function, which increments its arguments. *}
-  s | 
- -- {*
-  The projection function, where @{text "id i j"} returns the @{text "j"}-th
-  argment out of the @{text "i"} arguments.
-  *}
+  z | s | 
+  -- {* The projection function, where @{text "id i j"} returns the @{text "j"}-th
+  argment out of the @{text "i"} arguments. *}
   id nat nat | 
- -- {*
-  The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} 
+  -- {* The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} 
   computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , 
-  gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}.
-  *}
+  gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. *}
   Cn nat recf "recf list" | 
--- {*
-  The primitive resursive operator, where @{text "Pr n f g"} computes:
+  -- {* The primitive resursive operator, where @{text "Pr n f g"} computes:
   @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"} 
   and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k, 
-                                                  Pr n f g (x1, \<dots>, xn-1, k))"}.
+                                            Pr n f g (x1, \<dots>, xn-1, k))"}.
   *}
   Pr nat recf recf | 
--- {*
-  The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} 
+  -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} 
   computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all
-  @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}.
-  *}
+  @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *}
   Mn nat recf 
 
 text {* 
@@ -72,8 +56,7 @@
              \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk> 
             \<Longrightarrow> rec_calc_rel (Mn n f) args r" 
 
-inductive_cases calc_pr_reverse:
-              "rec_calc_rel (Pr n f g) (lm) rSucy"
+inductive_cases calc_pr_reverse: "rec_calc_rel (Pr n f g) (lm) rSucy"
 
 inductive_cases calc_z_reverse: "rec_calc_rel z lm x"
 
diff -r 582916f289ea -r 99a180fd4194 thys/Recursive.thy
--- a/thys/Recursive.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/Recursive.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -2,9 +2,7 @@
 imports Rec_Def Abacus
 begin
 
-section {* 
-  Compiling from recursive functions to Abacus machines
-  *}
+section {* Compiling from recursive functions to Abacus machines *}
 
 text {*
   Some auxilliary Abacus machines used to construct the result Abacus machines.
@@ -24,8 +22,7 @@
 
 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
-  "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, 
-                       Inc m, Goto 4]"
+  "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
 
 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
@@ -47,25 +44,18 @@
   "abc_append al bl = (let al_len = length al in 
                            al @ abc_shift bl al_len)"
 
-text {*
-  The compilation of @{text "z"}-operator.
-*}
+text {* The compilation of @{text "z"}-operator. *}
 definition rec_ci_z :: "abc_inst list"
   where
   "rec_ci_z \<equiv> [Goto 1]"
 
-text {*
-  The compilation of @{text "s"}-operator.
-*}
+text {* The compilation of @{text "s"}-operator. *}
 definition rec_ci_s :: "abc_inst list"
   where
   "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
 
 
-text {*
-  The compilation of @{text "id i j"}-operator
-*}
-
+text {* The compilation of @{text "id i j"}-operator *}
 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
   where
   "rec_ci_id i j = addition j i (i + 1)"
@@ -73,8 +63,7 @@
 fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
   where
   "mv_boxes ab bb 0 = []" |
-  "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n)
-  (bb + n)"
+  "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) (bb + n)"
 
 fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
   where
@@ -94,7 +83,7 @@
   The compiler of recursive functions, where @{text "rec_ci recf"} return 
   @{text "(ap, arity, fp)"}, where @{text "ap"} is the Abacus program, @{text "arity"} is the 
   arity of the recursive function @{text "recf"}, 
-@{text "fp"} is the amount of memory which is going to be
+  @{text "fp"} is the amount of memory which is going to be
   used by @{text "ap"} for its execution. 
 *}
 
@@ -127,11 +116,10 @@
          (let (fprog, fpara, fn) = rec_ci f in 
           let len = length (fprog) in 
             (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
-             Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn) )"
+             Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"
   by pat_completeness auto
 termination 
 proof
-term size
   show "wf (measure size)" by auto
 next
   fix n f gs x
@@ -154,8 +142,6 @@
         mv_boxes.simps[simp del] abc_append.simps[simp del]
         mv_box.simps[simp del] addition.simps[simp del]
   
-thm rec_calc_rel.induct
-
 declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] 
         abc_step_l.simps[simp del] 
 
@@ -797,12 +783,6 @@
 apply(arith)
 done
 
-(*
-lemma pr_para_ge_suc0: "rec_calc_rel (Pr n f g) lm xs \<Longrightarrow> 0 < n"
-apply(erule calc_pr_reverse, simp, simp)
-done
-*)
-
 lemma ci_pr_para_eq: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)
                   \<Longrightarrow> rs_pos = Suc n"
 apply(simp add: rec_ci.simps)
@@ -1443,7 +1423,6 @@
   \<exists> stp. (\<lambda> (as, lm). as = 3 \<and> 
   mv_box_inv (as, lm) m n initlm) 
              (abc_steps_l (0::nat, initlm) (mv_box m n) stp)"
-thm halt_lemma2
 apply(insert halt_lemma2[of mv_box_LE
     "\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm"
     "\<lambda> stp. (abc_steps_l (0, initlm) (Recursive.mv_box m n) stp, m)"
@@ -1539,12 +1518,6 @@
 apply(arith)
 done
 
-thm nth_replicate
-(*
-lemma exp_nth[simp]: "n < m \<Longrightarrow> a\<up>m ! n = a"
-apply(sim)
-done
-*)
 lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < n \<Longrightarrow> 
                       lm[n - Suc 0 := 0::nat] = butlast lm @ [0]"
 apply(auto)
@@ -1938,8 +1911,6 @@
     done
 qed
 
-thm rec_calc_rel.induct
-
 lemma eq_switch: "x = y \<Longrightarrow> y = x"
 by simp
 
@@ -1956,14 +1927,7 @@
   "rec_ci (Mn n f) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n"
 apply(case_tac "rec_ci f", simp add: rec_ci.simps)
 done
-(*
-lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> aa = Suc rs_pos"
-apply(rule_tac calc_mn_reverse, simp)
-apply(insert para_pattern [of f a aa ba "lm @ [rs]" 0], simp)
-apply(subgoal_tac "rs_pos = length lm", simp)
-apply(drule_tac ci_mn_para_eq, simp)
-done
-*)
+
 lemma [simp]: "rec_ci f = (a, aa, ba) \<Longrightarrow> aa < ba"
 apply(simp add: ci_ad_ge_paras)
 done
@@ -2057,7 +2021,6 @@
                      ((nat \<times> nat list) \<times> nat \<times> nat)) set"
   where "mn_LE \<equiv> (inv_image lex_triple mn_measure)"
 
-thm halt_lemma2
 lemma wf_mn_le[intro]: "wf mn_LE"
 by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def)
 
@@ -2078,7 +2041,6 @@
 apply(erule_tac rec_ci_not_null)
 done
 
-thm rec_ci.simps
 lemma [simp]: 
   "\<lbrakk>rec_ci f = (a, aa, ba); 
     rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
@@ -2189,14 +2151,6 @@
                 Suc (a_md - Suc (Suc rs_pos)) = a_md - Suc rs_pos"
 by arith
 
-term rec_ci
-(*
-lemma [simp]: "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk>  \<Longrightarrow> Suc rs_pos < a_md"
-apply(case_tac "rec_ci f")
-apply(subgoal_tac "c > b \<and> b = Suc rs_pos \<and> a_md \<ge> c")
-apply(arith, auto)
-done
-*)
 lemma mn_ind_step: 
   assumes ind:  
   "\<And>aprog a_md rs_pos rs suf_lm lm.
@@ -2212,7 +2166,6 @@
          "aa = Suc rs_pos"
   shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm) 
              aprog stp = (0, lm @ Suc x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
-thm abc_add_exc1
 proof -
   have k1: 
     "\<exists> stp. abc_steps_l (0, lm @ x #  0\<up>(a_md - Suc (rs_pos)) @ suf_lm)
@@ -2349,7 +2302,6 @@
   from h and ind have k1:
     "\<exists>stp.  abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) 
         aprog stp = (length a,  lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
-    thm mn_calc_f
     apply(insert mn_calc_f[of f a aa ba n aprog 
                                rs_pos a_md lm rs 0 suf_lm], simp)
     apply(subgoal_tac "aa = Suc n", simp add: exponent_cons_iff)
@@ -2397,7 +2349,6 @@
   hence k1:
     "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog
                   stp = (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
-    thm mn_ind_steps
     apply(auto intro: mn_ind_steps ind)
     done
   from h have k2: 
@@ -2502,8 +2453,6 @@
 apply(rule_tac x = "lm ! m" in exI, simp)
 done
 
-thm addition.simps
-
 lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
 by(simp add: abc_fetch.simps addition.simps)
 
@@ -2845,7 +2794,6 @@
         (\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list),
              lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
     apply(simp add: cn_merge_gs_tl_app)
-    thm abc_append_exc2
     apply(rule_tac as = 
   "(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list"    
       and bm = "lm @ 0\<up>(pstr - n) @ butlast ys @ 
@@ -3036,22 +2984,6 @@
        "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp)
     done
 qed
-(*    
-lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; 
-                ba < aa; 
-               length lm2 = aa - Suc (ba + n)\<rbrakk>
-      \<Longrightarrow> ((0::nat) # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa - ba)
-         = last lm3"
-proof -
-  assume h: "Suc n \<le> aa - ba"
-    and g: " ba < aa" "length lm2 = aa - Suc (ba + n)"
-  from h and g have k: "aa - ba = Suc (length lm2 + n)"
-    by arith
-  thus "((0::nat) # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa - ba) = last lm3"
-    apply(simp,  simp add: nth_append)
-    done
-qed
-*)
 
 lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba; 
         length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk>
@@ -3152,7 +3084,6 @@
                0\<up>(a_md - pstr - length ys) @ suf_lm) 
                  (mv_boxes 0 (pstr + Suc (length ys)) n) stp
         = (3 * n, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
-thm mv_boxes_ex
 apply(insert mv_boxes_ex[of n "pstr + Suc (length ys)" 0 "[]" "lm" 
          "0\<up>(pstr - n) @ ys @ [0]" "0\<up>(a_md - pstr - length ys - n - Suc 0) @ suf_lm"], simp)
 apply(erule_tac exE, rule_tac x = stp in exI,
@@ -3361,7 +3292,6 @@
    \<exists>stp. abc_steps_l (0, 0\<up>pstr @ ys @ 0 # lm @  0\<up>(a_md - Suc (pstr + length ys + n)) @
           suf_lm) (mv_boxes pstr 0 (length ys)) stp =
   (3 * length ys, ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
-thm mv_boxes_ex2
 apply(insert mv_boxes_ex2[of "length ys" "pstr" 0 "[]"
      "0\<up>(pstr - length ys)" "ys" 
      "0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm"], 
@@ -3431,7 +3361,6 @@
     "rec_ci f = (a, aa, ba)"
     and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                                          (map rec_ci (f # gs))))"
-  thm rec_ci.simps
   from h and g have k1:
     "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 
     (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
@@ -3473,8 +3402,6 @@
   qed
 qed
 
-thm rec_ci.simps 
-
 lemma calc_f_prog_ex: 
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
     rec_ci f = (a, aa, ba);
@@ -3647,7 +3574,6 @@
   ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys @ lm @ 
                                0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
 proof -
-  thm rec_ci.simps
   from h and pdef have k1: 
     "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
     length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
@@ -3927,7 +3853,6 @@
                          lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)
   aprog stp = (ss + 3 * n, lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)"
 proof -
-  thm rec_ci.simps
   from h and pdef and starts have k1:
     "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
                      bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n"
@@ -3996,13 +3921,11 @@
     apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs)
     apply(rule_tac ind, auto)
     done  
-  thm rec_ci.simps
   from g have k2: 
     "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs,  lm @ 
         0\<up>(?pstr - n) @ ys @ 0\<up>(a_md - ?pstr - length ys) @ suf_lm) aprog stp = 
     (?gs_len + 3 * length gs + 3 * n, 0\<up>?pstr @ ys @ 0 # lm @ 
                               0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)"
-    thm save_paras
     apply(erule_tac ba = c in save_paras, auto intro: ci_cn_para_eq)
     done
   from g have k3: 
@@ -4022,7 +3945,6 @@
    ys @ rs # 0\<up>?pstr  @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)"
     apply(rule_tac ba = c in calc_cn_f, rule_tac ind, auto)
     done
-thm rec_ci.simps
   from g h have k5:
     "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a,
     ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)
@@ -4207,7 +4129,6 @@
     "p = ap [+] bp [+] cp"
   have "\<exists> stp. (abc_steps_l (0, am) p stp) = (length ap, lm)"
     using h
-    thm abc_add_exc1
     apply(simp add: abc_append.simps)
     apply(rule_tac abc_add_exc1, auto)
     done
@@ -4267,7 +4188,6 @@
             "rec_ci rf = (aprog, rs_pos, a_md)"
             "rec_ci f = (aprog', rs_pos', a_md')" 
             "\<forall>y. \<exists>rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0" "length lm = n"
-  thm mn_ind_step
   have "\<exists>stpa \<ge> stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog stpa 
          = (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
   proof(induct stp, auto)
@@ -4441,7 +4361,6 @@
     apply(rule_tac A = "set (take i gs)" in subsetD, 
       simp add: set_take_subset, simp)
     done
-  thm cn_merge_gs.simps
   from this obtain stpa where g2: 
     "abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) 
     (cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa =
@@ -4510,7 +4429,6 @@
       apply(rule_tac Max_ge, simp, simp)
       apply(rule_tac disjI2)
       using h2
-      thm rev_image_eqI
       apply(rule_tac x = "gs!i" in rev_image_eqI, simp, simp)
       done
   next
@@ -4770,8 +4688,6 @@
   assume h: "rec_calc_rel recf args r"  
     "abc_steps_l (0, args) ap stp = (length ap, lm')" 
     "abc_list_crsp lm' (args @ r # 0\<up>m)"
-  thm abc_append_exc2
-  thm abc_lm_s.simps
   have "\<exists>stp. abc_steps_l (0, args) (ap [+] 
     (dummy_abc (length args))) stp = (length ap + 3, 
     abc_lm_s lm' (length args) (abc_lm_v lm' (length args)))"
diff -r 582916f289ea -r 99a180fd4194 thys/UF.thy
--- a/thys/UF.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/UF.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -14,10 +14,6 @@
 subsection {* The construction of component functions *}
 
 text {*
-  This section constructs a set of component functions used to construct @{text "rec_F"}.
-  *}
-
-text {*
   The recursive function used to do arithmatic addition.
 *}
 definition rec_add :: "recf"
@@ -2428,7 +2424,6 @@
      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]],
      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],
      Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"
-  thm embranch_lemma
   have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
                          = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
     apply(rule_tac embranch_lemma )
@@ -2644,8 +2639,6 @@
   where
   "rght c = lo c (Pi 2)"
 
-thm Prime.simps
-
 fun inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "inpt m xs = trpl 0 1 (strt xs)"
@@ -3103,7 +3096,6 @@
         apply(rule_tac calc_pr_zero, simp)
         using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"]
         apply(simp add: rec_exec.simps, simp, simp, simp)
-        thm calc_pr_ind
         apply(rule_tac rk = "rec_exec (Pr n f g)
                (butlast xs@[last xs - Suc 0])" in calc_pr_ind)
         using ind2[of "rec_exec (Pr n f g)
@@ -3540,7 +3532,6 @@
 subsection {* Relating interperter functions to the execution of TMs *}
 
 lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
-term trpl
 
 lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
 apply(simp add: fetch.simps)
@@ -3586,7 +3577,6 @@
 apply(simp)
 done
 
-term set_of
 lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
 proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
       rule_tac classical, simp)
diff -r 582916f289ea -r 99a180fd4194 thys/UTM.thy
--- a/thys/UTM.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/UTM.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -5,17 +5,27 @@
 section {* Wang coding of input arguments *}
 
 text {*
-  The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2,
-  where the first argument represents the Godel coding of the TM being simulated and the second argument represents the right number (in Wang's coding) of the TM tape. 
-  (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may
-  very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential 
-  composition of these two TMs will give rise to the UTM we are seeking. The purpose of this initialization TM is to transform the multiple 
-  input arguments of the TM being simulated into Wang's coding, so that it can be consumed by the TM compiled from @{text "rec_F"} as the second
-  argument. 
-
-  However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive 
-  function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into 
-  Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions.
+  The direct compilation of the universal function @{text "rec_F"} can
+  not give us UTM, because @{text "rec_F"} is of arity 2, where the
+  first argument represents the Godel coding of the TM being simulated
+  and the second argument represents the right number (in Wang's
+  coding) of the TM tape.  (Notice, left number is always @{text "0"}
+  at the very beginning). However, UTM needs to simulate the execution
+  of any TM which may very well take many input arguments. Therefore,
+  a initialization TM needs to run before the TM compiled from @{text
+  "rec_F"}, and the sequential composition of these two TMs will give
+  rise to the UTM we are seeking. The purpose of this initialization
+  TM is to transform the multiple input arguments of the TM being
+  simulated into Wang's coding, so that it can be consumed by the TM
+  compiled from @{text "rec_F"} as the second argument.
+
+  However, this initialization TM (named @{text "t_wcode"}) can not be
+  constructed by compiling from any resurve function, because every
+  recursive function takes a fixed number of input arguments, while
+  @{text "t_wcode"} needs to take varying number of arguments and
+  tranform them into Wang's coding. Therefore, this section give a
+  direct construction of @{text "t_wcode"} with just some parts being
+  obtained from recursive functions.
 
 \newlength{\basewidth}
 \settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx}
@@ -71,10 +81,22 @@
 \caption{The output of TM $prepare$} \label{prepare_output}
 \end{figure}
 
-As shown in Figure \ref{prepare_input}, the input of $prepare$ is the same as the the input
-of UTM, where $m$ is the Godel coding of the TM being interpreted and $a_1$ through $a_n$ are the $n$ input arguments of the TM under interpretation. The purpose of $purpose$ is to transform this initial tape layout to the one shown in Figure \ref{prepare_output},
-which is convenient for the generation of Wang's codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$ and ends after $a_1$ is encoded. The coding result is stored in an accumulator at the end of the tape (initially represented by the $1$ two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure \ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by two blanks on both ends with the rest so that movement conditions can be implemented conveniently in subsequent TMs, because, by convention,
-two consecutive blanks are usually used to signal the end or start of a large chunk of data. The diagram of $prepare$ is given in Figure \ref{prepare_diag}.
+As shown in Figure \ref{prepare_input}, the input of $prepare$ is the
+same as the the input of UTM, where $m$ is the Godel coding of the TM
+being interpreted and $a_1$ through $a_n$ are the $n$ input arguments
+of the TM under interpretation. The purpose of $purpose$ is to
+transform this initial tape layout to the one shown in Figure
+\ref{prepare_output}, which is convenient for the generation of Wang's
+codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$
+and ends after $a_1$ is encoded. The coding result is stored in an
+accumulator at the end of the tape (initially represented by the $1$
+two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure
+\ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by
+two blanks on both ends with the rest so that movement conditions can
+be implemented conveniently in subsequent TMs, because, by convention,
+two consecutive blanks are usually used to signal the end or start of
+a large chunk of data. The diagram of $prepare$ is given in Figure
+\ref{prepare_diag}.
 
 
 \begin{figure}[h!]
@@ -840,7 +862,6 @@
 
 lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"
 by(auto intro:wf_inv_image simp: wcode_double_case_le_def )
-term fetch
 
 lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"
 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
@@ -1326,7 +1347,7 @@
         (Suc (length ap div 2), l', r')"
 proof -
   have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))"
-    thm before_final using exec
+    using exec
     by(erule_tac before_final)
   then obtain stpa where a: 
     "\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" ..
@@ -1377,7 +1398,6 @@
   hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
     (adjust t_twice_compile) stp
      = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
-    thm adjust_halt_eq
     apply(rule_tac stp = stp in adjust_halt_eq)
     apply(simp add: t_twice_compile_def, auto)
     done
@@ -3310,15 +3330,6 @@
 apply(simp add:tm_wf.simps t_wcode_prepare_def)
 done
    
-(* 
-lemma t_correct_termi: "t_correct tp \<Longrightarrow> 
-      list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (change_termi_state tp)"
-apply(auto simp: t_correct.simps List.list_all_length)
-apply(erule_tac x = n in allE, simp)
-apply(case_tac "tp!n", auto simp: change_termi_state.simps split: if_splits)
-done
-*)
-
 lemma t_correct_shift:
          "list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow>
           list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) "
@@ -3326,20 +3337,6 @@
 apply(erule_tac x = n in allE, simp add: length_shift)
 apply(case_tac "tp!n", auto simp: shift.simps)
 done
-(*
-lemma [intro]: 
-  "t_correct (tm_of abc_twice @ tMp (Suc 0) 
-        (start_of twice_ly (length abc_twice) - Suc 0))"
-apply(rule_tac t_compiled_correct, simp_all)
-apply(simp add: twice_ly_def)
-done
-
-lemma [intro]: "t_correct (tm_of abc_fourtimes @ tMp (Suc 0) 
-   (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))"
-apply(rule_tac t_compiled_correct, simp_all)
-apply(simp add: fourtimes_ly_def)
-done
-*)
 
 lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0"
 apply(auto simp: t_twice_compile_def t_fourtimes_compile_def)
@@ -3664,7 +3661,6 @@
 apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, auto)
 done
 
-thm numeral_6_eq_6
 lemma [simp]: "fetch t_wcode_adjust 6 Oc = (R, 7)"
 apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6)
 done
@@ -4665,112 +4661,6 @@
   where
   "UTM_pre = t_wcode |+| t_utm"
 
-(*
-lemma F_abc_halt_eq:
-  "\<lbrakk>Turing.t_correct tp; 
-    length lm = k;
-    steps (Suc 0, Bk\<up>(l), <lm>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n));
-    rs > 0\<rbrakk>
-    \<Longrightarrow> \<exists> stp m. abc_steps_l (0, [code tp, bl2wc (<lm>)]) (F_aprog) stp =
-                       (length (F_aprog), code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m))"
-apply(drule_tac  F_t_halt_eq, simp, simp, simp)
-apply(case_tac "rec_ci rec_F")
-apply(frule_tac abc_append_dummy_complie, simp, simp, erule_tac exE,
-      erule_tac exE)
-apply(rule_tac x = stp in exI, rule_tac x = m in exI)
-apply(simp add: F_aprog_def dummy_abc_def)
-done
-
-lemma F_abc_utm_halt_eq: 
-  "\<lbrakk>rs > 0; 
-  abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp =
-        (length F_aprog, code tp #  bl2wc (<lm>) # (rs - 1) # 0\<up>(m))\<rbrakk>
-  \<Longrightarrow> \<exists>stp m n.(steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp =
-                                             (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n)))"
-  thm abacus_turing_eq_halt
-  using abacus_turing_eq_halt
-  [of "layout_of F_aprog" "F_aprog" "F_tprog" "length (F_aprog)" 
-    "[code tp, bl2wc (<lm>)]" stp "code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m)" "Suc (Suc 0)"
-    "start_of (layout_of (F_aprog)) (length (F_aprog))" "[]" 0]
-apply(simp add: F_tprog_def t_utm_def abc_lm_v.simps nth_append)
-apply(erule_tac exE)+
-apply(rule_tac x = stpa in exI, rule_tac x = "Suc (Suc ma)" in exI, 
-       rule_tac x = l in exI, simp add: exp_ind)
-done
-
-declare tape_of_nl_abv_cons[simp del]
-
-lemma t_utm_halt_eq': 
-  "\<lbrakk>Turing.t_correct tp;
-   0 < rs;
-  steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
-  \<Longrightarrow>  \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp = 
-                                                (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-apply(drule_tac  l = l in F_abc_halt_eq, simp, simp, simp)
-apply(erule_tac exE, erule_tac exE)
-apply(rule_tac F_abc_utm_halt_eq, simp_all)
-done
-*)
-(*
-lemma [simp]: "tinres xs (xs @ Bk\<up>(i))"
-apply(auto simp: tinres_def)
-done
-
-lemma [elim]: "\<lbrakk>rs > 0; Oc\<up>(rs) @ Bk\<up>(na) = c @ Bk\<up>(n)\<rbrakk>
-        \<Longrightarrow> \<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n)"
-apply(case_tac "na > n")
-apply(subgoal_tac "\<exists> d. na = d + n", auto simp: exp_add)
-apply(rule_tac x = "na - n" in exI, simp)
-apply(subgoal_tac "\<exists> d. n = d + na", auto simp: exp_add)
-apply(case_tac rs, simp_all add: exp_ind, case_tac d, 
-           simp_all add: exp_ind)
-apply(rule_tac x = "n - na" in exI, simp)
-done
-*)
-(*
-lemma t_utm_halt_eq'': 
-  "\<lbrakk>Turing.t_correct tp;
-   0 < rs;
-   steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
-  \<Longrightarrow>  \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = 
-                                                (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-apply(drule_tac t_utm_halt_eq', simp_all)
-apply(erule_tac exE)+
-proof -
-  fix stpa ma na
-  assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))"
-  and gr: "rs > 0"
-  thus "\<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-    apply(rule_tac x = stpa in exI, rule_tac x = ma in exI,  simp)
-  proof(case_tac "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa", simp)
-    fix a b c
-    assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))"
-            "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa = (a, b, c)"
-    thus " a = 0 \<and> b = Bk\<up>(ma) \<and> (\<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n))"
-      using tinres_steps2[of "<[code tp, bl2wc (<lm>)]>" "<[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)" 
-                           "Suc 0" " [Bk, Bk]" t_utm stpa 0 "Bk\<up>(ma)" "Oc\<up>(rs) @ Bk\<up>(na)" a b c]
-      apply(simp)
-      using gr
-      apply(simp only: tinres_def, auto)
-      apply(rule_tac x = "na + n" in exI, simp add: exp_add)
-      done
-  qed
-qed
-
-lemma [simp]: "tinres [Bk, Bk] [Bk]"
-apply(auto simp: tinres_def)
-done
-
-lemma [elim]: "Bk\<up>(ma) = b @ Bk\<up>(n)  \<Longrightarrow> \<exists>m. b = Bk\<up>(m)"
-apply(subgoal_tac "ma = length b + n")
-apply(rule_tac x = "ma - n" in exI, simp add: exp_add)
-apply(drule_tac length_equal)
-apply(simp)
-done
-*)
-
-
-
 lemma tinres_step1: 
   "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); 
                  step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
@@ -5083,15 +4973,6 @@
 apply(rule_tac nonstop_t_uhalt_eq, simp_all)
 done
 
-(*
-lemma [simp]: 
-  "\<forall>j<Suc k. Ex (rec_calc_rel (get_fstn_args (Suc k) (Suc k) ! j)
-                                                     (code tp # lm))"
-apply(auto simp: get_fstn_args_nth)
-apply(rule_tac x = "(code tp # lm) ! j" in exI)
-apply(rule_tac calc_id, simp_all)
-done
-*)
 declare ci_cn_para_eq[simp]
 
 lemma F_aprog_uhalt: 
@@ -5180,7 +5061,6 @@
   \<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog 
        stp of (ss, e) \<Rightarrow> ss < length F_aprog"
 apply(case_tac "rec_ci rec_F", simp add: F_aprog_def)
-thm uabc_uhalt'
 apply(drule_tac ap = a and pos = b and md = c in uabc_uhalt', simp_all)
 proof -
   fix a b c