diff -r 5317c92ff2a7 -r bd320b5365e2 thys/uncomputable.thy --- a/thys/uncomputable.thy Tue Jan 29 13:00:51 2013 +0000 +++ b/thys/uncomputable.thy Tue Jan 29 16:37:38 2013 +0000 @@ -9,14 +9,6 @@ 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" @@ -92,9 +84,11 @@ using assms unfolding tcopy_begin_def apply(case_tac cf) -apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits) -apply(case_tac "hd c", auto simp: inv_begin.simps) -apply(case_tac c, simp_all) +apply(auto simp: numeral split: if_splits) +apply(case_tac "hd c") +apply(auto) +apply(case_tac c) +apply(simp_all) done lemma inv_begin_steps: @@ -102,48 +96,34 @@ and "x > 0" shows "inv_begin x (steps0 cf tcopy_begin stp)" apply(induct stp) -apply(simp add: steps.simps assms) -apply(auto simp: step_red) +apply(simp add: assms) +apply(auto simp del: steps.simps) apply(rule_tac inv_begin_step) apply(simp_all add: assms) done -fun begin_state :: "config \ nat" +fun measure_begin_state :: "config \ nat" where - "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" + "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" -fun begin_step :: "config \ nat" +fun measure_begin_step :: "config \ nat" where - "begin_step (s, l, r) = + "measure_begin_step (s, l, r) = (if s = 2 then length r else if s = 3 then (if r = [] \ r = [Bk] then 1 else 0) else if s = 4 then length l else 0)" -fun begin_measure :: "config \ nat \ nat" - where - "begin_measure c = (begin_state c, begin_step c)" - - -definition lex_pair :: "((nat \ nat) \ nat \ nat) set" - where - "lex_pair \ less_than <*lex*> less_than" - -definition begin_LE :: "(config \ config) set" - where - "begin_LE \ (inv_image lex_pair begin_measure)" +definition + "begin_LE = measures [measure_begin_state, measure_begin_step]" lemma [simp]: "\tl r = []; r \ []; r \ [Bk]\ \ r = [Oc]" by (case_tac r, auto, case_tac a, auto) - -lemma wf_begin_le: "wf begin_LE" -by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def) - lemma begin_halt: "x > 0 \ \ stp. is_final (steps0 (1, [], Oc\x) tcopy_begin stp)" proof(rule_tac LE = begin_LE in halt_lemma) - show "wf begin_LE" by(simp add: wf_begin_le) + show "wf begin_LE" unfolding begin_LE_def by (auto) next assume h: "0 < x" show "\n. \ is_final (steps (1, [], Oc \ x) (tcopy_begin, 0) n) \ @@ -164,10 +144,10 @@ ultimately show "(steps (1, [], Oc \ x) (tcopy_begin, 0) (Suc n), steps (1, [], Oc \ x) (tcopy_begin, 0) n) \ begin_LE" using a - proof(simp del: inv_begin.simps) + proof(simp del: inv_begin.simps step.simps steps.simps) assume "inv_begin x (s, l, r)" "0 < s" thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \ begin_LE" - apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits) + apply(auto simp: begin_LE_def step.simps tcopy_begin_def numeral split: if_splits) apply(case_tac r, auto, case_tac a, auto) done qed @@ -194,6 +174,13 @@ done qed +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] + (* tcopy_loop *) @@ -477,25 +464,13 @@ else if s = 6 then length l else 0)" -definition lex_triple :: - "((nat \ (nat \ nat)) \ (nat \ (nat \ nat))) set" - where - "lex_triple \ less_than <*lex*> lex_pair" - -lemma wf_lex_triple: "wf lex_triple" - by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def) - -fun loop_measure :: "config \ nat \ nat \ nat" - where - "loop_measure c = - (loop_stage c, loop_state c, loop_step c)" - definition loop_LE :: "(config \ config) set" where - "loop_LE \ (inv_image lex_triple loop_measure)" + "loop_LE = measures [loop_stage, loop_state, loop_step]" lemma wf_loop_le: "wf loop_LE" -by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple) +unfolding loop_LE_def +by (auto) lemma [simp]: "inv_loop2 x ([], b) = False" by (auto simp: inv_loop2.simps) @@ -615,8 +590,7 @@ hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \ loop_LE" using h apply(case_tac r', case_tac [2] a) - apply(auto simp: inv_loop.simps step.simps tcopy_loop_def - numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits) + apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral loop_LE_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" @@ -833,17 +807,13 @@ else if s = 3 then 0 else 0)" -fun end_measure :: "config \ nat \ nat \ nat" - where - "end_measure c = - (end_state c, end_stage c, end_step c)" - definition end_LE :: "(config \ config) set" where - "end_LE \ (inv_image lex_triple end_measure)" + "end_LE = measures [end_state, end_stage, end_step]" lemma wf_end_le: "wf end_LE" -by (auto intro: wf_inv_image simp: end_LE_def wf_lex_triple) +unfolding end_LE_def +by (auto) lemma [simp]: "inv_end5 x ([], Oc # list) = False" by (auto simp: inv_end5.simps inv_end5_loop.simps) @@ -870,8 +840,7 @@ done 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 end_LE_def lex_triple_def lex_pair_def split: if_splits) + apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_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"