
diff -r e33306b4c62e -r 35fe8fe12e65 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/uncomputable.thy	Wed Jan 23 08:01:35 2013 +0100
@@ -9,6 +9,24 @@
 imports Main turing_hoare
 begin
 
+declare tm_comp.simps [simp del] 
+declare adjust.simps[simp del] 
+declare shift.simps[simp del]
+declare tm_wf.simps[simp del]
+declare step.simps[simp del]
+declare steps.simps[simp del]
+
+
+lemma numeral:
+  shows "1 = Suc 0"
+  and "2 = Suc 1"
+  and "3 = Suc 2"
+  and "4 = Suc 3" 
+  and "5 = Suc 4" 
+  and "6 = Suc 5" by arith+
+
+
+
 text {*
   The {\em Copying} TM, which duplicates its input. 
 *}
@@ -51,8 +69,6 @@
 
 declare inv_init.simps[simp del]
 
-lemma numeral_4_eq_4: "4 = Suc 3"
-by arith
 
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
@@ -62,9 +78,9 @@
 lemma inv_init_step: 
   "\<lbrakk>inv_init x cf; x > 0\<rbrakk>
  \<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"
+unfolding tcopy_init_def
 apply(case_tac cf)
-apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral_2_eq_2 
-  numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral split: if_splits)
 apply(case_tac "hd c", auto simp: inv_init.simps)
 apply(case_tac c, simp_all)
 done
@@ -137,8 +153,8 @@
     proof(simp)
       assume "inv_init x (s, l, r)" "0 < s"
       thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
-        apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral_2_eq_2
-          numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+        apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral 
+          split: if_splits)
         apply(case_tac r, auto, case_tac a, auto)
         done
     qed
@@ -254,9 +270,6 @@
 apply(case_tac t, auto)
 done
 
-lemma numeral_5_eq_5: "5 = Suc 4" by arith
-
-lemma numeral_6_eq_6: "6 = Suc (Suc 4)" by arith
 
 lemma [simp]: "inv_loop1 x (b, []) = False"
 by(simp add: inv_loop1.simps)
@@ -472,8 +485,7 @@
   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
  \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
 apply(case_tac cf, case_tac c, case_tac [2] aa)
-apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral_2_eq_2  
-  numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 numeral_6_eq_6 split: if_splits)
+apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
 done
 
 lemma inv_loop_steps:
@@ -648,8 +660,7 @@
       using h 
       apply(case_tac r', case_tac [2] a)
       apply(auto simp: inv_loop.simps step.simps tcopy_loop_def 
-                       numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
-                       numeral_5_eq_5 numeral_6_eq_6 loop_LE_def lex_triple_def lex_pair_def split: if_splits)
+                       numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits)
       done
     thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), 
           steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
@@ -862,8 +873,7 @@
  inv_end x cf\<rbrakk>
  \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
 apply(case_tac cf, case_tac c, case_tac [2] aa)
-apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral_2_eq_2 
-  numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 split: if_splits)
+apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
 done
 
 lemma inv_end_steps:
@@ -937,8 +947,7 @@
     hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"
       apply(case_tac r', case_tac [2] a)
       apply(auto simp: inv_end.simps step.simps tcopy_end_def 
-                       numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4 
-                       numeral_5_eq_5 numeral_6_eq_6 end_LE_def lex_triple_def lex_pair_def split: if_splits)
+                       numeral end_LE_def lex_triple_def lex_pair_def split: if_splits)
       done
     thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), 
       steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
@@ -1037,7 +1046,7 @@
                                  (0, Bk\<up>m, [Oc, Oc])"
 apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
 apply(simp add: dither_def steps.simps 
-                step.simps fetch.simps numeral_2_eq_2)
+                step.simps fetch.simps numeral)
 done
 
 lemma dither_unhalt_state: 
@@ -1046,7 +1055,7 @@
    (steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
   apply(induct stp, simp add: steps.simps)
   apply(simp add: step_red, auto)
-  apply(auto simp: step.simps fetch.simps dither_def numeral_2_eq_2)
+  apply(auto simp: step.simps fetch.simps dither_def numeral)
   done
 
 lemma dither_unhalt_rs: 
@@ -1324,14 +1333,17 @@
     apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
     apply(simp, auto)
     apply(erule_tac x = nd in allE, erule_tac x = 2 in allE)
-    apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv)
+    apply(simp add: numeral replicate_Suc tape_of_nl_abv)
     apply(erule_tac x = 0 in allE, simp)
     done
 qed
   
 
-lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)]
-       \<Longrightarrow> \<not> haltP (tcontra H, 0) [code (tcontra H)]"
+
+
+lemma h_uh: 
+  assumes "haltP (tcontra H, 0) [code (tcontra H)]"
+  shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]"
 proof(simp only: tcontra_def)
   let ?tcontr = "(tcopy |+| H) |+| dither"
   let ?cn = "Suc (code ?tcontr)"
@@ -1340,7 +1352,6 @@
   let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
   let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
   let ?P3 = ?Q2
-  assume h: "haltP (?tcontr, 0) [code ?tcontr]"
   have "{?P1} ?tcontr \<up>"
   proof(rule_tac Hoare_plus_unhalt, auto)
     show "?Q2 \<mapsto> ?P3"
@@ -1373,7 +1384,8 @@
       qed
     next
       show "{?P2} H {?Q2}"
-        using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
+        using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] assms
+        unfolding tcontra_def
         apply(auto)
         apply(rule_tac x = na in exI)
         apply(simp add: replicate_Suc tape_of_nl_abv)
@@ -1390,8 +1402,9 @@
         by simp
     qed
   qed    
-  thus "\<not> True"
-    using h
+  thus "\<not> haltP ((tcopy |+| H) |+| dither, 0) [code ((tcopy |+| H) |+| dither)]"
+    using assms
+    unfolding tcontra_def
     apply(auto simp: haltP_def Hoare_unhalt_def)
     apply(erule_tac x = n in allE)
     apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
@@ -1399,6 +1412,7 @@
     done
 qed
       
+      
 text {*
   @{text "False"} is finally derived.
 *}
@@ -1406,6 +1420,7 @@
 lemma false: "False"
 using uh_h h_uh
 by auto
+
 end
 
 end




