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