# HG changeset patch # User Sebastiaan Joosten # Date 1545232258 -3600 # Node ID a9003e6d046325e4eb27c9360e7a9af9975aa1e6 # Parent d5a0e25c4742f1c549863611c0ca54a2316f332e Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM diff -r d5a0e25c4742 -r a9003e6d0463 thys/Abacus.thy --- a/thys/Abacus.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Abacus.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,7 +2,7 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Abacus Machines *} +chapter {* Abacus Machines *} theory Abacus imports Turing_Hoare Abacus_Mopup @@ -203,7 +203,7 @@ fun start_of :: "nat list \ nat \ nat" where - "start_of ly x = (Suc (listsum (take x ly))) " + "start_of ly x = (Suc (sum_list (take x ly))) " text {* @{text "ci lo ss i"} complies Abacus instruction @{text "i"} @@ -451,10 +451,10 @@ concat (take (Suc n) tps)") apply(simp only: append_assoc[THEN sym], simp only: append_assoc) apply(subgoal_tac " concat (drop (Suc n) tps) = tps ! Suc n @ - concat (drop (Suc (Suc n)) tps)", simp) -apply(rule_tac concat_drop_suc_iff, simp) -apply(rule_tac concat_take_suc_iff, simp) -done + concat (drop (Suc (Suc n)) tps)") + apply (metis append_take_drop_id concat_append) + apply(rule concat_drop_suc_iff,force) + by (simp add: concat_suc) declare append_assoc[simp] @@ -498,59 +498,48 @@ lemma div_apart: "\x mod (2::nat) = 0; y mod 2 = 0\ \ (x + y) div 2 = x div 2 + y div 2" -apply(drule mod_eqD)+ -apply(auto) -done + by(auto) lemma div_apart_iff: "\x mod (2::nat) = 0; y mod 2 = 0\ \ (x + y) mod 2 = 0" -apply(auto) -done +by(auto) lemma [simp]: "length (layout_of aprog) = length aprog" -apply(auto simp: layout_of.simps) -done +by(auto simp: layout_of.simps) lemma start_of_ind: "\as < length aprog; ly = layout_of aprog\ \ start_of ly (Suc as) = start_of ly as + length ((tms_of aprog) ! as) div 2" -apply(simp only: start_of.simps, simp) -apply(auto simp: start_of.simps tms_of.simps layout_of.simps - tpairs_of.simps) -apply(simp add: ci_length take_Suc take_Suc_conv_app_nth) -done + by (auto simp: start_of.simps tms_of.simps layout_of.simps + tpairs_of.simps ci_length take_Suc take_Suc_conv_app_nth) lemma concat_take_suc: "Suc n \ length xs \ concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)" -apply(subgoal_tac "take (Suc n) xs = - take n xs @ [xs ! n]") -apply(auto) -done + using concat_suc. lemma [simp]: "\as < length aprog; (abc_fetch as aprog) = Some ins\ \ ci (layout_of aprog) (start_of (layout_of aprog) as) (ins) \ set (tms_of aprog)" -apply(insert ci_nth[of "layout_of aprog" aprog as], simp) -done + by(insert ci_nth[of "layout_of aprog" aprog as], simp) lemma [simp]: "length (tms_of ap) = length ap" by(auto simp: tms_of.simps tpairs_of.simps) lemma [intro]: "n < length ap \ length (tms_of ap ! n) mod 2 = 0" -apply(auto simp: tms_of.simps tpairs_of.simps) -apply(case_tac "ap ! n", auto simp: ci.simps length_findnth tinc_b_def tdec_b_def) -apply arith -by arith + apply(cases "ap ! n") + by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def) lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0" -apply(induct n, auto) -apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto) -(*apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0") -apply arith -by auto -*) -done +proof(induct n) + case 0 + then show ?case by (auto simp add: take_Suc_conv_app_nth) +next + case (Suc n) + hence "n < length (tms_of ap) \ is_even (length (concat (take (Suc n) (tms_of ap))))" + unfolding take_Suc_conv_app_nth by fastforce + with Suc show ?case by(cases "n < length (tms_of ap)", auto) +qed lemma tpa_states: "\tp = concat (take as (tms_of ap)); @@ -615,8 +604,7 @@ tp1 = concat (take as (tms_of ap)) \ tp2 = concat (drop (Suc as) (tms_of ap))" by blast then have b: "start_of (layout_of ap) as = Suc (length tp1 div 2)" using fetch - apply(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits) - done + by(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits) have "fetch (tp1 @ (ci ly (start_of ly as) ins) @ tp2) s b = fetch (ci ly (start_of ly as) ins) (s - length tp1 div 2) b" proof(rule_tac append_append_fetch) @@ -625,8 +613,7 @@ by(auto, rule_tac compile_mod2) next show "length (ci ly (start_of ly as) ins) mod 2 = 0" - apply(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def) - by(arith, arith) + by(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def) next show "length tp1 div 2 < s \ s \ length tp1 div 2 + length (ci ly (start_of ly as) ins) div 2" @@ -694,17 +681,12 @@ using abc_fetch layout apply(case_tac b, simp_all add: Suc_diff_le) apply(case_tac [!] ins, simp_all add: start_of_Suc2 start_of_Suc1 start_of_Suc3) - apply(simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto) - using layout - apply(subgoal_tac [!] "start_of ly (Suc as) = start_of ly as + 2*nat1 + 16", simp_all) - apply(rule_tac [!] start_of_Suc2, auto) - done + by (simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto) from fetch and notfinal this show "?thesis"by simp qed ultimately show "?thesis" using assms - apply(drule_tac b= b and ins = ins in step_eq_fetch', auto) - done + by(drule_tac b= b and ins = ins in step_eq_fetch', auto) qed @@ -1245,8 +1227,7 @@ (is "\lm1 tn rn. ?P lm1 tn rn") proof - from k have "?P lm1 tn (rn - 1)" - apply(auto simp: Oc_def) - by(case_tac [!] "rn::nat", auto) + by (auto simp: Cons_replicate_eq) thus ?thesis by blast qed next @@ -1264,21 +1245,20 @@ (is "\lm1 tn rn. ?P lm1 tn rn") proof - from h1 and h2 have "?P lm1 0 (rn - 1)" - apply(auto simp: Oc_def - tape_of_nl_abv tape_of_nat_list.simps) + apply(auto simp:tape_of_nat_def) by(case_tac "rn::nat", simp, simp) thus ?thesis by blast qed qed -lemma [simp]: "inv_locate_a (as, am) (q, aaa, []) ires \ +lemma inv_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, []) ires \ inv_locate_a (as, am) (q, aaa, [Oc]) ires" apply(insert locate_a_2_locate_a [of as am q aaa "[]"]) apply(subgoal_tac "inv_locate_a (as, am) (q, aaa, [Bk]) ires", auto) done (*inv: from locate_b to locate_b*) -lemma [simp]: "inv_locate_b (as, am) (q, aaa, Oc # xs) ires +lemma inv_locate_b[simp]: "inv_locate_b (as, am) (q, aaa, Oc # xs) ires \ inv_locate_b (as, am) (q, Oc # aaa, xs) ires" apply(simp only: inv_locate_b.simps in_middle.simps) apply(erule exE)+ @@ -1289,15 +1269,15 @@ apply(case_tac mr, simp_all, auto) done -lemma [simp]: "<[x::nat]> = Oc\(Suc x)" -apply(simp add: tape_of_nat_abv tape_of_nl_abv) +lemma tape_nat[simp]: "<[x::nat]> = Oc\(Suc x)" +apply(simp add: tape_of_nat_def tape_of_list_def) done -lemma [simp]: " <([]::nat list)> = []" -apply(simp add: tape_of_nl_abv) +lemma tape_empty_list[simp]: " <([]::nat list)> = []" +apply(simp add: tape_of_list_def) done -lemma [simp]: "\inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \n. xs = Bk\n\ +lemma inv_locate[simp]: "\inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \n. xs = Bk\n\ \ inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires" apply(simp add: inv_locate_b.simps inv_locate_a.simps) apply(rule_tac disjI2, rule_tac disjI1) @@ -1628,8 +1608,8 @@ apply(rule_tac x = "lm2" in exI, simp) apply(simp only: Suc_diff_le exp_ind) apply(subgoal_tac "lm2 = []", simp) -apply(drule_tac length_equal, simp) -done + apply(drule_tac length_equal, simp) + by (metis (no_types, lifting) add_diff_inverse_nat append.assoc append_eq_append_conv length_append length_replicate list.inject) lemma [simp]: "inv_locate_b (as, am) (n, aaa, []) ires \ inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) @@ -1819,15 +1799,14 @@ apply(case_tac "hd l", simp, simp, simp) done -(*inv: from on_left_moving to check_left_moving*) -lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) +lemma from_on_left_moving_to_check_left_moving[simp]: "inv_on_left_moving_in_middle_B (as, lm) (s, Bk # list, Bk # r) ires \ inv_check_left_moving_on_leftmost (as, lm) (s', list, Bk # Bk # r) ires" apply(auto simp: inv_on_left_moving_in_middle_B.simps inv_check_left_moving_on_leftmost.simps split: if_splits) apply(case_tac [!] "rev lm1", simp_all) -apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps) +apply(case_tac [!] lista, simp_all add: tape_of_nat_def tape_of_list_def) done lemma [simp]: @@ -1895,11 +1874,11 @@ apply(erule_tac exE)+ apply(rule_tac x = "rev (tl (rev lm1))" in exI, rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto) -apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_abv tape_of_nl_abv tape_of_nat_list.simps) +apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_def tape_of_list_def tape_of_nat_list.simps) apply(case_tac [!] a, simp_all) -apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto) -apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto) -apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps) +apply(case_tac [1] lm2, auto simp:tape_of_nat_def) +apply(case_tac [3] lm2, auto simp:tape_of_nat_def) +apply(case_tac [!] lista, simp_all add: tape_of_nat_def) done lemma [simp]: @@ -3320,7 +3299,7 @@ by(auto intro:wf_inv_image simp:abc_dec_2_LE_def lex_square_def lex_triple_def lex_pair_def) lemma fix_add: "fetch ap ((x::nat) + 2*n) b = fetch ap (2*n + x) b" -by (metis Suc_1 mult_2 nat_add_commute) + using Suc_1 add.commute by metis lemma [elim]: "\0 < abc_lm_v am n; inv_locate_n_b (as, am) (n, aaa, Bk # xs) ires\ @@ -3486,9 +3465,7 @@ abc_fetch as ap = Some (Dec n e)\ \ crsp (layout_of ap) (abc_step_l (as, lm) (Some (Dec n e))) (start_of (layout_of ap) as + 2 * n + 16, a, b) ires" -apply(auto simp: inv_stop.simps crsp.simps abc_step_l.simps startof_Suc2) -apply(drule_tac startof_Suc2, simp) -done + by(auto simp: inv_stop.simps crsp.simps abc_step_l.simps startof_Suc2) lemma crsp_step_dec_b_suc: assumes layout: "ly = layout_of ap" @@ -3693,7 +3670,7 @@ lemma length_tp'[simp]: "\ly = layout_of ap; tp = tm_of ap\ \ - length tp = 2 * listsum (take (length ap) (layout_of ap))" + length tp = 2 * sum_list (take (length ap) (layout_of ap))" proof(induct ap arbitrary: ly tp rule: rev_induct) case Nil thus "?case" @@ -3701,18 +3678,18 @@ next fix x xs ly tp assume ind: "\ly tp. \ly = layout_of xs; tp = tm_of xs\ \ - length tp = 2 * listsum (take (length xs) (layout_of xs))" + length tp = 2 * sum_list (take (length xs) (layout_of xs))" and layout: "ly = layout_of (xs @ [x])" and tp: "tp = tm_of (xs @ [x])" obtain ly' where a: "ly' = layout_of xs" by metis obtain tp' where b: "tp' = tm_of xs" by metis - have c: "length tp' = 2 * listsum (take (length xs) (layout_of xs))" + have c: "length tp' = 2 * sum_list (take (length xs) (layout_of xs))" using a b by(erule_tac ind, simp) thus "length tp = 2 * - listsum (take (length (xs @ [x])) (layout_of (xs @ [x])))" + sum_list (take (length (xs @ [x])) (layout_of (xs @ [x])))" using tp b apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci) apply(case_tac x) diff -r d5a0e25c4742 -r a9003e6d0463 thys/Abacus_Mopup.thy --- a/thys/Abacus_Mopup.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Abacus_Mopup.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,7 +2,7 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Mopup Turing Machine that deletes all "registers", except one *} +chapter {* Mopup Turing Machine that deletes all "registers", except one *} theory Abacus_Mopup imports Uncomputable @@ -156,7 +156,7 @@ "\n < length lm; 0 < s; s \ 2 * n; s mod 2 = 0\ \ (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)" apply(subgoal_tac "\ q. s = 2 * q", auto) -apply(case_tac qa, simp, simp) +apply(case_tac q, simp, simp) apply(auto simp: fetch.simps nth_of.simps nth_append) apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! ((4 * nat) + 2)", @@ -290,12 +290,12 @@ lemma tape_of_nl_cons: " = (if lm = [] then Oc\(Suc m) else Oc\(Suc m) @ Bk # )" -apply(case_tac lm, simp_all add: tape_of_nl_abv tape_of_nat_abv split: if_splits) -done + by(case_tac lm, simp_all add: tape_of_list_def tape_of_nat_def split: if_splits) lemma drop_tape_of_cons: "\Suc q < length lm; x = lm ! q\ \ = Oc # Oc \ x @ Bk # " -by (metis Suc_lessD append_Cons list.simps(2) nth_drop' replicate_Suc tape_of_nl_cons) + using Suc_lessD append_Cons list.simps(2) Cons_nth_drop_Suc replicate_Suc tape_of_nl_cons + by metis lemma erase2jumpover1: "\q < length list; @@ -307,8 +307,8 @@ apply(rule_tac drop_tape_of_cons, simp_all) apply(subgoal_tac "length list = Suc q", auto) apply(subgoal_tac "drop q list = [list ! q]") -apply(simp add: tape_of_nl_abv tape_of_nat_abv replicate_Suc) -by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI) +apply(simp add: tape_of_nat_def tape_of_list_def replicate_Suc) +by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI) lemma erase2jumpover2: "\q < length list; \rn. @ Bk # Bk \ n \ @@ -319,8 +319,8 @@ apply(erule_tac notE, simp add: replicate_Suc) apply(rule_tac drop_tape_of_cons, simp_all) apply(subgoal_tac "length list = Suc q", auto) -apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv) -by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons) +apply(erule_tac x = "n" in allE, simp add: tape_of_list_def) +by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI replicate_Suc tape_of_list_def tape_of_nl_cons) lemma mod_ex1: "(a mod 2 = Suc 0) = (\ q. a = Suc (2 * q))" by arith @@ -449,12 +449,10 @@ apply(rule mopup_jump_over1_2_aft_erase_a, simp) apply(auto simp: mopup_jump_over1.simps) apply(rule_tac x = ln in exI, rule_tac x = "Suc (lm ! n)" in exI, - rule_tac x = 0 in exI, simp add: tape_of_nl_abv ) + rule_tac x = 0 in exI, simp add: tape_of_list_def ) done -lemma [simp]: "<[]> = []" -apply(simp add: tape_of_nl_abv) -done +lemma [simp]: "<[]> = []" by(simp add: tape_of_list_def) lemma [simp]: "\n < length lm; @@ -467,7 +465,7 @@ apply(case_tac a, simp_all) apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) -apply(case_tac a, simp, simp add: tape_of_nl_abv tape_of_nat_abv) +apply(case_tac a, simp, simp add: tape_of_list_def tape_of_nat_def) apply(case_tac a, simp_all) apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp) apply(rule_tac x = rn in exI, simp) @@ -519,7 +517,7 @@ apply(case_tac a, simp_all) apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) -apply(simp add: tape_of_nl_abv tape_of_nat_abv) +apply(simp add: tape_of_list_def tape_of_nat_def) done lemma [intro]: "\rna ml. Oc \ a @ Bk # @ Bk \ rn = @@ -655,7 +653,7 @@ "\n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\ \ mopup_stop (0, Bk # l, xs) lm n ires" apply(auto simp: mopup_jump_over2.simps mopup_stop.simps) -apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym]) +apply(simp_all add: tape_of_nat_def exp_ind[THEN sym]) done lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False" @@ -791,8 +789,7 @@ have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \ abc_mopup_measure" apply(case_tac c, case_tac [2] aa) apply(auto split:if_splits simp add:step.simps mopup_inv.simps) - apply(simp_all add: mopupfetchs abc_mopup_measure_def) - done + by (auto split:if_splits simp: mopupfetchs abc_mopup_measure_def) thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) (mopup_a n @ shift mopup_b (2 * n), 0), n), steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) @@ -840,7 +837,7 @@ (mopup_a n @ shift mopup_b (2 * n), 0) stp") apply(simp add: mopup_inv.simps mopup_stop.simps rs) using rs - apply(simp add: tape_of_nat_abv) + apply(simp add: tape_of_nat_def) done qed diff -r d5a0e25c4742 -r a9003e6d0463 thys/Rec_Def.thy --- a/thys/Rec_Def.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Rec_Def.thy Wed Dec 19 16:10:58 2018 +0100 @@ -28,7 +28,7 @@ termination apply(relation "measures [\ (r, xs). size r, (\ (r, xs). last xs)]") -apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation') +apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 size_list_estimation'[THEN trans_le_add1]) done inductive terminate :: "recf \ nat list \ bool" diff -r d5a0e25c4742 -r a9003e6d0463 thys/Recursive.thy --- a/thys/Recursive.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Recursive.thy Wed Dec 19 16:10:58 2018 +0100 @@ -165,9 +165,8 @@ ((nat \ nat list) \ nat \ nat)) set" where "addition_LE \ (inv_image lex_triple addition_measure)" -lemma [simp]: "wf addition_LE" -by(auto simp: wf_inv_image addition_LE_def lex_triple_def - lex_pair_def) +lemma wf_additon_LE[simp]: "wf addition_LE" + by(auto simp: addition_LE_def lex_triple_def lex_pair_def) declare addition_inv.simps[simp del] @@ -178,28 +177,28 @@ apply(rule_tac x = "lm ! m" in exI, simp) done -lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)" +lemma abs_fetch_0[simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)" by(simp add: abc_fetch.simps addition.simps) -lemma [simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)" +lemma abs_fetch_1[simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)" by(simp add: abc_fetch.simps addition.simps) -lemma [simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)" +lemma abs_fetch_2[simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)" by(simp add: abc_fetch.simps addition.simps) -lemma [simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)" +lemma abs_fetch_3[simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)" by(simp add: abc_fetch.simps addition.simps) -lemma [simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)" +lemma abs_fetch_4[simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)" by(simp add: abc_fetch.simps addition.simps) -lemma [simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)" +lemma abs_fetch_5[simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)" by(simp add: abc_fetch.simps addition.simps) -lemma [simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)" +lemma abs_fetch_6[simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)" by(simp add: abc_fetch.simps addition.simps) -lemma [simp]: +lemma exists_small_list_elem1[simp]: "\m \ n; p < length lm; lm ! p = 0; m < p; n < p; x \ lm ! m; 0 < x\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xam \ n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\ \ \xa\lm ! m. lm[m := x, n := lm ! n + lm ! m - x, p := lm ! m - x] = @@ -238,7 +237,7 @@ apply(rule_tac x = x in exI, simp) done -lemma [simp]: +lemma exists_small_list_elem5[simp]: "\m \ n; p < length lm; lm ! p = 0; m < p; n < p; x \ lm ! m; lm ! m \ x\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xa\lm ! m. lm[m := Suc x, n := lm ! n + lm ! m, p := lm ! m - Suc x] @@ -311,8 +310,8 @@ by(auto simp: addition.simps) lemma addition_correct: - "\m \ n; max m n < p; length lm > p; lm ! p = 0\ - \ {\ a. a = lm} (addition m n p) {\ nl. addition_inv (7, nl) m n p lm}" + assumes "m \ n" "max m n < p" "length lm > p" "lm ! p = 0" + shows "{\ a. a = lm} (addition m n p) {\ nl. addition_inv (7, nl) m n p lm}" using assms proof(rule_tac abc_Hoare_haltI, simp) fix lma @@ -480,27 +479,27 @@ rule_tac x = "initlm ! n" in exI, simp) done -lemma [simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)" +lemma abc_fetch_0[simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)" apply(simp add: mv_box.simps abc_fetch.simps) done -lemma [simp]: "abc_fetch (Suc 0) (mv_box m n) = +lemma abc_fetch_1[simp]: "abc_fetch (Suc 0) (mv_box m n) = Some (Inc n)" apply(simp add: mv_box.simps abc_fetch.simps) done -lemma [simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)" +lemma abc_fetch_2[simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)" apply(simp add: mv_box.simps abc_fetch.simps) done -lemma [simp]: "abc_fetch 3 (mv_box m n) = None" +lemma abc_fetch_3[simp]: "abc_fetch 3 (mv_box m n) = None" apply(simp add: mv_box.simps abc_fetch.simps) done lemma replicate_Suc_iff_anywhere: "x # x\b @ ys = x\(Suc b) @ ys" by simp -lemma [simp]: +lemma exists_smaller_in_list0[simp]: "\m \ n; m < length initlm; n < length initlm; k + l = initlm ! m + initlm ! n; k \ initlm ! m; 0 < k\ \ \ka la. initlm[m := k, n := l, m := k - Suc 0] = @@ -517,7 +516,7 @@ apply(simp add: list_update_swap) done -lemma [simp]: +lemma exists_smaller_in_list1[simp]: "\m \ n; m < length initlm; n < length initlm; Suc (k + l) = initlm ! m + initlm ! n; k < initlm ! m\ @@ -528,7 +527,7 @@ apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, auto) done -lemma [simp]: +lemma abc_steps_prop[simp]: "\length initlm > max m n; m \ n\ \ \na. \ (\(as, lm) m. as = 3) (abc_steps_l (0, initlm) (mv_box m n) na) m \ @@ -598,7 +597,7 @@ declare list_update.simps(2)[simp del] -lemma [simp]: +lemma zero_case_rec_exec[simp]: "\length xs < gf; gf \ ft; n < length gs\ \ (rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) [ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] = @@ -676,8 +675,9 @@ hence c: "length xs = ga" using a param_pattern by metis have d: "gf > ga" using footprint_ge a by simp - have e: "ft \ gf" using ft a h - by(simp, rule_tac min_max.le_supI2, rule_tac Max_ge, simp, + have e: "ft \ gf" + using ft a h Max_ge image_eqI + by(simp, rule_tac max.coboundedI2, rule_tac Max_ge, simp, rule_tac insertI2, rule_tac f = "(\(aprog, p, n). n)" and x = "rec_ci (gs!n)" in image_eqI, simp, rule_tac x = "gs!n" in image_eqI, simp, simp) @@ -780,7 +780,7 @@ lemma exp_suc: "a\Suc b = a\b @ [a]" by(simp add: exp_ind del: replicate.simps) -lemma [simp]: +lemma last_0[simp]: "\Suc n \ ba - aa; length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\ \ (last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = (0::nat)" @@ -796,25 +796,25 @@ done qed -lemma [simp]: "length lm1 = aa \ +lemma butlast_last[simp]: "length lm1 = aa \ (lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (aa + n) = last lm2" apply(simp add: nth_append) done -lemma [simp]: "\Suc n \ ba - aa; aa < ba\ \ +lemma arith_as_simp[simp]: "\Suc n \ ba - aa; aa < ba\ \ (ba < Suc (aa + (ba - Suc (aa + n) + n))) = False" apply arith done -lemma [simp]: "\Suc n \ ba - aa; aa < ba; length lm1 = aa; +lemma butlast_elem[simp]: "\Suc n \ ba - aa; aa < ba; length lm1 = aa; length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\ \ (lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba + n) = 0" -using nth_append[of "lm1 @ (0\'a)\n @ last lm2 # lm3 @ butlast lm2" - "(0\'a) # lm4" "ba + n"] +using nth_append[of "lm1 @ (0::'a)\n @ last lm2 # lm3 @ butlast lm2" + "(0::'a) # lm4" "ba + n"] apply(simp) done -lemma [simp]: +lemma update_butlast_eq0[simp]: "\Suc n \ ba - aa; aa < ba; length lm1 = aa; length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\ \ (lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2 @ (0::nat) # lm4) @@ -822,18 +822,17 @@ lm1 @ 0 # 0\n @ lm3 @ lm2 @ lm4" using list_update_append[of "lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2" "0 # lm4" "ba + n" "last lm2"] -apply(simp) -apply(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere exp_suc - del: replicate_Suc) +apply(simp add: list_update_append list_update.simps(2-) replicate_Suc_iff_anywhere exp_suc + del: replicate_Suc) apply(case_tac lm2, simp, simp) done -lemma [simp]: +lemma update_butlast_eq1[simp]: "\Suc (length lm1 + n) \ ba; length lm2 = Suc n; length lm3 = ba - Suc (length lm1 + n); \ ba - Suc (length lm1) < ba - Suc (length lm1 + n); \ ba + n - length lm1 < n\ \ (0::nat) \ n @ (last lm2 # lm3 @ butlast lm2 @ 0 # lm4)[ba - length lm1 := last lm2, 0 := 0] = 0 # 0 \ n @ lm3 @ lm2 @ lm4" -apply(subgoal_tac "ba - length lm1 = Suc n + length lm3", simp add: list_update.simps list_update_append) +apply(subgoal_tac "ba - length lm1 = Suc n + length lm3", simp add: list_update.simps(2-) list_update_append) apply(simp add: replicate_Suc_iff_anywhere exp_suc del: replicate_Suc) apply(case_tac lm2, simp, simp) apply(auto) @@ -892,7 +891,7 @@ by(simp add: mv_boxes.simps) qed -lemma [simp]: +lemma update_butlast_eq2[simp]: "\Suc n \ aa - length lm1; length lm1 < aa; length lm2 = aa - Suc (length lm1 + n); length lm3 = Suc n; @@ -980,9 +979,9 @@ by(simp add: replicate_merge_anywhere) qed -lemma [intro]: - "length gs \ ffp \ length gs \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" - apply(rule_tac min_max.le_supI2) +lemma length_le_max_insert_rec_ci[intro]: + "length gs \ ffp \ length gs \ max x1 (Max (insert ffp (x2 ` x3 ` set gs)))" + apply(rule_tac max.coboundedI2) apply(simp add: Max_ge_iff) done @@ -1006,10 +1005,8 @@ by(simp add: replicate_merge_anywhere le_add_diff_inverse) qed -lemma [intro]: "ffp \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" -apply(rule_tac min_max.le_supI2) -apply(rule_tac Max_ge, auto) -done +lemma le_max_insert[intro]: "ffp \ max x0 (Max (insert ffp (x1 ` x2 ` set gs)))" + by (rule max.coboundedI2) auto declare max_less_iff_conj[simp del] @@ -1046,7 +1043,7 @@ by(simp) qed -lemma [simp]: "length (empty_boxes n) = 2*n" +lemma length_empty_boxes[simp]: "length (empty_boxes n) = 2*n" apply(induct n, simp, simp) done @@ -1101,17 +1098,17 @@ show "{\nl. nl = 0 \ n @ drop n lm} [Dec n 2, Goto 0] {\nl. nl = 0 # 0 \ n @ drop (Suc n) lm}" using empty_one_box_correct[of n "lm ! n" "drop (Suc n) lm"] using h - by(simp add: nth_drop') + by(simp add: Cons_nth_drop_Suc) qed thus "?case" by(simp add: empty_boxes.simps) qed -lemma [simp]: "length gs \ ffp \ - length gs + (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) = - max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" +lemma insert_dominated[simp]: "length gs \ ffp \ + length gs + (max xs (Max (insert ffp (x1 ` x2 ` set gs))) - length gs) = + max xs (Max (insert ffp (x1 ` x2 ` set gs)))" apply(rule_tac le_add_diff_inverse) -apply(rule_tac min_max.le_supI2) +apply(rule_tac max.coboundedI2) apply(simp add: Max_ge_iff) done @@ -1317,14 +1314,14 @@ done qed -lemma [simp]: +lemma mv_box_correct_simp[simp]: "\length xs = n; ft = max (n+3) (max fft gft)\ \ {\nl. nl = xs @ 0 # 0 \ (ft - n) @ anything} mv_box n ft {\nl. nl = xs @ 0 # 0 \ (ft - n) @ anything}" using mv_box_correct[of n ft "xs @ 0 # 0 \ (ft - n) @ anything"] by(auto) -lemma [simp]: "length xs < max (length xs + 3) (max fft gft)" +lemma length_under_max[simp]: "length xs < max (length xs + 3) fft" by auto lemma save_init_rs: @@ -1336,13 +1333,13 @@ apply(case_tac "(max (length xs + 3) (max fft gft))", simp_all add: list_update.simps Suc_diff_le) done -lemma [simp]: "n + (2::nat) < max (n + 3) (max fft gft)" +lemma less_then_max_plus2[simp]: "n + (2::nat) < max (n + 3) x" by auto -lemma [simp]: "n < max (n + (3::nat)) (max fft gft)" +lemma less_then_max_plus3[simp]: "n < max (n + (3::nat)) x" by auto -lemma [simp]: +lemma mv_box_max_plus_3_correct[simp]: "length xs = n \ {\nl. nl = xs @ x # 0 \ (max (n + (3::nat)) (max fft gft) - n) @ anything} mv_box n (max (n + 3) (max fft gft)) {\nl. nl = xs @ 0 \ (max (n + 3) (max fft gft) - n) @ x # anything}" @@ -1373,13 +1370,13 @@ by simp qed -lemma [simp]: "max n (Suc n) < Suc (Suc (max (n + 3) (max fft gft) + length anything - Suc 0))" +lemma max_less_suc_suc[simp]: "max n (Suc n) < Suc (Suc (max (n + 3) x + anything - Suc 0))" by arith -lemma [simp]: "Suc n < max (n + 3) (max fft gft)" +lemma suc_less_plus_3[simp]: "Suc n < max (n + 3) x" by arith -lemma [simp]: +lemma mv_box_ok_suc_simp[simp]: "length xs = n \ {\nl. nl = xs @ rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything} mv_box n (Suc n) {\nl. nl = xs @ 0 # rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything}" @@ -1462,11 +1459,11 @@ apply(rule_tac abc_append_frist_steps_halt_eq', simp_all) done -lemma [simp]: "Suc (Suc (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))) - = max (length xs + 3) (max fft gft) - (length xs)" +lemma suc_suc_max_simp[simp]: "Suc (Suc (max (xs + 3) fft - Suc (Suc ( xs)))) + = max ( xs + 3) fft - ( xs)" by arith -lemma [simp]: "\ft = max (n + 3) (max fft gft); length xs = n\ \ +lemma contract_dec_ft_length_plus_7[simp]: "\ft = max (n + 3) (max fft gft); length xs = n\ \ {\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything} [Dec ft (length gap + 7)] {\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything}" @@ -1506,9 +1503,8 @@ then obtain stp where "abc_steps_l (0, xs @ Suc x # y # anything) [Dec (Suc n) 2, Goto 0] stp = (2, xs @ Suc x # 0 # anything)" using h - apply(auto simp: abc_Hoare_halt_def) - by(case_tac "abc_steps_l (0, xs @ Suc x # y # anything) [Dec (Suc (length xs)) 2, Goto 0] n", - simp_all add: numeral_2_eq_2) + apply(auto simp: abc_Hoare_halt_def numeral_2_eq_2) + by (metis (mono_tags, lifting) abc_final.simps abc_holds_for.elims(2) length_Cons list.size(3)) moreover have "abc_steps_l (0, xs @ Suc x # Suc y # anything) [Dec (Suc n) 2, Goto 0] 2 = (0, xs @ Suc x # y # anything)" using h @@ -1526,7 +1522,7 @@ using adjust_paras'[of xs n x y anything] by(simp add: abc_comp.simps abc_shift.simps numeral_2_eq_2 numeral_3_eq_3) -lemma [simp]: "\rec_ci g = (gap, gar, gft); \yrec_ci g = (gap, gar, gft); \yx\ \ gar = Suc (Suc n)" apply(erule_tac x = y in allE, simp) apply(drule_tac param_pattern, auto) @@ -1583,7 +1579,7 @@ apply(simp add: rec_exec.simps) done -lemma [simp]: "Suc (max (n + 3) (max fft gft) - Suc (Suc (Suc n))) = max (n + 3) (max fft gft) - Suc (Suc n)" +lemma suc_max_simp[simp]: "Suc (max (n + 3) fft - Suc (Suc (Suc n))) = max (n + 3) fft - Suc (Suc n)" by arith lemma pr_loop: @@ -1691,7 +1687,7 @@ by(auto, rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add replicate_Suc_iff_anywhere del: replicate_Suc) qed -lemma [simp]: +lemma abc_lm_s_simp0[simp]: "length xs = n \ abc_lm_s (xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ 0 # anything) (max (n + 3) (max fft gft)) 0 = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything" @@ -1702,11 +1698,11 @@ apply(simp add: exp_suc[THEN sym] Suc_diff_Suc del: replicate_Suc) done -lemma [simp]: - "(xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # 0 \ (max (length xs + 3) +lemma index_at_zero_elem[simp]: + "(xs @ x # re # 0 \ (max (length xs + 3) (max fft gft) - Suc (Suc (length xs))) @ 0 # anything) ! max (length xs + 3) (max fft gft) = 0" -using nth_append_length[of "xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # +using nth_append_length[of "xs @ x # re # 0 \ (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" 0 anything] by(simp) @@ -1920,14 +1916,14 @@ declare mn_ind_inv.simps[simp del] -lemma [simp]: +lemma put_in_tape_small_enough0[simp]: "0 < rsx \ \y. (xs @ x # rsx # anything)[Suc (length xs) := rsx - Suc 0] = xs @ x # y # anything \ y \ rsx" apply(rule_tac x = "rsx - 1" in exI) apply(simp add: list_update_append list_update.simps) done -lemma [simp]: +lemma put_in_tape_small_enough1[simp]: "\y \ rsx; 0 < y\ \ \ya. (xs @ x # y # anything)[Suc (length xs) := y - Suc 0] = xs @ x # ya # anything \ ya \ rsx" apply(rule_tac x = "y - 1" in exI) @@ -1939,9 +1935,9 @@ lemma rec_ci_not_null[simp]: "(rec_ci f \ ([], a, b))" apply(case_tac f, auto simp: rec_ci_z_def rec_ci_s_def rec_ci.simps addition.simps rec_ci_id.simps) -apply(case_tac "rec_ci recf", auto simp: mv_box.simps) -apply(case_tac "rec_ci recf1", case_tac "rec_ci recf2", simp) -apply(case_tac "rec_ci recf", simp) +apply(case_tac "rec_ci x42", auto simp: mv_box.simps) +apply(case_tac "rec_ci x52", case_tac "rec_ci x53", simp) +apply(case_tac "rec_ci x62", simp) done lemma mn_correct: @@ -2231,12 +2227,12 @@ "\abc_list_crsp lma lmb; \ n. lma = lmb @ 0\n \ lmb = lma @ 0\n \ P \ \ P" by(auto simp: abc_list_crsp_def) -lemma [simp]: +lemma abc_list_crsp_simp[simp]: "\abc_list_crsp lma lmb; m < length lma; m < length lmb\ \ abc_list_crsp (lma[m := n]) (lmb[m := n])" by(auto simp: abc_list_crsp_def list_update_append) -lemma [simp]: +lemma abc_list_crsp_simp2[simp]: "\abc_list_crsp lma lmb; m < length lma; \ m < length lmb\ \ abc_list_crsp (lma[m := n]) (lmb @ 0 \ (m - length lmb) @ [n])" apply(auto simp: abc_list_crsp_def list_update_append) @@ -2245,7 +2241,7 @@ apply(simp add: upd_conv_take_nth_drop min_absorb1) done -lemma [simp]: +lemma abc_list_crsp_simp3[simp]: "\abc_list_crsp lma lmb; \ m < length lma; m < length lmb\ \ abc_list_crsp (lma @ 0 \ (m - length lma) @ [n]) (lmb[m := n])" apply(auto simp: abc_list_crsp_def list_update_append) @@ -2254,7 +2250,7 @@ apply(simp add: upd_conv_take_nth_drop min_absorb1) done -lemma [simp]: "\abc_list_crsp lma lmb; \ m < length lma; \ m < length lmb\ \ +lemma abc_list_crsp_simp4[simp]: "\abc_list_crsp lma lmb; \ m < length lma; \ m < length lmb\ \ abc_list_crsp (lma @ 0 \ (m - length lma) @ [n]) (lmb @ 0 \ (m - length lmb) @ [n])" by(auto simp: abc_list_crsp_def list_update_append replicate_merge_anywhere) @@ -2285,13 +2281,9 @@ "\a lm'. aa = a \ b = lm' \ \lma. abc_steps_l (0, lm) aprog stp = (a, lma) \ abc_list_crsp lm' lma" - and h: "abc_steps_l (0, lm @ 0\m) aprog (Suc stp) = (a, lm')" + and h: "abc_step_l (aa, b) (abc_fetch aa aprog) = (a, lm')" "abc_steps_l (0, lm @ 0\m) aprog stp = (aa, b)" "aprog \ []" - hence g1: "abc_steps_l (0, lm @ 0\m) aprog (Suc stp) - = abc_step_l (aa, b) (abc_fetch aa aprog)" - apply(rule_tac abc_step_red, simp) - done have "\lma. abc_steps_l (0, lm) aprog stp = (aa, lma) \ abc_list_crsp b lma" apply(rule_tac ind, simp) @@ -2304,7 +2296,7 @@ apply(rule_tac abc_step_red, simp) done show "\lma. abc_steps_l (0, lm) aprog (Suc stp) = (a, lma) \ abc_list_crsp lm' lma" - using g1 g2 g3 h + using g2 g3 h apply(auto) apply(case_tac "abc_step_l (aa, b) (abc_fetch aa aprog)", case_tac "abc_step_l (aa, lma) (abc_fetch aa aprog)", simp) @@ -2343,7 +2335,7 @@ apply(rule_tac list_crsp_simp2, auto) done -lemma [simp]: +lemma find_exponent_rec_exec[simp]: assumes a: "args @ [rec_exec f args] = lm @ 0 \ n" and b: "length args < length lm" shows "\m. lm = args @ rec_exec f args # 0 \ m" @@ -2353,7 +2345,7 @@ apply(drule_tac length_equal, simp) done -lemma [simp]: +lemma find_exponent_complex[simp]: "\args @ [rec_exec f args] = lm @ 0 \ n; \ length args < length lm\ \ \m. (lm @ 0 \ (length args - length lm) @ [Suc 0])[length args := 0] = args @ rec_exec f args # 0 \ m" @@ -2421,7 +2413,7 @@ by simp moreover have "?ft \ gft" using g compile2 - apply(rule_tac min_max.le_supI2, rule_tac Max_ge, simp, rule_tac insertI2) + apply(rule_tac max.coboundedI2, rule_tac Max_ge, simp, rule_tac insertI2) apply(rule_tac x = "rec_ci (gs ! i)" in image_eqI, simp) by(rule_tac x = "gs!i" in image_eqI, simp, simp) then have b:"?Q_tmp = ?Q" @@ -2526,12 +2518,12 @@ fix ap ar fp assume "rec_ci recf = (ap, ar, fp)" thus "\stp m l. steps0 (Suc 0, [Bk, Bk], ) - (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (listsum (layout_of (ap [+] dummy_abc ar)))) stp = + (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (sum_list (layout_of (ap [+] dummy_abc ar)))) stp = (0, Bk # Bk # Bk \ m, Oc # Oc \ rec_exec recf args @ Bk \ l)" using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0] assms param_pattern[of recf args ap ar fp] - by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc tm_of_rec_def, - simp add: exp_suc del: replicate_Suc) + by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc, + simp add: exp_suc del: replicate_Suc) qed lemma recursive_compile_to_tm_correct3: @@ -2541,12 +2533,12 @@ using recursive_compile_to_tm_correct2[OF assms] apply(auto simp add: Hoare_halt_def) apply(rule_tac x = stp in exI) -apply(auto simp add: tape_of_nat_abv) +apply(auto simp add: tape_of_nat_def) apply(rule_tac x = "Suc (Suc m)" in exI) apply(simp) done -lemma [simp]: +lemma list_all_suc_many[simp]: "list_all (\(acn, s). s \ Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \ list_all (\(acn, s). s \ Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" apply(induct xs, simp, simp) @@ -2557,7 +2549,7 @@ apply(simp add: shift.simps) done -lemma [simp]: "length (shift (mopup n) ss) = 4 * n + 12" +lemma length_shift_mopup[simp]: "length (shift (mopup n) ss) = 4 * n + 12" apply(auto simp: mopup.simps shift_append mopup_b_def) done @@ -2565,7 +2557,7 @@ apply(simp add: tm_of.simps) done -lemma [simp]: "k < length ap \ tms_of ap ! k = +lemma tms_of_at_index[simp]: "k < length ap \ tms_of ap ! k = ci (layout_of ap) (start_of (layout_of ap) k) (ap ! k)" apply(simp add: tms_of.simps tpairs_of.simps) done @@ -2668,7 +2660,6 @@ apply(erule_tac inc_state_all_le, simp_all) apply(erule_tac findnth_state_all_le2, simp_all) apply(rule_tac start_of_all_le) -apply(rule_tac dec_state_all_le, simp_all) apply(rule_tac start_of_all_le) done @@ -2682,7 +2673,7 @@ apply(simp add: nth_append) done -lemma [simp]: "length (tms_of ap) = length ap" +lemma length_tms_of[simp]: "length (tms_of ap) = length ap" apply(simp add: tms_of.simps tpairs_of.simps) done @@ -2709,12 +2700,12 @@ length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps) done -lemma [intro]: "length (ci ly y i) mod 2 = 0" +lemma ci_even[intro]: "length (ci ly y i) mod 2 = 0" apply(case_tac i, auto simp: ci.simps length_findnth tinc_b_def adjust.simps tdec_b_def) done -lemma [intro]: "listsum (map (length \ (\(x, y). ci ly x y)) zs) mod 2 = 0" +lemma sum_list_ci_even[intro]: "sum_list (map (length \ (\(x, y). ci ly x y)) zs) mod 2 = 0" apply(induct zs rule: rev_induct, simp) apply(case_tac x, simp) apply(subgoal_tac "length (ci ly a b) mod 2 = 0") @@ -2740,13 +2731,11 @@ apply(simp add: tm_of.simps) done -lemma [elim]: "list_all (\(acn, s). s \ Suc q) xs +lemma list_all_add_6E[elim]: "list_all (\(acn, s). s \ Suc q) xs \ list_all (\(acn, s). s \ q + (2 * n + 6)) xs" -apply(simp add: list_all_length) -apply(auto) -done +by(auto simp: list_all_length) -lemma [simp]: "length mopup_b = 12" +lemma mopup_b_12[simp]: "length mopup_b = 12" apply(simp add: mopup_b_def) done @@ -2756,43 +2745,43 @@ (W0, Suc (Suc (Suc (2 * n + q)))), (R, Suc (Suc (2 * n + q))), (W0, Suc (Suc (Suc (2 * n + q)))), (L, 5 + 2 * n + q), (L, 6 + 2 * n + q), (R, 0), (L, 6 + 2 * n + q)]" -apply(auto) -done +by(auto) -lemma [simp]: "(a, b) \ set (mopup_a n) \ b \ 2 * n + 6" +lemma mopup_le6[simp]: "(a, b) \ set (mopup_a n) \ b \ 2 * n + 6" apply(induct n, auto simp: mopup_a.simps) done -lemma [simp]: "(a, b) \ set (shift (mopup n) (listsum (layout_of ap))) - \ b \ (2 * listsum (layout_of ap) + length (mopup n)) div 2" +lemma shift_le2[simp]: "(a, b) \ set (shift (mopup n) x) + \ b \ (2 * x + length (mopup n)) div 2" apply(auto simp: mopup.simps shift_append shift.simps) -apply(auto simp: mopup_a.simps mopup_b_def) +apply(auto simp: mopup_b_def) done -lemma [intro]: " 2 \ 2 * listsum (layout_of ap) + length (mopup n)" +lemma mopup_ge2[intro]: " 2 \ x + length (mopup n)" apply(simp add: mopup.simps) done -lemma [intro]: " (2 * listsum (layout_of ap) + length (mopup n)) mod 2 = 0" -apply(auto simp: mopup.simps) -apply arith -done +lemma mopup_even[intro]: " (2 * x + length (mopup n)) mod 2 = 0" +by(auto simp: mopup.simps) -lemma [simp]: "b \ Suc x +lemma mopup_div_2[simp]: "b \ Suc x \ b \ (2 * x + length (mopup n)) div 2" -apply(auto simp: mopup.simps) -done +by(auto simp: mopup.simps) -lemma wf_tm_from_abacus: - "tp = tm_of ap \ - tm_wf (tp @ shift( mopup n) (length tp div 2), 0)" - using length_start_of_tm[of ap] all_le_start_of[of ap] -apply(auto simp: tm_wf.simps List.list_all_iff) -apply(case_tac n) -apply(simp add: mopup.simps) -apply(simp add: mopup.simps) -apply (metis mod_mult_right_eq mod_mult_self2 mod_mult_self2_is_0 mult_2_right nat_mult_commute numeral_Bit0) -sorry +lemma wf_tm_from_abacus: assumes "tp = tm_of ap" + shows "tm_wf0 (tp @ shift (mopup n) (length tp div 2))" +proof - + have "is_even (length (mopup n))" for n using tm_wf.simps by blast + moreover have "(aa, ba) \ set (mopup n) \ ba \ length (mopup n) div 2" for aa ba + by (metis (no_types, lifting) add_cancel_left_right case_prodD tm_wf.simps wf_mopup) + moreover have "(\x\set (tm_of ap). case x of (acn, s) \ s \ Suc (sum_list (layout_of ap))) \ + (a, b) \ set (tm_of ap) \ b \ sum_list (layout_of ap) + length (mopup n) div 2" + for a b s + by (metis (no_types, lifting) add_Suc add_cancel_left_right case_prodD div_mult_mod_eq le_SucE mult_2_right not_numeral_le_zero tm_wf.simps trans_le_add1 wf_mopup) + ultimately show ?thesis unfolding assms + using length_start_of_tm[of ap] all_le_start_of[of ap] tm_wf.simps + by(auto simp: List.list_all_iff shift.simps) +qed lemma wf_tm_from_recf: assumes compile: "tp = tm_of_rec recf" diff -r d5a0e25c4742 -r a9003e6d0463 thys/Turing.thy --- a/thys/Turing.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Turing.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,7 +2,7 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Turing Machines *} +chapter {* Turing Machines *} theory Turing imports Main @@ -216,25 +216,33 @@ abbreviation exponent :: "'a \ nat \ 'a list" ("_ \ _" [100, 99] 100) where "x \ n == replicate n x" -consts tape_of :: "'a \ cell list" ("<_>" 100) - -defs (overloaded) - tape_of_nat_abv: "<(n::nat)> \ Oc \ (Suc n)" - -fun tape_of_nat_list :: "'a list \ cell list" - where - "tape_of_nat_list [] = []" | - "tape_of_nat_list [n] = " | - "tape_of_nat_list (n#ns) = @ Bk # (tape_of_nat_list ns)" - -fun tape_of_nat_pair :: "'a \ 'b \ cell list" - where - "tape_of_nat_pair (n, m) = @ [Bk] @ " +class tape = + fixes tape_of :: "'a \ cell list" ("<_>" 100) -defs (overloaded) - tape_of_nl_abv: "<(ns::'a list)> \ tape_of_nat_list ns" - tape_of_nat_pair: "<(np::'a\'b)> \ tape_of_nat_pair np" +instantiation nat::tape begin + definition tape_of_nat where "tape_of_nat (n::nat) \ Oc \ (Suc n)" + instance by standard +end + +type_synonym nat_list = "nat list" + +instantiation list::(tape) tape begin + fun tape_of_nat_list :: "('a::tape) list \ cell list" + where + "tape_of_nat_list [] = []" | + "tape_of_nat_list [n] = " | + "tape_of_nat_list (n#ns) = @ Bk # (tape_of_nat_list ns)" + definition tape_of_list where "tape_of_list \ tape_of_nat_list" + instance by standard +end + +instantiation prod:: (tape, tape) tape begin + fun tape_of_nat_prod :: "('a::tape) \ ('b::tape) \ cell list" + where "tape_of_nat_prod (n, m) = @ [Bk] @ " + definition tape_of_prod where "tape_of_prod \ tape_of_nat_prod" + instance by standard +end fun shift :: "instr list \ nat \ instr list" @@ -270,7 +278,7 @@ lemma tm_comp_wf[intro]: "\tm_wf (A, 0); tm_wf (B, 0)\ \ tm_wf (A |+| B, 0)" -by (auto) +by (fastforce) lemma tm_comp_step: assumes unfinal: "\ is_final (step0 c A)" @@ -333,9 +341,8 @@ apply(auto simp del: tm_comp.simps) apply(case_tac "fetch A a Bk") apply(simp del: tm_comp.simps) -apply(subst tm_comp_fetch_in_A) -apply(auto)[4] -apply(case_tac "fetch A a (hd c)") +apply(subst tm_comp_fetch_in_A;force) +apply(case_tac "fetch A a (hd ca)") apply(simp del: tm_comp.simps) apply(subst tm_comp_fetch_in_A) apply(auto)[4] @@ -348,9 +355,9 @@ using h1 h2 apply(case_tac c) apply(case_tac a) -apply(auto simp add: prod_case_unfold Let_def) -apply(case_tac "hd c") -apply(auto simp add: prod_case_unfold) +apply(auto simp add: Let_def case_prod_beta') +apply(case_tac "hd ca") +apply(auto simp add: case_prod_beta') done lemma steps_in_range: diff -r d5a0e25c4742 -r a9003e6d0463 thys/Turing_Hoare.thy --- a/thys/Turing_Hoare.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Turing_Hoare.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,7 +2,7 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Hoare Rules for TMs *} +chapter {* Hoare Rules for TMs *} theory Turing_Hoare imports Turing @@ -145,7 +145,8 @@ next case False then obtain n3 where "n = n2 - n3" - by (metis diff_le_self le_imp_diff_is_add nat_add_commute nat_le_linear) + using diff_le_self le_imp_diff_is_add nat_le_linear + add.commute by metis moreover with eq show "\ is_final (steps0 (1, l, r) (A |+| B) n)" by (simp add: not_is_final[where ?n1.0="n2"]) diff -r d5a0e25c4742 -r a9003e6d0463 thys/UF.thy --- a/thys/UF.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/UF.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,10 +2,10 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Construction of a Universal Function *} +chapter {* Construction of a Universal Function *} theory UF -imports Rec_Def GCD Abacus +imports Rec_Def HOL.GCD Abacus begin text {* @@ -289,9 +289,6 @@ arity.simps[simp del] Sigma.simps[simp del] rec_sigma.simps[simp del] -lemma [simp]: "arity z = 1" - by(simp add: arity.simps) - lemma rec_pr_0_simp_rewrite: " rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs" by(simp add: rec_exec.simps) @@ -341,7 +338,7 @@ take_Suc_conv_app_nth) qed -lemma [simp]: "primerec f n \ arity f = n" +lemma arity_primerec[simp]: "primerec f n \ arity f = n" apply(case_tac f) apply(auto simp: arity.simps ) apply(erule_tac prime_mn_reverse) @@ -527,30 +524,28 @@ apply(rule_tac Min_le, auto) done -lemma [simp]: "{x. x \ Suc w \ Rr (xs @ [x])} +lemma expand_conj_in_set: "{x. x \ Suc w \ Rr (xs @ [x])} = (if Rr (xs @ [Suc w]) then insert (Suc w) {x. x \ w \ Rr (xs @ [x])} else {x. x \ w \ Rr (xs @ [x])})" by(auto, case_tac "x = Suc w", auto) -lemma [simp]: "Minr Rr xs w \ w \ Minr Rr xs (Suc w) = Minr Rr xs w" -apply(simp add: Minr.simps, auto) -apply(case_tac "\x\w. \ Rr (xs @ [x])", auto) -done - -lemma [simp]: "\x\w. \ Rr (xs @ [x]) \ +lemma Minr_strip_Suc[simp]: "Minr Rr xs w \ w \ Minr Rr xs (Suc w) = Minr Rr xs w" +by(cases "\x\w. \ Rr (xs @ [x])",auto simp add: Minr.simps expand_conj_in_set) + +lemma x_empty_set[simp]: "\x\w. \ Rr (xs @ [x]) \ {x. x \ w \ Rr (xs @ [x])} = {} " by auto -lemma [simp]: "\Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\ \ +lemma Minr_is_Suc[simp]: "\Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\ \ Minr Rr xs (Suc w) = Suc w" -apply(simp add: Minr.simps) +apply(simp add: Minr.simps expand_conj_in_set) apply(case_tac "\x\w. \ Rr (xs @ [x])", auto) done -lemma [simp]: "\Minr Rr xs w = Suc w; \ Rr (xs @ [Suc w])\ \ +lemma Minr_is_Suc_Suc[simp]: "\Minr Rr xs w = Suc w; \ Rr (xs @ [Suc w])\ \ Minr Rr xs (Suc w) = Suc (Suc w)" -apply(simp add: Minr.simps) +apply(simp add: Minr.simps expand_conj_in_set) apply(case_tac "\x\w. \ Rr (xs @ [x])", auto) apply(subgoal_tac "Min {x. x \ w \ Rr (xs @ [x])} \ {x. x \ w \ Rr (xs @ [x])}", simp) @@ -612,50 +607,45 @@ declare numeral_3_eq_3[simp] -lemma [intro]: "primerec rec_pred (Suc 0)" +lemma primerec_rec_pred_1[intro]: "primerec rec_pred (Suc 0)" apply(simp add: rec_pred_def) apply(rule_tac prime_cn, auto) apply(case_tac i, auto intro: prime_id) done -lemma [intro]: "primerec rec_minus (Suc (Suc 0))" +lemma primerec_rec_minus_2[intro]: "primerec rec_minus (Suc (Suc 0))" apply(auto simp: rec_minus_def) done -lemma [intro]: "primerec (constn n) (Suc 0)" +lemma primerec_constn_1[intro]: "primerec (constn n) (Suc 0)" apply(induct n) apply(auto simp: constn.simps intro: prime_z prime_cn prime_s) done -lemma [intro]: "primerec rec_sg (Suc 0)" +lemma primerec_rec_sg_1[intro]: "primerec rec_sg (Suc 0)" apply(simp add: rec_sg_def) apply(rule_tac k = "Suc (Suc 0)" in prime_cn, auto) apply(case_tac i, auto) apply(case_tac ia, auto intro: prime_id) done -lemma [simp]: "length (get_fstn_args m n) = n" - apply(induct n) - apply(auto simp: get_fstn_args.simps) - done - -lemma primerec_getpren[elim]: "\i < n; n \ m\ \ primerec (get_fstn_args m n ! i) m" +lemma primerec_getpren[elim]: "\i < n; n \ m\ \ primerec (get_fstn_args m n ! i) m" apply(induct n, auto simp: get_fstn_args.simps) apply(case_tac "i = n", auto simp: nth_append intro: prime_id) done -lemma [intro]: "primerec rec_add (Suc (Suc 0))" +lemma primerec_rec_add_2[intro]: "primerec rec_add (Suc (Suc 0))" apply(simp add: rec_add_def) apply(rule_tac prime_pr, auto) done -lemma [intro]:"primerec rec_mult (Suc (Suc 0))" +lemma primerec_rec_mult_2[intro]:"primerec rec_mult (Suc (Suc 0))" apply(simp add: rec_mult_def ) apply(rule_tac prime_pr, auto intro: prime_z) apply(case_tac i, auto intro: prime_id) done -lemma [elim]: "\primerec rf n; n \ Suc (Suc 0)\ \ +lemma primerec_ge_2_elim[elim]: "\primerec rf n; n \ Suc (Suc 0)\ \ primerec (rec_accum rf) n" apply(auto simp: rec_accum.simps) apply(simp add: nth_append, auto) @@ -670,11 +660,11 @@ apply(auto, simp add: nth_append, auto) done -lemma [simp]: "Rr (xs @ [0]) \ +lemma min_P0[simp]: "Rr (xs @ [0]) \ Min {x. x = (0::nat) \ Rr (xs @ [x])} = 0" by(rule_tac Min_eqI, simp, simp, simp) -lemma [intro]: "primerec rec_not (Suc 0)" +lemma primerec_rec_not_1[intro]: "primerec rec_not (Suc 0)" apply(simp add: rec_not_def) apply(rule prime_cn, auto) apply(case_tac i, auto intro: prime_id) @@ -825,24 +815,24 @@ declare rec_maxr.simps[simp del] Maxr.simps[simp del] declare le_lemma[simp] -lemma [simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x" +lemma min_with_suc3[simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x" by simp declare numeral_2_eq_2[simp] -lemma [intro]: "primerec rec_disj (Suc (Suc 0))" +lemma primerec_rec_disj_2[intro]: "primerec rec_disj (Suc (Suc 0))" apply(simp add: rec_disj_def, auto) apply(auto) apply(case_tac ia, auto intro: prime_id) done -lemma [intro]: "primerec rec_less (Suc (Suc 0))" +lemma primerec_rec_less_2[intro]: "primerec rec_less (Suc (Suc 0))" apply(simp add: rec_less_def, auto) apply(auto) apply(case_tac ia , auto intro: prime_id) done -lemma [intro]: "primerec rec_eq (Suc (Suc 0))" +lemma primerec_rec_eq_2[intro]: "primerec rec_eq (Suc (Suc 0))" apply(simp add: rec_eq_def) apply(rule_tac prime_cn, auto) apply(case_tac i, auto) @@ -850,13 +840,13 @@ apply(case_tac [!] i, auto intro: prime_id) done -lemma [intro]: "primerec rec_le (Suc (Suc 0))" +lemma primerec_rec_le_2[intro]: "primerec rec_le (Suc (Suc 0))" apply(simp add: rec_le_def) apply(rule_tac prime_cn, auto) apply(case_tac i, auto) done -lemma [simp]: +lemma take_butlast_list_plus_two[simp]: "length ys = Suc n \ (take n ys @ [ys ! n, ys ! n]) = ys @ [ys ! n]" apply(simp) @@ -868,11 +858,11 @@ lemma Maxr_Suc_simp: "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w else Maxr Rr xs w)" -apply(auto simp: Maxr.simps Max.insert) +apply(auto simp: Maxr.simps expand_conj_in_set) apply(rule_tac Max_eqI, auto) done -lemma [simp]: "min (Suc n) n = n" by simp +lemma min_Suc_1[simp]: "min (Suc n) n = n" by simp lemma Sigma_0: "\ i \ n. (f (xs @ [i]) = 0) \ Sigma f (xs @ [n]) = 0" @@ -880,7 +870,7 @@ apply(simp add: Sigma_Suc_simp_rewrite) done -lemma [elim]: "\kk Sigma f (xs @ [w]) = Suc w" apply(induct w) apply(simp add: Sigma.simps, simp) @@ -1058,28 +1048,23 @@ text {* The following lemmas shows more directly the menaing of @{text "quo"}: *} -lemma [elim!]: "y > 0 \ quo [x, y] = x div y" -proof(simp add: quo.simps Maxr.simps, auto, - rule_tac Max_eqI, simp, auto) +lemma quo_is_div: "y > 0 \ quo [x, y] = x div y" +proof - + { fix xa ya assume h: "y * ya \ x" "y > 0" hence "(y * ya) div y \ x div y" by(insert div_le_mono[of "y * ya" x y], simp) - from this and h show "ya \ x div y" by simp -next - fix xa - show "y * (x div y) \ x" - apply(subgoal_tac "y * (x div y) + x mod y = x") - apply(rule_tac k = "x mod y" in add_leD1, simp) - apply(simp) - done + from this and h have "ya \ x div y" by simp} + thus ?thesis by(simp add: quo.simps Maxr.simps, auto, + rule_tac Max_eqI, simp, auto) qed -lemma [intro]: "quo [x, 0] = 0" +lemma quo_zero[intro]: "quo [x, 0] = 0" by(simp add: quo.simps Maxr.simps) lemma quo_div: "quo [x, y] = x div y" -by(case_tac "y=0", auto) +by(case_tac "y=0", auto elim!:quo_is_div) text {* @{text "rec_noteq"} is the recursive function testing whether its @@ -1120,13 +1105,13 @@ (0),id (Suc (Suc 0)) (Suc (0)), id (Suc (Suc 0)) (0)]" -lemma [intro]: "primerec rec_conj (Suc (Suc 0))" +lemma primerec_rec_conj_2[intro]: "primerec rec_conj (Suc (Suc 0))" apply(simp add: rec_conj_def) apply(rule_tac prime_cn, auto)+ apply(case_tac i, auto intro: prime_id) done -lemma [intro]: "primerec rec_noteq (Suc (Suc 0))" +lemma primerec_rec_noteq_2[intro]: "primerec rec_noteq (Suc (Suc 0))" apply(simp add: rec_noteq_def) apply(rule_tac prime_cn, auto)+ apply(case_tac i, auto intro: prime_id) @@ -1189,13 +1174,7 @@ The correctness of @{text "rec_mod"}: *} lemma mod_lemma: "\ x y. rec_exec rec_mod [x, y] = (x mod y)" -proof(simp add: rec_exec.simps rec_mod_def quo_lemma2) - fix x y - show "x - x div y * y = x mod (y::nat)" - using mod_div_equality2[of y x] - apply(subgoal_tac "y * (x div y) = (x div y ) * y", arith, simp) - done -qed + by(simp add: rec_exec.simps rec_mod_def quo_lemma2 minus_div_mult_eq_mod) text{* lemmas for embranch function*} type_synonym ftype = "nat list \ nat" @@ -1604,7 +1583,7 @@ "fac 0 = 1" | "fac (Suc x) = (Suc x) * fac x" -lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0" +lemma rec_exec_rec_dummyfac_0: "rec_exec rec_dummyfac [0, 0] = Suc 0" by(simp add: rec_dummyfac_def rec_exec.simps) lemma rec_cn_simp: "rec_exec (Cn n f gs) xs = @@ -1648,7 +1627,7 @@ Cn 2 rec_prime [id 2 1]] in Cn 1 (rec_Minr Rr) [id 1 0, Cn 1 s [rec_fac]])" -lemma [simp]: "n < Suc (n!)" +lemma n_le_fact[simp]: "n < Suc (n!)" apply(induct n, simp) apply(simp add: fac.simps) apply(case_tac n, auto simp: fac.simps) @@ -1667,7 +1646,7 @@ apply(rule_tac x = u in exI, simp, auto) done -lemma [intro]: "0 < n!" +lemma fact_pos[intro]: "0 < n!" apply(induct n) apply(auto simp: fac.simps) done @@ -1740,7 +1719,7 @@ primerec (ys ! 0) n; primerec (ys ! 1) n\ \ primerec (ys ! i) n" by(case_tac i, auto) -lemma [intro]: "primerec rec_prime (Suc 0)" +lemma primerec_rec_prime_1[intro]: "primerec rec_prime (Suc 0)" apply(auto simp: rec_prime_def, auto) apply(rule_tac primerec_all_iff, auto, auto) apply(rule_tac primerec_all_iff, auto, auto simp: @@ -1835,7 +1814,7 @@ declare lo.simps[simp del] -lemma [elim]: "primerec rf n \ n > 0" +lemma primerec_then_ge_0[elim]: "primerec rf n \ n > 0" apply(induct rule: primerec.induct, auto) done @@ -1846,7 +1825,7 @@ apply(auto, auto simp: nth_append) done -lemma [intro!]: "\primerec rf n; n > 0\ \ primerec (rec_maxr rf) n" +lemma primerec_rec_maxr[intro!]: "\primerec rf n; n > 0\ \ primerec (rec_maxr rf) n" apply(simp add: rec_maxr.simps) apply(rule_tac prime_cn, auto) apply(rule_tac primerec_all_iff, auto, auto simp: nth_append) @@ -1859,23 +1838,10 @@ apply(case_tac i, auto, case_tac nat, simp, simp add: numeral_2_eq_2) done -lemma [intro]: "primerec rec_quo (Suc (Suc 0))" -apply(simp add: rec_quo_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}] 1*}, auto+)+ -done - -lemma [intro]: "primerec rec_mod (Suc (Suc 0))" -apply(simp add: rec_mod_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}] 1*}, auto+)+ -done - -lemma [intro]: "primerec rec_power (Suc (Suc 0))" -apply(simp add: rec_power_def numeral_2_eq_2 numeral_3_eq_3) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ -done +lemma primerec_2[intro]: +"primerec rec_quo (Suc (Suc 0))" "primerec rec_mod (Suc (Suc 0))" +"primerec rec_power (Suc (Suc 0))" + by(force simp: prime_cn prime_id rec_mod_def rec_quo_def rec_power_def prime_pr numeral)+ text {* @{text "rec_lo"} is the recursive function used to implement @{text "Lo"}. @@ -1919,14 +1885,12 @@ done qed -lemma [simp]: "Max {ya. ya = 0 \ loR [0, y, ya]} = 0" +lemma MaxloR0[simp]: "Max {ya. ya = 0 \ loR [0, y, ya]} = 0" apply(rule_tac Max_eqI, auto simp: loR.simps) done -lemma [simp]: "Suc 0 < y \ Suc (Suc 0) < y * y" -apply(induct y, simp) -apply(case_tac y, simp, simp) -done +lemma two_less_square[simp]: "Suc 0 < y \ Suc (Suc 0) < y * y" + by(induct y, auto) lemma less_mult: "\x > 0; y > Suc 0\ \ x < y * x" apply(case_tac y, simp, simp) @@ -1942,17 +1906,16 @@ lemma le_mult: "y \ (0::nat) \ x \ x * y" by(induct y, simp, simp) -lemma uplimit_loR: "\Suc 0 < x; Suc 0 < y; loR [x, y, xa]\ \ - xa \ x" -apply(simp add: loR.simps) -apply(rule_tac classical, auto) -apply(subgoal_tac "xa < y^xa") -apply(subgoal_tac "y^xa \ y^xa * q", simp) -apply(rule_tac le_mult, case_tac q, simp, simp) -apply(rule_tac x_less_exp, simp) -done - -lemma [simp]: "\xa \ x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\ \ +lemma uplimit_loR: + assumes "Suc 0 < x" "Suc 0 < y" "loR [x, y, xa]" + shows "xa \ x" +proof - + have "Suc 0 < x \ Suc 0 < y \ y ^ xa dvd x \ xa \ x" + by (meson Suc_lessD le_less_trans nat_dvd_not_less nat_le_linear x_less_exp) + thus ?thesis using assms by(auto simp: loR.simps) +qed + +lemma loR_set_strengthen[simp]: "\xa \ x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\ \ {u. loR [x, y, u]} = {ya. ya \ x \ loR [x, y, ya]}" apply(rule_tac Collect_cong, auto) apply(erule_tac uplimit_loR, simp, simp) @@ -2043,20 +2006,20 @@ by simp qed -lemma [simp]: "\Suc 0 < y; lgR [x, y, xa]\ \ xa \ x" +lemma lgR_ok: "\Suc 0 < y; lgR [x, y, xa]\ \ xa \ x" apply(simp add: lgR.simps) apply(subgoal_tac "y^xa > xa", simp) apply(erule x_less_exp) done -lemma [simp]: "\Suc 0 < x; Suc 0 < y; lgR [x, y, xa]\ \ +lemma lgR_set_strengthen[simp]: "\Suc 0 < x; Suc 0 < y; lgR [x, y, xa]\ \ {u. lgR [x, y, u]} = {ya. ya \ x \ lgR [x, y, ya]}" -apply(rule_tac Collect_cong, auto) +apply(rule_tac Collect_cong, auto simp:lgR_ok) done lemma maxr_lg: "\Suc 0 < x; Suc 0 < y\ \ Maxr lgR [x, y] x = lg x y" apply(simp add: lg.simps Maxr.simps, auto) -apply(erule_tac x = xa in allE, simp) +apply(erule_tac x = xa in allE, auto simp:lgR_ok) done lemma lg_lemma': "\Suc 0 < x; Suc 0 < y\ \ rec_exec rec_lg [x, y] = lg x y" @@ -2445,7 +2408,7 @@ apply(case_tac nat, auto simp: numeral_3_eq_3 numeral_4_eq_4) done -lemma [intro]: "primerec rec_scan (Suc 0)" +lemma primerec_rec_scan_1[intro]: "primerec rec_scan (Suc 0)" apply(auto simp: rec_scan_def, auto) done @@ -2682,7 +2645,7 @@ done qed -lemma [elim]: +lemma nonempty_listE: "Suc 0 \ length xs \ (map ((\a. rec_exec a (m # xs)) \ (\i. recf.id (Suc (length xs)) (i))) @@ -2703,7 +2666,7 @@ "(map ((\a. rec_exec a (m # xs)) \ (\i. recf.id (Suc (length xs)) (i))) [Suc 0.. n > 0" by(induct f n rule: primerec.induct, auto) -lemma [elim]: "primerec f 0 \ RR" +lemma primerec_not0E[elim]: "primerec f 0 \ RR" apply(drule_tac primerec_not0, simp) done -lemma [simp]: "length xs = Suc n \ length (butlast xs) = n" -apply(subgoal_tac "\ y ys. xs = ys @ [y]", auto) +lemma length_butlast[simp]: "length xs = Suc n \ length (butlast xs) = n" +apply(subgoal_tac "\ y ys. xs = ys @ [y]",force) apply(rule_tac x = "last xs" in exI) apply(rule_tac x = "butlast xs" in exI) apply(case_tac "xs = []", auto) done text {* - The lemma relates the interpreter of primitive fucntions with + The lemma relates the interpreter of primitive functions with the calculation relation of general recursive functions. *} declare numeral_2_eq_2[simp] numeral_3_eq_3[simp] -lemma [intro]: "primerec rec_right (Suc 0)" -apply(simp add: rec_right_def rec_lo_def Let_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ -done - -lemma [intro]: "primerec rec_pi (Suc 0)" -apply(simp add: rec_pi_def rec_dummy_pi_def - rec_np_def rec_fac_def rec_prime_def - rec_Minr.simps Let_def get_fstn_args.simps - arity.simps - rec_all.simps rec_sigma.simps rec_accum.simps) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ -apply(simp add: rec_dummyfac_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, +lemma primerec_rec_right_1[intro]: "primerec rec_right (Suc 0)" + by(auto simp: rec_right_def rec_lo_def Let_def;force) + +lemma primerec_rec_pi_helper: + "\ii0 < vl; n \ vl\ \ primerec (rec_listsum2 vl n) vl" +lemma primerec_rec_listsum2[intro!]: "\0 < vl; n \ vl\ \ primerec (rec_listsum2 vl n) vl" apply(induct n) apply(simp_all add: rec_strt'.simps Let_def rec_listsum2.simps) -apply(tactic {* resolve_tac [@{thm prime_cn}, +apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ done -lemma [elim]: "\0 < vl; n \ vl\ \ primerec (rec_strt' vl n) vl" +lemma primerec_rec_strt': "\0 < vl; n \ vl\ \ primerec (rec_strt' vl n) vl" apply(induct n) apply(simp_all add: rec_strt'.simps Let_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, +apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, @{thm prime_id}, @{thm prime_pr}] 1*}, auto+) done -lemma [elim]: "vl > 0 \ primerec (rec_strt vl) vl" +lemma primerec_rec_strt: "vl > 0 \ primerec (rec_strt vl) vl" apply(simp add: rec_strt.simps rec_strt'.simps) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ -done - -lemma [elim]: +by(tactic {* resolve_tac @{context} [@{thm prime_cn}, + @{thm prime_id}, @{thm prime_pr}] 1*}; force elim:primerec_rec_strt') + +lemma primerec_map_vl: "i < vl \ primerec ((map (\i. recf.id (Suc vl) (i)) [Suc 0.. primerec (rec_inpt (Suc vl)) (Suc vl)" -apply(simp add: rec_inpt_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ +apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, + @{thm prime_id}, @{thm prime_pr}] 1*};force)+ done -lemma [intro]: "primerec rec_conf (Suc (Suc (Suc 0)))" -apply(simp add: rec_conf_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ -apply(auto simp: numeral_4_eq_4) +lemma primerec_rec_newconf[intro]: "primerec rec_newconf (Suc (Suc 0))" +apply(simp add: rec_newconf_def) +by(tactic {* resolve_tac @{context} [@{thm prime_cn}, + @{thm prime_id}, @{thm prime_pr}] 1*};force) + +lemma primerec_rec_inpt[intro]: "0 < vl \ primerec (rec_inpt (Suc vl)) (Suc vl)" +apply(simp add: rec_inpt_def) +apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, + @{thm prime_id}, @{thm prime_pr}] 1*}; fastforce elim:primerec_rec_strt primerec_map_vl) done -lemma [intro]: "primerec rec_lg (Suc (Suc 0))" -apply(simp add: rec_lg_def Let_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ -done - -lemma [intro]: "primerec rec_nonstop (Suc (Suc (Suc 0)))" -apply(simp add: rec_nonstop_def rec_NSTD_def rec_stat_def +lemma primerec_rec_conf[intro]: "primerec rec_conf (Suc (Suc (Suc 0)))" +apply(simp add: rec_conf_def) +by(tactic {* resolve_tac @{context} [@{thm prime_cn}, + @{thm prime_id}, @{thm prime_pr}] 1*};force simp: numeral) + +lemma primerec_recs2[intro]: + "primerec rec_lg (Suc (Suc 0))" + "primerec rec_nonstop (Suc (Suc (Suc 0)))" +apply(simp_all add: rec_lg_def rec_nonstop_def rec_NSTD_def rec_stat_def rec_lo_def Let_def rec_left_def rec_right_def rec_newconf_def rec_newstat_def) -apply(tactic {* resolve_tac [@{thm prime_cn}, - @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ -done +by(tactic {* resolve_tac @{context} [@{thm prime_cn}, + @{thm prime_id}, @{thm prime_pr}] 1*};fastforce)+ lemma primerec_terminate: "\primerec f x; length xs = x\ \ terminate f xs" @@ -3087,9 +3005,7 @@ and ind2: "\xs. length xs = Suc (Suc n) \ terminate g xs" and h: "primerec f n" " primerec g (Suc (Suc n))" " m = Suc n" "length (xs::nat list) = m" have "\y (get_fstn_args m n ! k) = id m (k)" apply(induct n, simp) apply(case_tac "k = n", simp_all add: get_fstn_args.simps nth_append) done -lemma [simp]: +lemma get_fstn_args_is_id[simp]: "\ys \ []; k < length ys\ \ (get_fstn_args (length ys) (length ys) ! k) = @@ -3268,9 +3176,9 @@ subsection {* Relating interperter functions to the execution of TMs *} -lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps) - -lemma [simp]: "\fetch tp 0 b = (nact, ns)\ \ action_map nact = 4" +lemma bl2wc_0[simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps) + +lemma fetch_action_map_4[simp]: "\fetch tp 0 b = (nact, ns)\ \ action_map nact = 4" apply(simp add: fetch.simps) done @@ -3295,7 +3203,7 @@ declare godel_code.simps[simp del] -lemma [simp]: "0 < godel_code' nl n" +lemma godel_code'_nonzero[simp]: "0 < godel_code' nl n" apply(induct nl arbitrary: n) apply(auto simp: godel_code'.simps) done @@ -3308,14 +3216,14 @@ apply(auto simp: godel_code.simps) done -lemma [elim]: +lemma godel_code_1_iff[elim]: "\i < length nl; \ Suc 0 < godel_code nl\ \ nl ! i = 0" using godel_code_great[of nl] godel_code_eq_1[of nl] apply(simp) done lemma prime_coprime: "\Prime x; Prime y; x\y\ \ coprime x y" -proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def, +proof (simp only: Prime.simps coprime_def, auto simp: dvd_def, rule_tac classical, simp) fix d k ka assume case_ka: "\uv d * ka" @@ -3323,10 +3231,7 @@ and h: "(0::nat) < d" "d \ Suc 0" "Suc 0 < d * ka" "ka \ k" "Suc 0 < d * k" from h have "k > Suc 0 \ ka >Suc 0" - apply(auto) - apply(case_tac ka, simp, simp) - apply(case_tac k, simp, simp) - done + by (cases ka;cases k;force+) from this show "False" proof(erule_tac disjE) assume "(Suc 0::nat) < k" @@ -3402,7 +3307,7 @@ apply(simp) done -lemma [intro]: "Prime (Suc (Suc 0))" +lemma prime_2[intro]: "Prime (Suc (Suc 0))" apply(auto simp: Prime.simps) apply(case_tac u, simp, case_tac nat, simp, simp) done @@ -3431,15 +3336,10 @@ done lemma Pi_power_coprime: "i \ j \ coprime ((Pi i)^m) ((Pi j)^n)" -by(rule_tac coprime_exp2_nat, erule_tac Pi_coprime) + unfolding coprime_power_right_iff coprime_power_left_iff using Pi_coprime by auto lemma coprime_dvd_mult_nat2: "\coprime (k::nat) n; k dvd n * m\ \ k dvd m" -apply(erule_tac coprime_dvd_mult_nat) -apply(simp add: dvd_def, auto) -apply(rule_tac x = ka in exI) -apply(subgoal_tac "n * m = m * n", simp) -apply(simp add: nat_mult_commute) -done + unfolding coprime_dvd_mult_right_iff. declare godel_code'.simps[simp del] @@ -3504,7 +3404,7 @@ lemma Pi_coprime_pre: "length ps \ i \ coprime (Pi (Suc i)) (godel_code' ps (Suc 0))" -proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps) +proof(induct "length ps" arbitrary: ps) fix x ps assume ind: "\ps. \x = length ps; length ps \ i\ \ @@ -3518,20 +3418,19 @@ godel_code' (butlast ps) (Suc 0) * Pi (length ps)^(last ps)" using godel_code'_butlast_last_id[of ps 0] h by(case_tac ps, simp, simp) - from g have + from g have "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)" + unfolding coprime_power_right_iff using Pi_coprime h(2) by auto + with g have "coprime (Pi (Suc i)) (godel_code' (butlast ps) (Suc 0) * Pi (length ps)^(last ps)) " - proof(rule_tac coprime_mult_nat, simp) - show "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)" - apply(rule_tac coprime_exp_nat, rule prime_coprime, auto) - using Pi_notEq[of "Suc i" "length ps"] h by simp - qed + unfolding coprime_mult_right_iff coprime_power_right_iff by auto + from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))" by simp -qed +qed (auto simp add: godel_code'.simps) lemma Pi_coprime_suf: "i < j \ coprime (Pi i) (godel_code' ps j)" -proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps) +proof(induct "length ps" arbitrary: ps) fix x ps assume ind: "\ps. \x = length ps; i < j\ \ @@ -3547,13 +3446,11 @@ from g have "coprime (Pi i) (godel_code' (butlast ps) j * Pi (length ps + j - 1)^last ps)" - apply(rule_tac coprime_mult_nat, simp) - using Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h - apply(auto) - done + using Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h + by(auto) from k and this show "coprime (Pi i) (godel_code' ps j)" by auto -qed +qed (simp add: godel_code'.simps) lemma godel_finite: "finite {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}" @@ -3619,26 +3516,14 @@ assume mult_dvd: "Pi (Suc i) ^ y dvd ?pref * Pi (Suc i) ^ nl ! i * ?suf'" hence "Pi (Suc i) ^ y dvd ?pref * Pi (Suc i) ^ nl ! i" - proof(rule_tac coprime_dvd_mult_nat) - show "coprime (Pi (Suc i)^y) ?suf'" - proof - - have "coprime (Pi (Suc i) ^ y) (?suf'^(Suc 0))" - apply(rule_tac coprime_exp2_nat) - apply(rule_tac Pi_coprime_suf, simp) - done - thus "?thesis" by simp - qed + proof - + have "coprime (Pi (Suc i)^y) ?suf'" by (simp add: Pi_coprime_suf) + thus ?thesis using coprime_dvd_mult_left_iff mult_dvd by blast qed hence "Pi (Suc i) ^ y dvd Pi (Suc i) ^ nl ! i" proof(rule_tac coprime_dvd_mult_nat2) - show "coprime (Pi (Suc i) ^ y) ?pref" - proof - - have "coprime (Pi (Suc i)^y) (?pref^Suc 0)" - apply(rule_tac coprime_exp2_nat) - apply(rule_tac Pi_coprime_pre, simp) - done - thus "?thesis" by simp - qed + have "coprime (Pi (Suc i)^y) (?pref^Suc 0)" using Pi_coprime_pre by simp + thus "coprime (Pi (Suc i) ^ y) ?pref" by simp qed hence "Pi (Suc i) ^ y \ Pi (Suc i) ^ nl ! i " apply(rule_tac dvd_imp_le, auto) @@ -3654,7 +3539,7 @@ by(rule_tac godel_code_in, simp) qed -lemma [simp]: +lemma godel_code'_set[simp]: "{u. Pi (Suc i) ^ u dvd (Suc (Suc 0)) ^ length nl * godel_code' nl (Suc 0)} = {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}" @@ -3662,17 +3547,9 @@ apply(rule_tac n = " (Suc (Suc 0)) ^ length nl" in coprime_dvd_mult_nat2) proof - - fix u - show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)" - proof(rule_tac coprime_exp2_nat) - have "Pi 0 = (2::nat)" - apply(simp add: Pi.simps) - done - moreover have "coprime (Pi (Suc i)) (Pi 0)" - apply(rule_tac Pi_coprime, simp) - done - ultimately show "coprime (Pi (Suc i)) (Suc (Suc 0))" by simp - qed + have "Pi 0 = (2::nat)" by(simp add: Pi.simps) + show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)" for u + using Pi_coprime Pi.simps(1) by force qed lemma godel_code_get_nth: @@ -3680,10 +3557,6 @@ Max {u. Pi (Suc i) ^ u dvd godel_code nl} = nl ! i" by(simp add: godel_code.simps godel_code'_get_nth) -lemma "trpl l st r = godel_code' [l, st, r] 0" -apply(simp add: trpl.simps godel_code'.simps) -done - lemma mod_dvd_simp: "(x mod y = (0::nat)) = (y dvd x)" by(simp add: dvd_def, auto) @@ -3694,10 +3567,10 @@ done -lemma [elim]: "Pi n = 0 \ RR" +lemma Pi_nonzeroE[elim]: "Pi n = 0 \ RR" using Pi_not_0[of n] by simp -lemma [elim]: "Pi n = Suc 0 \ RR" +lemma Pi_not_oneE[elim]: "Pi n = Suc 0 \ RR" using Pi_gr_1[of n] by simp lemma finite_power_dvd: @@ -3725,15 +3598,9 @@ have "Pi m ^ y dvd Pi m ^ l" proof - have "Pi m ^ y dvd Pi m ^ l * Pi n ^ st" - using h g - apply(rule_tac n = "Pi k^r" in coprime_dvd_mult_nat) - apply(rule Pi_power_coprime, simp, simp) - done - thus "Pi m^y dvd Pi m^l" - apply(rule_tac n = " Pi n ^ st" in coprime_dvd_mult_nat) - using g - apply(rule_tac Pi_power_coprime, simp, simp) - done + using h g Pi_power_coprime + by (simp add: coprime_dvd_mult_left_iff) + thus "Pi m^y dvd Pi m^l" using g Pi_power_coprime coprime_dvd_mult_left_iff by blast qed thus "y \ (l::nat)" apply(rule_tac a = "Pi m" in power_le_imp_le_exp) @@ -3751,7 +3618,7 @@ apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto) done -lemma [simp]: "left (trpl l st r) = l" +lemma left_trpl_fst[simp]: "left (trpl l st r) = l" apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp) apply(auto simp: conf_decode1) apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r") @@ -3759,7 +3626,7 @@ apply(erule_tac x = l in allE, auto) done -lemma [simp]: "stat (trpl l st r) = st" +lemma stat_trpl_snd[simp]: "stat (trpl l st r) = st" apply(simp add: stat.simps trpl.simps lo.simps loR.simps mod_dvd_simp, auto) apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r @@ -3770,7 +3637,7 @@ apply(erule_tac x = st in allE, auto) done -lemma [simp]: "rght (trpl l st r) = r" +lemma rght_trpl_trd[simp]: "rght (trpl l st r) = r" apply(simp add: rght.simps trpl.simps lo.simps loR.simps mod_dvd_simp, auto) apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r @@ -3938,7 +3805,7 @@ by simp qed -lemma [simp]: "fetch tp 0 b = (nact, ns) \ ns = 0" +lemma fetch_zero_zero[simp]: "fetch tp 0 b = (nact, ns) \ ns = 0" by(simp add: fetch.simps) lemma Five_Suc: "5 = Suc 4" by simp @@ -4029,11 +3896,11 @@ qed -lemma [intro!]: +lemma tpl_eqI[intro!]: "\a = a'; b = b'; c = c'\ \ trpl a b c = trpl a' b' c'" by simp -lemma [simp]: "bl2wc [Bk] = 0" +lemma bl2wc_Bk[simp]: "bl2wc [Bk] = 0" by(simp add: bl2wc.simps bl2nat.simps) lemma bl2nat_double: "bl2nat xs (Suc n) = 2 * bl2nat xs n" @@ -4058,45 +3925,17 @@ qed -lemma [simp]: "2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 " -apply(case_tac c, simp, case_tac a) -apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double) -done - -lemma [simp]: +lemma bl2wc_simps[simp]: "bl2wc (Oc # tl c) = Suc (bl2wc c) - bl2wc c mod 2 " -apply(case_tac c, case_tac [2] a, simp) -apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double) -done - -lemma [simp]: "bl2wc (Bk # c) = 2*bl2wc (c)" -apply(simp add: bl2wc.simps bl2nat.simps bl2nat_double) -done - -lemma [simp]: "bl2wc [Oc] = Suc 0" - by(simp add: bl2wc.simps bl2nat.simps) - -lemma [simp]: "b \ [] \ bl2wc (tl b) = bl2wc b div 2" -apply(case_tac b, simp, case_tac a) -apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double) -done - -lemma [simp]: "b \ [] \ bl2wc ([hd b]) = bl2wc b mod 2" -apply(case_tac b, simp, case_tac a) -apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double) -done - -lemma [simp]: "\b \ []\ \ bl2wc (hd b # c) = 2 * bl2wc c + bl2wc b mod 2" -apply(case_tac b, simp, case_tac a) -apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double) -done - -lemma [simp]: " 2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2" - by(simp add: mult_div_cancel) - -lemma [simp]: "bl2wc (Oc # list) mod 2 = Suc 0" - by(simp add: bl2wc.simps bl2nat.simps bl2nat_double) - + "bl2wc (Bk # c) = 2*bl2wc (c)" + "2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 " + "bl2wc [Oc] = Suc 0" + "c \ [] \ bl2wc (tl c) = bl2wc c div 2" + "c \ [] \ bl2wc [hd c] = bl2wc c mod 2" + "c \ [] \ bl2wc (hd c # d) = 2 * bl2wc d + bl2wc c mod 2" + "2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2" + "bl2wc (Oc # list) mod 2 = Suc 0" + by(cases c;cases "hd c";force simp: bl2wc.simps bl2nat.simps bl2nat_double)+ declare code.simps[simp del] declare nth_of.simps[simp del] @@ -4136,21 +3975,15 @@ done qed -lemma [simp]: "bl2nat (Oc # Oc\x) 0 = (2 * 2 ^ x - Suc 0)" -apply(induct x) -apply(simp add: bl2nat.simps) -apply(simp add: bl2nat.simps bl2nat_double exp_ind) -done - -lemma [simp]: "bl2nat (Oc\y) 0 = 2^y - Suc 0" +lemma bl2nat_simps[simp]: "bl2nat (Oc # Oc\x) 0 = (2 * 2 ^ x - Suc 0)" + "bl2nat (Bk\x) n = 0" + by(induct x;force simp: bl2nat.simps bl2nat_double exp_ind)+ + +lemma bl2nat_exp_zero[simp]: "bl2nat (Oc\y) 0 = 2^y - Suc 0" apply(induct y, auto simp: bl2nat.simps bl2nat_double) apply(case_tac "(2::nat)^y", auto) done -lemma [simp]: "bl2nat (Bk\l) n = 0" -apply(induct l, auto simp: bl2nat.simps bl2nat_double exp_ind) -done - lemma bl2nat_cons_bk: "bl2nat (ks @ [Bk]) 0 = bl2nat ks 0" apply(induct ks, auto simp: bl2nat.simps) apply(case_tac a, auto simp: bl2nat.simps bl2nat_double) @@ -4200,9 +4033,8 @@ lemma tape_of_nat_list_butlast_last: "ys \ [] \ = @ Bk # Oc\Suc y" apply(induct ys, simp, simp) -apply(case_tac "ys = []", simp add: tape_of_nl_abv tape_of_nat_abv - tape_of_nat_list.simps) -apply(simp add: tape_of_nl_cons tape_of_nat_abv) +apply(case_tac "ys = []", simp add: tape_of_list_def tape_of_nat_def) +apply(simp add: tape_of_nl_cons tape_of_nat_def) done lemma listsum2_append: @@ -4244,8 +4076,8 @@ thus "length () = Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)" apply(case_tac "xs = []") - apply(simp add: tape_of_nl_abv listsum2.simps - tape_of_nat_list.simps tape_of_nat_abv) + apply(simp add: tape_of_list_def listsum2.simps + tape_of_nat_list.simps tape_of_nat_def) apply(simp add: tape_of_nat_list_butlast_last) using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"] apply(simp) @@ -4267,7 +4099,7 @@ apply(simp) done -lemma [simp]: +lemma trpl_code_simp[simp]: "trpl_code (steps0 (Suc 0, Bk\l, ) tp 0) = rec_exec rec_conf [code tp, bl2wc (), 0]" apply(simp add: steps.simps rec_exec.simps conf_lemma conf.simps @@ -4354,12 +4186,12 @@ qed qed -lemma [simp]: "bl2wc (Bk\ m) = 0" +lemma bl2wc_Bk_0[simp]: "bl2wc (Bk\ m) = 0" apply(induct m) apply(simp, simp) done -lemma [simp]: "bl2wc (Oc\ rs@Bk\ n) = bl2wc (Oc\ rs)" +lemma bl2wc_Oc_then_Bk[simp]: "bl2wc (Oc\ rs@Bk\ n) = bl2wc (Oc\ rs)" apply(induct rs, simp, simp add: bl2wc.simps bl2nat.simps bl2nat_double) done @@ -4438,10 +4270,10 @@ qed qed -lemma [simp]: "actn m 0 r = 4" +lemma actn_0_is_4[simp]: "actn m 0 r = 4" by(simp add: actn.simps) -lemma [simp]: "newstat m 0 r = 0" +lemma newstat_0_0[simp]: "newstat m 0 r = 0" by(simp add: newstat.simps) declare step_red[simp del] @@ -4536,7 +4368,7 @@ apply(auto) done -lemma [elim]: "x > Suc 0 \ Max {u. x ^ u dvd x ^ r} = r" +lemma max_divisors: "x > Suc 0 \ Max {u. x ^ u dvd x ^ r} = r" proof(rule_tac Max_eqI) assume "x > Suc 0" thus "finite {u. x ^ u dvd x ^ r}" @@ -4555,10 +4387,16 @@ show "r \ {u. x ^ u dvd x ^ r}" by simp qed -lemma lo_power: "x > Suc 0 \ lo (x ^ r) x = r" -apply(auto simp: lo.simps loR.simps mod_dvd_simp) -apply(case_tac "x^r", simp_all) -done +lemma lo_power: + assumes "x > Suc 0" shows "lo (x ^ r) x = r" +proof - + have "\ Suc 0 < x ^ r \ r = 0" using assms + by (metis Suc_lessD Suc_lessI nat_power_eq_Suc_0_iff zero_less_power) + moreover have "\xa. \ x ^ xa dvd x ^ r \ r = 0" + using dvd_refl assms by(cases "x^r";blast) + ultimately show ?thesis using assms + by(auto simp: lo.simps loR.simps mod_dvd_simp elim:max_divisors) +qed lemma lo_rgt: "lo (trpl 0 0 r) (Pi 2) = r" apply(simp add: trpl.simps lo_power) diff -r d5a0e25c4742 -r a9003e6d0463 thys/UTM.thy --- a/thys/UTM.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/UTM.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,10 +2,10 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Construction of a Universal Turing Machine *} +chapter {* Construction of a Universal Turing Machine *} theory UTM -imports Recursive Abacus UF GCD Turing_Hoare +imports Recursive Abacus UF HOL.GCD Turing_Hoare begin section {* Wang coding of input arguments *} @@ -684,23 +684,6 @@ declare wcode_backto_standard_pos.simps[simp del] -lemma [simp]: "<0::nat> = [Oc]" -apply(simp add: tape_of_nat_abv tape_of_nat_list.simps) -done - -lemma tape_of_Suc_nat: " = replicate a Oc @ [Oc, Oc]" -apply(simp only: tape_of_nat_abv exp_ind, simp) -done - -lemma [simp]: "length () = Suc a" -apply(simp add: tape_of_nat_abv tape_of_nat_list.simps) -done - -lemma [simp]: "<[a::nat]> = " -apply(simp add: tape_of_nat_abv tape_of_nl_abv - tape_of_nat_list.simps) -done - lemma bin_wc_eq: "bl_bin xs = bl2wc xs" proof(induct xs) show " bl_bin [] = bl2wc []" @@ -715,16 +698,6 @@ done qed -lemma bl_bin_nat_Suc: - "bl_bin () = bl_bin () + 2^(Suc a)" -apply(simp add: tape_of_nat_abv bl_bin.simps) -apply(induct a, auto simp: bl_bin.simps) -done - -lemma [simp]: " rev (a\(aa)) = a\(aa)" -apply(simp) -done - lemma tape_of_nl_append_one: "lm \ [] \ = @ Bk # Oc\Suc a" apply(induct lm, auto simp: tape_of_nl_cons split:if_splits) done @@ -735,12 +708,11 @@ apply(simp add: exp_ind[THEN sym]) done -lemma [simp]: "a\(Suc 0) = [a]" +lemma exp_1[simp]: "a\(Suc 0) = [a]" by(simp) lemma tape_of_nl_cons_app1: "() = (Oc\(Suc a) @ Bk # ())" -apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) -apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) +apply(case_tac xs; simp add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def) done lemma bl_bin_bk_oc[simp]: @@ -752,18 +724,17 @@ done lemma tape_of_nat[simp]: "() = Oc\(Suc a)" -apply(simp add: tape_of_nat_abv) +apply(simp add: tape_of_nat_def) done lemma tape_of_nl_cons_app2: "() = ( @ Bk # Oc\(Suc b))" -proof(induct "length xs" arbitrary: xs c, - simp add: tape_of_nl_abv tape_of_nat_list.simps) +proof(induct "length xs" arbitrary: xs c, simp add: tape_of_list_def) fix x xs c assume ind: "\xs c. x = length xs \ = @ Bk # Oc\(Suc b)" and h: "Suc x = length (xs::nat list)" show " = @ Bk # Oc\(Suc b)" - proof(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps) + proof(case_tac xs, simp add: tape_of_list_def tape_of_nat_list.simps) fix a list assume g: "xs = a # list" hence k: " = @ Bk # Oc\(Suc b)" @@ -772,16 +743,16 @@ apply(simp) done from g and k show " = @ Bk # Oc\(Suc b)" - apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) + apply(simp add: tape_of_list_def tape_of_nat_list.simps) done qed qed -lemma [simp]: "length () = Suc (Suc aa) + length ()" -apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) +lemma length_2_elems[simp]: "length () = Suc (Suc aa) + length ()" +apply(simp add: tape_of_list_def tape_of_nat_list.simps) done -lemma [simp]: "bl_bin (Oc\(Suc aa) @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) = +lemma bl_bin_addition[simp]: "bl_bin (Oc\(Suc aa) @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) = bl_bin (Oc\(Suc aa) @ Bk # tape_of_nat_list (a # lista)) + 2* 2^(length (Oc\(Suc aa) @ Bk # tape_of_nat_list (a # lista)))" using bl_bin_bk_oc[of "Oc\(Suc aa) @ Bk # tape_of_nat_list (a # lista)"] @@ -790,23 +761,22 @@ declare replicate_Suc[simp del] -lemma [simp]: +lemma bl_bin_2[simp]: "bl_bin () + (4 * rs + 4) * 2 ^ (length () - Suc 0) = bl_bin (Oc\(Suc aa) @ Bk # ) + rs * (2 * 2 ^ (aa + length ()))" - apply(case_tac "list", simp add: add_mult_distrib) apply(simp add: tape_of_nl_cons_app2 add_mult_distrib) -apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) +apply(simp add: tape_of_list_def tape_of_nat_list.simps) done lemma tape_of_nl_app_Suc: "(()) = () @ [Oc]" apply(induct list) -apply(simp add: tape_of_nl_abv tape_of_nat_list.simps exp_ind) +apply(simp add: tape_of_list_def tape_of_nat_list.simps exp_ind) apply(case_tac list) -apply(simp_all add:tape_of_nl_abv tape_of_nat_list.simps exp_ind) +apply(simp_all add:tape_of_list_def tape_of_nat_list.simps exp_ind) done -lemma [simp]: "bl_bin (Oc # Oc\(aa) @ Bk # @ [Oc]) +lemma bl_bin_3[simp]: "bl_bin (Oc # Oc\(aa) @ Bk # @ [Oc]) = bl_bin (Oc # Oc\(aa) @ Bk # ) + 2^(length (Oc # Oc\(aa) @ Bk # ))" apply(simp add: bin_wc_eq) @@ -814,7 +784,7 @@ using bl2nat_cons_oc[of "Oc # Oc\(aa) @ Bk # "] apply(simp) done -lemma [simp]: "bl_bin (Oc # Oc\(aa) @ Bk # ) + (4 * 2 ^ (aa + length ()) + +lemma bl_bin_4[simp]: "bl_bin (Oc # Oc\(aa) @ Bk # ) + (4 * 2 ^ (aa + length ()) + 4 * (rs * 2 ^ (aa + length ()))) = bl_bin (Oc # Oc\(aa) @ Bk # ) + rs * (2 * 2 ^ (aa + length ()))" @@ -863,82 +833,37 @@ definition wcode_double_case_le :: "(config \ config) set" where "wcode_double_case_le \ (inv_image lex_pair wcode_double_case_measure)" -lemma [intro]: "wf lex_pair" +lemma wf_lex_pair[intro]: "wf lex_pair" by(auto intro:wf_lex_prod simp:lex_pair_def) lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le" by(auto intro:wf_inv_image simp: wcode_double_case_le_def ) -lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)" -apply(simp add: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))" -apply(simp add: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)" -apply(simp add: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)" -apply(simp add: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)" -apply(simp add: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_main 4 Bk = (R, 4)" -apply(subgoal_tac "4 = Suc 3") -apply(simp only: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps, auto) -done - -lemma [simp]: "fetch t_wcode_main 4 Oc = (R, 5)" -apply(subgoal_tac "4 = Suc 3") -apply(simp only: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps, auto) -done - -lemma [simp]: "fetch t_wcode_main 5 Oc = (R, 5)" -apply(subgoal_tac "5 = Suc 4") -apply(simp only: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps, auto) -done - -lemma [simp]: "fetch t_wcode_main 5 Bk = (W1, 6)" -apply(subgoal_tac "5 = Suc 4") -apply(simp only: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps, auto) -done - -lemma [simp]: "fetch t_wcode_main 6 Bk = (R, 13)" -apply(subgoal_tac "6 = Suc 5") -apply(simp only: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps, auto) -done - -lemma [simp]: "fetch t_wcode_main 6 Oc = (L, 6)" -apply(subgoal_tac "6 = Suc 5") -apply(simp only: t_wcode_main_def t_wcode_main_first_part_def - fetch.simps nth_of.simps, auto) -done - -lemma [elim]: "Bk\(mr) = [] \ mr = 0" -apply(case_tac mr, auto) -done - -lemma [simp]: "wcode_on_left_moving_1 ires rs (b, []) = False" -apply(simp add: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps - wcode_on_left_moving_1_O.simps) -done - +lemma fetch_t_wcode_main[simp]: + "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)" + "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))" + "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)" + "fetch t_wcode_main (Suc (Suc 0)) Bk = (L, 7)" + "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)" + "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)" + "fetch t_wcode_main 4 Bk = (R, 4)" + "fetch t_wcode_main 4 Oc = (R, 5)" + "fetch t_wcode_main 5 Oc = (R, 5)" + "fetch t_wcode_main 5 Bk = (W1, 6)" + "fetch t_wcode_main 6 Bk = (R, 13)" + "fetch t_wcode_main 6 Oc = (L, 6)" + "fetch t_wcode_main 7 Oc = (R, 8)" + "fetch t_wcode_main 7 Bk = (R, 0)" + "fetch t_wcode_main 8 Bk = (R, 9)" + "fetch t_wcode_main 9 Bk = (R, 10)" + "fetch t_wcode_main 9 Oc = (W0, 9)" + "fetch t_wcode_main 10 Bk = (R, 10)" + "fetch t_wcode_main 10 Oc = (R, 11)" + "fetch t_wcode_main 11 Bk = (W1, 12)" + "fetch t_wcode_main 11 Oc = (R, 11)" + "fetch t_wcode_main 12 Oc = (L, 12)" + "fetch t_wcode_main 12 Bk = (R, t_twice_len + 14)" +by(auto simp: t_wcode_main_def t_wcode_main_first_part_def fetch.simps numeral) declare wcode_on_checking_1.simps[simp del] @@ -949,12 +874,13 @@ wcode_goon_right_moving_1.simps wcode_backto_standard_pos.simps -lemma [simp]: "wcode_on_left_moving_1 ires rs (b, r) \ b \ []" -apply(simp add: wcode_double_case_inv_simps, auto) -done - - -lemma [elim]: "\wcode_on_left_moving_1 ires rs (b, Bk # list); +lemma wcode_on_left_moving_1[simp]: + "wcode_on_left_moving_1 ires rs (b, []) = False" + "wcode_on_left_moving_1 ires rs (b, r) \ b \ []" +by(auto simp: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps + wcode_on_left_moving_1_O.simps) + +lemma wcode_on_left_moving_1E[elim]: "\wcode_on_left_moving_1 ires rs (b, Bk # list); tl b = aa \ hd b # Bk # list = ba\ \ wcode_on_left_moving_1 ires rs (aa, ba)" apply(simp only: wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps @@ -973,7 +899,7 @@ declare replicate_Suc[simp] -lemma [elim]: +lemma wcode_on_moving_1_Elim[elim]: "\wcode_on_left_moving_1 ires rs (b, Oc # list); tl b = aa \ hd b # Oc # list = ba\ \ wcode_on_checking_1 ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) @@ -982,43 +908,28 @@ apply(case_tac mr, simp, auto) done -lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False" -apply(auto simp: wcode_double_case_inv_simps) -done - -lemma [simp]: "wcode_on_checking_1 ires rs (b, Bk # list) = False" -apply(auto simp: wcode_double_case_inv_simps) -done - -lemma [elim]: "\wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \ list = ba\ +lemma wcode_on_checking_1_Elim[elim]: "\wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \ list = ba\ \ wcode_erase1 ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) apply(erule_tac exE)+ apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp) done - -lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False" -apply(simp add: wcode_double_case_inv_simps) -done - -lemma [simp]: "wcode_on_checking_1 ires rs ([], Bk # list) = False" +lemma wcode_on_checking_1_simp[simp]: + "wcode_on_checking_1 ires rs (b, []) = False" + "wcode_on_checking_1 ires rs (b, Bk # list) = False" +by(auto simp: wcode_double_case_inv_simps) + +lemma wcode_erase1_nonempty_snd[simp]: "wcode_erase1 ires rs (b, []) = False" apply(simp add: wcode_double_case_inv_simps) done -lemma [simp]: "wcode_erase1 ires rs (b, []) = False" -apply(simp add: wcode_double_case_inv_simps) -done - -lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False" +lemma wcode_on_right_moving_1_nonempty_snd[simp]: "wcode_on_right_moving_1 ires rs (b, []) = False" apply(simp add: wcode_double_case_inv_simps) done -lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False" -apply(simp add: wcode_double_case_inv_simps) -done - -lemma [elim]: "\wcode_on_right_moving_1 ires rs (b, Bk # ba); Bk # b = aa \ list = b\ \ +lemma wcode_on_right_moving_1_BkE[elim]: + "\wcode_on_right_moving_1 ires rs (b, Bk # ba); Bk # b = aa \ list = b\ \ wcode_on_right_moving_1 ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) apply(erule_tac exE)+ @@ -1028,7 +939,7 @@ apply(case_tac mr, simp, simp) done -lemma [elim]: +lemma wcode_on_right_moving_1_OcE[elim]: "\wcode_on_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \ list = ba\ \ wcode_goon_right_moving_1 ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) @@ -1039,12 +950,7 @@ apply(case_tac ml, simp, case_tac nat, simp, simp) done -lemma [simp]: - "wcode_on_right_moving_1 ires rs (b, []) \ False" -apply(simp add: wcode_double_case_inv_simps) -done - -lemma [elim]: "\wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \ list = ba; c = Bk # ba\ +lemma wcode_erase1_BkE[elim]: "\wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \ list = ba; c = Bk # ba\ \ wcode_on_right_moving_1 ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) apply(erule_tac exE)+ @@ -1052,14 +958,14 @@ rule_tac x = rn in exI, simp add: exp_ind del: replicate_Suc) done -lemma [elim]: "\wcode_erase1 ires rs (aa, Oc # list); b = aa \ Bk # list = ba\ \ +lemma wcode_erase1_OcE[elim]: "\wcode_erase1 ires rs (aa, Oc # list); b = aa \ Bk # list = ba\ \ wcode_erase1 ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) apply(erule_tac exE)+ apply(rule_tac x = ln in exI, rule_tac x = rn in exI, auto) done -lemma [elim]: "\wcode_goon_right_moving_1 ires rs (aa, []); b = aa \ [Oc] = ba\ +lemma wcode_goon_right_moving_1_emptyE[elim]: "\wcode_goon_right_moving_1 ires rs (aa, []); b = aa \ [Oc] = ba\ \ wcode_backto_standard_pos ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) apply(erule_tac exE)+ @@ -1069,7 +975,7 @@ rule_tac x = rn in exI, simp) done -lemma [elim]: +lemma wcode_goon_right_moving_1_BkE[elim]: "\wcode_goon_right_moving_1 ires rs (aa, Bk # list); b = aa \ Oc # list = ba\ \ wcode_backto_standard_pos ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) @@ -1081,7 +987,7 @@ apply(case_tac mr, simp, case_tac rn, simp, simp_all) done -lemma [elim]: "\wcode_goon_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \ list = ba\ +lemma wcode_goon_right_moving_1_OcE[elim]: "\wcode_goon_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \ list = ba\ \ wcode_goon_right_moving_1 ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps) apply(erule_tac exE)+ @@ -1091,12 +997,8 @@ apply(case_tac mr, simp, case_tac rn, simp_all) done -lemma [elim]: "\wcode_backto_standard_pos ires rs (b, []); Bk # b = aa\ \ False" -apply(auto simp: wcode_double_case_inv_simps wcode_backto_standard_pos_O.simps - wcode_backto_standard_pos_B.simps) -done - -lemma [elim]: "\wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \ list = ba\ + +lemma wcode_backto_standard_pos_BkE[elim]: "\wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \ list = ba\ \ wcode_before_double ires rs (aa, ba)" apply(simp only: wcode_double_case_inv_simps wcode_backto_standard_pos_B.simps wcode_backto_standard_pos_O.simps wcode_before_double.simps) @@ -1107,17 +1009,17 @@ apply(case_tac [!] mr, simp_all) done -lemma [simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False" +lemma wcode_backto_standard_pos_no_Oc[simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False" apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps wcode_backto_standard_pos_O.simps) done -lemma [simp]: "wcode_backto_standard_pos ires rs (b, []) = False" +lemma wcode_backto_standard_pos_nonempty_snd[simp]: "wcode_backto_standard_pos ires rs (b, []) = False" apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps wcode_backto_standard_pos_O.simps) done -lemma [elim]: "\wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list = ba\ +lemma wcode_backto_standard_pos_OcE[elim]: "\wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list = ba\ \ wcode_backto_standard_pos ires rs (aa, ba)" apply(simp only: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps wcode_backto_standard_pos_O.simps) @@ -1210,10 +1112,6 @@ by simp qed -lemma t_twice_len_ge: "Suc 0 \ length t_twice div 2" -apply(simp add: t_twice_def mopup.simps t_twice_compile_def) -done - declare start_of.simps[simp del] lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs" @@ -1242,7 +1140,7 @@ by(simp add: abc_twice_def) qed thus "?thesis" - apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma) + apply(simp add: tape_of_list_def tape_of_nat_def rec_exec.simps twice_lemma) done qed @@ -1368,7 +1266,7 @@ declare tm_wf.simps[simp del] -lemma [simp]: " tm_wf (t_twice_compile, 0)" +lemma tm_wf_t_twice_compile [simp]: "tm_wf (t_twice_compile, 0)" apply(simp only: t_twice_compile_def) apply(rule_tac wf_tm_from_abacus, simp) done @@ -1399,7 +1297,7 @@ by metis qed -lemma [intro]: "length t_wcode_main_first_part mod 2 = 0" +lemma length_t_wcode_main_first_part_even[intro]: "length t_wcode_main_first_part mod 2 = 0" apply(auto simp: t_wcode_main_first_part_def) done @@ -1428,10 +1326,9 @@ done lemma mopup_mod2: "length (mopup k) mod 2 = 0" -apply(auto simp: mopup.simps) -by arith - -lemma [simp]: "fetch t_wcode_main (Suc (t_twice_len + length t_wcode_main_first_part div 2)) Oc + by(auto simp: mopup.simps) + +lemma fetch_t_wcode_main_Oc[simp]: "fetch t_wcode_main (Suc (t_twice_len + length t_wcode_main_first_part div 2)) Oc = (L, Suc 0)" apply(subgoal_tac "length (t_twice) mod 2 = 0") apply(simp add: t_wcode_main_def nth_append fetch.simps t_wcode_main_first_part_def @@ -1452,7 +1349,7 @@ apply(simp add: exp_ind[THEN sym]) done -lemma wcode_main_first_part_len: +lemma wcode_main_first_part_len[simp]: "length t_wcode_main_first_part = 24" apply(simp add: t_wcode_main_first_part_def) done @@ -1659,117 +1556,21 @@ where "wcode_fourtimes_case_le \ (inv_image lex_pair wcode_fourtimes_case_measure)" lemma wf_wcode_fourtimes_case_le[intro]: "wf wcode_fourtimes_case_le" -by(auto intro:wf_inv_image simp: wcode_fourtimes_case_le_def) - -lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Bk = (L, 7)" -apply(simp add: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_main 7 Oc = (R, 8)" -apply(subgoal_tac "7 = Suc 6") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 8 Bk = (R, 9)" -apply(subgoal_tac "8 = Suc 7") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - - -lemma [simp]: "fetch t_wcode_main 9 Bk = (R, 10)" -apply(subgoal_tac "9 = Suc 8") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 9 Oc = (W0, 9)" -apply(subgoal_tac "9 = Suc 8") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 10 Bk = (R, 10)" -apply(subgoal_tac "10 = Suc 9") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 10 Oc = (R, 11)" -apply(subgoal_tac "10 = Suc 9") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 11 Bk = (W1, 12)" -apply(subgoal_tac "11 = Suc 10") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 11 Oc = (R, 11)" -apply(subgoal_tac "11 = Suc 10") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 12 Oc = (L, 12)" -apply(subgoal_tac "12 = Suc 11") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_main 12 Bk = (R, t_twice_len + 14)" -apply(subgoal_tac "12 = Suc 11") -apply(simp only: t_wcode_main_def fetch.simps - t_wcode_main_first_part_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "wcode_on_left_moving_2 ires rs (b, []) = False" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_on_checking_2 ires rs (b, []) = False" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_goon_checking ires rs (b, []) = False" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_right_move ires rs (b, []) = False" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_erase2 ires rs (b, []) = False" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_on_right_moving_2 ires rs (b, []) = False" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, []) = False" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Bk # list) \ b \ []" -apply(simp add: wcode_fourtimes_invs, auto) -done - -lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Bk # list) \ wcode_on_left_moving_2 ires rs (tl b, hd b # Bk # list)" +by(auto simp: wcode_fourtimes_case_le_def) + +lemma nonempty_snd [simp]: + "wcode_on_left_moving_2 ires rs (b, []) = False" + "wcode_on_checking_2 ires rs (b, []) = False" + "wcode_goon_checking ires rs (b, []) = False" + "wcode_right_move ires rs (b, []) = False" + "wcode_erase2 ires rs (b, []) = False" + "wcode_on_right_moving_2 ires rs (b, []) = False" + "wcode_backto_standard_pos_2 ires rs (b, []) = False" + "wcode_on_checking_2 ires rs (b, Oc # list) = False" + by(auto simp: wcode_fourtimes_invs) + +lemma wcode_on_left_moving_2[simp]: + "wcode_on_left_moving_2 ires rs (b, Bk # list) \ wcode_on_left_moving_2 ires rs (tl b, hd b # Bk # list)" apply(simp only: wcode_fourtimes_invs) apply(erule_tac disjE) apply(erule_tac exE)+ @@ -1782,55 +1583,32 @@ apply(simp) done -lemma [simp]: "wcode_on_checking_2 ires rs (b, Bk # list) \ b \ []" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_on_checking_2 ires rs (b, Bk # list) +lemma wcode_goon_checking_via_2 [simp]: "wcode_on_checking_2 ires rs (b, Bk # list) \ wcode_goon_checking ires rs (tl b, hd b # Bk # list)" apply(simp only: wcode_fourtimes_invs) apply(auto) -done - -lemma [simp]: "wcode_goon_checking ires rs (b, Bk # list) = False" -apply(simp add: wcode_fourtimes_invs) -done - -lemma [simp]: " wcode_right_move ires rs (b, Bk # list) \ b\ []" -apply(simp add: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_right_move ires rs (b, Bk # list) \ wcode_erase2 ires rs (Bk # b, list)" + done + +lemma wcode_erase2_via_move [simp]: "wcode_right_move ires rs (b, Bk # list) \ wcode_erase2 ires rs (Bk # b, list)" apply(auto simp:wcode_fourtimes_invs ) apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp) -done - -lemma [simp]: "wcode_erase2 ires rs (b, Bk # list) \ b \ []" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_erase2 ires rs (b, Bk # list) \ wcode_on_right_moving_2 ires rs (Bk # b, list)" + done +lemma wcode_on_right_moving_2_via_erase2[simp]: + "wcode_erase2 ires rs (b, Bk # list) \ wcode_on_right_moving_2 ires rs (Bk # b, list)" apply(auto simp:wcode_fourtimes_invs ) apply(rule_tac x = "Suc (Suc 0)" in exI, simp add: exp_ind) apply(rule_tac x = "Suc (Suc ln)" in exI, simp add: exp_ind del: replicate_Suc) done -lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list) \ b \ []" -apply(auto simp:wcode_fourtimes_invs ) -done - -lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list) +lemma wcode_on_right_moving_2_move_Bk[simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list) \ wcode_on_right_moving_2 ires rs (Bk # b, list)" apply(auto simp: wcode_fourtimes_invs) apply(rule_tac x = "Suc ml" in exI, simp) apply(rule_tac x = "mr - 1" in exI, case_tac mr,auto) -done - -lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Bk # list) \ b \ []" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Bk # list) \ + done + +lemma wcode_backto_standard_pos_2_via_right[simp]: + "wcode_goon_right_moving_2 ires rs (b, Bk # list) \ wcode_backto_standard_pos_2 ires rs (b, Oc # list)" apply(simp add: wcode_fourtimes_invs, auto) apply(rule_tac x = ml in exI, auto) @@ -1838,27 +1616,16 @@ apply(case_tac mr, simp_all) apply(rule_tac x = "rn - 1" in exI, simp) apply(case_tac rn, simp, simp) -done - -lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list) \ b \ []" -apply(simp add: wcode_fourtimes_invs, auto) -done - -lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \ b \ []" -apply(simp add: wcode_fourtimes_invs, auto) -done - -lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \ + done + +lemma wcode_on_checking_2_via_left[simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \ wcode_on_checking_2 ires rs (tl b, hd b # Oc # list)" apply(auto simp: wcode_fourtimes_invs) apply(case_tac [!] mr, simp_all) -done - -lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, []) \ b \ []" -apply(auto simp: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, []) \ + done + +lemma wcode_backto_standard_pos_2_empty_via_right[simp]: + "wcode_goon_right_moving_2 ires rs (b, []) \ wcode_backto_standard_pos_2 ires rs (b, [Oc])" apply(simp only: wcode_fourtimes_invs) apply(erule_tac exE)+ @@ -1867,18 +1634,7 @@ rule_tac x = ln in exI, rule_tac x = rn in exI, simp) done -lemma "wcode_backto_standard_pos_2 ires rs (b, Bk # list) - \ (\ln. b = Bk # Bk\(ln) @ Oc # ires) \ (\rn. list = Oc\(Suc (Suc rs)) @ Bk\(rn))" -apply(auto simp: wcode_fourtimes_invs) -apply(case_tac [!] mr, auto) -done - - -lemma [simp]: "wcode_on_checking_2 ires rs (b, Oc # list) \ False" -apply(simp add: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_goon_checking ires rs (b, Oc # list) \ +lemma wcode_goon_checking_cases[simp]: "wcode_goon_checking ires rs (b, Oc # list) \ (b = [] \ wcode_right_move ires rs ([Oc], list)) \ (b \ [] \ wcode_right_move ires rs (Oc # b, list))" apply(simp only: wcode_fourtimes_invs) @@ -1886,25 +1642,17 @@ apply(auto) done -lemma [simp]: "wcode_right_move ires rs (b, Oc # list) = False" +lemma wcode_right_move_no_Oc[simp]: "wcode_right_move ires rs (b, Oc # list) = False" apply(auto simp: wcode_fourtimes_invs) done -lemma [simp]: " wcode_erase2 ires rs (b, Oc # list) \ b \ []" -apply(simp add: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_erase2 ires rs (b, Oc # list) +lemma wcode_erase2_Bk_via_Oc[simp]: "wcode_erase2 ires rs (b, Oc # list) \ wcode_erase2 ires rs (b, Bk # list)" apply(auto simp: wcode_fourtimes_invs) done -lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Oc # list) \ b \ []" -apply(simp only: wcode_fourtimes_invs) -apply(auto) -done - -lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Oc # list) +lemma wcode_goon_right_moving_2_Oc_move[simp]: + "wcode_on_right_moving_2 ires rs (b, Oc # list) \ wcode_goon_right_moving_2 ires rs (Oc # b, list)" apply(auto simp: wcode_fourtimes_invs) apply(case_tac mr, simp_all) @@ -1913,33 +1661,23 @@ apply(case_tac ml, simp, case_tac nat, simp_all) done -lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \ b \ []" -apply(simp only:wcode_fourtimes_invs, auto) -done - -lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list) +lemma wcode_backto_standard_pos_2_exists[simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list) \ (\ln. b = Bk # Bk\(ln) @ Oc # ires) \ (\rn. list = Oc\(Suc (Suc rs)) @ Bk\(rn))" apply(simp add: wcode_fourtimes_invs, auto) apply(case_tac [!] mr, simp_all) done -lemma [simp]: "wcode_on_checking_2 ires rs (b, Oc # list) = False" -apply(simp add: wcode_fourtimes_invs) -done - -lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \ +lemma wcode_goon_right_moving_2_move_Oc[simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \ wcode_goon_right_moving_2 ires rs (Oc # b, list)" apply(simp only:wcode_fourtimes_invs, auto) apply(rule_tac x = "Suc ml" in exI, simp) apply(rule_tac x = "mr - 1" in exI) apply(case_tac mr, case_tac rn, auto) -done - -lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Oc # list) \ b \ []" -apply(simp only: wcode_fourtimes_invs, auto) -done - -lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Oc # list) + done + + +lemma wcode_backto_standard_pos_2_Oc_mv_hd[simp]: + "wcode_backto_standard_pos_2 ires rs (b, Oc # list) \ wcode_backto_standard_pos_2 ires rs (tl b, hd b # Oc # list)" apply(simp only: wcode_fourtimes_invs) apply(erule_tac disjE) @@ -1949,6 +1687,24 @@ apply(rule_tac x = "Suc mr" in exI, simp) done +lemma nonempty_fst[simp]: + "wcode_on_left_moving_2 ires rs (b, Bk # list) \ b \ []" + "wcode_on_checking_2 ires rs (b, Bk # list) \ b \ []" + "wcode_goon_checking ires rs (b, Bk # list) = False" + "wcode_right_move ires rs (b, Bk # list) \ b\ []" + "wcode_erase2 ires rs (b, Bk # list) \ b \ []" + "wcode_on_right_moving_2 ires rs (b, Bk # list) \ b \ []" + "wcode_goon_right_moving_2 ires rs (b, Bk # list) \ b \ []" + "wcode_backto_standard_pos_2 ires rs (b, Bk # list) \ b \ []" + "wcode_on_left_moving_2 ires rs (b, Oc # list) \ b \ []" + "wcode_goon_right_moving_2 ires rs (b, []) \ b \ []" + "wcode_erase2 ires rs (b, Oc # list) \ b \ []" + "wcode_on_right_moving_2 ires rs (b, Oc # list) \ b \ []" + "wcode_goon_right_moving_2 ires rs (b, Oc # list) \ b \ []" + "wcode_backto_standard_pos_2 ires rs (b, Oc # list) \ b \ []" + by(auto simp: wcode_fourtimes_invs) + + lemma wcode_fourtimes_case_first_correctness: shows "let P = (\ (st, l, r). st = t_twice_len + 14) in let Q = (\ (st, l, r). wcode_fourtimes_case_inv st ires rs (l, r)) in @@ -1997,18 +1753,13 @@ where "t_fourtimes_len = (length t_fourtimes div 2)" -lemma t_fourtimes_len_gr: "t_fourtimes_len > 0" -apply(simp add: t_fourtimes_len_def t_fourtimes_def mopup.simps t_fourtimes_compile_def) -done - -lemma [intro]: "primerec rec_fourtimes (Suc 0)" +lemma primerec_rec_fourtimes_1[intro]: "primerec rec_fourtimes (Suc 0)" apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps) by auto lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs" by(simp add: rec_exec.simps rec_fourtimes_def) - lemma t_fourtimes_correct: "\stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\(Suc rs) @ Bk\(n)) (tm_of abc_fourtimes @ shift (mopup 1) (length (tm_of abc_fourtimes) div 2)) stp = @@ -2031,7 +1782,7 @@ by(simp add: abc_fourtimes_def) qed thus "?thesis" - apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv fourtimes_lemma) + apply(simp add: tape_of_list_def tape_of_nat_def fourtimes_lemma) done qed @@ -2067,9 +1818,8 @@ by metis qed -lemma [intro]: "length t_twice mod 2 = 0" -apply(auto simp: t_twice_def t_twice_compile_def) -by (metis mopup_mod2) +lemma length_t_twice_even[intro]: "is_even (length t_twice)" + by(auto simp: t_twice_def t_twice_compile_def intro!:mopup_mod2) lemma t_fourtimes_append_pre: "steps0 (Suc 0, Bk # Bk # ires, Oc\(Suc rs) @ Bk\(n)) t_fourtimes stp @@ -2084,25 +1834,12 @@ = ((Suc t_fourtimes_len) + length (t_wcode_main_first_part @ shift t_twice (length t_wcode_main_first_part div 2) @ [(L, 1), (L, 1)]) div 2, Bk\(ln) @ Bk # Bk # ires, Oc\(Suc (4 * rs)) @ Bk\(rn))" -apply(rule_tac tm_append_shift_append_steps, simp_all) -apply(auto simp: t_wcode_main_first_part_def) -done - - -lemma [simp]: "length t_wcode_main_first_part = 24" -apply(simp add: t_wcode_main_first_part_def) -done - -lemma [simp]: "(26 + length t_twice) div 2 = (length t_twice) div 2 + 13" -apply(simp add: t_twice_def t_twice_def) -done - -lemma [simp]: "((26 + length (shift t_twice 12)) div 2) - = (length (shift t_twice 12) div 2 + 13)" -apply(simp add: t_twice_def) -done - -lemma [simp]: "t_twice_len + 14 = 14 + length (shift t_twice 12) div 2" + using length_t_twice_even + by(intro tm_append_shift_append_steps, auto) + +lemma split_26_even[simp]: "(26 + l::nat) div 2 = l div 2 + 13" by(simp) + +lemma t_twice_len_plust_14[simp]: "t_twice_len + 14 = 14 + length (shift t_twice 12) div 2" apply(simp add: t_twice_def t_twice_len_def) done @@ -2125,43 +1862,34 @@ apply(simp add: t_twice_len_def) done -lemma t_wcode_main_len: "length t_wcode_main = length t_twice + length t_fourtimes + 28" -apply(simp add: t_wcode_main_def) -done - -lemma even_twice_len: "length t_twice mod 2 = 0" -apply(auto simp: t_twice_def t_twice_compile_def) -by (metis mopup_mod2) - lemma even_fourtimes_len: "length t_fourtimes mod 2 = 0" apply(auto simp: t_fourtimes_def t_fourtimes_compile_def) by (metis mopup_mod2) -lemma [simp]: "2 * (length t_twice div 2) = length t_twice" -using even_twice_len -by arith - -lemma [simp]: "2 * (length t_fourtimes div 2) = length t_fourtimes" +lemma t_twice_even[simp]: "2 * (length t_twice div 2) = length t_twice" +using length_t_twice_even by arith + +lemma t_fourtimes_even[simp]: "2 * (length t_fourtimes div 2) = length t_fourtimes" using even_fourtimes_len by arith -lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Oc +lemma fetch_t_wcode_14_Oc: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Oc = (L, Suc 0)" apply(subgoal_tac "14 = Suc 13") apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def) -apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append) +apply(simp add:length_t_twice_even t_fourtimes_len_def nth_append) by arith -lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk +lemma fetch_t_wcode_14_Bk: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk = (L, Suc 0)" apply(subgoal_tac "14 = Suc 13") apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def) -apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append) +apply(simp add:length_t_twice_even t_fourtimes_len_def nth_append) by arith -lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) b +lemma fetch_t_wcode_14 [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) b = (L, Suc 0)" -apply(case_tac b, simp_all) +apply(case_tac b, simp_all add:fetch_t_wcode_14_Bk fetch_t_wcode_14_Oc) done lemma wcode_jump2: @@ -2224,7 +1952,7 @@ from stp1 stp2 stp3 show "?thesis" apply(rule_tac x = "stpa + stpb + stpc" in exI, rule_tac x = lnc in exI, rule_tac x = rnc in exI) - apply(simp add: steps_add) + apply(simp) done qed @@ -2309,27 +2037,8 @@ wcode_on_checking_3.simps wcode_goon_checking_3.simps wcode_on_left_moving_3.simps wcode_stop.simps -lemma [simp]: "fetch t_wcode_main 7 Bk = (R, 0)" -apply(subgoal_tac "7 = Suc 6") -apply(simp only: fetch.simps t_wcode_main_def nth_append nth_of.simps - t_wcode_main_first_part_def) -apply(auto) -done - -lemma [simp]: "wcode_on_left_moving_3 ires rs (b, []) = False" -apply(simp only: wcode_halt_invs) -apply(simp) -done - -lemma [simp]: "wcode_on_checking_3 ires rs (b, []) = False" -apply(simp add: wcode_halt_invs) -done - -lemma [simp]: "wcode_goon_checking_3 ires rs (b, []) = False" -apply(simp add: wcode_halt_invs) -done - -lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list) + +lemma wcode_on_left_moving_3_mv_Bk[simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list) \ wcode_on_left_moving_3 ires rs (tl b, hd b # Bk # list)" apply(simp only: wcode_halt_invs) apply(erule_tac disjE) @@ -2344,43 +2053,34 @@ apply(simp) done -lemma [simp]: "wcode_goon_checking_3 ires rs (b, Bk # list) \ +lemma wcode_goon_checking_3_cases[simp]: "wcode_goon_checking_3 ires rs (b, Bk # list) \ (b = [] \ wcode_stop ires rs ([Bk], list)) \ (b \ [] \ wcode_stop ires rs (Bk # b, list))" apply(auto simp: wcode_halt_invs) done -lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \ b \ []" -apply(auto simp: wcode_halt_invs) -done - -lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \ +lemma wcode_on_checking_3_mv_Oc[simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \ wcode_on_checking_3 ires rs (tl b, hd b # Oc # list)" apply(simp add:wcode_halt_invs, auto) apply(case_tac [!] mr, simp_all) done -lemma [simp]: "wcode_on_checking_3 ires rs (b, Oc # list) = False" -apply(auto simp: wcode_halt_invs) -done - -lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list) \ b \ []" -apply(simp add: wcode_halt_invs, auto) -done - -lemma [simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \ b \ []" -apply(auto simp: wcode_halt_invs) -done - -lemma [simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \ +lemma wcode_3_nonempty[simp]: + "wcode_on_left_moving_3 ires rs (b, []) = False" + "wcode_on_checking_3 ires rs (b, []) = False" + "wcode_goon_checking_3 ires rs (b, []) = False" + "wcode_on_left_moving_3 ires rs (b, Oc # list) \ b \ []" + "wcode_on_checking_3 ires rs (b, Oc # list) = False" + "wcode_on_left_moving_3 ires rs (b, Bk # list) \ b \ []" + "wcode_on_checking_3 ires rs (b, Bk # list) \ b \ []" + "wcode_goon_checking_3 ires rs (b, Oc # list) = False" + by(auto simp: wcode_halt_invs) + +lemma wcode_goon_checking_3_mv_Bk[simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \ wcode_goon_checking_3 ires rs (tl b, hd b # Bk # list)" apply(auto simp: wcode_halt_invs) done -lemma [simp]: "wcode_goon_checking_3 ires rs (b, Oc # list) = False" -apply(simp add: wcode_goon_checking_3.simps) -done - lemma t_halt_case_correctness: shows "let P = (\ (st, l, r). st = 0) in let Q = (\ (st, l, r). wcode_halt_case_inv st ires rs (l, r)) in @@ -2418,7 +2118,7 @@ qed declare wcode_halt_case_inv.simps[simp del] -lemma [intro]: "\ xs. ( :: cell list) = Oc # xs" +lemma leading_Oc[intro]: "\ xs. ( :: cell list) = Oc # xs" apply(case_tac "rev list", simp) apply(simp add: tape_of_nl_cons) done @@ -2436,15 +2136,11 @@ rule_tac x = rn in exI, simp) done -lemma bl_bin_one: "bl_bin [Oc] = Suc 0" +lemma bl_bin_one[simp]: "bl_bin [Oc] = 1" apply(simp add: bl_bin.simps) done -lemma [simp]: "bl_bin [Oc] = 1" -apply(simp add: bl_bin.simps) -done - -lemma [intro]: "2 * 2 ^ a = Suc (Suc (2 * bl_bin (Oc \ a)))" +lemma twice_power[intro]: "2 * 2 ^ a = Suc (Suc (2 * bl_bin (Oc \ a)))" apply(induct a, auto simp: bl_bin.simps) done declare replicate_Suc[simp del] @@ -2508,14 +2204,14 @@ "\stp ln rn. steps0 (Suc 0, Bk # Bk\(lna) @ rev () @ Bk # Bk # ires, Bk # Oc\(Suc (2 * rs + 2)) @ Bk\(rna)) t_wcode_main stp = (0, Bk # ires, Bk # Oc # Bk\(ln) @ Bk # Bk # Oc\(bl_bin () + (2*rs + 2) * 2 ^ a) @ Bk\(rn))" - using ind2[of lna ires "2*rs + 2" rna] by(simp add: tape_of_nl_abv tape_of_nat_abv) + using ind2[of lna ires "2*rs + 2" rna] by(simp add: tape_of_list_def tape_of_nat_def) from this obtain stpb lnb rnb where stp2: "steps0 (Suc 0, Bk # Bk\(lna) @ rev () @ Bk # Bk # ires, Bk # Oc\(Suc (2 * rs + 2)) @ Bk\(rna)) t_wcode_main stpb = (0, Bk # ires, Bk # Oc # Bk\(lnb) @ Bk # Bk # Oc\(bl_bin () + (2*rs + 2) * 2 ^ a) @ Bk\(rnb))" by blast from stp1 and stp2 show "?thesis" apply(rule_tac x = "stpa + stpb" in exI, - rule_tac x = lnb in exI, rule_tac x = rnb in exI, simp add: tape_of_nat_abv) + rule_tac x = lnb in exI, rule_tac x = rnb in exI, simp add: tape_of_nat_def) apply(simp add: bl_bin.simps replicate_Suc) apply(auto) done @@ -2781,9 +2477,6 @@ definition wcode_prepare_le :: "(config \ config) set" where "wcode_prepare_le \ (inv_image lex_triple wcode_prepare_measure)" -lemma [intro]: "wf lex_pair" -by(auto intro:wf_lex_prod simp:lex_pair_def) - lemma wf_wcode_prepare_le[intro]: "wf wcode_prepare_le" by(auto intro:wf_inv_image simp: wcode_prepare_le_def lex_triple_def) @@ -2799,103 +2492,48 @@ wprepare_add_one2.simps declare wprepare_inv.simps[simp del] -lemma [simp]: "fetch t_wcode_prepare (Suc 0) Bk = (W1, 2)" -apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_prepare (Suc 0) Oc = (L, 1)" -apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_prepare (Suc (Suc 0)) Bk = (L, 3)" -apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_prepare (Suc (Suc 0)) Oc = (R, 2)" -apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Bk = (R, 4)" -apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Oc = (W0, 3)" -apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_prepare 4 Bk = (R, 4)" -apply(subgoal_tac "4 = Suc 3") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_prepare 4 Oc = (R, 5)" -apply(subgoal_tac "4 = Suc 3") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - - -lemma [simp]: "fetch t_wcode_prepare 5 Oc = (R, 5)" -apply(subgoal_tac "5 = Suc 4") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_prepare 5 Bk = (R, 6)" -apply(subgoal_tac "5 = Suc 4") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_prepare 6 Oc = (R, 5)" -apply(subgoal_tac "6 = Suc 5") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_prepare 6 Bk = (R, 7)" -apply(subgoal_tac "6 = Suc 5") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_prepare 7 Oc = (L, 0)" -apply(subgoal_tac "7 = Suc 6") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "fetch t_wcode_prepare 7 Bk = (W1, 7)" -apply(subgoal_tac "7 = Suc 6") -apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps) -apply(auto) -done - -lemma [simp]: "lm \ [] \ wprepare_add_one m lm (b, []) = False" + +lemma fetch_t_wcode_prepare[simp]: + "fetch t_wcode_prepare (Suc 0) Bk = (W1, 2)" + "fetch t_wcode_prepare (Suc 0) Oc = (L, 1)" + "fetch t_wcode_prepare (Suc (Suc 0)) Bk = (L, 3)" + "fetch t_wcode_prepare (Suc (Suc 0)) Oc = (R, 2)" + "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Bk = (R, 4)" + "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Oc = (W0, 3)" + "fetch t_wcode_prepare 4 Bk = (R, 4)" + "fetch t_wcode_prepare 4 Oc = (R, 5)" + "fetch t_wcode_prepare 5 Oc = (R, 5)" + "fetch t_wcode_prepare 5 Bk = (R, 6)" + "fetch t_wcode_prepare 6 Oc = (R, 5)" + "fetch t_wcode_prepare 6 Bk = (R, 7)" + "fetch t_wcode_prepare 7 Oc = (L, 0)" + "fetch t_wcode_prepare 7 Bk = (W1, 7)" + unfolding fetch.simps t_wcode_prepare_def nth_of.simps + numeral by auto + +lemma wprepare_add_one_nonempty_snd[simp]: "lm \ [] \ wprepare_add_one m lm (b, []) = False" apply(simp add: wprepare_invs) done -lemma [simp]: "lm \ [] \ wprepare_goto_first_end m lm (b, []) = False" +lemma wprepare_goto_first_end_nonempty_snd[simp]: "lm \ [] \ wprepare_goto_first_end m lm (b, []) = False" apply(simp add: wprepare_invs) done -lemma [simp]: "lm \ [] \ wprepare_erase m lm (b, []) = False" +lemma wprepare_erase_nonempty_snd[simp]: "lm \ [] \ wprepare_erase m lm (b, []) = False" apply(simp add: wprepare_invs) done -lemma [simp]: "lm \ [] \ wprepare_goto_start_pos m lm (b, []) = False" +lemma wprepare_goto_start_pos_nonempty_snd[simp]: "lm \ [] \ wprepare_goto_start_pos m lm (b, []) = False" apply(simp add: wprepare_invs) done -lemma [simp]: "\lm \ []; wprepare_loop_start m lm (b, [])\ \ b \ []" +lemma wprepare_loop_start_empty_nonempty_fst[simp]: "\lm \ []; wprepare_loop_start m lm (b, [])\ \ b \ []" apply(simp add: wprepare_invs) done -lemma rev_eq: "rev xs = rev ys \ xs = ys" -by auto - -lemma [simp]: "\lm \ []; wprepare_loop_start m lm (b, [])\ \ +lemma rev_eq: "rev xs = rev ys \ xs = ys" by auto + +lemma wprepare_loop_goon_Bk_empty_snd[simp]: "\lm \ []; wprepare_loop_start m lm (b, [])\ \ wprepare_loop_goon m lm (Bk # b, [])" apply(simp only: wprepare_invs) apply(erule_tac disjE) @@ -2905,118 +2543,110 @@ apply(rule_tac rev_eq, simp add: tape_of_nl_rev) done -lemma [simp]: "\lm \ []; wprepare_loop_goon m lm (b, [])\ \ b \ []" +lemma wprepare_loop_goon_nonempty_fst[simp]: "\lm \ []; wprepare_loop_goon m lm (b, [])\ \ b \ []" apply(simp only: wprepare_invs, auto) done -lemma [simp]:"\lm \ []; wprepare_loop_goon m lm (b, [])\ \ +lemma wprepare_add_one2_Bk_empty[simp]:"\lm \ []; wprepare_loop_goon m lm (b, [])\ \ wprepare_add_one2 m lm (Bk # b, [])" apply(simp only: wprepare_invs, auto split: if_splits) done -lemma [simp]: "wprepare_add_one2 m lm (b, []) \ b \ []" +lemma wprepare_add_one2_nonempty_fst[simp]: "wprepare_add_one2 m lm (b, []) \ b \ []" apply(simp only: wprepare_invs, auto) done -lemma [simp]: "wprepare_add_one2 m lm (b, []) \ wprepare_add_one2 m lm (b, [Oc])" +lemma wprepare_add_one2_Oc[simp]: "wprepare_add_one2 m lm (b, []) \ wprepare_add_one2 m lm (b, [Oc])" apply(simp only: wprepare_invs, auto) done -lemma [simp]: "Bk # list = <(m::nat) # lm> @ ys = False" +lemma Bk_not_tape_start[simp]: "(Bk # list = <(m::nat) # lm> @ ys) = False" apply(case_tac lm, auto simp: tape_of_nl_cons replicate_Suc) done -lemma [simp]: "\lm \ []; wprepare_add_one m lm (b, Bk # list)\ +lemma wprepare_goto_first_end_cases[simp]: + "\lm \ []; wprepare_add_one m lm (b, Bk # list)\ \ (b = [] \ wprepare_goto_first_end m lm ([], Oc # list)) \ (b \ [] \ wprepare_goto_first_end m lm (b, Oc # list))" apply(simp only: wprepare_invs) apply(auto simp: tape_of_nl_cons split: if_splits) apply(rule_tac x = 0 in exI, simp add: replicate_Suc) -apply(case_tac lm, simp, simp add: tape_of_nl_abv tape_of_nat_list.simps replicate_Suc) +apply(case_tac lm, simp, simp add: tape_of_list_def tape_of_nat_list.simps replicate_Suc) done -lemma [simp]: "wprepare_goto_first_end m lm (b, Bk # list) \ b \ []" +lemma wprepare_goto_first_end_Bk_nonempty_fst[simp]: + "wprepare_goto_first_end m lm (b, Bk # list) \ b \ []" apply(simp only: wprepare_invs , auto simp: replicate_Suc) done declare replicate_Suc[simp] -lemma [simp]: "wprepare_goto_first_end m lm (b, Bk # list) \ +lemma wprepare_erase_elem_Bk_rest[simp]: "wprepare_goto_first_end m lm (b, Bk # list) \ wprepare_erase m lm (tl b, hd b # Bk # list)" apply(simp only: wprepare_invs, auto) apply(case_tac mr, simp_all) apply(case_tac mr, auto) done -lemma [simp]: "wprepare_erase m lm (b, Bk # list) \ b \ []" +lemma wprepare_erase_Bk_nonempty_fst[simp]: "wprepare_erase m lm (b, Bk # list) \ b \ []" apply(simp only: wprepare_invs, auto) done -lemma [simp]: "wprepare_erase m lm (b, Bk # list) \ +lemma wprepare_goto_start_pos_Bk[simp]: "wprepare_erase m lm (b, Bk # list) \ wprepare_goto_start_pos m lm (Bk # b, list)" apply(simp only: wprepare_invs, auto) done -lemma [simp]: "\wprepare_add_one m lm (b, Bk # list)\ \ list \ []" +lemma wprepare_add_one_Bk_nonempty_snd[simp]: "\wprepare_add_one m lm (b, Bk # list)\ \ list \ []" apply(simp only: wprepare_invs) -apply(case_tac lm, simp_all add: tape_of_nl_abv - tape_of_nat_list.simps tape_of_nat_abv, auto) +apply(case_tac lm, simp_all add: tape_of_list_def tape_of_nat_def, auto) done -lemma [simp]: "\lm \ []; wprepare_goto_first_end m lm (b, Bk # list)\ \ list \ []" +lemma wprepare_goto_first_end_nonempty_snd_tl[simp]: + "\lm \ []; wprepare_goto_first_end m lm (b, Bk # list)\ \ list \ []" apply(simp only: wprepare_invs, auto) apply(case_tac mr, simp_all) -done - -lemma [simp]: "\lm \ []; wprepare_goto_first_end m lm (b, Bk # list)\ \ b \ []" + done + +lemma wprepare_erase_Bk_nonempty_list[simp]: "\lm \ []; wprepare_erase m lm (b, Bk # list)\ \ list \ []" apply(simp only: wprepare_invs, auto) done -lemma [simp]: "\lm \ []; wprepare_erase m lm (b, Bk # list)\ \ list \ []" -apply(simp only: wprepare_invs, auto) -done - -lemma [simp]: "\lm \ []; wprepare_erase m lm (b, Bk # list)\ \ b \ []" -apply(simp only: wprepare_invs, auto) -done - -lemma [simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Bk # list)\ \ list \ []" -apply(simp only: wprepare_invs, auto) -apply(case_tac lm, simp, case_tac list) -apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) -done - -lemma [simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Bk # list)\ \ b \ []" + +lemma wprepare_goto_start_pos_Bk_nonempty[simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Bk # list)\ \ list \ []" + by(cases lm;cases list;simp only: wprepare_invs, auto) + +lemma wprepare_goto_start_pos_Bk_nonempty_fst[simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Bk # list)\ \ b \ []" apply(simp only: wprepare_invs) apply(auto) done -lemma [simp]: "\lm \ []; wprepare_loop_goon m lm (b, Bk # list)\ \ b \ []" +lemma wprepare_loop_goon_Bk_nonempty[simp]: "\lm \ []; wprepare_loop_goon m lm (b, Bk # list)\ \ b \ []" apply(simp only: wprepare_invs, auto) done -lemma [simp]: "\lm \ []; wprepare_loop_goon m lm (b, Bk # list)\ \ +lemma wprepare_loop_goon_wprepare_add_one2_cases[simp]: "\lm \ []; wprepare_loop_goon m lm (b, Bk # list)\ \ (list = [] \ wprepare_add_one2 m lm (Bk # b, [])) \ (list \ [] \ wprepare_add_one2 m lm (Bk # b, list))" -apply(simp only: wprepare_invs, simp) -apply(case_tac list, simp_all split: if_splits, auto) + unfolding wprepare_invs +apply(cases list;auto split:nat.split if_splits) apply(case_tac [1-3] mr, simp_all add: ) apply(case_tac mr, simp_all) apply(case_tac [1-2] mr, simp_all add: ) -apply(case_tac rn, simp, case_tac nat, auto simp: ) +apply(case_tac rn, force, case_tac nat, auto simp: ) done -lemma [simp]: "wprepare_add_one2 m lm (b, Bk # list) \ b \ []" +lemma wprepare_add_one2_nonempty[simp]: "wprepare_add_one2 m lm (b, Bk # list) \ b \ []" apply(simp only: wprepare_invs, simp) done -lemma [simp]: "wprepare_add_one2 m lm (b, Bk # list) \ +lemma wprepare_add_one2_cases[simp]: "wprepare_add_one2 m lm (b, Bk # list) \ (list = [] \ wprepare_add_one2 m lm (b, [Oc])) \ (list \ [] \ wprepare_add_one2 m lm (b, Oc # list))" apply(simp only: wprepare_invs, auto) done -lemma [simp]: "wprepare_goto_first_end m lm (b, Oc # list) +lemma wprepare_goto_first_end_cases_Oc[simp]: "wprepare_goto_first_end m lm (b, Oc # list) \ (b = [] \ wprepare_goto_first_end m lm ([Oc], list)) \ (b \ [] \ wprepare_goto_first_end m lm (Oc # b, list))" apply(simp only: wprepare_invs, auto) @@ -3027,41 +2657,30 @@ apply(rule_tac x = "mr - 1" in exI, simp) done -lemma [simp]: "wprepare_erase m lm (b, Oc # list) \ b \ []" +lemma wprepare_erase_nonempty[simp]: "wprepare_erase m lm (b, Oc # list) \ b \ []" apply(simp only: wprepare_invs, auto simp: ) done -lemma [simp]: "wprepare_erase m lm (b, Oc # list) +lemma wprepare_erase_Bk[simp]: "wprepare_erase m lm (b, Oc # list) \ wprepare_erase m lm (b, Bk # list)" apply(simp only:wprepare_invs, auto simp: ) done -lemma [simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Bk # list)\ +lemma wprepare_goto_start_pos_Bk_move[simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Bk # list)\ \ wprepare_goto_start_pos m lm (Bk # b, list)" apply(simp only:wprepare_invs, auto) apply(case_tac [!] lm, simp, simp_all) done -lemma [simp]: "wprepare_loop_start m lm (b, aa) \ b \ []" +lemma wprepare_loop_start_b_nonempty[simp]: "wprepare_loop_start m lm (b, aa) \ b \ []" apply(simp only:wprepare_invs, auto) done -lemma [elim]: "Bk # list = Oc\(mr) @ Bk\(rn) \ \rn. list = Bk\(rn)" +lemma exists_exp_of_Bk[elim]: "Bk # list = Oc\(mr) @ Bk\(rn) \ \rn. list = Bk\(rn)" apply(case_tac mr, simp_all) apply(case_tac rn, simp_all) done -lemma rev_equal_iff: "x = y \ rev x = rev y" -by simp - -lemma tape_of_nl_false1: - "lm \ [] \ rev b @ [Bk] \ Bk\(ln) @ Oc # Oc\(m) @ Bk # Bk # " -apply(auto) -apply(drule_tac rev_equal_iff, simp add: tape_of_nl_rev) -apply(case_tac "rev lm") -apply(case_tac [2] list, auto simp: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) -done - -lemma [simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False" +lemma wprepare_loop_start_in_middle_Bk_False[simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False" apply(simp add: wprepare_loop_start_in_middle.simps, auto) apply(case_tac mr, simp_all add: ) done @@ -3072,11 +2691,11 @@ wprepare_loop_goon_in_middle.simps[simp del] wprepare_loop_goon_on_rightmost.simps[simp del] -lemma [simp]: "wprepare_loop_goon_in_middle m lm (Bk # b, []) = False" +lemma wprepare_loop_goon_in_middle_Bk_False[simp]: "wprepare_loop_goon_in_middle m lm (Bk # b, []) = False" apply(simp add: wprepare_loop_goon_in_middle.simps, auto) done -lemma [simp]: "\lm \ []; wprepare_loop_start m lm (b, [Bk])\ \ +lemma wprepare_loop_goon_Bk[simp]: "\lm \ []; wprepare_loop_start m lm (b, [Bk])\ \ wprepare_loop_goon m lm (Bk # b, [])" apply(simp only: wprepare_invs, simp) apply(simp add: wprepare_loop_goon_on_rightmost.simps @@ -3087,13 +2706,13 @@ apply(simp add: exp_ind replicate_Suc[THEN sym] del: replicate_Suc) done -lemma [simp]: "wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista) +lemma wprepare_loop_goon_in_middle_Bk_False2[simp]: "wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista) \ wprepare_loop_goon_in_middle m lm (Bk # b, a # lista) = False" apply(auto simp: wprepare_loop_start_on_rightmost.simps wprepare_loop_goon_in_middle.simps) done -lemma [simp]: "\lm \ []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\ +lemma wprepare_loop_goon_on_rightbmost_Bk_False[simp]: "\lm \ []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\ \ wprepare_loop_goon_on_rightmost m lm (Bk # b, a # lista)" apply(simp only: wprepare_loop_start_on_rightmost.simps wprepare_loop_goon_on_rightmost.simps, auto) @@ -3102,20 +2721,20 @@ apply(simp add: replicate_Suc[THEN sym] exp_ind del: replicate_Suc) done -lemma [simp]: "\lm \ []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\ +lemma wprepare_loop_goon_on_rightbmost_Bk_False_2[simp]: "\lm \ []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\ \ wprepare_loop_goon_on_rightmost m lm (Bk # b, a # lista) = False" apply(simp add: wprepare_loop_start_in_middle.simps wprepare_loop_goon_on_rightmost.simps, auto) apply(case_tac mr, simp_all add: ) apply(case_tac "lm1::nat list", simp_all, case_tac list, simp) -apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv ) +apply(simp add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def ) apply(case_tac [!] rna, simp_all add: ) apply(case_tac mr, simp_all add: ) apply(case_tac lm1, simp, case_tac list, simp) -apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) +apply(simp_all add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def) done -lemma [simp]: +lemma wprepare_loop_goon_in_middle_Bk_False3[simp]: "\lm \ []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\ \ wprepare_loop_goon_in_middle m lm (Bk # b, a # lista)" apply(simp add: wprepare_loop_start_in_middle.simps @@ -3125,10 +2744,10 @@ apply(case_tac lm1, simp) apply(rule_tac x = "Suc aa" in exI, simp) apply(rule_tac x = list in exI) -apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) +apply(case_tac list, simp_all add: tape_of_list_def tape_of_nat_def) done -lemma [simp]: "\lm \ []; wprepare_loop_start m lm (b, Bk # a # lista)\ \ +lemma wprepare_loop_goon_Bk2[simp]: "\lm \ []; wprepare_loop_start m lm (b, Bk # a # lista)\ \ wprepare_loop_goon m lm (Bk # b, a # lista)" apply(simp add: wprepare_loop_start.simps wprepare_loop_goon.simps) @@ -3148,20 +2767,16 @@ (hd b \ Oc \ (b = [] \ wprepare_add_one m lm ([], Bk # Oc # list)) \ (b \ [] \ wprepare_add_one m lm (tl b, hd b # Oc # list)))" apply(simp only: wprepare_add_one.simps, auto) -done - -lemma [simp]: "wprepare_loop_start m lm (b, Oc # list) \ b \ []" -apply(simp) -done - -lemma [simp]: "wprepare_loop_start_on_rightmost m lm (b, Oc # list) \ + done + +lemma wprepare_loop_start_on_rightmost_Oc[simp]: "wprepare_loop_start_on_rightmost m lm (b, Oc # list) \ wprepare_loop_start_on_rightmost m lm (Oc # b, list)" apply(simp add: wprepare_loop_start_on_rightmost.simps, auto) apply(rule_tac x = rn in exI, auto) apply(case_tac mr, simp_all add: ) done -lemma [simp]: "wprepare_loop_start_in_middle m lm (b, Oc # list) \ +lemma wprepare_loop_start_in_middle_Oc[simp]: "wprepare_loop_start_in_middle m lm (b, Oc # list) \ wprepare_loop_start_in_middle m lm (Oc # b, list)" apply(simp add: wprepare_loop_start_in_middle.simps, auto) apply(rule_tac x = rn in exI, auto) @@ -3176,18 +2791,18 @@ apply(erule_tac disjE, simp_all ) done -lemma [simp]: "wprepare_loop_goon m lm (b, Oc # list) \ b \ []" +lemma wprepare_loop_goon_Oc_nonempty[simp]: "wprepare_loop_goon m lm (b, Oc # list) \ b \ []" apply(simp add: wprepare_loop_goon.simps wprepare_loop_goon_in_middle.simps wprepare_loop_goon_on_rightmost.simps) apply(auto) done -lemma [simp]: "wprepare_goto_start_pos m lm (b, Oc # list) \ b \ []" +lemma wprepare_goto_start_pos_Oc_nonempty[simp]: "wprepare_goto_start_pos m lm (b, Oc # list) \ b \ []" apply(simp add: wprepare_goto_start_pos.simps) done -lemma [simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False" +lemma wprepare_loop_goon_on_rightmost_Oc_False[simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False" apply(simp add: wprepare_loop_goon_on_rightmost.simps) done @@ -3209,26 +2824,26 @@ apply(rule_tac x = "a#lista" in exI, simp) done -lemma [simp]: "wprepare_loop_goon_in_middle m lm (b, Oc # list) \ +lemma wprepare_loop_goon_in_middle_cases[simp]: "wprepare_loop_goon_in_middle m lm (b, Oc # list) \ wprepare_loop_start_on_rightmost m lm (Oc # b, list) \ wprepare_loop_start_in_middle m lm (Oc # b, list)" apply(simp add: wprepare_loop_goon_in_middle.simps split: if_splits) apply(case_tac lm1, simp_all add: wprepare_loop1 wprepare_loop2) done -lemma [simp]: "wprepare_loop_goon m lm (b, Oc # list) +lemma wprepare_loop_start_Oc[simp]: "wprepare_loop_goon m lm (b, Oc # list) \ wprepare_loop_start m lm (Oc # b, list)" apply(simp add: wprepare_loop_goon.simps wprepare_loop_start.simps) done -lemma [simp]: "wprepare_add_one m lm (b, Oc # list) +lemma wprepare_add_one_b[simp]: "wprepare_add_one m lm (b, Oc # list) \ b = [] \ wprepare_add_one m lm ([], Bk # Oc # list)" apply(auto) apply(simp add: wprepare_add_one.simps) done -lemma [simp]: "wprepare_goto_start_pos m [a] (b, Oc # list) +lemma wprepare_loop_start_on_rightmost_Oc2[simp]: "wprepare_goto_start_pos m [a] (b, Oc # list) \ wprepare_loop_start_on_rightmost m [a] (Oc # b, list) " apply(auto simp: wprepare_goto_start_pos.simps wprepare_loop_start_on_rightmost.simps) @@ -3236,7 +2851,7 @@ apply(simp add: replicate_Suc[THEN sym] exp_ind del: replicate_Suc) done -lemma [simp]: "wprepare_goto_start_pos m (a # aa # listaa) (b, Oc # list) +lemma wprepare_loop_start_in_middle_2_Oc[simp]: "wprepare_goto_start_pos m (a # aa # listaa) (b, Oc # list) \wprepare_loop_start_in_middle m (a # aa # listaa) (Oc # b, list)" apply(auto simp: wprepare_goto_start_pos.simps wprepare_loop_start_in_middle.simps) @@ -3246,20 +2861,20 @@ apply(simp add: tape_of_nl_cons) done -lemma [simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Oc # list)\ +lemma wprepare_loop_start_Oc2[simp]: "\lm \ []; wprepare_goto_start_pos m lm (b, Oc # list)\ \ wprepare_loop_start m lm (Oc # b, list)" apply(case_tac lm, simp_all) apply(case_tac lista, simp_all add: wprepare_loop_start.simps) done -lemma [simp]: "wprepare_add_one2 m lm (b, Oc # list) \ b \ []" +lemma wprepare_add_one2_Oc_nonempty[simp]: "wprepare_add_one2 m lm (b, Oc # list) \ b \ []" apply(auto simp: wprepare_add_one2.simps) done lemma add_one_2_stop: "wprepare_add_one2 m lm (b, Oc # list) \ wprepare_stop m lm (tl b, hd b # Oc # list)" -apply(simp add: wprepare_stop.simps wprepare_add_one2.simps) +apply(simp add: wprepare_add_one2.simps) done declare wprepare_stop.simps[simp del] @@ -3285,7 +2900,7 @@ simp add: step_red step.simps) apply(case_tac c, simp, case_tac [2] aa) apply(simp_all add: wprepare_inv.simps wcode_prepare_le_def lex_triple_def lex_pair_def - split: if_splits) + split: if_splits) (* slow *) apply(simp_all add: start_2_goon start_2_start add_one_2_add_one add_one_2_stop) apply(auto simp: wprepare_add_one2.simps) @@ -3304,35 +2919,33 @@ done qed -lemma [intro]: "tm_wf (t_wcode_prepare, 0)" +lemma tm_wf_t_wcode_prepare[intro]: "tm_wf (t_wcode_prepare, 0)" apply(simp add:tm_wf.simps t_wcode_prepare_def) -done - -lemma t_correct_shift: - "list_all (\(acn, st). (st \ y)) tp \ - list_all (\(acn, st). (st \ y + off)) (shift tp off) " -apply(auto simp: List.list_all_length) -apply(erule_tac x = n in allE, simp add: length_shift) -apply(case_tac "tp!n", auto simp: shift.simps) -done - -lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0" -apply(auto simp: t_twice_compile_def t_fourtimes_compile_def) -by arith - -lemma [elim]: "(a, b) \ set t_wcode_main_first_part \ + done + +lemma is_28_even[intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0" + by(auto simp: t_twice_compile_def t_fourtimes_compile_def) + +lemma b_le_28[elim]: "(a, b) \ set t_wcode_main_first_part \ b \ (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2" apply(auto simp: t_wcode_main_first_part_def t_twice_def) done -lemma tm_wf_change_termi: "tm_wf (tp, 0) \ - list_all (\(acn, st). (st \ Suc (length tp div 2))) (adjust0 tp)" -apply(auto simp: tm_wf.simps List.list_all_length) -apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits) -apply(erule_tac x = "(a, b)" in ballE, auto) -by (metis in_set_conv_nth) +lemma tm_wf_change_termi: + assumes "tm_wf (tp, 0)" + shows "list_all (\(acn, st). (st \ Suc (length tp div 2))) (adjust0 tp)" +proof - + { fix acn st n + assume "tp ! n = (acn, st)" "n < length tp" "0 < st" + hence "(acn, st)\set tp" by (metis nth_mem) + with assms tm_wf.simps have "st \ length tp div 2 + 0" by auto + hence "st \ Suc (length tp div 2)" by auto + } + thus ?thesis + by(auto simp: tm_wf.simps List.list_all_length adjust.simps split: if_splits prod.split) +qed lemma tm_wf_shift: "list_all (\(acn, st). (st \ y)) tp \ @@ -3344,11 +2957,11 @@ declare length_tp'[simp del] -lemma [simp]: "length (mopup (Suc 0)) = 16" +lemma length_mopup_1[simp]: "length (mopup (Suc 0)) = 16" apply(auto simp: mopup.simps) done -lemma [elim]: "(a, b) \ set (shift (adjust0 t_twice_compile) 12) \ +lemma twice_plus_28_elim[elim]: "(a, b) \ set (shift (adjust0 t_twice_compile) 12) \ b \ (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2" apply(simp add: t_twice_compile_def t_fourtimes_compile_def) proof - @@ -3364,8 +2977,11 @@ ultimately have "list_all (\(acn, st). (st \ (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)) (shift (adjust0 t_twice_compile) 12)" proof(auto simp add: mod_ex1 del: adjust.simps) - fix q qa - assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa" + assume "even (length (tm_of abc_twice))" + then obtain q where q:"length (tm_of abc_twice) = 2 * q" by auto + assume "even (length (tm_of abc_fourtimes))" + then obtain qa where qa:"length (tm_of abc_fourtimes) = 2 * qa" by auto + note h = q qa hence "list_all (\(acn, st). st \ (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)" proof(rule_tac tm_wf_shift t_twice_compile_def) have "list_all (\(acn, st). st \ Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)" @@ -3375,9 +2991,8 @@ apply(simp add: t_twice_compile_def, auto simp: List.list_all_length) done qed - thus "list_all (\(acn, st). st \ 30 + (q + qa)) - (shift - (adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)" + thus "list_all (\(acn, st). st \ 30 + (length (tm_of abc_twice) div 2 + length (tm_of abc_fourtimes) div 2)) + (shift (adjust0 t_twice_compile) 12)" using h by simp qed thus "b \ (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2" @@ -3388,25 +3003,26 @@ done qed -lemma [elim]: "(a, b) \ set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13)) +lemma length_plus_28_elim2[elim]: "(a, b) \ set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13)) \ b \ (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2" apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def) proof - assume g: "(a, b) \ set (shift - (adjust - (tm_of abc_fourtimes @ - shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2)) - (Suc ((length (tm_of abc_fourtimes) + 16) div 2))) - (length t_twice div 2 + 13))" + (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2)) + (Suc ((length (tm_of abc_fourtimes) + 16) div 2))) + (length t_twice div 2 + 13))" moreover have "length (tm_of abc_twice) mod 2 = 0" by auto moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto ultimately have "list_all (\(acn, st). (st \ (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)) (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))" proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def) - fix q qa - assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa" + assume "even (length (tm_of abc_twice))" + then obtain q where q:"length (tm_of abc_twice) = 2 * q" by auto + assume "even (length (tm_of abc_fourtimes))" + then obtain qa where qa:"length (tm_of abc_fourtimes) = 2 * qa" by auto + note h = q qa hence "list_all (\(acn, st). st \ (9 + qa + (21 + q))) (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))" proof(rule_tac tm_wf_shift t_twice_compile_def) @@ -3424,11 +3040,12 @@ apply(simp) done qed - thus "list_all (\(acn, st). st \ 30 + (q + qa)) - (shift - (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa) - (9 + qa)) - (21 + q))" + thus "list_all + (\(acn, st). st \ 30 + (length (tm_of abc_twice) div 2 + length (tm_of abc_fourtimes) div 2)) + (shift + (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2)) + (9 + length (tm_of abc_fourtimes) div 2)) + (21 + length (tm_of abc_twice) div 2))" apply(subgoal_tac "qa + q = q + qa") apply(simp add: h) apply(simp) @@ -3441,20 +3058,14 @@ done qed -lemma [intro]: "tm_wf (t_wcode_main, 0)" -apply(auto simp: t_wcode_main_def tm_wf.simps +lemma tm_wf_t_wcode_main[intro]: "tm_wf (t_wcode_main, 0)" +by(auto simp: t_wcode_main_def tm_wf.simps t_twice_def t_fourtimes_def del: List.list_all_iff) -done declare tm_comp.simps[simp del] lemma tm_wf_comp: "\tm_wf (A, 0); tm_wf (B, 0)\ \ tm_wf (A |+| B, 0)" -apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length - tm_comp.simps) -done - -lemma [intro]: "tm_wf (t_wcode_prepare |+| t_wcode_main, 0)" -apply(rule_tac tm_wf_comp, auto) -done + by(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length + tm_comp.simps) auto lemma prepare_mainpart_lemma: "args \ [] \ @@ -3517,40 +3128,32 @@ where "tinres xs ys = (\n. xs = ys @ Bk \ n \ ys = xs @ Bk \ n)" -lemma [simp]: "tinres r r' \ +lemma tinres_fetch_congr[simp]: "tinres r r' \ fetch t ss (read r) = fetch t ss (read r')" apply(simp add: fetch.simps, auto split: if_splits simp: tinres_def) apply(case_tac [!] n, simp_all) done -lemma [intro]: "\ n. (a::cell)\(n) = []" -by auto - -lemma [simp]: "\tinres r r'; r \ []; r' \ []\ \ hd r = hd r'" +lemma nonempty_hd_tinres[simp]: "\tinres r r'; r \ []; r' \ []\ \ hd r = hd r'" apply(auto simp: tinres_def) done -lemma [intro]: "hd (Bk\(Suc n)) = Bk" -apply(simp add: ) -done - -lemma [simp]: "\tinres r []; r \ []\ \ hd r = Bk" -apply(auto simp: tinres_def) -done - -lemma [simp]: "\tinres [] r'; r' \ []\ \ hd r' = Bk" -apply(auto simp: tinres_def) -done - -lemma [intro]: "\na. tl r = tl (r @ Bk\(n)) @ Bk\(na) \ tl (r @ Bk\(n)) = tl r @ Bk\(na)" +lemma tinres_nonempty[simp]: + "\tinres r []; r \ []\ \ hd r = Bk" + "\tinres [] r'; r' \ []\ \ hd r' = Bk" + "\tinres r []; r \ []\ \ tinres (tl r) []" + "tinres r r' \ tinres (b # r) (b # r')" + by(auto simp: tinres_def) + +lemma ex_move_tl[intro]: "\na. tl r = tl (r @ Bk\(n)) @ Bk\(na) \ tl (r @ Bk\(n)) = tl r @ Bk\(na)" apply(case_tac r, simp) apply(case_tac n, simp, simp) apply(rule_tac x = nat in exI, simp) apply(rule_tac x = n in exI, simp) done -lemma [simp]: "tinres r r' \ tinres (tl r) (tl r')" +lemma tinres_tails[simp]: "tinres r r' \ tinres (tl r) (tl r')" apply(auto simp: tinres_def) apply(case_tac r', simp) apply(case_tac n, simp_all) @@ -3558,39 +3161,22 @@ apply(rule_tac x = n in exI, simp) done -lemma [simp]: "\tinres r []; r \ []\ \ tinres (tl r) []" -apply(case_tac r, auto simp: tinres_def) -apply(case_tac n, simp_all add: ) -apply(rule_tac x = nat in exI, simp) -done - -lemma [simp]: "\tinres [] r'\ \ tinres [] (tl r')" -apply(case_tac r', auto simp: tinres_def) -apply(case_tac n, simp_all add: ) -apply(rule_tac x = nat in exI, simp) -done - -lemma [simp]: "tinres r r' \ tinres (b # r) (b # r')" -apply(auto simp: tinres_def) -done - -lemma [simp]: "tinres r [] \ tinres (Bk # tl r) [Bk]" -apply(auto simp: tinres_def) -done - -lemma [simp]: "tinres r [] \ tinres (Oc # tl r) [Oc]" -apply(auto simp: tinres_def) -done - -lemma tinres_step2: - "\tinres r r'; step0 (ss, l, r) t = (sa, la, ra); step0 (ss, l, r') t = (sb, lb, rb)\ - \ la = lb \ tinres ra rb \ sa = sb" -apply(case_tac "ss = 0", simp add: step_0) -apply(simp add: step.simps [simp del], auto) -apply(case_tac [!] "fetch t ss (read r')", simp) -apply(auto simp: update.simps) -apply(case_tac [!] a, auto split: if_splits) -done +lemma tinres_empty[simp]: + "\tinres [] r'\ \ tinres [] (tl r')" + "tinres r [] \ tinres (Bk # tl r) [Bk]" + "tinres r [] \ tinres (Oc # tl r) [Oc]" + by(auto simp: tinres_def) + +lemma tinres_step2: + assumes "tinres r r'" "step0 (ss, l, r) t = (sa, la, ra)" "step0 (ss, l, r') t = (sb, lb, rb)" + shows "la = lb \ tinres ra rb \ sa = sb" +proof (cases "fetch t ss (read r')") + case (Pair a b) + have sa:"sa = sb" using assms Pair by(force simp: step.simps) + have "la = lb \ tinres ra rb" using assms Pair + by(cases a, auto simp: step.simps split: if_splits) + thus ?thesis using sa by auto +qed lemma tinres_steps2: "\tinres r r'; steps0 (ss, l, r) t stp = (sa, la, ra); steps0 (ss, l, r') t stp = (sb, lb, rb)\ @@ -3624,85 +3210,29 @@ (W1, 2), (Nop, 7), (L, 9), (W0, 8), (L, 9), (L, 10), (L, 11), (L, 10), (R, 0), (L, 11)]" -lemma [simp]: "fetch t_wcode_adjust (Suc 0) Bk = (W1, 1)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_adjust (Suc 0) Oc = (R, 2)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_adjust (Suc (Suc 0)) Oc = (R, 3)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Oc = (R, 4)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Bk = (R, 3)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps) -done - -lemma [simp]: "fetch t_wcode_adjust 4 Bk = (L, 8)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4) -done - -lemma [simp]: "fetch t_wcode_adjust 4 Oc = (L, 5)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4) -done - -lemma [simp]: "fetch t_wcode_adjust 5 Oc = (W0, 5)" -apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, simp) -done - -lemma [simp]: "fetch t_wcode_adjust 5 Bk = (L, 6)" -apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, auto) -done - -lemma [simp]: "fetch t_wcode_adjust 6 Oc = (R, 7)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6) -done - -lemma [simp]: "fetch t_wcode_adjust 6 Bk = (L, 6)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6) -done - -lemma [simp]: "fetch t_wcode_adjust 7 Bk = (W1, 2)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_7_eq_7) -done - -lemma [simp]: "fetch t_wcode_adjust 8 Bk = (L, 9)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_8_eq_8) -done - -lemma [simp]: "fetch t_wcode_adjust 8 Oc = (W0, 8)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_8_eq_8) -done - -lemma [simp]: "fetch t_wcode_adjust 9 Oc = (L, 10)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_9_eq_9) -done - -lemma [simp]: "fetch t_wcode_adjust 9 Bk = (L, 9)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_9_eq_9) -done - -lemma [simp]: "fetch t_wcode_adjust 10 Bk = (L, 11)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_10_eq_10) -done - -lemma [simp]: "fetch t_wcode_adjust 10 Oc = (L, 10)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral) -done - -lemma [simp]: "fetch t_wcode_adjust 11 Oc = (L, 11)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral) -done - -lemma [simp]: "fetch t_wcode_adjust 11 Bk = (R, 0)" -apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral) -done +lemma fetch_t_wcode_adjust[simp]: + "fetch t_wcode_adjust (Suc 0) Bk = (W1, 1)" + "fetch t_wcode_adjust (Suc 0) Oc = (R, 2)" + "fetch t_wcode_adjust (Suc (Suc 0)) Oc = (R, 3)" + "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Oc = (R, 4)" + "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Bk = (R, 3)" + "fetch t_wcode_adjust 4 Bk = (L, 8)" + "fetch t_wcode_adjust 4 Oc = (L, 5)" + "fetch t_wcode_adjust 5 Oc = (W0, 5)" + "fetch t_wcode_adjust 5 Bk = (L, 6)" + "fetch t_wcode_adjust 6 Oc = (R, 7)" + "fetch t_wcode_adjust 6 Bk = (L, 6)" + "fetch t_wcode_adjust 7 Bk = (W1, 2)" + "fetch t_wcode_adjust 8 Bk = (L, 9)" + "fetch t_wcode_adjust 8 Oc = (W0, 8)" + "fetch t_wcode_adjust 9 Oc = (L, 10)" + "fetch t_wcode_adjust 9 Bk = (L, 9)" + "fetch t_wcode_adjust 10 Bk = (L, 11)" + "fetch t_wcode_adjust 10 Oc = (L, 10)" + "fetch t_wcode_adjust 11 Oc = (L, 11)" + "fetch t_wcode_adjust 11 Bk = (R, 0)" +by(auto simp: fetch.simps t_wcode_adjust_def nth_of.simps numeral) + fun wadjust_start :: "nat \ nat \ tape \ bool" where @@ -3913,7 +3443,7 @@ definition wadjust_le :: "((nat \ config) \ nat \ config) set" where "wadjust_le \ (inv_image lex_square wadjust_measure)" -lemma [intro]: "wf lex_square" +lemma wf_lex_square[intro]: "wf lex_square" by(auto intro:wf_lex_prod simp: Abacus.lex_pair_def lex_square_def Abacus.lex_triple_def) @@ -3921,141 +3451,97 @@ by(auto intro:wf_inv_image simp: wadjust_le_def Abacus.lex_triple_def Abacus.lex_pair_def) -lemma [simp]: "wadjust_start m rs (c, []) = False" +lemma wadjust_start_snd_nonempty[simp]: "wadjust_start m rs (c, []) = False" apply(auto simp: wadjust_start.simps) done -lemma [simp]: "wadjust_loop_right_move m rs (c, []) \ c \ []" +lemma wadjust_loop_right_move_fst_nonempty[simp]: "wadjust_loop_right_move m rs (c, []) \ c \ []" apply(auto simp: wadjust_loop_right_move.simps) done -lemma [simp]: "wadjust_loop_right_move m rs (c, []) - \ wadjust_loop_check m rs (Bk # c, [])" -apply(simp only: wadjust_loop_right_move.simps wadjust_loop_check.simps) -apply(auto) -done - -lemma [simp]: "wadjust_loop_check m rs (c, []) \ c \ []" +lemma wadjust_loop_check_fst_nonempty[simp]: "wadjust_loop_check m rs (c, []) \ c \ []" apply(simp only: wadjust_loop_check.simps, auto) done -lemma [simp]: "wadjust_loop_start m rs (c, []) = False" +lemma wadjust_loop_start_snd_nonempty[simp]: "wadjust_loop_start m rs (c, []) = False" apply(simp add: wadjust_loop_start.simps) done -lemma [simp]: "wadjust_loop_right_move m rs (c, []) \ - wadjust_loop_right_move m rs (Bk # c, [])" -apply(simp only: wadjust_loop_right_move.simps) -apply(erule_tac exE)+ -apply(auto) -done - -lemma [simp]: "wadjust_loop_check m rs (c, []) \ wadjust_erase2 m rs (tl c, [hd c])" +lemma wadjust_erase2_singleton[simp]: "wadjust_loop_check m rs (c, []) \ wadjust_erase2 m rs (tl c, [hd c])" apply(simp only: wadjust_loop_check.simps wadjust_erase2.simps, auto) done -lemma [simp]: " wadjust_loop_erase m rs (c, []) - \ (c = [] \ wadjust_loop_on_left_moving m rs ([], [Bk])) \ - (c \ [] \ wadjust_loop_on_left_moving m rs (tl c, [hd c]))" -apply(simp add: wadjust_loop_erase.simps) -done - -lemma [simp]: "wadjust_loop_on_left_moving m rs (c, []) = False" -apply(auto simp: wadjust_loop_on_left_moving.simps) -done - - -lemma [simp]: "wadjust_loop_right_move2 m rs (c, []) = False" -apply(auto simp: wadjust_loop_right_move2.simps) -done - -lemma [simp]: "wadjust_erase2 m rs ([], []) = False" -apply(auto simp: wadjust_erase2.simps) -done - -lemma [simp]: "wadjust_on_left_moving_B m rs +lemma wadjust_loop_on_left_moving_snd_nonempty[simp]: + "wadjust_loop_on_left_moving m rs (c, []) = False" +"wadjust_loop_right_move2 m rs (c, []) = False" +"wadjust_erase2 m rs ([], []) = False" + by(auto simp: wadjust_loop_on_left_moving.simps + wadjust_loop_right_move2.simps + wadjust_erase2.simps) + +lemma wadjust_on_left_moving_B_Bk1[simp]: "wadjust_on_left_moving_B m rs (Oc # Oc # Oc\(rs) @ Bk # Oc # Oc\(m), [Bk])" apply(simp add: wadjust_on_left_moving_B.simps, auto) done -lemma [simp]: "wadjust_on_left_moving_B m rs +lemma wadjust_on_left_moving_B_Bk2[simp]: "wadjust_on_left_moving_B m rs (Bk\(n) @ Bk # Oc # Oc # Oc\(rs) @ Bk # Oc # Oc\(m), [Bk])" apply(simp add: wadjust_on_left_moving_B.simps , auto) apply(rule_tac x = "Suc n" in exI, simp add: exp_ind del: replicate_Suc) done -lemma [simp]: "\wadjust_erase2 m rs (c, []); c \ []\ \ +lemma wadjust_on_left_moving_singleton[simp]: "\wadjust_erase2 m rs (c, []); c \ []\ \ wadjust_on_left_moving m rs (tl c, [hd c])" apply(simp only: wadjust_erase2.simps) apply(erule_tac exE)+ apply(case_tac ln, simp_all add: wadjust_on_left_moving.simps) done -lemma [simp]: "wadjust_erase2 m rs (c, []) +lemma wadjust_erase2_cases[simp]: "wadjust_erase2 m rs (c, []) \ (c = [] \ wadjust_on_left_moving m rs ([], [Bk])) \ (c \ [] \ wadjust_on_left_moving m rs (tl c, [hd c]))" apply(auto) done -lemma [simp]: "wadjust_on_left_moving m rs ([], []) = False" -apply(simp add: wadjust_on_left_moving.simps +lemma wadjust_on_left_moving_nonempty[simp]: + "wadjust_on_left_moving m rs ([], []) = False" + "wadjust_on_left_moving_O m rs (c, []) = False" +apply(auto simp: wadjust_on_left_moving.simps wadjust_on_left_moving_O.simps wadjust_on_left_moving_B.simps) done -lemma [simp]: "wadjust_on_left_moving_O m rs (c, []) = False" -apply(simp add: wadjust_on_left_moving_O.simps) -done - -lemma [simp]: " \wadjust_on_left_moving_B m rs (c, []); c \ []; hd c = Bk\ \ +lemma wadjust_on_left_moving_B_singleton_Bk[simp]: + " \wadjust_on_left_moving_B m rs (c, []); c \ []; hd c = Bk\ \ wadjust_on_left_moving_B m rs (tl c, [Bk])" apply(simp add: wadjust_on_left_moving_B.simps, auto) apply(case_tac [!] ln, simp_all) done -lemma [simp]: "\wadjust_on_left_moving_B m rs (c, []); c \ []; hd c = Oc\ \ +lemma wadjust_on_left_moving_B_singleton_Oc[simp]: + "\wadjust_on_left_moving_B m rs (c, []); c \ []; hd c = Oc\ \ wadjust_on_left_moving_O m rs (tl c, [Oc])" apply(simp add: wadjust_on_left_moving_B.simps wadjust_on_left_moving_O.simps, auto) apply(case_tac [!] ln, simp_all add: ) -done - -lemma [simp]: "\wadjust_on_left_moving m rs (c, []); c \ []\ \ + done + +lemma wadjust_on_left_moving_singleton2[simp]: + "\wadjust_on_left_moving m rs (c, []); c \ []\ \ wadjust_on_left_moving m rs (tl c, [hd c])" apply(simp add: wadjust_on_left_moving.simps) apply(case_tac "hd c", simp_all) done -lemma [simp]: "wadjust_on_left_moving m rs (c, []) - \ (c = [] \ wadjust_on_left_moving m rs ([], [Bk])) \ - (c \ [] \ wadjust_on_left_moving m rs (tl c, [hd c]))" -apply(auto) -done - -lemma [simp]: "wadjust_goon_left_moving m rs (c, []) = False" -apply(auto simp: wadjust_goon_left_moving.simps wadjust_goon_left_moving_B.simps - wadjust_goon_left_moving_O.simps) -done - -lemma [simp]: "wadjust_backto_standard_pos m rs (c, []) = False" -apply(auto simp: wadjust_backto_standard_pos.simps +lemma wadjust_nonempty[simp]: "wadjust_goon_left_moving m rs (c, []) = False" +"wadjust_backto_standard_pos m rs (c, []) = False" + by(auto simp: wadjust_goon_left_moving.simps wadjust_goon_left_moving_B.simps + wadjust_goon_left_moving_O.simps wadjust_backto_standard_pos.simps wadjust_backto_standard_pos_B.simps wadjust_backto_standard_pos_O.simps) -done - -lemma [simp]: - "wadjust_start m rs (c, Bk # list) \ - (c = [] \ wadjust_start m rs ([], Oc # list)) \ - (c \ [] \ wadjust_start m rs (c, Oc # list))" -apply(auto simp: wadjust_start.simps) -done - -lemma [simp]: "wadjust_loop_start m rs (c, Bk # list) = False" + +lemma wadjust_loop_start_no_Bk[simp]: "wadjust_loop_start m rs (c, Bk # list) = False" apply(auto simp: wadjust_loop_start.simps) done -lemma [simp]: "wadjust_loop_right_move m rs (c, b) \ c \ []" -apply(simp only: wadjust_loop_right_move.simps, auto) -done - -lemma [simp]: "wadjust_loop_right_move m rs (c, Bk # list) +lemma wadjust_loop_right_move_Bk[simp]: "wadjust_loop_right_move m rs (c, Bk # list) \ wadjust_loop_right_move m rs (Bk # c, list)" apply(simp only: wadjust_loop_right_move.simps) apply(erule_tac exE)+ @@ -4066,24 +3552,20 @@ apply(rule_tac x = nat in exI, auto) done -lemma [simp]: "wadjust_loop_check m rs (c, b) \ c \ []" +lemma wadjust_loop_check_nonempty[simp]: "wadjust_loop_check m rs (c, b) \ c \ []" apply(simp only: wadjust_loop_check.simps, auto) done -lemma [simp]: "wadjust_loop_check m rs (c, Bk # list) +lemma wadjust_erase2_via_loop_check_Bk[simp]: "wadjust_loop_check m rs (c, Bk # list) \ wadjust_erase2 m rs (tl c, hd c # Bk # list)" apply(auto simp: wadjust_loop_check.simps wadjust_erase2.simps) apply(case_tac [!] mr, simp_all) done -lemma [simp]: "wadjust_loop_erase m rs (c, b) \ c \ []" -apply(simp only: wadjust_loop_erase.simps, auto) -done - declare wadjust_loop_on_left_moving_O.simps[simp del] wadjust_loop_on_left_moving_B.simps[simp del] -lemma [simp]: "\wadjust_loop_erase m rs (c, Bk # list); hd c = Bk\ +lemma wadjust_loop_on_left_moving_B_via_erase[simp]: "\wadjust_loop_erase m rs (c, Bk # list); hd c = Bk\ \ wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)" apply(simp only: wadjust_loop_erase.simps wadjust_loop_on_left_moving_B.simps) @@ -4094,28 +3576,22 @@ apply(simp add: exp_ind [THEN sym]) done -lemma [simp]: "\wadjust_loop_erase m rs (c, Bk # list); c \ []; hd c = Oc\ \ +lemma wadjust_loop_on_left_moving_O_Bk_via_erase[simp]: + "\wadjust_loop_erase m rs (c, Bk # list); c \ []; hd c = Oc\ \ wadjust_loop_on_left_moving_O m rs (tl c, Oc # Bk # list)" apply(simp only: wadjust_loop_erase.simps wadjust_loop_on_left_moving_O.simps, auto) apply(case_tac [!] ln, simp_all add: ) done -lemma [simp]: "\wadjust_loop_erase m rs (c, Bk # list); c \ []\ \ +lemma wadjust_loop_on_left_moving_Bk_via_erase[simp]: "\wadjust_loop_erase m rs (c, Bk # list); c \ []\ \ wadjust_loop_on_left_moving m rs (tl c, hd c # Bk # list)" apply(case_tac "hd c", simp_all add:wadjust_loop_on_left_moving.simps) done -lemma [simp]: "wadjust_loop_on_left_moving m rs (c, b) \ c \ []" -apply(simp add: wadjust_loop_on_left_moving.simps -wadjust_loop_on_left_moving_O.simps wadjust_loop_on_left_moving_B.simps, auto) -done - -lemma [simp]: "wadjust_loop_on_left_moving_O m rs (c, Bk # list) = False" -apply(simp add: wadjust_loop_on_left_moving_O.simps) -done - -lemma [simp]: "\wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\ + +lemma wadjust_loop_on_left_moving_B_Bk_move[simp]: + "\wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\ \ wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)" apply(simp only: wadjust_loop_on_left_moving_B.simps) apply(erule_tac exE)+ @@ -4124,7 +3600,8 @@ apply(rule_tac x = "Suc nr" in exI, auto simp: ) done -lemma [simp]: "\wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Oc\ +lemma wadjust_loop_on_left_moving_O_Oc_move[simp]: + "\wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Oc\ \ wadjust_loop_on_left_moving_O m rs (tl c, Oc # Bk # list)" apply(simp only: wadjust_loop_on_left_moving_O.simps wadjust_loop_on_left_moving_B.simps) @@ -4133,17 +3610,35 @@ apply(case_tac nl, simp_all add: , auto) done -lemma [simp]: "wadjust_loop_on_left_moving m rs (c, Bk # list) +lemma wadjust_loop_on_left_moving_O_noBk[simp]: + "wadjust_loop_on_left_moving_O m rs (c, Bk # list) = False" +apply(simp add: wadjust_loop_on_left_moving_O.simps) +done +lemma wadjust_loop_on_left_moving_Bk_move[simp]: + "wadjust_loop_on_left_moving m rs (c, Bk # list) \ wadjust_loop_on_left_moving m rs (tl c, hd c # Bk # list)" apply(simp add: wadjust_loop_on_left_moving.simps) apply(case_tac "hd c", simp_all) done -lemma [simp]: "wadjust_loop_right_move2 m rs (c, b) \ c \ []" -apply(simp only: wadjust_loop_right_move2.simps, auto) -done - -lemma [simp]: "wadjust_loop_right_move2 m rs (c, Bk # list) \ wadjust_loop_start m rs (c, Oc # list)" +lemma wadjust_loop_erase_nonempty[simp]: "wadjust_loop_erase m rs (c, b) \ c \ []" +"wadjust_loop_on_left_moving m rs (c, b) \ c \ []" +"wadjust_loop_right_move2 m rs (c, b) \ c \ []" +"wadjust_erase2 m rs (c, Bk # list) \ c \ []" +"wadjust_on_left_moving m rs (c,b) \ c \ []" +"wadjust_on_left_moving_O m rs (c, Bk # list) = False" +"wadjust_goon_left_moving m rs (c, b) \ c \ []" + by(auto simp: wadjust_loop_erase.simps wadjust_loop_on_left_moving.simps + wadjust_loop_on_left_moving_O.simps wadjust_loop_on_left_moving_B.simps + wadjust_loop_right_move2.simps wadjust_erase2.simps + wadjust_on_left_moving.simps + wadjust_on_left_moving_O.simps + wadjust_on_left_moving_B.simps wadjust_goon_left_moving.simps + wadjust_goon_left_moving_B.simps + wadjust_goon_left_moving_O.simps) + +lemma wadjust_loop_start_Oc_via_Bk_move[simp]: +"wadjust_loop_right_move2 m rs (c, Bk # list) \ wadjust_loop_start m rs (c, Oc # list)" apply(auto simp: wadjust_loop_right_move2.simps wadjust_loop_start.simps) apply(case_tac ln, simp_all add: ) apply(rule_tac x = 0 in exI, simp) @@ -4152,13 +3647,9 @@ apply(rule_tac x = "Suc nat" in exI, simp add: exp_ind del: replicate_Suc) apply(rule_tac x = rn in exI, auto) apply(rule_tac x = "Suc ml" in exI, auto ) -done - -lemma [simp]: "wadjust_erase2 m rs (c, Bk # list) \ c \ []" -apply(auto simp:wadjust_erase2.simps ) -done - -lemma [simp]: "wadjust_erase2 m rs (c, Bk # list) \ + done + +lemma wadjust_on_left_moving_Bk_via_erase[simp]: "wadjust_erase2 m rs (c, Bk # list) \ wadjust_on_left_moving m rs (tl c, hd c # Bk # list)" apply(auto simp: wadjust_erase2.simps) apply(case_tac ln, simp_all add: wadjust_on_left_moving.simps @@ -4167,88 +3658,39 @@ apply(rule_tac x = "(Suc (Suc rn))" in exI, simp add: ) apply(rule_tac x = "Suc nat" in exI, simp add: exp_ind del: replicate_Suc) apply(rule_tac x = "(Suc (Suc rn))" in exI, simp add: ) -done - -lemma [simp]: "wadjust_on_left_moving m rs (c,b) \ c \ []" -apply(simp only:wadjust_on_left_moving.simps - wadjust_on_left_moving_O.simps - wadjust_on_left_moving_B.simps - , auto) -done - -lemma [simp]: "wadjust_on_left_moving_O m rs (c, Bk # list) = False" -apply(simp add: wadjust_on_left_moving_O.simps) -done - -lemma [simp]: "\wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Bk\ + done + + +lemma wadjust_on_left_moving_B_Bk_drop_one: "\wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Bk\ \ wadjust_on_left_moving_B m rs (tl c, Bk # Bk # list)" apply(auto simp: wadjust_on_left_moving_B.simps) apply(case_tac ln, simp_all) done -lemma [simp]: "\wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Oc\ +lemma wadjust_on_left_moving_B_Bk_drop_Oc: "\wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Oc\ \ wadjust_on_left_moving_O m rs (tl c, Oc # Bk # list)" apply(auto simp: wadjust_on_left_moving_O.simps wadjust_on_left_moving_B.simps) apply(case_tac ln, simp_all add: ) done -lemma [simp]: "wadjust_on_left_moving m rs (c, Bk # list) \ +lemma wadjust_on_left_moving_B_drop[simp]: "wadjust_on_left_moving m rs (c, Bk # list) \ wadjust_on_left_moving m rs (tl c, hd c # Bk # list)" -apply(simp add: wadjust_on_left_moving.simps) -apply(case_tac "hd c", simp_all) -done - -lemma [simp]: "wadjust_goon_left_moving m rs (c, b) \ c \ []" -apply(simp add: wadjust_goon_left_moving.simps - wadjust_goon_left_moving_B.simps - wadjust_goon_left_moving_O.simps , auto) -done - -lemma [simp]: "wadjust_goon_left_moving_O m rs (c, Bk # list) = False" + by(cases "hd c", auto simp:wadjust_on_left_moving.simps wadjust_on_left_moving_B_Bk_drop_one + wadjust_on_left_moving_B_Bk_drop_Oc) + +lemma wadjust_goon_left_moving_O_no_Bk[simp]: "wadjust_goon_left_moving_O m rs (c, Bk # list) = False" apply(simp add: wadjust_goon_left_moving_O.simps, auto) apply(case_tac mr, simp_all add: ) done -lemma [simp]: "\wadjust_goon_left_moving_B m rs (c, Bk # list); hd c = Bk\ - \ wadjust_backto_standard_pos_B m rs (tl c, Bk # Bk # list)" -apply(auto simp: wadjust_goon_left_moving_B.simps - wadjust_backto_standard_pos_B.simps ) -done - -lemma [simp]: "\wadjust_goon_left_moving_B m rs (c, Bk # list); hd c = Oc\ - \ wadjust_backto_standard_pos_O m rs (tl c, Oc # Bk # list)" -apply(auto simp: wadjust_goon_left_moving_B.simps - wadjust_backto_standard_pos_O.simps) -done - -lemma [simp]: "wadjust_goon_left_moving m rs (c, Bk # list) \ +lemma wadjust_backto_standard_pos_via_left_Bk[simp]: + "wadjust_goon_left_moving m rs (c, Bk # list) \ wadjust_backto_standard_pos m rs (tl c, hd c # Bk # list)" -apply(case_tac "hd c", simp_all add: wadjust_backto_standard_pos.simps - wadjust_goon_left_moving.simps) -done - -lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list) \ - (c = [] \ wadjust_stop m rs ([Bk], list)) \ (c \ [] \ wadjust_stop m rs (Bk # c, list))" -apply(auto simp: wadjust_backto_standard_pos.simps - wadjust_backto_standard_pos_B.simps - wadjust_backto_standard_pos_O.simps wadjust_stop.simps) -apply(case_tac [!] mr, simp_all add: ) -done - -lemma [simp]: "wadjust_start m rs (c, Oc # list) - \ (c = [] \ wadjust_loop_start m rs ([Oc], list)) \ - (c \ [] \ wadjust_loop_start m rs (Oc # c, list))" -apply(auto simp:wadjust_loop_start.simps wadjust_start.simps ) -apply(rule_tac x = ln in exI, rule_tac x = rn in exI, - rule_tac x = "Suc 0" in exI, simp) -done - -lemma [simp]: "wadjust_loop_start m rs (c, b) \ c \ []" -apply(simp add: wadjust_loop_start.simps, auto) -done - -lemma [simp]: "wadjust_loop_start m rs (c, Oc # list) +by(case_tac "hd c", simp_all add: wadjust_backto_standard_pos.simps wadjust_goon_left_moving.simps + wadjust_goon_left_moving_B.simps wadjust_backto_standard_pos_O.simps) + +lemma wadjust_loop_right_move_Oc[simp]: "wadjust_loop_start m rs (c, Oc # list) \ wadjust_loop_right_move m rs (Oc # c, list)" apply(simp add: wadjust_loop_start.simps wadjust_loop_right_move.simps, auto) apply(rule_tac x = ml in exI, rule_tac x = mr in exI, @@ -4256,7 +3698,7 @@ apply(rule_tac x = "Suc ln" in exI, simp add: exp_ind del: replicate_Suc) done -lemma [simp]: "wadjust_loop_right_move m rs (c, Oc # list) \ +lemma wadjust_loop_check_Oc[simp]: "wadjust_loop_right_move m rs (c, Oc # list) \ wadjust_loop_check m rs (Oc # c, list)" apply(simp add: wadjust_loop_right_move.simps wadjust_loop_check.simps, auto) @@ -4266,7 +3708,7 @@ apply(case_tac [!] nr, simp_all) done -lemma [simp]: "wadjust_loop_check m rs (c, Oc # list) \ +lemma wadjust_loop_erase_move_Oc[simp]: "wadjust_loop_check m rs (c, Oc # list) \ wadjust_loop_erase m rs (tl c, hd c # Oc # list)" apply(simp only: wadjust_loop_check.simps wadjust_loop_erase.simps) apply(erule_tac exE)+ @@ -4274,45 +3716,41 @@ apply(case_tac mr, simp_all add: ) done -lemma [simp]: "wadjust_loop_erase m rs (c, Oc # list) \ +lemma wadjust_loop_erase_Bk_via_Oc[simp]: "wadjust_loop_erase m rs (c, Oc # list) \ wadjust_loop_erase m rs (c, Bk # list)" apply(auto simp: wadjust_loop_erase.simps) done -lemma [simp]: "wadjust_loop_on_left_moving_B m rs (c, Oc # list) = False" +lemma wadjust_loop_on_left_moving_B_no_Oc[simp]: "wadjust_loop_on_left_moving_B m rs (c, Oc # list) = False" apply(auto simp: wadjust_loop_on_left_moving_B.simps) apply(case_tac nr, simp_all add: ) done -lemma [simp]: "wadjust_loop_on_left_moving m rs (c, Oc # list) +lemma wadjust_loop_right_move2_via_left_moving[simp]: + "wadjust_loop_on_left_moving m rs (c, Oc # list) \ wadjust_loop_right_move2 m rs (Oc # c, list)" apply(simp add:wadjust_loop_on_left_moving.simps) apply(auto simp: wadjust_loop_on_left_moving_O.simps wadjust_loop_right_move2.simps) done -lemma [simp]: "wadjust_loop_right_move2 m rs (c, Oc # list) = False" +lemma wadjust_loop_right_move2_no_Oc[simp]: "wadjust_loop_right_move2 m rs (c, Oc # list) = False" apply(auto simp: wadjust_loop_right_move2.simps ) apply(case_tac ln, simp_all add: ) done -lemma [simp]: "wadjust_erase2 m rs (c, Oc # list) - \ (c = [] \ wadjust_erase2 m rs ([], Bk # list)) - \ (c \ [] \ wadjust_erase2 m rs (c, Bk # list))" -apply(auto simp: wadjust_erase2.simps ) -done - -lemma [simp]: "wadjust_on_left_moving_B m rs (c, Oc # list) = False" +lemma wadjust_on_left_moving_B_no_Oc[simp]: + "wadjust_on_left_moving_B m rs (c, Oc # list) = False" apply(auto simp: wadjust_on_left_moving_B.simps) done -lemma [simp]: "\wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Bk\ \ +lemma wadjust_goon_left_moving_B_Bk_Oc: "\wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Bk\ \ wadjust_goon_left_moving_B m rs (tl c, Bk # Oc # list)" apply(auto simp: wadjust_on_left_moving_O.simps wadjust_goon_left_moving_B.simps ) done -lemma [simp]: "\wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Oc\ +lemma wadjust_goon_left_moving_O_Oc_Oc: "\wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Oc\ \ wadjust_goon_left_moving_O m rs (tl c, Oc # Oc # list)" apply(auto simp: wadjust_on_left_moving_O.simps wadjust_goon_left_moving_O.simps ) @@ -4320,31 +3758,18 @@ done -lemma [simp]: "wadjust_on_left_moving m rs (c, Oc # list) \ +lemma wadjust_goon_left_moving_Oc[simp]: "wadjust_on_left_moving m rs (c, Oc # list) \ wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)" -apply(simp add: wadjust_on_left_moving.simps - wadjust_goon_left_moving.simps) -apply(case_tac "hd c", simp_all) -done - -lemma [simp]: "wadjust_on_left_moving m rs (c, Oc # list) \ - wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)" -apply(simp add: wadjust_on_left_moving.simps - wadjust_goon_left_moving.simps) -apply(case_tac "hd c", simp_all) -done - -lemma [simp]: "wadjust_goon_left_moving_B m rs (c, Oc # list) = False" -apply(auto simp: wadjust_goon_left_moving_B.simps) -done - -lemma [simp]: "\wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Bk\ + by(cases "hd c"; force simp: wadjust_on_left_moving.simps wadjust_goon_left_moving.simps + wadjust_goon_left_moving_B_Bk_Oc wadjust_goon_left_moving_O_Oc_Oc)+ + +lemma left_moving_Bk_Oc[simp]: "\wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Bk\ \ wadjust_goon_left_moving_B m rs (tl c, Bk # Oc # list)" apply(auto simp: wadjust_goon_left_moving_O.simps wadjust_goon_left_moving_B.simps) apply(case_tac [!] ml, auto simp: ) done -lemma [simp]: "\wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Oc\ \ +lemma left_moving_Oc_Oc[simp]: "\wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Oc\ \ wadjust_goon_left_moving_O m rs (tl c, Oc # Oc # list)" apply(auto simp: wadjust_goon_left_moving_O.simps wadjust_goon_left_moving_B.simps) apply(rule_tac x = "ml - 1" in exI, simp) @@ -4352,48 +3777,54 @@ apply(rule_tac x = "Suc mr" in exI, auto simp: ) done -lemma [simp]: "wadjust_goon_left_moving m rs (c, Oc # list) \ +lemma wadjust_goon_left_moving_B_no_Oc[simp]: + "wadjust_goon_left_moving_B m rs (c, Oc # list) = False" +apply(auto simp: wadjust_goon_left_moving_B.simps) + done + +lemma wadjust_goon_left_moving_Oc_move[simp]: "wadjust_goon_left_moving m rs (c, Oc # list) \ wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)" -apply(simp add: wadjust_goon_left_moving.simps) -apply(case_tac "hd c", simp_all) -done - -lemma [simp]: "wadjust_backto_standard_pos_B m rs (c, Oc # list) = False" +by(cases "hd c",auto simp: wadjust_goon_left_moving.simps) + +lemma wadjust_backto_standard_pos_B_no_Oc[simp]: + "wadjust_backto_standard_pos_B m rs (c, Oc # list) = False" apply(simp add: wadjust_backto_standard_pos_B.simps) done -lemma [simp]: "wadjust_backto_standard_pos_O m rs (c, Bk # xs) = False" +lemma wadjust_backto_standard_pos_O_no_Bk[simp]: + "wadjust_backto_standard_pos_O m rs (c, Bk # xs) = False" apply(simp add: wadjust_backto_standard_pos_O.simps, auto) apply(case_tac mr, simp_all add: ) done -lemma [simp]: "wadjust_backto_standard_pos_O m rs ([], Oc # list) \ +lemma wadjust_backto_standard_pos_B_Bk_Oc[simp]: + "wadjust_backto_standard_pos_O m rs ([], Oc # list) \ wadjust_backto_standard_pos_B m rs ([], Bk # Oc # list)" apply(auto simp: wadjust_backto_standard_pos_O.simps wadjust_backto_standard_pos_B.simps) done -lemma [simp]: +lemma wadjust_backto_standard_pos_B_Bk_Oc_via_O[simp]: "\wadjust_backto_standard_pos_O m rs (c, Oc # list); c \ []; hd c = Bk\ \ wadjust_backto_standard_pos_B m rs (tl c, Bk # Oc # list)" apply(simp add:wadjust_backto_standard_pos_O.simps wadjust_backto_standard_pos_B.simps, auto) done -lemma [simp]: "\wadjust_backto_standard_pos_O m rs (c, Oc # list); c \ []; hd c = Oc\ +lemma wadjust_backto_standard_pos_B_Oc_Oc_via_O[simp]: "\wadjust_backto_standard_pos_O m rs (c, Oc # list); c \ []; hd c = Oc\ \ wadjust_backto_standard_pos_O m rs (tl c, Oc # Oc # list)" apply(simp add: wadjust_backto_standard_pos_O.simps, auto) apply(case_tac ml, simp_all add: , auto) done -lemma [simp]: "wadjust_backto_standard_pos m rs (c, Oc # list) +lemma wadjust_backto_standard_pos_cases[simp]: "wadjust_backto_standard_pos m rs (c, Oc # list) \ (c = [] \ wadjust_backto_standard_pos m rs ([], Bk # Oc # list)) \ (c \ [] \ wadjust_backto_standard_pos m rs (tl c, hd c # Oc # list))" apply(auto simp: wadjust_backto_standard_pos.simps) apply(case_tac "hd c", simp_all) done -lemma [simp]: "wadjust_loop_right_move m rs (c, []) = False" +lemma wadjust_loop_right_move_nonempty_snd[simp]: "wadjust_loop_right_move m rs (c, []) = False" apply(simp only: wadjust_loop_right_move.simps) apply(rule_tac iffI) apply(erule_tac exE)+ @@ -4401,11 +3832,11 @@ apply(case_tac mr, simp_all add: ) done -lemma [simp]: "wadjust_loop_erase m rs (c, []) = False" +lemma wadjust_loop_erase_nonempty_snd[simp]: "wadjust_loop_erase m rs (c, []) = False" apply(simp only: wadjust_loop_erase.simps, auto) done -lemma [simp]: "\Suc (Suc rs) = a; wadjust_loop_erase m rs (c, Bk # list)\ +lemma wadjust_loop_erase_cases2[simp]: "\Suc (Suc rs) = a; wadjust_loop_erase m rs (c, Bk # list)\ \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) < a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Bk # list)))) \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) = @@ -4413,17 +3844,7 @@ apply(simp only: wadjust_loop_erase.simps) apply(rule_tac disjI2) apply(case_tac c, simp, simp) -done - -lemma [simp]: - "\Suc (Suc rs) = a; wadjust_loop_on_left_moving m rs (c, Bk # list)\ - \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) - < a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Bk # list)))) \ - a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) = - a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Bk # list))))" -apply(subgoal_tac "c \ []") -apply(case_tac c, simp_all) -done + done lemma dropWhile_exp1: "dropWhile (\a. a = Oc) (Oc\(n) @ xs) = dropWhile (\a. a = Oc) xs" apply(induct n, simp_all add: ) @@ -4432,19 +3853,39 @@ apply(induct n, simp_all add: ) done -lemma [simp]: "\Suc (Suc rs) = a; wadjust_loop_right_move2 m rs (c, Bk # list)\ - \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Oc # list)))) +lemma wadjust_correctness_helper_1: + assumes "Suc (Suc rs) = a" " wadjust_loop_right_move2 m rs (c, Bk # list)" + shows "a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Oc # list)))) < a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Bk # list))))" -apply(simp add: wadjust_loop_right_move2.simps, auto) -apply(simp add: dropWhile_exp1 takeWhile_exp1) -apply(case_tac ln, simp, simp add: ) -done - -lemma [simp]: "wadjust_loop_check m rs ([], b) = False" +proof - + have "ml + mr = Suc rs \ 0 < mr \ + rs - (ml + length (takeWhile (\a. a = Oc) list)) + < Suc rs - + (ml + + length + (takeWhile (\a. a = Oc) + (Bk \ ln @ Bk # Bk # Oc \ mr @ Bk \ rn))) " + for ml mr ln rn + by(cases ln, auto) + thus ?thesis using assms + by (auto simp: wadjust_loop_right_move2.simps dropWhile_exp1 takeWhile_exp1) +qed + +lemma wadjust_correctness_helper_2: + "\Suc (Suc rs) = a; wadjust_loop_on_left_moving m rs (c, Bk # list)\ + \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) + < a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Bk # list)))) \ + a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) = + a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Bk # list))))" + apply(subgoal_tac "c \ []") + apply(case_tac c, simp_all) + done + +lemma wadjust_loop_check_empty_false[simp]: "wadjust_loop_check m rs ([], b) = False" apply(simp add: wadjust_loop_check.simps) done -lemma [simp]: "\Suc (Suc rs) = a; wadjust_loop_check m rs (c, Oc # list)\ +lemma wadjust_loop_check_cases: "\Suc (Suc rs) = a; wadjust_loop_check m rs (c, Oc # list)\ \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Oc # list)))) < a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Oc # list)))) \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev (tl c) @ hd c # Oc # list)))) = @@ -4452,7 +3893,7 @@ apply(case_tac "c", simp_all) done -lemma [simp]: +lemma wadjust_loop_erase_cases_or: "\Suc (Suc rs) = a; wadjust_loop_erase m rs (c, Oc # list)\ \ a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Bk # list)))) < a - length (takeWhile (\a. a = Oc) (tl (dropWhile (\a. a = Oc) (rev c @ Oc # list)))) \ @@ -4464,20 +3905,22 @@ apply(simp add: dropWhile_exp1 takeWhile_exp1) done +lemmas wadjust_correctness_helpers = wadjust_correctness_helper_2 wadjust_correctness_helper_1 wadjust_loop_erase_cases_or wadjust_loop_check_cases + declare numeral_2_eq_2[simp del] -lemma [simp]: "wadjust_start m rs (c, Bk # list) +lemma wadjust_start_Oc[simp]: "wadjust_start m rs (c, Bk # list) \ wadjust_start m rs (c, Oc # list)" apply(auto simp: wadjust_start.simps) done -lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list) +lemma wadjust_stop_Bk[simp]: "wadjust_backto_standard_pos m rs (c, Bk # list) \ wadjust_stop m rs (Bk # c, list)" apply(auto simp: wadjust_backto_standard_pos.simps wadjust_stop.simps wadjust_backto_standard_pos_B.simps) done -lemma [simp]: "wadjust_start m rs (c, Oc # list) +lemma wadjust_loop_start_Oc[simp]: "wadjust_start m rs (c, Oc # list) \ wadjust_loop_start m rs (Oc # c, list)" apply(auto simp: wadjust_start.simps wadjust_loop_start.simps) apply(rule_tac x = ln in exI, simp) @@ -4485,7 +3928,7 @@ apply(rule_tac x = 1 in exI, simp) done -lemma [simp]:" wadjust_erase2 m rs (c, Oc # list) +lemma erase2_Bk_if_Oc[simp]:" wadjust_erase2 m rs (c, Oc # list) \ wadjust_erase2 m rs (c, Bk # list)" apply(auto simp: wadjust_erase2.simps) done @@ -4507,13 +3950,14 @@ next show "\ n. \ ?P (?f n) \ ?Q (?f n) \ ?Q (?f (Suc n)) \ (?f (Suc n), ?f n) \ wadjust_le" - apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp) - apply(simp add: step.simps) - apply(case_tac d, case_tac [2] aa, simp_all) + apply(rule_tac allI, rule_tac impI, case_tac "?f n") + apply((case_tac d, case_tac [2] aa); simp add: step.simps) apply(simp_all only: wadjust_inv.simps split: if_splits) apply(simp_all) apply(simp_all add: wadjust_inv.simps wadjust_le_def + wadjust_correctness_helpers Abacus.lex_triple_def Abacus.lex_pair_def lex_square_def split: if_splits) + done next show "?Q (?f 0)" @@ -4529,16 +3973,13 @@ done qed -lemma [intro]: "tm_wf (t_wcode_adjust, 0)" +lemma tm_wf_t_wcode_adjust[intro]: "tm_wf (t_wcode_adjust, 0)" apply(auto simp: t_wcode_adjust_def tm_wf.simps) done -declare tm_comp.simps[simp del] - -lemma [simp]: "args \ [] \ bl_bin () > 0" -apply(case_tac args) -apply(auto simp: tape_of_nl_cons bl_bin.simps split: if_splits) -done +lemma bl_bin_nonzero[simp]: "args \ [] \ bl_bin () > 0" + by(cases args) + (auto simp: tape_of_nl_cons bl_bin.simps) lemma wcode_lemma_pre': "args \ [] \ @@ -4625,7 +4066,7 @@ \ stp ln rn. steps0 (Suc 0, [], ) (t_wcode) stp = (0, [Bk], <[m ,bl_bin ()]> @ Bk\(rn))" using wcode_lemma_1[of args m] -apply(simp add: t_wcode_def tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) +apply(simp add: t_wcode_def tape_of_list_def tape_of_nat_list.simps tape_of_nat_def) done section {* The universal TM *} @@ -4661,22 +4102,18 @@ "UTM_pre = t_wcode |+| t_utm" lemma tinres_step1: - "\tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); - step (ss, l', r) (t, 0) = (sb, lb, rb)\ - \ tinres la lb \ ra = rb \ sa = sb" -apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell") -apply(auto simp: step.simps fetch.simps nth_of.simps - split: if_splits ) -apply(case_tac [!] "t ! (2 * nat)", - auto simp: tinres_def split: if_splits) -apply(case_tac [1-8] a, auto split: if_splits) -apply(case_tac [!] "t ! (2 * nat)", - auto simp: tinres_def split: if_splits) -apply(case_tac [1-4] a, auto split: if_splits) -apply(case_tac [!] "t ! Suc (2 * nat)", - auto simp: if_splits) -apply(case_tac [!] aa, auto split: if_splits) -done + assumes "tinres l l'" "step (ss, l, r) (t, 0) = (sa, la, ra)" + "step (ss, l', r) (t, 0) = (sb, lb, rb)" + shows "tinres la lb \ ra = rb \ sa = sb" +proof(cases "r") + case Nil + then show ?thesis using assms + by (cases "(fetch t ss Bk)";cases "fst (fetch t ss Bk)";auto simp:step.simps split:if_splits) +next + case (Cons a list) + then show ?thesis using assms + by (cases "(fetch t ss a)";cases "fst (fetch t ss a)";auto simp:step.simps split:if_splits) +qed lemma tinres_steps1: "\tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra); @@ -4694,17 +4131,12 @@ "step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)" "steps (ss, l', r) (t, 0) stp = (aa, ba, ca)" have "tinres b ba \ c = ca \ a = aa" - apply(rule_tac ind, simp_all add: h) - done + using ind h by metis thus "tinres la lb \ ra = rb \ sa = sb" - apply(rule_tac l = b and l' = ba and r = c and ss = a - and t = t in tinres_step1) - using h - apply(simp, simp, simp) - done + using tinres_step1 h by metis qed -lemma [simp]: +lemma tinres_some_exp[simp]: "tinres (Bk \ m @ [Bk, Bk]) la \ \m. la = Bk \ m" apply(auto simp: tinres_def) apply(case_tac n, simp add: exp_ind) @@ -4780,16 +4212,11 @@ done qed -lemma [intro]: "tm_wf (t_wcode, 0)" -apply(simp add: t_wcode_def) -apply(rule_tac tm_wf_comp) -apply(rule_tac tm_wf_comp, auto) -done - -lemma [intro]: "tm_wf (t_utm, 0)" -apply(simp only: t_utm_def F_tprog_def) -apply(rule_tac wf_tm_from_abacus, auto) -done +lemma tm_wf_t_wcode[intro]: "tm_wf (t_wcode, 0)" + apply(simp add: t_wcode_def) + apply(rule_tac tm_wf_comp) + apply(rule_tac tm_wf_comp, auto) + done lemma UTM_halt_lemma_pre: assumes wf_tm: "tm_wf (tp, 0)" @@ -4825,7 +4252,7 @@ Oc # Oc \ code tp @ Bk # Oc # Oc \ bl_bin () @ Bk \ rn) t_utm n" using t_utm_halt_eq[of tp i "args" stp m rs k rn] assms apply(auto simp: bin_wc_eq) - apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv) + apply(rule_tac x = stpa in exI, simp add: tape_of_list_def tape_of_nat_def) done qed qed @@ -4860,7 +4287,7 @@ apply(simp add: NSTD.simps trpl_code.simps) done -lemma [simp]: "\m. b \ Bk\(m) \ 0 < bl2wc b" +lemma nonzero_bl2wc[simp]: "\m. b \ Bk\(m) \ 0 < bl2wc b" apply(rule classical, simp) apply(induct b, erule_tac x = 0 in allE, simp) apply(simp add: bl2wc.simps, case_tac a, simp_all @@ -4873,7 +4300,7 @@ apply(simp add: NSTD.simps trpl_code.simps) done -lemma [elim]: "Suc (2 * x) = 2 * y \ RR" +lemma even_not_odd[elim]: "Suc (2 * x) = 2 * y \ RR" apply(induct x arbitrary: y, simp, simp) apply(case_tac y, simp, simp) done @@ -5200,7 +4627,7 @@ thus "False" using h apply(erule_tac x = n in allE) - apply(simp add: tape_of_nl_abv bin_wc_eq tape_of_nat_abv) + apply(simp add: tape_of_list_def bin_wc_eq tape_of_nat_def) done qed qed @@ -5258,7 +4685,7 @@ (Suc 0, [Bk], Oc \ Suc (code p) @ Bk # Oc \ Suc (bl_bin ()) @ Bk \ rn) t_utm n" using t_utm_halt_eq[of p i "args" stp m rs k rn] assms k apply(auto simp: bin_wc_eq, auto) - apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv) + apply(rule_tac x = stpa in exI, simp add: tape_of_list_def tape_of_nat_def) done qed next @@ -5286,7 +4713,7 @@ shows "{(\tp. tp = ([], ))} UTM {(\tp. (\ m k. tp = (Bk\m, @ Bk\k)))}" using UTM_halt_lemma[OF assms(1) _ assms(2), where i="0"] using assms(3) -apply(simp add: tape_of_nat_abv) +apply(simp add: tape_of_nat_def) done @@ -5318,7 +4745,7 @@ shows "{(\tp. tp = ([], ))} UTM \" using UTM_unhalt_lemma[OF assms(1), where i="0"] using assms(2-3) -apply(simp add: tape_of_nat_abv) +apply(simp add: tape_of_nat_def) done -end \ No newline at end of file +end \ No newline at end of file diff -r d5a0e25c4742 -r a9003e6d0463 thys/Uncomputable.thy --- a/thys/Uncomputable.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Uncomputable.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,7 +2,7 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Undeciablity of the Halting Problem *} +chapter {* Undeciablity of the Halting Problem *} theory Uncomputable imports Turing_Hoare @@ -19,6 +19,8 @@ and "8 = Suc 7" and "9 = Suc 8" and "10 = Suc 9" + and "11 = Suc 10" + and "12 = Suc 11" by simp_all text {* The Copying TM, which duplicates its input. *} @@ -163,7 +165,7 @@ apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits) apply(subgoal_tac "r = [Oc]") apply(auto) - by (metis cell.exhaust list.exhaust tl.simps(2)) + by (metis cell.exhaust list.exhaust list.sel(3)) then show "(steps0 (1, [], Oc \ x) tcopy_begin (Suc n), steps0 (1, [], Oc \ x) tcopy_begin n) \ measure_begin" using eq by (simp only: step_red) @@ -596,7 +598,8 @@ qed lemma loop_correct: - shows "0 < n \ {inv_loop1 n} tcopy_loop {inv_loop0 n}" + assumes "0 < n" + shows "{inv_loop1 n} tcopy_loop {inv_loop0 n}" using assms proof(rule_tac Hoare_haltI) fix l r @@ -918,7 +921,7 @@ qed abbreviation (input) - "pre_tcopy n \ \tp. tp = ([]::cell list, <(n::nat)>)" + "pre_tcopy n \ \tp. tp = ([]::cell list, Oc \ (Suc n))" abbreviation (input) "post_tcopy n \ \tp. tp= ([Bk], <(n, n::nat)>)" @@ -928,11 +931,12 @@ have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}" by (rule tcopy_correct1) (simp) moreover - have "pre_tcopy n = inv_begin1 (Suc n)" - by (auto simp add: tape_of_nl_abv tape_of_nat_abv) + have "pre_tcopy n = inv_begin1 (Suc n)" + by (auto) moreover - have "inv_end0 (Suc n) = post_tcopy n" - by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nat_pair) + have "inv_end0 (Suc n) = post_tcopy n" + unfolding fun_eq_iff + by (auto simp add: inv_end0.simps tape_of_nat_def tape_of_prod_def) ultimately show "{pre_tcopy n} tcopy {post_tcopy n}" by simp @@ -961,14 +965,14 @@ "(steps0 (1, Bk \ m, [Oc]) dither stp = (1, Bk \ m, [Oc])) \ (steps0 (1, Bk \ m, [Oc]) dither stp = (2, Oc # Bk \ m, []))" apply(induct stp) - apply(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv) + apply(auto simp: steps.simps step.simps dither_def numeral) done lemma dither_loops: shows "{dither_unhalt_inv} dither \" apply(rule Hoare_unhaltI) using dither_loops_aux -apply(auto simp add: numeral tape_of_nat_abv) +apply(auto simp add: numeral tape_of_nat_def) by (metis Suc_neq_Zero is_final_eq) lemma dither_halts_aux: @@ -980,8 +984,8 @@ shows "{dither_halt_inv} dither {dither_halt_inv}" apply(rule Hoare_haltI) using dither_halts_aux -apply(auto simp add: tape_of_nat_abv) -by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) +apply(auto simp add: tape_of_nat_def) +by (metis (lifting, mono_tags) holds_for.simps is_final_eq) section {* The diagnal argument below shows the undecidability of Halting problem *} @@ -1009,17 +1013,17 @@ *} locale uncomputable = - -- {* The coding function of TM, interestingly, the detailed definition of this - funciton @{text "code"} does not affect the final result. *} + (* The coding function of TM, interestingly, the detailed definition of this + funciton @{text "code"} does not affect the final result. *) fixes code :: "instr list \ nat" - -- {* + (* The TM @{text "H"} is the one which is assummed being able to solve the Halting problem. - *} + *) and H :: "instr list" assumes h_wf[intro]: "tm_wf0 H" - -- {* + (* The following two assumptions specifies that @{text "H"} does solve the Halting problem. - *} + *) and h_case: "\ M ns. halts M ns \ {(\tp. tp = ([Bk], <(code M, ns)>))} H {(\tp. \k. tp = (Bk \ k, <0::nat>))}" and nh_case: @@ -1060,9 +1064,9 @@ shows "False" proof - (* invariants *) - def P1 \ "\tp. tp = ([]::cell list, )" - def P2 \ "\tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" - def P3 \ "\tp. \k. tp = (Bk \ k, <1::nat>)" + define P1 where "P1 \ \tp. tp = ([]::cell list, )" + define P2 where "P2 \ \tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" + define P3 where "P3 \ \tp. \k. tp = (Bk \ k, <1::nat>)" (* {P1} tcopy {P2} {P2} H {P3} @@ -1078,14 +1082,14 @@ have first: "{P1} (tcopy |+| H) {P3}" proof (cases rule: Hoare_plus_halt) case A_halt (* of tcopy *) - show "{P1} tcopy {P2}" unfolding P1_def P2_def + show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def by (rule tcopy_correct) next case B_halt (* of H *) show "{P2} H {P3}" unfolding P2_def P3_def using H_halt_inv[OF assms] - by (simp add: tape_of_nat_pair tape_of_nl_abv) + by (simp add: tape_of_prod_def tape_of_list_def) qed (simp) (* {P3} dither {P3} *) @@ -1104,7 +1108,7 @@ apply(auto) apply(drule_tac x = n in spec) apply(case_tac "steps0 (Suc 0, [], ) tcontra n") - apply(auto simp add: tape_of_nl_abv) + apply(auto simp add: tape_of_list_def) by (metis append_Nil2 replicate_0) qed @@ -1114,9 +1118,9 @@ shows "False" proof - (* invariants *) - def P1 \ "\tp. tp = ([]::cell list, )" - def P2 \ "\tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" - def Q3 \ "\tp. \k. tp = (Bk \ k, <0::nat>)" + define P1 where "P1 \ \tp. tp = ([]::cell list, )" + define P2 where "P2 \ \tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" + define Q3 where "Q3 \ \tp. \k. tp = (Bk \ k, <0::nat>)" (* {P1} tcopy {P2} {P2} H {Q3} @@ -1132,13 +1136,13 @@ have first: "{P1} (tcopy |+| H) {Q3}" proof (cases rule: Hoare_plus_halt) case A_halt (* of tcopy *) - show "{P1} tcopy {P2}" unfolding P1_def P2_def + show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def by (rule tcopy_correct) next case B_halt (* of H *) then show "{P2} H {Q3}" unfolding P2_def Q3_def using H_unhalt_inv[OF assms] - by(simp add: tape_of_nat_pair tape_of_nl_abv) + by(simp add: tape_of_prod_def tape_of_list_def) qed (simp) (* {P3} dither loops *) @@ -1154,7 +1158,7 @@ unfolding P1_def unfolding halts_def unfolding Hoare_halt_def Hoare_unhalt_def - by (auto simp add: tape_of_nl_abv) + by (auto simp add: tape_of_list_def) qed diff -r d5a0e25c4742 -r a9003e6d0463 thys2/Turing2.thy --- a/thys2/Turing2.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys2/Turing2.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,7 +2,7 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Turing Machines *} +chapter {* Turing Machines *} theory Turing2 imports Main