# HG changeset patch # User Christian Urban # Date 1360786094 0 # Node ID 6013ca0e6e22d12902990b9ea9eafb570a4b53fc # Parent d7570dbf9f06e1d129dc86b78c3e60432ba008d7 tuned diff -r d7570dbf9f06 -r 6013ca0e6e22 Paper/Paper.thy --- a/Paper/Paper.thy Tue Feb 12 13:37:07 2013 +0000 +++ b/Paper/Paper.thy Wed Feb 13 20:08:14 2013 +0000 @@ -15,8 +15,7 @@ consts DUMMY::'a - -(* THEOREMS *) +(* Theorems as inference rules from LaTeXsugar.thy *) notation (Rule output) "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") @@ -59,7 +58,6 @@ W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and update2 ("update") and tm_wf0 ("wf") and - (*is_even ("iseven") and*) tcopy_begin ("cbegin") and tcopy_loop ("cloop") and tcopy_end ("cend") and diff -r d7570dbf9f06 -r 6013ca0e6e22 thys/Rec_Def.thy --- a/thys/Rec_Def.thy Tue Feb 12 13:37:07 2013 +0000 +++ b/thys/Rec_Def.thy Wed Feb 13 20:08:14 2013 +0000 @@ -1,3 +1,10 @@ +(* Title: thys/Rec_Def.thy + Author: Jian Xu, Xingyuan Zhang, and Christian Urban +*) + +header {* Definition of Recursive Functions *} + + theory Rec_Def imports Main begin diff -r d7570dbf9f06 -r 6013ca0e6e22 thys/Recursive.thy --- a/thys/Recursive.thy Tue Feb 12 13:37:07 2013 +0000 +++ b/thys/Recursive.thy Wed Feb 13 20:08:14 2013 +0000 @@ -1,8 +1,13 @@ +(* Title: thys/Recursive.thy + Author: Jian Xu, Xingyuan Zhang, and Christian Urban +*) + +header {* Translating Recursive Functions into Abacus Machines *} + theory Recursive imports Rec_Def Abacus begin -section {* Compiling from recursive functions to Abacus machines *} text {* Some auxilliary Abacus machines used to construct the result Abacus machines. diff -r d7570dbf9f06 -r 6013ca0e6e22 thys/UF.thy --- a/thys/UF.thy Tue Feb 12 13:37:07 2013 +0000 +++ b/thys/UF.thy Wed Feb 13 20:08:14 2013 +0000 @@ -1,3 +1,9 @@ +(* Title: thys/UF.thy + Author: Jian Xu, Xingyuan Zhang, and Christian Urban +*) + +header {* Construction of a Universal Function *} + theory UF imports Rec_Def GCD Abacus begin @@ -9,7 +15,7 @@ UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine. *} -section {* Univeral Function *} +section {* Universal Function *} subsection {* The construction of component functions *} diff -r d7570dbf9f06 -r 6013ca0e6e22 thys/UTM.thy --- a/thys/UTM.thy Tue Feb 12 13:37:07 2013 +0000 +++ b/thys/UTM.thy Wed Feb 13 20:08:14 2013 +0000 @@ -1,3 +1,9 @@ +(* Title: thys/UTM.thy + Author: Jian Xu, Xingyuan Zhang, and Christian Urban +*) + +header {* Construction of a Universal Turing Machine *} + theory UTM imports Recursive Abacus UF GCD Turing_Hoare begin @@ -20,7 +26,7 @@ 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 + constructed by compiling from any recursive 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 diff -r d7570dbf9f06 -r 6013ca0e6e22 thys/Uncomputable.thy --- a/thys/Uncomputable.thy Tue Feb 12 13:37:07 2013 +0000 +++ b/thys/Uncomputable.thy Wed Feb 13 20:08:14 2013 +0000 @@ -987,13 +987,13 @@ section {* The diagnal argument below shows the undecidability of Halting problem *} text {* - @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} + @{text "halts tp x"} means TM @{text "tp"} terminates on input @{text "x"} and the final configuration is standard. *} -definition haltP :: "tprog0 \ nat list \ bool" +definition halts :: "tprog0 \ nat list \ bool" where - "haltP p ns \ {(\tp. tp = ([], ))} p {(\tp. (\k n l. tp = (Bk \ k, @ Bk \ l)))}" + "halts p ns \ {(\tp. tp = ([], ))} p {(\tp. (\k n l. tp = (Bk \ k, @ Bk \ l)))}" lemma [intro, simp]: "tm_wf0 tcopy" by (auto simp: tcopy_def) @@ -1021,9 +1021,9 @@ The following two assumptions specifies that @{text "H"} does solve the Halting problem. *} and h_case: - "\ M ns. haltP M ns \ {(\tp. tp = ([Bk], <(code M, ns)>))} H {(\tp. \k. tp = (Bk \ k, <0::nat>))}" + "\ M ns. halts M ns \ {(\tp. tp = ([Bk], <(code M, ns)>))} H {(\tp. \k. tp = (Bk \ k, <0::nat>))}" and nh_case: - "\ M ns. \ haltP M ns \ {(\tp. tp = ([Bk], <(code M, ns)>))} H {(\tp. \k. tp = (Bk \ k, <1::nat>))}" + "\ M ns. \ halts M ns \ {(\tp. tp = ([Bk], <(code M, ns)>))} H {(\tp. \k. tp = (Bk \ k, <1::nat>))}" begin (* invariants for H *) @@ -1038,12 +1038,12 @@ lemma H_halt_inv: - assumes "\ haltP M ns" + assumes "\ halts M ns" shows "{pre_H_inv M ns} H {post_H_halt_inv}" using assms nh_case by auto lemma H_unhalt_inv: - assumes "haltP M ns" + assumes "halts M ns" shows "{pre_H_inv M ns} H {post_H_unhalt_inv}" using assms h_case by auto @@ -1056,7 +1056,7 @@ (* assume tcontra does not halt on its code *) lemma tcontra_unhalt: - assumes "\ haltP tcontra [code tcontra]" + assumes "\ halts tcontra [code tcontra]" shows "False" proof - (* invariants *) @@ -1099,7 +1099,7 @@ with assms show "False" unfolding P1_def P3_def - unfolding haltP_def + unfolding halts_def unfolding Hoare_halt_def apply(auto) apply(drule_tac x = n in spec) @@ -1110,7 +1110,7 @@ (* asumme tcontra halts on its code *) lemma tcontra_halt: - assumes "haltP tcontra [code tcontra]" + assumes "halts tcontra [code tcontra]" shows "False" proof - (* invariants *) @@ -1152,7 +1152,7 @@ with assms show "False" unfolding P1_def - unfolding haltP_def + unfolding halts_def unfolding Hoare_halt_def Hoare_unhalt_def by (auto simp add: tape_of_nl_abv) qed