Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/uncomputable.thy
changeset 71 8c7f10b3da7b
parent 70 2363eb91d9fd
child 76 04399b471108
equal deleted inserted replaced
70:2363eb91d9fd 71:8c7f10b3da7b 
    55   "tcopy \<equiv> (tcopy_init |+| tcopy_loop) |+| tcopy_end"
 
    55   "tcopy \<equiv> (tcopy_init |+| tcopy_loop) |+| tcopy_end"
 
    56 
    56 
    57 
    57 
    58 (* tcopy_init *)
 
    58 (* tcopy_init *)
 
    59 
    59 
    60 fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
    60 fun 
    61   where
 
    61   inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
    62    "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
 
    62   inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
    63 
    63   inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
    64 fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
    64   inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
    65   where 
    65   inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
    66   "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
 
    66 where
 
    67 
       
    68 fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
    69   where
 
       
    70   "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
 
       
    71 
       
    72 fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
    73   where
 
       
    74   "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
 
       
    75 
       
    76 fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
    77   where
 
       
    78   "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   
    67   "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   
    79                          (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
 
    68                          (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
 
       
    69 | "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
 
       
    70 | "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
 
       
    71 | "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
 
       
    72 | "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
 
    80 
    73 
    81 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
    74 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
    82   where
 
    75   where
 
    83   "inv_init x (s, l, r) = 
    76   "inv_init x (s, l, r) = 
    84         (if s = 0 then inv_init0 x (l, r) 
    77         (if s = 0 then inv_init0 x (l, r) 
   182   qed
 
   175   qed
 
   183 qed
 
   176 qed
 
   184     
   177     
   185 lemma init_correct: 
   178 lemma init_correct: 
   186   "x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
 
   179   "x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
 
   187 proof(rule_tac HoareI)
 
   180 proof(rule_tac Hoare_haltI)
 
   188   fix l r
 
   181   fix l r
 
   189   assume h: "0 < x"
 
   182   assume h: "0 < x"
 
   190     "inv_init1 x (l, r)"
 
   183     "inv_init1 x (l, r)"
 
   191   hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
 
   184   hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
 
   192     by(erule_tac init_halt)    
   185     by(erule_tac init_halt)    
   688   qed
 
   681   qed
 
   689 qed
 
   682 qed
 
   690 
   683 
   691 lemma loop_correct:
 
   684 lemma loop_correct:
 
   692   "x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
 
   685   "x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
 
   693 proof(rule_tac HoareI)
 
   686 proof(rule_tac Hoare_haltI)
 
   694   fix l r
 
   687   fix l r
 
   695   assume h: "0 < x"
 
   688   assume h: "0 < x"
 
   696     "inv_loop1 x (l, r)"
 
   689     "inv_loop1 x (l, r)"
 
   697   hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
 
   690   hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
 
   698     apply(rule_tac loop_halt, simp_all add: inv_loop.simps)
 
   691     apply(rule_tac loop_halt, simp_all add: inv_loop.simps)
 
   971   qed
 
   964   qed
 
   972 qed
 
   965 qed
 
   973 
   966 
   974 lemma end_correct:
 
   967 lemma end_correct:
 
   975   "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
 
   968   "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
 
   976 proof(rule_tac HoareI)
 
   969 proof(rule_tac Hoare_haltI)
 
   977   fix l r
 
   970   fix l r
 
   978   assume h: "0 < x"
 
   971   assume h: "0 < x"
 
   979     "inv_end1 x (l, r)"
 
   972     "inv_end1 x (l, r)"
 
   980   hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
 
   973   hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
 
   981     apply(rule_tac end_halt, simp_all add: inv_end.simps)
 
   974     apply(rule_tac end_halt, simp_all add: inv_end.simps)
 
  1058   moreover
 
  1051   moreover
 
  1059   have "inv_end0 (Suc n) \<mapsto> post_tcopy n" 
  1052   have "inv_end0 (Suc n) \<mapsto> post_tcopy n" 
  1060     by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
 
  1053     by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
 
  1061   ultimately
 
  1054   ultimately
 
  1062   show "{pre_tcopy n} tcopy {post_tcopy n}" 
  1055   show "{pre_tcopy n} tcopy {post_tcopy n}" 
  1063     by (rule Hoare_weak)
 
  1056     by (rule Hoare_weaken)
 
  1064 qed
 
  1057 qed
 
  1065 
  1058 
  1066 
  1059 
  1067 section {* The {\em Dithering} Turing Machine *}
 
  1060 section {* The {\em Dithering} Turing Machine *}
 
  1068 
  1061 
  1111 done 
  1104 done 
  1112 
  1105 
  1113 
  1106 
  1114 lemma dither_halts:
 
  1107 lemma dither_halts:
 
  1115   shows "{dither_halt_inv} dither {dither_halt_inv}" 
  1108   shows "{dither_halt_inv} dither {dither_halt_inv}" 
  1116 apply(rule HoareI)
 
  1109 apply(rule Hoare_haltI)
 
  1117 using dither_halt_rs
 
  1110 using dither_halt_rs
 
  1118 apply(auto)
 
  1111 apply(auto)
 
  1119 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
  1112 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
  1120 
  1113 
  1121 
  1114 
  1312 proof -
 
  1305 proof -
 
  1313   obtain stp i
 
  1306   obtain stp i
 
  1314     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
 
  1307     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
 
  1315     using nh_newcase[of "M" "[n]" "1", OF assms] by auto 
  1308     using nh_newcase[of "M" "[n]" "1", OF assms] by auto 
  1316   then show "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1309   then show "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1317     unfolding Hoare_def
 
  1310     unfolding Hoare_halt_def
 
  1318     apply(auto)
 
  1311     apply(auto)
 
  1319     apply(rule_tac x = stp in exI)
 
  1312     apply(rule_tac x = stp in exI)
 
  1320     apply(auto)
 
  1313     apply(auto)
 
  1321     done
 
  1314     done
 
  1322 qed
 
  1315 qed
 
  1327 proof -
 
  1320 proof -
 
  1328   obtain stp i
 
  1321   obtain stp i
 
  1329     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
 
  1322     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
 
  1330     using h_newcase[of "M" "[n]" "1", OF assms] by auto 
  1323     using h_newcase[of "M" "[n]" "1", OF assms] by auto 
  1331   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1324   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1332     unfolding Hoare_def
 
  1325     unfolding Hoare_halt_def
 
  1333     apply(auto)
 
  1326     apply(auto)
 
  1334     apply(rule_tac x = stp in exI)
 
  1327     apply(rule_tac x = stp in exI)
 
  1335     apply(auto)
 
  1328     apply(auto)
 
  1336     done
 
  1329     done
 
  1337 qed
 
  1330 qed
 
  1385     by (rule Hoare_plus_halt_simple[OF first second H_wf])
 
  1378     by (rule Hoare_plus_halt_simple[OF first second H_wf])
 
  1386 
  1379 
  1387   with assms show "False"
 
  1380   with assms show "False"
 
  1388     unfolding P1_def P3_def
 
  1381     unfolding P1_def P3_def
 
  1389     unfolding haltP_def
 
  1382     unfolding haltP_def
 
  1390     unfolding Hoare_def 
  1383     unfolding Hoare_halt_def 
  1391     apply(auto)
 
  1384     apply(auto)
 
  1392     apply(erule_tac x = n in allE)
 
  1385     apply(erule_tac x = n in allE)
 
  1393     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
 
  1386     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
 
  1394     apply(simp, auto)
 
  1387     apply(simp, auto)
 
  1395     apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
 
  1388     apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
tm