# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1359151921 0
# Node ID 8dc659af1bd232a6f4c15529ce7871d956352c9f
# Parent  c470f1705baa64fdc8741a7ac3bb534446163759
simplified uncomputable-locale

diff -r c470f1705baa -r 8dc659af1bd2 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Fri Jan 25 22:03:03 2013 +0000
+++ b/thys/uncomputable.thy	Fri Jan 25 22:12:01 2013 +0000
@@ -1037,68 +1037,6 @@
 lemma [intro, simp]: "tm_wf0 dither"
 by (auto simp: tm_wf.simps dither_def)
 
-
-text {*
-  The following lemma shows the meaning of @{text "tinres"} with respect to 
-  one step execution.
-  *}
-lemma tinres_step: 
-  "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); 
-                 step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
-    \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
-apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell")
-apply(auto simp: step.simps fetch.simps
-        split: if_splits )
-apply(case_tac [!] "t ! (2 * nat)", 
-     auto simp: tinres_def split: if_splits)
-apply(case_tac [1-8] a, auto split: if_splits)
-apply(case_tac [!] "t ! (2 * nat)", 
-     auto simp: tinres_def split: if_splits)
-apply(case_tac [1-4] a, auto split: if_splits)
-apply(case_tac [!] "t ! Suc (2 * nat)", 
-     auto simp: if_splits)
-apply(case_tac [!] aa, auto split: if_splits)
-done
-
-text {*
-  The following lemma shows the meaning of @{text "tinres"} with respect to 
-  many step execution.
-  *}
-
-lemma tinres_steps: 
-  "\<lbrakk>tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra); 
-                 steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk>
-    \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
-apply(induct stp arbitrary: sa la ra sb lb rb, simp add: steps.simps)
-apply(simp add: step_red)
-apply(case_tac "(steps (ss, l, r) (t, 0) stp)")
-apply(case_tac "(steps (ss, l', r) (t, 0) stp)")
-proof -
-  fix stp sa la ra sb lb rb a b c aa ba ca
-  assume ind: "\<And>sa la ra sb lb rb. \<lbrakk>steps (ss, l, r) (t, 0) stp = (sa, (la::cell list), ra); 
-          steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk> \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
-  and h: " tinres l l'" "step (steps (ss, l, r) (t, 0) stp) (t, 0) = (sa, la, ra)"
-         "step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)" 
-         "steps (ss, l', r) (t, 0) stp = (aa, ba, ca)"
-  have "tinres b ba \<and> c = ca \<and> a = aa"
-    apply(rule_tac ind, simp_all add: h)
-    done
-  thus "tinres la lb \<and> ra = rb \<and> sa = sb"
-    apply(rule_tac l = b and l' = ba and r = c  and ss = a   
-            and t = t in tinres_step)
-    using h
-    apply(simp, simp, simp)
-    done
-qed
-
-lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb"
-  apply(auto simp: tinres_def replicate_add[THEN sym])
-  apply(case_tac "nb > n")
-  apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)
-  apply arith
-  by (metis Nil_is_append_conv add_diff_inverse append_assoc nat_add_commute replicate_0 replicate_add 
-    self_append_conv2)
-
 text {*
   The following locale specifies that TM @{text "H"} can be used to solve 
   the {\em Halting Problem} and @{text "False"} is going to be derived