# HG changeset patch # User Christian Urban # Date 1358924495 -3600 # Node ID 35fe8fe12e659d021b45be7a219d18c44e5272cb # Parent e33306b4c62e45471fa7bea54847067b05a14b70 small updates diff -r e33306b4c62e -r 35fe8fe12e65 Paper/Paper.thy --- a/Paper/Paper.thy Tue Jan 22 14:46:02 2013 +0000 +++ b/Paper/Paper.thy Wed Jan 23 08:01:35 2013 +0100 @@ -1,6 +1,6 @@ (*<*) theory Paper -imports "../thys/recursive" +imports "../thys/uncomputable" "~~/src/HOL/Library/LaTeXsugar" begin (* @@ -21,6 +21,7 @@ W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and update2 ("update") and + tm_wf0 ("wf") and (* abc_lm_v ("lookup") and abc_lm_s ("set") and*) haltP ("stdhalt") and @@ -90,7 +91,7 @@ of register machines) and recursive functions. To see the difficulties involved with this work, one has to understand that Turing machine programs can be completely \emph{unstructured}, behaving -similar Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the +similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the general case a compositional Hoare-style reasoning about Turing programs. We provide such Hoare-rules for when it \emph{is} possible to reason in a compositional manner (which is fortunately quite often), but also tackle @@ -309,14 +310,14 @@ %states.\footnote{The usual disjoint union operation in Isabelle/HOL %cannot be used as it does not preserve types.} This renaming can be %quite cumbersome to reason about. - We followed the choice made by \cite{AspertiRicciotti12} + We followed the choice made in \cite{AspertiRicciotti12} representing a state by a natural number and the states of a Turing machine by the initial segment of natural numbers starting from @{text 0}. In doing so we can compose two Turing machine by shifting the states of one by an appropriate amount to a higher segment and adjusting some ``next states'' in the other. {\it composition here?} - An \emph{instruction} @{term i} of a Turing machine is a pair consisting of + An \emph{instruction} of a Turing machine is a pair consisting of an action and a natural number (the next state). A \emph{program} @{term p} of a Turing machine is then a list of such pairs. Using as an example the following Turing machine program, which consists of four instructions @@ -398,13 +399,12 @@ configuration and a program, we can calculate what the next configuration is by fetching the appropriate action and next state from the program, and by updating the state and tape accordingly. - This single step of execution is defined as the function @{term tstep} + This single step of execution is defined as the function @{term step} \begin{center} - \begin{tabular}{l} - @{text "step (s, (l, r)) p"} @{text "\"}\\ - \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\ - \hspace{10mm}@{text "in (s', update (l, r) a)"} + \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + @{text "step (s, (l, r)) p"} & @{text "\"} & @{text "let (a, s') = fetch p s (read r)"}\\ + & & @{text "in (s', update (l, r) a)"} \end{tabular} \end{center} @@ -540,6 +540,20 @@ halting problem *} +text {* + \begin{center} + \begin{tabular}{@ {}p{3cm}p{3cm}@ {}} + @{thm[mode=Rule] + Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]} + & + @{thm[mode=Rule] + Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]} + \end{tabular} + \end{center} + + +*} + section {* Abacus Machines *} text {* diff -r e33306b4c62e -r 35fe8fe12e65 Paper/ROOT.ML --- a/Paper/ROOT.ML Tue Jan 22 14:46:02 2013 +0000 +++ b/Paper/ROOT.ML Wed Jan 23 08:01:35 2013 +0100 @@ -1,7 +1,7 @@ no_document -use_thys ["../thys/turing_basic"(*, +use_thys ["../thys/turing_basic", "../thys/turing_hoare", - "../thys/uncomputable", + "../thys/uncomputable"(*, "../thys/abacus", "../thys/rec_def", "../thys/recursive"*)]; diff -r e33306b4c62e -r 35fe8fe12e65 Paper/document/root.tex --- a/Paper/document/root.tex Tue Jan 22 14:46:02 2013 +0000 +++ b/Paper/document/root.tex Wed Jan 23 08:01:35 2013 +0100 @@ -5,6 +5,7 @@ \usepackage{times} \usepackage{amssymb} \usepackage{amsmath} +\usepackage{stmaryrd} \usepackage{mathpartir} \usepackage{pdfsetup} \usepackage{tikz} @@ -18,6 +19,11 @@ \urlstyle{rm} \isabellestyle{it} +% mathpatir +\mprset{sep=0.8em} +\mprset{center=false} +\mprset{flushleft=true} + % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} diff -r e33306b4c62e -r 35fe8fe12e65 paper.pdf Binary file paper.pdf has changed diff -r e33306b4c62e -r 35fe8fe12e65 thys/abacus.thy --- a/thys/abacus.thy Tue Jan 22 14:46:02 2013 +0000 +++ b/thys/abacus.thy Wed Jan 23 08:01:35 2013 +0100 @@ -3,7 +3,7 @@ *} theory abacus -imports Main turing_hoare +imports Main turing_basic begin text {* diff -r e33306b4c62e -r 35fe8fe12e65 thys/turing_basic.thy --- a/thys/turing_basic.thy Tue Jan 22 14:46:02 2013 +0000 +++ b/thys/turing_basic.thy Wed Jan 23 08:01:35 2013 +0100 @@ -174,6 +174,10 @@ "tm_wf (p, off) = (length p \ 2 \ length p mod 2 = 0 \ (\(a, s) \ set p. s \ length p div 2 + off \ s \ off))" +abbreviation + "tm_wf0 p \ tm_wf (p, 0)" + + lemma halt_lemma: "\wf LE; \n. (\ P (f n) \ (f (Suc n), (f n)) \ LE)\ \ \n. P (f n)" by (metis wf_iff_no_infinite_down_chain) diff -r e33306b4c62e -r 35fe8fe12e65 thys/turing_hoare.thy --- a/thys/turing_hoare.thy Tue Jan 22 14:46:02 2013 +0000 +++ b/thys/turing_hoare.thy Wed Jan 23 08:01:35 2013 +0100 @@ -53,17 +53,17 @@ text {* - {P1} A {Q1} {P2} B {Q2} Q1 \ P2 A, B well-formed - ------------------------------------------------------ + {P1} A {Q1} {P2} B {Q2} Q1 \ P2 A well-formed + --------------------------------------------------- {P1} A |+| B {Q2} *} lemma Hoare_plus_halt: - assumes a_imp: "Q1 \ P2" + assumes A_halt : "{P1} A {Q1}" + and B_halt : "{P2} B {Q2}" + and a_imp: "Q1 \ P2" and A_wf : "tm_wf (A, 0)" - and A_halt : "{P1} A {Q1}" - and B_halt : "{P2} B {Q2}" shows "{P1} A |+| B {Q2}" proof(rule HoareI) fix l r @@ -103,10 +103,10 @@ lemma Hoare_plus_unhalt: - assumes a_imp: "Q1 \ P2" + assumes A_halt: "{P1} A {Q1}" + and B_uhalt: "{P2} B \" + and a_imp: "Q1 \ P2" and A_wf : "tm_wf (A, 0)" - and A_halt : "{P1} A {Q1}" - and B_uhalt : "{P2} B \" shows "{P1} (A |+| B) \" proof(rule_tac Hoare_unhalt_I) fix n l r @@ -155,13 +155,5 @@ by (metis holds_for.simps surj_pair) -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] - - end \ No newline at end of file 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]: "\0 < i; 0 < j\ \ \ia>0. ia + j - Suc 0 = i + j \ Oc # Oc \ i = Oc \ ia" @@ -62,9 +78,9 @@ lemma inv_init_step: "\inv_init x cf; x > 0\ \ 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) \ 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 @@ "\inv_loop x cf; x > 0\ \ 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) \ loop_LE" @@ -862,8 +873,7 @@ inv_end x cf\ \ 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') \ 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) \ end_LE" @@ -1037,7 +1046,7 @@ (0, Bk\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\m, [Oc]) (dither, 0) stp = (2, Oc # Bk\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 \ ?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)] - \ \ haltP (tcontra H, 0) [code (tcontra H)]" + + +lemma h_uh: + assumes "haltP (tcontra H, 0) [code (tcontra H)]" + shows "\ 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 = "\ (l, r). (l = [Bk] \ r = Oc\?cn @ Bk # Oc\?cn)" let ?Q2 = "\(l, r). (\nd. l = Bk \ nd) \ r = [Oc]" let ?P3 = ?Q2 - assume h: "haltP (?tcontr, 0) [code ?tcontr]" have "{?P1} ?tcontr \" proof(rule_tac Hoare_plus_unhalt, auto) show "?Q2 \ ?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 "\ True" - using h + thus "\ 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 \ ?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