# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358952167 -3600
# Node ID 140489a4020e6423b72c412b7adb2c83b3482f5c
# Parent  4a3cd7d70ec2eb15da33acdf5a7eb10d05f2dddb
using some abbreviations

diff -r 4a3cd7d70ec2 -r 140489a4020e thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Jan 23 15:33:26 2013 +0100
+++ b/thys/uncomputable.thy	Wed Jan 23 15:42:47 2013 +0100
@@ -1269,21 +1269,17 @@
   qed
 qed
    
-(* TM that produces the contradiction *)
-definition tcontra :: "instr list \<Rightarrow> instr list"
-  where
-  "tcontra h \<equiv> (tcopy |+| h) |+| dither"
+(* TM that produces the contradiction and its code *)
+abbreviation 
+  "tcontra \<equiv> (tcopy |+| H) |+| dither"
+abbreviation
+  "code_tcontra \<equiv> code tcontra"
 
-
-lemma uh_h: 
-  assumes "\<not> haltP0 (tcontra H) [code (tcontra H)]"
+(* assume tcontra does not halt on its code *)
+lemma tcontra_unhalt: 
+  assumes "\<not> haltP0 tcontra [code tcontra]"
   shows "False"
 proof -
-   (* code of tcontra *)
-  def code_tcontra \<equiv> "(code (tcontra H))"
-  have assms': "\<not> haltP0 (tcontra H) [code_tcontra]" 
-    using assms by (simp add: code_tcontra_def)
-
   (* invariants *)
   def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
@@ -1294,7 +1290,7 @@
   ----------------------------
      {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
   ------------------------------------------------
-           {P1} (tcontra H) {P3}
+           {P1} tcontra {P3}
   *)
 
   have H_wf: "tm_wf0 (tcopy |+| H)" by auto
@@ -1304,13 +1300,12 @@
   proof (induct rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
-      unfolding code_tcontra_def
       by (rule tcopy_correct1) (simp)
     moreover
     have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def
       by (simp add: assert_imp_def tape_of_nl_abv)
     moreover
-    have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def
+    have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def
       by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
     ultimately
     show "{P1} tcopy {P2}" by (rule Hoare_weak)
@@ -1318,7 +1313,7 @@
     case B_halt
     obtain n i
       where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])"
-      using nh_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def]
+      using nh_newcase[of "tcontra" "[code_tcontra]" 1, OF assms]
       by (auto)
     then show "{P2} H {P3}"
       unfolding P2_def P3_def dither_halt_inv_def
@@ -1334,31 +1329,27 @@
     by (rule dither_halts)
   
   (* {P1} tcontra {P3} *)
-  have "{P1} (tcontra H) {P3}" unfolding tcontra_def
+  have "{P1} tcontra {P3}" 
     by (rule Hoare_plus_halt_simple[OF first second H_wf])
 
-  with assms' show "False"
-    unfolding P1_def P3_def dither_halt_inv_def code_tcontra_def
+  with assms show "False"
+    unfolding P1_def P3_def dither_halt_inv_def 
     unfolding haltP_def
     unfolding Hoare_def 
     apply(auto)
     apply(erule_tac x = n in allE)
-    apply(case_tac "steps0 (Suc 0, [], <[code (tcontra H)]>) (tcontra H) n")
+    apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
     apply(simp, auto)
     apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
     apply(simp)
     by (smt replicate_0 replicate_Suc)
 qed
 
-lemma h_uh: 
-  assumes "haltP0 (tcontra H) [code (tcontra H)]"
+(* asumme tcontra halts on its code *)
+lemma tcontra_halt: 
+  assumes "haltP0 tcontra [code tcontra]"
   shows "False"
 proof - 
-  (* code of tcontra *)
-  def code_tcontra \<equiv> "(code (tcontra H))"
-  have assms': "haltP0 (tcontra H) [code_tcontra]" 
-    using assms by (simp add: code_tcontra_def)
-
   (* invariants *)
   def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
@@ -1369,7 +1360,7 @@
   ----------------------------
      {P1} (tcopy |+| H) {P3}     {P3} dither loops
   ------------------------------------------------
-           {P1} (tcontra H) loops
+           {P1} tcontra loops
   *)
 
   have H_wf: "tm_wf0 (tcopy |+| H)" by auto
@@ -1379,13 +1370,12 @@
   proof (induct rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
-      unfolding code_tcontra_def
       by (rule tcopy_correct1) (simp)
     moreover
     have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def
       by (simp add: assert_imp_def tape_of_nl_abv)
     moreover
-    have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def
+    have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def 
       by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
     ultimately
     show "{P1} tcopy {P2}" by (rule Hoare_weak)
@@ -1393,7 +1383,7 @@
     case B_halt
     obtain n i
       where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc])"
-      using h_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def]
+      using h_newcase[of "tcontra" "[code_tcontra]" 1, OF assms]
       by (auto)
     then show "{P2} H {P3}"
       unfolding P2_def P3_def
@@ -1409,25 +1399,23 @@
     by (rule dither_loops)
   
   (* {P1} tcontra loops *)
-  have "{P1} (tcontra H) \<up>" unfolding tcontra_def
+  have "{P1} tcontra \<up>" 
     by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
 
   with assms show "False"
     unfolding haltP_def
-    unfolding P1_def code_tcontra_def
+    unfolding P1_def
     unfolding Hoare_unhalt_def
     by (auto, metis is_final_eq)  
 qed
-
-
-
       
 text {*
   @{text "False"} can finally derived.
 *}
 
 lemma false: "False"
-using uh_h h_uh by auto
+using tcontra_halt tcontra_unhalt 
+by auto
 
 end