diff -r f2bda6ba4952 -r aeaf1374dc67 thys/uncomputable.thy --- a/thys/uncomputable.thy Mon Jan 28 02:38:57 2013 +0000 +++ b/thys/uncomputable.thy Tue Jan 29 12:37:06 2013 +0000 @@ -103,47 +103,47 @@ apply(rule_tac inv_begin_step, simp_all) done -fun init_state :: "config \ nat" +fun begin_state :: "config \ nat" where - "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)" + "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" -fun init_step :: "config \ nat" +fun begin_step :: "config \ nat" where - "init_step (s, l, r) = + "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 init_measure :: "config \ nat \ nat" +fun begin_measure :: "config \ nat \ nat" where - "init_measure c = (init_state c, init_step c)" + "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 init_LE :: "(config \ config) set" +definition begin_LE :: "(config \ config) set" where - "init_LE \ (inv_image lex_pair init_measure)" + "begin_LE \ (inv_image lex_pair begin_measure)" lemma [simp]: "\tl r = []; r \ []; r \ [Bk]\ \ r = [Oc]" by (case_tac r, auto, case_tac a, auto) -lemma wf_begin_le: "wf init_LE" -by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) +lemma wf_begin_le: "wf begin_LE" +by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def) -lemma init_halt: +lemma begin_halt: "x > 0 \ \ stp. is_final (steps0 (Suc 0, [], Oc\x) tcopy_begin stp)" -proof(rule_tac LE = init_LE in halt_lemma) - show "wf init_LE" by(simp add: wf_begin_le) +proof(rule_tac LE = begin_LE in halt_lemma) + show "wf begin_LE" by(simp add: wf_begin_le) next assume h: "0 < x" show "\n. \ is_final (steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) n) \ (steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) (Suc n), - steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) n) \ init_LE" + steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) n) \ begin_LE" proof(rule_tac allI, rule_tac impI) fix n assume a: "\ is_final (steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) n)" @@ -157,25 +157,25 @@ moreover hence "inv_begin x (s, l, r)" using c b by simp ultimately show "(steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) (Suc n), - steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) n) \ init_LE" + steps (Suc 0, [], Oc \ x) (tcopy_begin, 0) n) \ begin_LE" using a proof(simp del: inv_begin.simps) assume "inv_begin x (s, l, r)" "0 < s" - thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \ init_LE" - apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits) + 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(case_tac r, auto, case_tac a, auto) done qed qed qed -lemma init_correct: +lemma begin_correct: "0 < x \ {inv_begin1 x} tcopy_begin {inv_begin0 x}" proof(rule_tac Hoare_haltI) fix l r assume h: "0 < x" "inv_begin1 x (l, r)" hence "\ stp. is_final (steps0 (Suc 0, [], Oc \ x) tcopy_begin stp)" - by (rule_tac init_halt) + by (rule_tac begin_halt) then obtain stp where "is_final (steps (Suc 0, [], Oc\x) (tcopy_begin, 0) stp)" .. moreover have "inv_begin x (steps (Suc 0, [], Oc\x) (tcopy_begin, 0) stp)" apply(rule_tac inv_begin_steps) @@ -913,7 +913,7 @@ shows "{inv_begin1 x} tcopy {inv_end0 x}" proof - have "{inv_begin1 x} tcopy_begin {inv_begin0 x}" - by (metis assms init_correct) + by (metis assms begin_correct) moreover have "{inv_loop1 x} tcopy_loop {inv_loop0 x}" by (metis assms loop_correct) @@ -970,10 +970,10 @@ "dither \ [(W0, 1), (R, 2), (L, 1), (L, 0)] " (* invariants of dither *) -abbreviation +abbreviation (input) "dither_halt_inv \ \tp. (\n. tp = (Bk \ n, <1::nat>))" -abbreviation +abbreviation (input) "dither_unhalt_inv \ \tp. (\n. tp = (Bk \ n, <0::nat>))" lemma dither_loops_aux: @@ -1083,7 +1083,7 @@ (* invariants *) def P1 \ "\tp. tp = ([]::cell list, <[code_tcontra]>)" def P2 \ "\tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)" - def P3 \ "\tp. (\n. tp = (Bk \ n, <1::nat>))" + def P3 \ "\tp. \n. tp = (Bk \ n, <1::nat>)" (* {P1} tcopy {P2} {P2} H {P3} @@ -1136,7 +1136,7 @@ (* invariants *) def P1 \ "\tp. tp = ([]::cell list, <[code_tcontra]>)" def P2 \ "\tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)" - def Q3 \ "\tp. (\n. tp = (Bk \ n, <0::nat>))" + def Q3 \ "\tp. \n. tp = (Bk \ n, <0::nat>)" (* {P1} tcopy {P2} {P2} H {Q3}