# HG changeset patch # User Christian Urban # Date 1367495373 -3600 # Node ID aea02b5a58d2f7e24dd1d95450f1965669b7f1b6 # Parent 89ed51d72e4a77fa2941eaee19dba21ffa0a2bbc repaired old files diff -r 89ed51d72e4a -r aea02b5a58d2 thys/Rec_Def.thy --- a/thys/Rec_Def.thy Thu May 02 12:49:15 2013 +0100 +++ b/thys/Rec_Def.thy Thu May 02 12:49:33 2013 +0100 @@ -9,10 +9,14 @@ | Pr nat recf recf | Mn nat recf +definition pred_of_nl :: "nat list \ nat list" + where + "pred_of_nl xs = butlast xs @ [last xs - 1]" + function rec_exec :: "recf \ nat list \ nat" where "rec_exec z xs = 0" | - "rec_exec s xs = Suc (xs ! 0)" | + "rec_exec s xs = (Suc (xs ! 0))" | "rec_exec (id m n) xs = (xs ! n)" | "rec_exec (Cn n f gs) xs = rec_exec f (map (\ a. rec_exec a xs) gs)" | @@ -27,33 +31,20 @@ apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation') done -inductive - terminates :: "recf \ nat list \ bool" -where - termi_z: "terminates z [n]" -| termi_s: "terminates s [n]" -| termi_id: "\n < m; length xs = m\ \ terminates (id m n) xs" -| termi_cn: "\terminates f (map (\g. rec_exec g xs) gs); - \g \ set gs. terminates g xs; length xs = n\ \ terminates (Cn n f gs) xs" -| termi_pr: "\\ y < x. terminates g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]); - terminates f xs; +inductive terminate :: "recf \ nat list \ bool" + where + termi_z: "terminate z [n]" +| termi_s: "terminate s [n]" +| termi_id: "\n < m; length xs = m\ \ terminate (id m n) xs" +| termi_cn: "\terminate f (map (\g. rec_exec g xs) gs); + \g \ set gs. terminate g xs; length xs = n\ \ terminate (Cn n f gs) xs" +| termi_pr: "\\ y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]); + terminate f xs; length xs = n\ - \ terminates (Pr n f g) (xs @ [x])" -| termi_mn: "\length xs = n; terminates f (xs @ [r]); + \ terminate (Pr n f g) (xs @ [x])" +| termi_mn: "\length xs = n; terminate f (xs @ [r]); rec_exec f (xs @ [r]) = 0; - \ i < r. terminates f (xs @ [i]) \ rec_exec f (xs @ [i]) > 0\ \ terminates (Mn n f) xs" + \ i < r. terminate f (xs @ [i]) \ rec_exec f (xs @ [i]) > 0\ \ terminate (Mn n f) xs" -inductive_cases terminates_pr_reverse: "terminates (Pr n f g) xs" - -inductive_cases terminates_z_reverse[elim!]: "terminates z xs" - -inductive_cases terminates_s_reverse[elim!]: "terminates s xs" - -inductive_cases terminates_id_reverse[elim!]: "terminates (id m n) xs" - -inductive_cases terminates_cn_reverse[elim!]: "terminates (Cn n f gs) xs" - -inductive_cases terminates_mn_reverse[elim!]:"terminates (Mn n f) xs" - end \ No newline at end of file diff -r 89ed51d72e4a -r aea02b5a58d2 thys/Recursive.thy --- a/thys/Recursive.thy Thu May 02 12:49:15 2013 +0100 +++ b/thys/Recursive.thy Thu May 02 12:49:33 2013 +0100 @@ -6,7 +6,6 @@ where "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]" -(* moves register m to register n *) fun mv_box :: "nat \ nat \ abc_prog" where "mv_box m n = [Dec m 3, Inc n, Goto 0]" @@ -19,7 +18,7 @@ text {* The compilation of @{text "s"}-operator. *} definition rec_ci_s :: "abc_inst list" where - "rec_ci_s \ addition 0 1 2 [+] [Inc 1]" + "rec_ci_s \ (addition 0 1 2 [+] [Inc 1])" text {* The compilation of @{text "id i j"}-operator *} @@ -37,7 +36,8 @@ "empty_boxes 0 = []" | "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]" -fun cn_merge_gs :: "(abc_inst list \ nat \ nat) list \ nat \ abc_inst list" +fun cn_merge_gs :: + "(abc_inst list \ nat \ nat) list \ nat \ abc_inst list" where "cn_merge_gs [] p = []" | "cn_merge_gs (g # gs) p = @@ -91,7 +91,20 @@ declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] abc_step_l.simps[simp del] -fun addition_inv :: "nat \ nat list \ nat \ nat \ nat \ nat list \ bool" +inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs" + +inductive_cases terminate_z_reverse[elim!]: "terminate z xs" + +inductive_cases terminate_s_reverse[elim!]: "terminate s xs" + +inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs" + +inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs" + +inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs" + +fun addition_inv :: "nat \ nat list \ nat \ nat \ nat \ + nat list \ bool" where "addition_inv (as, lm') m n p lm = (let sn = lm ! n in @@ -140,18 +153,21 @@ else if as = 4 then 0 else 0)" -fun addition_measure :: "((nat \ nat list) \ nat \ nat) \ (nat \ nat \ nat)" +fun addition_measure :: "((nat \ nat list) \ nat \ nat) \ + (nat \ nat \ nat)" where "addition_measure ((as, lm), m, p) = (addition_stage1 (as, lm) m p, addition_stage2 (as, lm) m p, addition_stage3 (as, lm) m p)" -definition addition_LE :: "(((nat \ nat list) \ nat \ nat) \ ((nat \ nat list) \ nat \ nat)) set" +definition addition_LE :: "(((nat \ nat list) \ nat \ nat) \ + ((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) +by(auto simp: wf_inv_image addition_LE_def lex_triple_def + lex_pair_def) declare addition_inv.simps[simp del] @@ -313,23 +329,17 @@ qed lemma compile_s_correct': - "{\nl. nl = n # 0 \ 2 @ anything} - addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] - {\nl. nl = n # Suc n # 0 # anything}" + "{\nl. nl = n # 0 \ 2 @ anything} addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] {\nl. nl = n # Suc n # 0 # anything}" proof(rule_tac abc_Hoare_plus_halt) - show "{\nl. nl = n # 0 \ 2 @ anything} - addition 0 (Suc 0) 2 - {\nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)}" + show "{\nl. nl = n # 0 \ 2 @ anything} addition 0 (Suc 0) 2 {\ nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)}" by(rule_tac addition_correct, auto simp: numeral_2_eq_2) next - show "{\nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)} - [Inc (Suc 0)] - {\nl. nl = n # Suc n # 0 # anything}" + show "{\nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)} [Inc (Suc 0)] {\nl. nl = n # Suc n # 0 # anything}" by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps) qed -declare rec_eval.simps[simp del] +declare rec_exec.simps[simp del] lemma abc_comp_commute: "(A [+] B) [+] C = A [+] (B [+] C)" apply(auto simp: abc_comp.simps abc_shift.simps) @@ -339,24 +349,24 @@ lemma compile_z_correct: - "\rec_ci z = (ap, arity, fp); rec_eval z [n] = r\ \ + "\rec_ci z = (ap, arity, fp); rec_exec z [n] = r\ \ {\nl. nl = n # 0 \ (fp - arity) @ anything} ap {\nl. nl = n # r # 0 \ (fp - Suc arity) @ anything}" apply(rule_tac abc_Hoare_haltI) apply(rule_tac x = 1 in exI) apply(auto simp: abc_steps_l.simps rec_ci.simps rec_ci_z_def - numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_eval.simps) + numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_exec.simps) done lemma compile_s_correct: - "\rec_ci s = (ap, arity, fp); rec_eval s [n] = r\ \ + "\rec_ci s = (ap, arity, fp); rec_exec s [n] = r\ \ {\nl. nl = n # 0 \ (fp - arity) @ anything} ap {\nl. nl = n # r # 0 \ (fp - Suc arity) @ anything}" -apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_eval.simps) +apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_exec.simps) done lemma compile_id_correct': assumes "n < length args" shows "{\nl. nl = args @ 0 \ 2 @ anything} addition n (length args) (Suc (length args)) - {\nl. nl = args @ rec_eval (recf.id (length args) n) args # 0 # anything}" + {\nl. nl = args @ rec_exec (recf.id (length args) n) args # 0 # anything}" proof - have "{\nl. nl = args @ 0 \ 2 @ anything} addition n (length args) (Suc (length args)) {\nl. addition_inv (7, nl) n (length args) (Suc (length args)) (args @ 0 \ 2 @ anything)}" @@ -364,12 +374,12 @@ by(rule_tac addition_correct, auto simp: numeral_2_eq_2 nth_append) thus "?thesis" using assms - by(simp add: addition_inv.simps rec_eval.simps + by(simp add: addition_inv.simps rec_exec.simps nth_append numeral_2_eq_2 list_update_append) qed lemma compile_id_correct: - "\n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_eval (recf.id m n) xs = r\ + "\n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_exec (recf.id m n) xs = r\ \ {\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ r # 0 \ (fp - Suc arity) @ anything}" apply(auto simp: rec_ci.simps rec_ci_id.simps compile_id_correct') done @@ -391,8 +401,8 @@ done lemma param_pattern: - "\terminates f xs; rec_ci f = (p, arity, fp)\ \ length xs = arity" -apply(induct arbitrary: p arity fp rule: terminates.induct) + "\terminate f xs; rec_ci f = (p, arity, fp)\ \ length xs = arity" +apply(induct arbitrary: p arity fp rule: terminate.induct) apply(auto simp: rec_ci.simps) apply(case_tac "rec_ci f", simp) apply(case_tac "rec_ci f", case_tac "rec_ci g", simp) @@ -590,11 +600,11 @@ lemma [simp]: "\length xs < gf; gf \ ft; n < length gs\ - \ (rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) - [ft + n - length xs := rec_eval (gs ! n) xs, 0 := 0] = - 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything" -using list_update_append[of "rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_eval i xs) (take n gs)" - "0 \ (length gs - n) @ 0 # 0 \ length xs @ anything" "ft + n - length xs" "rec_eval (gs ! n) xs"] + \ (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] = + 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything" +using list_update_append[of "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"] apply(auto) apply(case_tac "length gs - n", simp, simp add: list_update.simps replicate_Suc_iff_anywhere Suc_diff_Suc del: replicate_Suc) apply(simp add: list_update.simps) @@ -602,14 +612,14 @@ lemma compile_cn_gs_correct': assumes - g_cond: "\g\set (take n gs). terminates g xs \ - (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_eval g xs # 0 \ (xb - Suc xa) @ xc}))" + g_cond: "\g\set (take n gs). terminate g xs \ + (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc}))" and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" shows "{\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft {\nl. nl = xs @ 0 \ (ft - length xs) @ - map (\i. rec_eval i xs) (take n gs) @ 0\(length gs - n) @ 0 \ Suc (length xs) @ anything}" + map (\i. rec_exec i xs) (take n gs) @ 0\(length gs - n) @ 0 \ Suc (length xs) @ anything}" using g_cond proof(induct n) case 0 @@ -624,17 +634,17 @@ next case (Suc n) have ind': "\g\set (take n gs). - terminates g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ - (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_eval g xs # 0 \ (xb - Suc xa) @ xc})) \ + terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ + (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc})) \ {\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything}" + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything}" by fact have g_newcond: "\g\set (take (Suc n) gs). - terminates g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_eval g xs # 0 \ (xb - Suc xa) @ xc}))" + terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc}))" by fact from g_newcond have ind: "{\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything}" + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything}" apply(rule_tac ind', rule_tac ballI, erule_tac x = g in ballE, simp_all add: take_Suc) by(case_tac "n < length gs", simp add:take_Suc_conv_app_nth, simp) show "?case" @@ -650,17 +660,17 @@ moreover have "{\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft [+] (gp [+] mv_box ga (ft + n)) - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ - rec_eval (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ + rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" proof(rule_tac abc_Hoare_plus_halt) show "{\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything}" + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything}" using ind by simp next have x: "gs!n \ set (take (Suc n) gs)" using h by(simp add: take_Suc_conv_app_nth) - have b: "terminates (gs!n) xs" + have b: "terminate (gs!n) xs" using a g_newcond h x by(erule_tac x = "gs!n" in ballE, simp_all) hence c: "length xs = ga" @@ -672,18 +682,18 @@ 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) show "{\nl. nl = xs @ 0 \ (ft - length xs) @ - map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything} gp [+] mv_box ga (ft + n) - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) - (take n gs) @ rec_eval (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" + map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything} gp [+] mv_box ga (ft + n) + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) + (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" proof(rule_tac abc_Hoare_plus_halt) - show "{\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything} gp - {\nl. nl = xs @ (rec_eval (gs!n) xs) # 0 \ (ft - Suc (length xs)) @ map (\i. rec_eval i xs) + show "{\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything} gp + {\nl. nl = xs @ (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}" proof - have - "({\nl. nl = xs @ 0 \ (gf - ga) @ 0\(ft - gf)@map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything} - gp {\nl. nl = xs @ (rec_eval (gs!n) xs) # 0 \ (gf - Suc ga) @ - 0\(ft - gf)@map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything})" + "({\nl. nl = xs @ 0 \ (gf - ga) @ 0\(ft - gf)@map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything} + gp {\nl. nl = xs @ (rec_exec (gs!n) xs) # 0 \ (gf - Suc ga) @ + 0\(ft - gf)@map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything})" using a g_newcond h x apply(erule_tac x = "gs!n" in ballE) apply(simp, simp) @@ -694,33 +704,33 @@ qed next show - "{\nl. nl = xs @ rec_eval (gs ! n) xs # - 0 \ (ft - Suc (length xs)) @ map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything} + "{\nl. nl = xs @ 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} mv_box ga (ft + n) - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ - rec_eval (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ + rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" proof - - have "{\nl. nl = xs @ rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ - map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything} - mv_box ga (ft + n) {\nl. nl = (xs @ rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ - map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) - [ft + n := (xs @ rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_eval i xs) (take n gs) @ + have "{\nl. nl = xs @ 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} + mv_box ga (ft + n) {\nl. nl = (xs @ 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 := (xs @ 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) ! ga + - (xs @ rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ - map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) ! + (xs @ 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), ga := 0]}" using a c d e h apply(rule_tac mv_box_correct) apply(simp, arith, arith) done - moreover have "(xs @ rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ - map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) - [ft + n := (xs @ rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_eval i xs) (take n gs) @ + moreover have "(xs @ 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 := (xs @ 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) ! ga + - (xs @ rec_eval (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ - map (\i. rec_eval i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) ! + (xs @ 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), ga := 0]= - xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything" + xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything" using a c d e h by(simp add: list_update_append nth_append length_replicate split: if_splits del: list_update.simps(2), auto) ultimately show "?thesis" @@ -732,7 +742,7 @@ "{\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft [+] (case rec_ci (gs ! n) of (gprog, gpara, gn) \ gprog [+] mv_box gpara (ft + min (length gs) n)) - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything}" by simp qed next @@ -740,7 +750,7 @@ have h: "\ n < length gs" by fact hence ind': "{\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci gs) ft - {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_eval i xs) gs @ 0 \ Suc (length xs) @ anything}" + {\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) gs @ 0 \ Suc (length xs) @ anything}" using ind by simp thus "?thesis" @@ -751,14 +761,14 @@ lemma compile_cn_gs_correct: assumes - g_cond: "\g\set gs. terminates g xs \ - (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_eval g xs # 0 \ (xb - Suc xa) @ xc}))" + g_cond: "\g\set gs. terminate g xs \ + (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc}))" and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" shows "{\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything} cn_merge_gs (map rec_ci gs) ft {\nl. nl = xs @ 0 \ (ft - length xs) @ - map (\i. rec_eval i xs) gs @ 0 \ Suc (length xs) @ anything}" + map (\i. rec_exec i xs) gs @ 0 \ Suc (length xs) @ anything}" using assms using compile_cn_gs_correct'[of "length gs" gs xs ft ffp anything ] apply(auto) @@ -957,14 +967,14 @@ lemma save_paras: "{\nl. nl = xs @ 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @ - map (\i. rec_eval i xs) gs @ 0 \ Suc (length xs) @ anything} + map (\i. rec_exec i xs) gs @ 0 \ Suc (length xs) @ anything} mv_boxes 0 (Suc (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) (length xs) - {\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\i. rec_eval i xs) gs @ 0 # xs @ anything}" + {\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\i. rec_exec i xs) gs @ 0 # xs @ anything}" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" - have "{\nl. nl = [] @ xs @ (0\(?ft - length xs) @ map (\i. rec_eval i xs) gs @ [0]) @ + have "{\nl. nl = [] @ xs @ (0\(?ft - length xs) @ map (\i. rec_exec i xs) gs @ [0]) @ 0 \ (length xs) @ anything} mv_boxes 0 (Suc ?ft + length gs) (length xs) - {\nl. nl = [] @ 0 \ (length xs) @ (0\(?ft - length xs) @ map (\i. rec_eval i xs) gs @ [0]) @ xs @ anything}" + {\nl. nl = [] @ 0 \ (length xs) @ (0\(?ft - length xs) @ map (\i. rec_exec i xs) gs @ [0]) @ xs @ anything}" by(rule_tac mv_boxes_correct, auto) thus "?thesis" by(simp add: replicate_merge_anywhere) @@ -978,15 +988,15 @@ lemma restore_new_paras: "ffp \ length gs - \ {\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\i. rec_eval i xs) gs @ 0 # xs @ anything} + \ {\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\i. rec_exec i xs) gs @ 0 # xs @ anything} mv_boxes (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) 0 (length gs) - {\nl. nl = map (\i. rec_eval i xs) gs @ 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ 0 # xs @ anything}" + {\nl. nl = map (\i. rec_exec i xs) gs @ 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ 0 # xs @ anything}" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" assume j: "ffp \ length gs" - hence "{\ nl. nl = [] @ 0\length gs @ 0\(?ft - length gs) @ map (\i. rec_eval i xs) gs @ ((0 # xs) @ anything)} + hence "{\ nl. nl = [] @ 0\length gs @ 0\(?ft - length gs) @ map (\i. rec_exec i xs) gs @ ((0 # xs) @ anything)} mv_boxes ?ft 0 (length gs) - {\ nl. nl = [] @ map (\i. rec_eval i xs) gs @ 0\(?ft - length gs) @ 0\length gs @ ((0 # xs) @ anything)}" + {\ nl. nl = [] @ map (\i. rec_exec i xs) gs @ 0\(?ft - length gs) @ 0\length gs @ ((0 # xs) @ anything)}" by(rule_tac mv_boxes_correct2, auto) moreover have "?ft \ length gs" using j @@ -1007,29 +1017,29 @@ "\far = length gs; ffp \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))); far < ffp\ -\ {\nl. nl = map (\i. rec_eval i xs) gs @ - rec_eval (Cn (length xs) f gs) xs # 0 \ max (Suc (length xs)) +\ {\nl. nl = map (\i. rec_exec i xs) gs @ + rec_exec (Cn (length xs) f gs) xs # 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ xs @ anything} mv_box far (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) - {\nl. nl = map (\i. rec_eval i xs) gs @ + {\nl. nl = map (\i. rec_exec i xs) gs @ 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @ - rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything}" + rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything}" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" thm mv_box_correct - let ?lm= " map (\i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0 \ ?ft @ xs @ anything" + let ?lm= " map (\i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ ?ft @ xs @ anything" assume h: "far = length gs" "ffp \ ?ft" "far < ffp" hence "{\ nl. nl = ?lm} mv_box far ?ft {\ nl. nl = ?lm[?ft := ?lm!far + ?lm!?ft, far := 0]}" apply(rule_tac mv_box_correct) by(case_tac "rec_ci a", auto) moreover have "?lm[?ft := ?lm!far + ?lm!?ft, far := 0] - = map (\i. rec_eval i xs) gs @ + = map (\i. rec_exec i xs) gs @ 0 \ (?ft - length gs) @ - rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" + rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" using h apply(simp add: nth_append) - using list_update_length[of "map (\i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs # - 0 \ (?ft - Suc (length gs))" 0 "0 \ length gs @ xs @ anything" "rec_eval (Cn (length xs) f gs) xs"] + using list_update_length[of "map (\i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # + 0 \ (?ft - Suc (length gs))" 0 "0 \ length gs @ xs @ anything" "rec_exec (Cn (length xs) f gs) xs"] apply(simp add: replicate_merge_anywhere replicate_Suc_iff_anywhere del: replicate_Suc) by(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere del: replicate_Suc) ultimately show "?thesis" @@ -1108,21 +1118,21 @@ lemma clean_paras: "ffp \ length gs \ - {\nl. nl = map (\i. rec_eval i xs) gs @ + {\nl. nl = map (\i. rec_exec i xs) gs @ 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @ - rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything} + rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything} empty_boxes (length gs) {\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ - rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything}" + rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything}" proof- let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" assume h: "length gs \ ffp" - let ?lm = "map (\i. rec_eval i xs) gs @ 0 \ (?ft - length gs) @ - rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" + let ?lm = "map (\i. rec_exec i xs) gs @ 0 \ (?ft - length gs) @ + rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" have "{\ nl. nl = ?lm} empty_boxes (length gs) {\ nl. nl = 0\length gs @ drop (length gs) ?lm}" by(rule_tac empty_boxes_correct, simp) moreover have "0\length gs @ drop (length gs) ?lm - = 0 \ ?ft @ rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" + = 0 \ ?ft @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" using h by(simp add: replicate_merge_anywhere) ultimately show "?thesis" @@ -1132,20 +1142,20 @@ lemma restore_rs: "{\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ - rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything} + rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything} mv_box (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs) {\nl. nl = 0 \ length xs @ - rec_eval (Cn (length xs) f gs) xs # + rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - (length xs)) @ 0 \ length gs @ xs @ anything}" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" - let ?lm = "0\(length xs) @ 0\(?ft - (length xs)) @ rec_eval (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" + let ?lm = "0\(length xs) @ 0\(?ft - (length xs)) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" thm mv_box_correct have "{\ nl. nl = ?lm} mv_box ?ft (length xs) {\ nl. nl = ?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0]}" by(rule_tac mv_box_correct, simp, simp) moreover have "?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0] - = 0 \ length xs @ rec_eval (Cn (length xs) f gs) xs # 0 \ (?ft - (length xs)) @ 0 \ length gs @ xs @ anything" + = 0 \ length xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft - (length xs)) @ 0 \ length gs @ xs @ anything" apply(auto simp: list_update_append nth_append) apply(case_tac ?ft, simp_all add: Suc_diff_le list_update.simps) apply(simp add: exp_suc replicate_Suc[THEN sym] del: replicate_Suc) @@ -1156,17 +1166,17 @@ lemma restore_orgin_paras: "{\nl. nl = 0 \ length xs @ - rec_eval (Cn (length xs) f gs) xs # + rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @ 0 \ length gs @ xs @ anything} mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs) - {\nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # 0 \ + {\nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" thm mv_boxes_correct2 - have "{\ nl. nl = [] @ 0\(length xs) @ (rec_eval (Cn (length xs) f gs) xs # 0 \ (?ft - length xs) @ 0 \ length gs) @ xs @ anything} + have "{\ nl. nl = [] @ 0\(length xs) @ (rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft - length xs) @ 0 \ length gs) @ xs @ anything} mv_boxes (Suc ?ft + length gs) 0 (length xs) - {\ nl. nl = [] @ xs @ (rec_eval (Cn (length xs) f gs) xs # 0 \ (?ft - length xs) @ 0 \ length gs) @ 0\length xs @ anything}" + {\ nl. nl = [] @ xs @ (rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft - length xs) @ 0 \ length gs) @ 0\length xs @ anything}" by(rule_tac mv_boxes_correct2, auto) thus "?thesis" by(simp add: replicate_merge_anywhere) @@ -1174,14 +1184,14 @@ lemma compile_cn_correct': assumes f_ind: - "\ anything r. rec_eval f (map (\g. rec_eval g xs) gs) = rec_eval (Cn (length xs) f gs) xs \ - {\nl. nl = map (\g. rec_eval g xs) gs @ 0 \ (ffp - far) @ anything} fap - {\nl. nl = map (\g. rec_eval g xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0 \ (ffp - Suc far) @ anything}" + "\ anything r. rec_exec f (map (\g. rec_exec g xs) gs) = rec_exec (Cn (length xs) f gs) xs \ + {\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (ffp - far) @ anything} fap + {\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (ffp - Suc far) @ anything}" and compile: "rec_ci f = (fap, far, ffp)" - and term_f: "terminates f (map (\g. rec_eval g xs) gs)" - and g_cond: "\g\set gs. terminates g xs \ + and term_f: "terminate f (map (\g. rec_exec g xs) gs)" + and g_cond: "\g\set gs. terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ - (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_eval g xs # 0 \ (xb - Suc xa) @ xc}))" + (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc}))" shows "{\nl. nl = xs @ 0 # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything} cn_merge_gs (map rec_ci gs) (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) [+] @@ -1191,7 +1201,7 @@ (empty_boxes (length gs) [+] (mv_box (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs) [+] mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs))))))) - {\nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # + {\nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" @@ -1204,8 +1214,8 @@ let ?G = "mv_box ?ft (length xs)" let ?H = "mv_boxes (Suc (?ft + length gs)) 0 (length xs)" let ?P1 = "\nl. nl = xs @ 0 # 0 \ (?ft + length gs) @ anything" - let ?S = "\nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # 0 \ (?ft + length gs) @ anything" - let ?Q1 = "\ nl. nl = xs @ 0\(?ft - length xs) @ map (\ i. rec_eval i xs) gs @ 0\(Suc (length xs)) @ anything" + let ?S = "\nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft + length gs) @ anything" + let ?Q1 = "\ nl. nl = xs @ 0\(?ft - length xs) @ map (\ i. rec_exec i xs) gs @ 0\(Suc (length xs)) @ anything" show "{?P1} (?A [+] (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))))) {?S}" proof(rule_tac abc_Hoare_plus_halt) show "{?P1} ?A {?Q1}" @@ -1213,13 +1223,13 @@ by(rule_tac compile_cn_gs_correct, auto) next let ?Q2 = "\nl. nl = 0 \ ?ft @ - map (\i. rec_eval i xs) gs @ 0 # xs @ anything" + map (\i. rec_exec i xs) gs @ 0 # xs @ anything" show "{?Q1} (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H)))))) {?S}" proof(rule_tac abc_Hoare_plus_halt) show "{?Q1} ?B {?Q2}" by(rule_tac save_paras) next - let ?Q3 = "\ nl. nl = map (\i. rec_eval i xs) gs @ 0\?ft @ 0 # xs @ anything" + let ?Q3 = "\ nl. nl = map (\i. rec_exec i xs) gs @ 0\?ft @ 0 # xs @ anything" show "{?Q2} (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))) {?S}" proof(rule_tac abc_Hoare_plus_halt) have "ffp \ length gs" @@ -1230,7 +1240,7 @@ thus "{?Q2} ?C {?Q3}" by(erule_tac restore_new_paras) next - let ?Q4 = "\ nl. nl = map (\i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0\?ft @ xs @ anything" + let ?Q4 = "\ nl. nl = map (\i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0\?ft @ xs @ anything" have a: "far = length gs" using compile term_f by(drule_tac param_pattern, auto) @@ -1241,23 +1251,23 @@ by(erule_tac footprint_ge) show "{?Q3} (?D [+] (?E [+] (?F [+] (?G [+] ?H)))) {?S}" proof(rule_tac abc_Hoare_plus_halt) - have "{\nl. nl = map (\g. rec_eval g xs) gs @ 0 \ (ffp - far) @ 0\(?ft - ffp + far) @ 0 # xs @ anything} fap - {\nl. nl = map (\g. rec_eval g xs) gs @ rec_eval (Cn (length xs) f gs) xs # + have "{\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (ffp - far) @ 0\(?ft - ffp + far) @ 0 # xs @ anything} fap + {\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (ffp - Suc far) @ 0\(?ft - ffp + far) @ 0 # xs @ anything}" - by(rule_tac f_ind, simp add: rec_eval.simps) + by(rule_tac f_ind, simp add: rec_exec.simps) thus "{?Q3} fap {?Q4}" using a b c by(simp add: replicate_merge_anywhere, case_tac "?ft", simp_all add: exp_suc del: replicate_Suc) next - let ?Q5 = "\nl. nl = map (\i. rec_eval i xs) gs @ - 0\(?ft - length gs) @ rec_eval (Cn (length xs) f gs) xs # 0\(length gs)@ xs @ anything" + let ?Q5 = "\nl. nl = map (\i. rec_exec i xs) gs @ + 0\(?ft - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0\(length gs)@ xs @ anything" show "{?Q4} (?E [+] (?F [+] (?G [+] ?H))) {?S}" proof(rule_tac abc_Hoare_plus_halt) from a b c show "{?Q4} ?E {?Q5}" by(erule_tac save_rs, simp_all) next - let ?Q6 = "\nl. nl = 0\?ft @ rec_eval (Cn (length xs) f gs) xs # 0\(length gs)@ xs @ anything" + let ?Q6 = "\nl. nl = 0\?ft @ rec_exec (Cn (length xs) f gs) xs # 0\(length gs)@ xs @ anything" show "{?Q5} (?F [+] (?G [+] ?H)) {?S}" proof(rule_tac abc_Hoare_plus_halt) have "length gs \ ffp" using a b c @@ -1265,7 +1275,7 @@ thus "{?Q5} ?F {?Q6}" by(erule_tac clean_paras) next - let ?Q7 = "\nl. nl = 0\length xs @ rec_eval (Cn (length xs) f gs) xs # 0\(?ft - (length xs)) @ 0\(length gs)@ xs @ anything" + let ?Q7 = "\nl. nl = 0\length xs @ rec_exec (Cn (length xs) f gs) xs # 0\(?ft - (length xs)) @ 0\(length gs)@ xs @ anything" show "{?Q6} (?G [+] ?H) {?S}" proof(rule_tac abc_Hoare_plus_halt) show "{?Q6} ?G {?Q7}" @@ -1283,24 +1293,24 @@ qed lemma compile_cn_correct: - assumes termi_f: "terminates f (map (\g. rec_eval g xs) gs)" + assumes termi_f: "terminate f (map (\g. rec_exec g xs) gs)" and f_ind: "\ap arity fp anything. rec_ci f = (ap, arity, fp) - \ {\nl. nl = map (\g. rec_eval g xs) gs @ 0 \ (fp - arity) @ anything} ap - {\nl. nl = map (\g. rec_eval g xs) gs @ rec_eval f (map (\g. rec_eval g xs) gs) # 0 \ (fp - Suc arity) @ anything}" + \ {\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (fp - arity) @ anything} ap + {\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec f (map (\g. rec_exec g xs) gs) # 0 \ (fp - Suc arity) @ anything}" and g_cond: - "\g\set gs. terminates g xs \ - (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_eval g xs # 0 \ (xb - Suc xa) @ xc}))" + "\g\set gs. terminate g xs \ + (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. {\nl. nl = xs @ 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc}))" and compile: "rec_ci (Cn n f gs) = (ap, arity, fp)" and len: "length xs = n" - shows "{\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ rec_eval (Cn n f gs) xs # 0 \ (fp - Suc arity) @ anything}" + shows "{\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \ (fp - Suc arity) @ anything}" proof(case_tac "rec_ci f") fix fap far ffp assume h: "rec_ci f = (fap, far, ffp)" - then have f_newind: "\ anything .{\nl. nl = map (\g. rec_eval g xs) gs @ 0 \ (ffp - far) @ anything} fap - {\nl. nl = map (\g. rec_eval g xs) gs @ rec_eval f (map (\g. rec_eval g xs) gs) # 0 \ (ffp - Suc far) @ anything}" + then have f_newind: "\ anything .{\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (ffp - far) @ anything} fap + {\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec f (map (\g. rec_exec g xs) gs) # 0 \ (ffp - Suc far) @ anything}" by(rule_tac f_ind, simp_all) - thus "{\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ rec_eval (Cn n f gs) xs # 0 \ (fp - Suc arity) @ anything}" + thus "{\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \ (fp - Suc arity) @ anything}" using compile len h termi_f g_cond apply(auto simp: rec_ci.simps abc_comp_commute) apply(rule_tac compile_cn_correct', simp_all) @@ -1319,9 +1329,9 @@ lemma save_init_rs: "\length xs = n; ft = max (n+3) (max fft gft)\ - \ {\nl. nl = xs @ rec_eval f xs # 0 \ (ft - n) @ anything} mv_box n (Suc n) - {\nl. nl = xs @ 0 # rec_eval f xs # 0 \ (ft - Suc n) @ anything}" -using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \ (ft - n) @ anything"] + \ {\nl. nl = xs @ rec_exec f xs # 0 \ (ft - n) @ anything} mv_box n (Suc n) + {\nl. nl = xs @ 0 # rec_exec f xs # 0 \ (ft - Suc n) @ anything}" +using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \ (ft - n) @ anything"] apply(auto simp: list_update_append list_update.simps nth_append split: if_splits) apply(case_tac "(max (length xs + 3) (max fft gft))", simp_all add: list_update.simps Suc_diff_le) done @@ -1371,9 +1381,9 @@ lemma [simp]: "length xs = n - \ {\nl. nl = xs @ rec_eval f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything} mv_box n (Suc n) - {\nl. nl = xs @ 0 # rec_eval f xs # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything}" -using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything"] + \ {\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}" +using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything"] apply(simp add: nth_append list_update_append list_update.simps) apply(case_tac "max (n + 3) (max fft gft)", simp_all) apply(case_tac nat, simp_all add: Suc_diff_le list_update.simps) @@ -1457,14 +1467,14 @@ by arith lemma [simp]: "\ft = max (n + 3) (max fft gft); length xs = n\ \ - {\nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything} + {\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_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything}" + {\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything}" apply(simp add: abc_Hoare_halt_def) apply(rule_tac x = 1 in exI) apply(auto simp: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps list_update_append) using list_update_length -[of "(x - Suc y) # rec_eval (Pr (length xs) f g) (xs @ [x - Suc y]) # +[of "(x - Suc y) # rec_exec (Pr (length xs) f g) (xs @ [x - Suc y]) # 0 \ (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" "Suc y" anything y] apply(simp) done @@ -1516,7 +1526,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) @@ -1563,14 +1573,14 @@ apply(simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps) done -lemma rec_eval_pr_0_simps: "rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs" - by(simp add: rec_eval.simps) +lemma rec_exec_pr_0_simps: "rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs" + by(simp add: rec_exec.simps) -lemma rec_eval_pr_Suc_simps: "rec_eval (Pr n f g) (xs @ [Suc y]) - = rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])" +lemma rec_exec_pr_Suc_simps: "rec_exec (Pr n f g) (xs @ [Suc y]) + = rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])" apply(induct y) -apply(simp add: rec_eval.simps) -apply(simp add: rec_eval.simps) +apply(simp add: rec_exec.simps) +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)" @@ -1580,44 +1590,44 @@ assumes code: "code = ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" and len: "length xs = n" - and g_ind: "\ yanything. {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap - {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" + and g_ind: "\ yanything. {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap + {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" and compile_g: "rec_ci g = (gap, gar, gft)" - and termi_g: "\ y y x" shows - "\stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) - code stp = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \ (ft - Suc (Suc n)) @ y # anything)" + "\stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) + code stp = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (ft - Suc (Suc n)) @ y # anything)" proof - let ?A = "[Dec ft (length gap + 7)]" let ?B = "gap" let ?C = "[Inc n, Dec (Suc n) 3, Goto (Suc 0)]" let ?D = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" - have "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) + have "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) ((?A [+] (?B [+] ?C)) @ ?D) stp = (length (?A [+] (?B [+] ?C)), - xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) + xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" proof - - have "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) + have "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) ((?A [+] (?B [+] ?C))) stp = (length (?A [+] (?B [+] ?C)), xs @ (x - y) # 0 # - rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" + rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" proof - - have "{\ nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything} + have "{\ nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything} (?A [+] (?B [+] ?C)) {\ nl. nl = xs @ (x - y) # 0 # - rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything}" + rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything}" proof(rule_tac abc_Hoare_plus_halt) - show "{\nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything} + show "{\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_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything}" + {\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything}" using ft len by(simp) next show - "{\nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything} + "{\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything} ?B [+] ?C - {\nl. nl = xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything}" + {\nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything}" proof(rule_tac abc_Hoare_plus_halt) have a: "gar = Suc (Suc n)" using compile_g termi_g len less @@ -1625,14 +1635,14 @@ have b: "gft > gar" using compile_g by(erule_tac footprint_ge) - show "{\nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything} gap - {\nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # - rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything}" + show "{\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything} gap + {\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # + rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything}" proof - have - "{\nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (gft - gar) @ 0\(ft - gft) @ y # anything} gap - {\nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # - rec_eval g (xs @ [(x - Suc y), rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (gft - Suc gar) @ 0\(ft - gft) @ y # anything}" + "{\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (gft - gar) @ 0\(ft - gft) @ y # anything} gap + {\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # + rec_exec g (xs @ [(x - Suc y), rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (gft - Suc gar) @ 0\(ft - gft) @ y # anything}" using g_ind less by simp thus "?thesis" using a b ft @@ -1640,41 +1650,41 @@ qed next show "{\nl. nl = xs @ (x - Suc y) # - rec_eval (Pr n f g) (xs @ [x - Suc y]) # - rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything} + rec_exec (Pr n f g) (xs @ [x - Suc y]) # + rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything} [Inc n, Dec (Suc n) 3, Goto (Suc 0)] - {\nl. nl = xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) + {\nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything}" using len less - using adjust_paras[of xs n "x - Suc y" " rec_eval (Pr n f g) (xs @ [x - Suc y])" - " rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # + using adjust_paras[of xs n "x - Suc y" " rec_exec (Pr n f g) (xs @ [x - Suc y])" + " rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything"] by(simp add: Suc_diff_Suc) qed qed thus "?thesis" - by(simp add: abc_Hoare_halt_def, auto, rule_tac x = na in exI, case_tac "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # + by(simp add: abc_Hoare_halt_def, auto, rule_tac x = na in exI, case_tac "abc_steps_l (0, 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)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) na", simp) qed - then obtain stpa where "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) + then obtain stpa where "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) ((?A [+] (?B [+] ?C))) stpa = (length (?A [+] (?B [+] ?C)), - xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) + xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" .. thus "?thesis" by(erule_tac abc_append_frist_steps_halt_eq) qed moreover have "\ stp. abc_steps_l (length (?A [+] (?B [+] ?C)), - xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything) - ((?A [+] (?B [+] ?C)) @ ?D) stp = (0, xs @ (x - y) # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # + xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything) + ((?A [+] (?B [+] ?C)) @ ?D) stp = (0, xs @ (x - y) # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" using len by(rule_tac loop_back, simp_all) - moreover have "rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) = rec_eval (Pr n f g) (xs @ [x - y])" + moreover have "rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) = rec_exec (Pr n f g) (xs @ [x - y])" using less - thm rec_eval.simps - apply(case_tac "x - y", simp_all add: rec_eval_pr_Suc_simps) + thm rec_exec.simps + apply(case_tac "x - y", simp_all add: rec_exec_pr_Suc_simps) by(subgoal_tac "nat = x - Suc y", simp, arith) ultimately show "?thesis" using code ft @@ -1682,21 +1692,21 @@ qed lemma [simp]: - "length xs = n \ abc_lm_s (xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) + "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_eval (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything" + xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything" apply(simp add: abc_lm_s.simps) -using list_update_length[of "xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n))" +using list_update_length[of "xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n))" 0 anything 0] apply(auto simp: Suc_diff_Suc) apply(simp add: exp_suc[THEN sym] Suc_diff_Suc del: replicate_Suc) done lemma [simp]: - "(xs @ x # rec_eval (Pr (length xs) f g) (xs @ [x]) # 0 \ (max (length xs + 3) + "(xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # 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_eval (Pr (length xs) f g) (xs @ [x]) # +using nth_append_length[of "xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # 0 \ (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" 0 anything] by(simp) @@ -1704,12 +1714,12 @@ assumes less: "y \ x" and len: "length xs = n" and compile_g: "rec_ci g = (gap, gar, gft)" - and termi_g: "\ y yanything. {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap - {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" - shows "{\nl. nl = xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything} + and termi_g: "\ y yanything. {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap + {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" + shows "{\nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything} ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)] - {\nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything}" + {\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything}" using less proof(induct y) case 0 @@ -1725,37 +1735,37 @@ let ?C = "[Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" have ind: "y \ x \ - {\nl. nl = xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything} - ?C {\nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything}" by fact + {\nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything} + ?C {\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything}" by fact have less: "Suc y \ x" by fact have stp1: - "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (?ft - Suc (Suc n)) @ Suc y # anything) - ?C stp = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything)" + "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (?ft - Suc (Suc n)) @ Suc y # anything) + ?C stp = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything)" using assms less by(rule_tac pr_loop, auto) then obtain stp1 where a: - "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \ (?ft - Suc (Suc n)) @ Suc y # anything) - ?C stp1 = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything)" .. + "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (?ft - Suc (Suc n)) @ Suc y # anything) + ?C stp1 = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything)" .. moreover have - "\ stp. abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) - ?C stp = (length ?C, xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything)" + "\ stp. abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) + ?C stp = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything)" using ind less - by(auto simp: abc_Hoare_halt_def, case_tac "abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) + by(auto simp: abc_Hoare_halt_def, case_tac "abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) ?C na", rule_tac x = na in exI, simp) then obtain stp2 where b: - "abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) - ?C stp2 = (length ?C, xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything)" .. + "abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) + ?C stp2 = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything)" .. from a b show "?case" by(simp add: abc_Hoare_halt_def, rule_tac x = "stp1 + stp2" in exI, simp add: abc_steps_add) qed lemma compile_pr_correct': - assumes termi_g: "\ y y yanything. {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap - {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" - and termi_f: "terminates f xs" - and f_ind: "\ anything. {\nl. nl = xs @ 0 \ (fft - far) @ anything} fap {\nl. nl = xs @ rec_eval f xs # 0 \ (fft - Suc far) @ anything}" + "\ yanything. {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap + {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" + and termi_f: "terminate f xs" + and f_ind: "\ anything. {\nl. nl = xs @ 0 \ (fft - far) @ anything} fap {\nl. nl = xs @ rec_exec f xs # 0 \ (fft - Suc far) @ anything}" and len: "length xs = n" and compile1: "rec_ci f = (fap, far, fft)" and compile2: "rec_ci g = (gap, gar, gft)" @@ -1765,7 +1775,7 @@ (fap [+] (mv_box n (Suc n) [+] ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]))) - {\nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything}" + {\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything}" proof - let ?ft = "max (n+3) (max fft gft)" let ?A = "mv_box n ?ft" @@ -1775,14 +1785,14 @@ let ?E = "gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]" let ?F = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" let ?P = "\nl. nl = xs @ x # 0 \ (?ft - n) @ anything" - let ?S = "\nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything" + let ?S = "\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything" let ?Q1 = "\nl. nl = xs @ 0 \ (?ft - n) @ x # anything" show "{?P} (?A [+] (?B [+] (?C [+] (?D [+] ?E @ ?F)))) {?S}" proof(rule_tac abc_Hoare_plus_halt) show "{?P} ?A {?Q1}" using len by simp next - let ?Q2 = "\nl. nl = xs @ rec_eval f xs # 0 \ (?ft - Suc n) @ x # anything" + let ?Q2 = "\nl. nl = xs @ rec_exec f xs # 0 \ (?ft - Suc n) @ x # anything" have a: "?ft \ fft" by arith have b: "far = n" @@ -1794,7 +1804,7 @@ show "{?Q1} (?B [+] (?C [+] (?D [+] ?E @ ?F))) {?S}" proof(rule_tac abc_Hoare_plus_halt) have "{\nl. nl = xs @ 0 \ (fft - far) @ 0\(?ft - fft) @ x # anything} fap - {\nl. nl = xs @ rec_eval f xs # 0 \ (fft - Suc far) @ 0\(?ft - fft) @ x # anything}" + {\nl. nl = xs @ rec_exec f xs # 0 \ (fft - Suc far) @ 0\(?ft - fft) @ x # anything}" by(rule_tac f_ind) moreover have "fft - far + ?ft - fft = ?ft - far" using a b c by arith @@ -1804,50 +1814,50 @@ using b by(simp add: replicate_merge_anywhere) next - let ?Q3 = "\ nl. nl = xs @ 0 # rec_eval f xs # 0\(?ft - Suc (Suc n)) @ x # anything" + let ?Q3 = "\ nl. nl = xs @ 0 # rec_exec f xs # 0\(?ft - Suc (Suc n)) @ x # anything" show "{?Q2} (?C [+] (?D [+] ?E @ ?F)) {?S}" proof(rule_tac abc_Hoare_plus_halt) show "{?Q2} (?C) {?Q3}" - using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything"] + using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything"] using len by(auto) next show "{?Q3} (?D [+] ?E @ ?F) {?S}" using pr_loop_correct[of x x xs n g gap gar gft f fft anything] assms - by(simp add: rec_eval_pr_0_simps) + by(simp add: rec_exec_pr_0_simps) qed qed qed qed lemma compile_pr_correct: - assumes g_ind: "\y + assumes g_ind: "\y (\x xa xb. rec_ci g = (x, xa, xb) \ - (\xc. {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \ (xb - xa) @ xc} x - {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \ (xb - Suc xa) @ xc}))" - and termi_f: "terminates f xs" + (\xc. {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (xb - xa) @ xc} x + {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (xb - Suc xa) @ xc}))" + and termi_f: "terminate f xs" and f_ind: "\ap arity fp anything. - rec_ci f = (ap, arity, fp) \ {\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ rec_eval f xs # 0 \ (fp - Suc arity) @ anything}" + rec_ci f = (ap, arity, fp) \ {\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ rec_exec f xs # 0 \ (fp - Suc arity) @ anything}" and len: "length xs = n" and compile: "rec_ci (Pr n f g) = (ap, arity, fp)" - shows "{\nl. nl = xs @ x # 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \ (fp - Suc arity) @ anything}" + shows "{\nl. nl = xs @ x # 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (fp - Suc arity) @ anything}" proof(case_tac "rec_ci f", case_tac "rec_ci g") fix fap far fft gap gar gft assume h: "rec_ci f = (fap, far, fft)" "rec_ci g = (gap, gar, gft)" have g: - "\y - (\anything. {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap - {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything}))" + "\y + (\anything. {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap + {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything}))" using g_ind h by(auto) - hence termi_g: "\ y y yanything. {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap - {\nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" + "\ yanything. {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything} gap + {\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything})" by auto - have f_newind: "\ anything. {\nl. nl = xs @ 0 \ (fft - far) @ anything} fap {\nl. nl = xs @ rec_eval f xs # 0 \ (fft - Suc far) @ anything}" + have f_newind: "\ anything. {\nl. nl = xs @ 0 \ (fft - far) @ anything} fap {\nl. nl = xs @ rec_exec f xs # 0 \ (fft - Suc far) @ anything}" using h by(rule_tac f_ind, simp) show "?thesis" @@ -1984,20 +1994,20 @@ and len: "length xs = arity" and far: "far = Suc arity" and ind: " (\xc. ({\nl. nl = xs @ x # 0 \ (fft - far) @ xc} fap - {\nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \ (fft - Suc far) @ xc}))" - and exec_less: "rec_eval f (xs @ [x]) > 0" + {\nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \ (fft - Suc far) @ xc}))" + and exec_less: "rec_exec f (xs @ [x]) > 0" and compile: "rec_ci f = (fap, far, fft)" shows "\ stp > 0. abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" proof - have "\ stp. abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = - (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" + (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "\ stp. abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) fap stp = - (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" + (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "{\nl. nl = xs @ x # 0 \ (fft - far) @ 0\(ft - fft) @ anything} fap - {\nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \ (fft - Suc far) @ 0\(ft - fft) @ anything}" + {\nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \ (fft - Suc far) @ 0\(ft - fft) @ anything}" using ind by simp moreover have "fft > far" using compile @@ -2008,17 +2018,17 @@ by(simp add: replicate_merge_anywhere max_absorb2) qed then obtain stp where "abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) fap stp = - (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" .. + (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" .. thus "?thesis" by(erule_tac abc_append_frist_steps_halt_eq) qed moreover have - "\ stp > 0. abc_steps_l (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = + "\ stp > 0. abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 # 0 \ (ft - Suc (Suc arity)) @ anything)" - using mn_correct[of f fap far fft "rec_eval f (xs @ [x])" xs arity B - "(\stp. (abc_steps_l (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))" + using mn_correct[of f fap far fft "rec_exec f (xs @ [x])" xs arity B + "(\stp. (abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))" x "0 \ (ft - Suc (Suc arity)) @ anything" "(\((as, lm), ss, arity). as = 0)" - "(\((as, lm), ss, aritya). mn_ind_inv (as, lm) (length fap) x (rec_eval f (xs @ [x])) (0 \ (ft - Suc (Suc arity)) @ anything) xs) "] + "(\((as, lm), ss, aritya). mn_ind_inv (as, lm) (length fap) x (rec_exec f (xs @ [x])) (0 \ (ft - Suc (Suc arity)) @ anything) xs) "] B compile exec_less len apply(subgoal_tac "fap \ []", auto) apply(rule_tac x = stp in exI, auto simp: mn_ind_inv.simps) @@ -2038,8 +2048,8 @@ and ft: "ft = max (Suc arity) fft" and len: "length xs = arity" and ind_all: "\i\x. (\xc. ({\nl. nl = xs @ i # 0 \ (fft - far) @ xc} fap - {\nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" - and exec_ge: "\ i\x. rec_eval f (xs @ [i]) > 0" + {\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" + and exec_ge: "\ i\x. rec_exec f (xs @ [i]) > 0" and compile: "rec_ci f = (fap, far, fft)" and far: "far = Suc arity" shows "\ stp > x. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = @@ -2052,12 +2062,12 @@ by(rule_tac mn_loop, simp_all) next case (Suc x) - have ind': "\\i\x. \xc. {\nl. nl = xs @ i # 0 \ (fft - far) @ xc} fap {\nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}; - \i\x. 0 < rec_eval f (xs @ [i])\ \ + have ind': "\\i\x. \xc. {\nl. nl = xs @ i # 0 \ (fft - far) @ xc} fap {\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}; + \i\x. 0 < rec_exec f (xs @ [i])\ \ \stp > x. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" by fact - have exec_ge: "\i\Suc x. 0 < rec_eval f (xs @ [i])" by fact + have exec_ge: "\i\Suc x. 0 < rec_exec f (xs @ [i])" by fact have ind_all: "\i\Suc x. \xc. {\nl. nl = xs @ i # 0 \ (fft - far) @ xc} fap - {\nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}" by fact + {\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}" by fact have ind: "\stp > x. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" using ind' exec_ge ind_all by simp have stp: "\ stp > 0. abc_steps_l (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = @@ -2074,8 +2084,8 @@ and ft: "ft = max (Suc arity) fft" and len: "length xs = arity" and ind_all: "\i\x. (\xc. ({\nl. nl = xs @ i # 0 \ (fft - far) @ xc} fap - {\nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" - and exec_ge: "\ i\x. rec_eval f (xs @ [i]) > 0" + {\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" + and exec_ge: "\ i\x. rec_exec f (xs @ [i]) > 0" and compile: "rec_ci f = (fap, far, fft)" and far: "far = Suc arity" shows "\ stp. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = @@ -2092,17 +2102,17 @@ assumes B: "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]" and ft: "ft = max (Suc arity) fft" and len: "length xs = arity" - and termi_f: "terminates f (xs @ [r])" + and termi_f: "terminate f (xs @ [r])" and f_ind: "\anything. {\nl. nl = xs @ r # 0 \ (fft - far) @ anything} fap {\nl. nl = xs @ r # 0 # 0 \ (fft - Suc far) @ anything}" and ind_all: "\i < r. (\xc. ({\nl. nl = xs @ i # 0 \ (fft - far) @ xc} fap - {\nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" - and exec_less: "\ i 0" - and exec: "rec_eval f (xs @ [r]) = 0" + {\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" + and exec_less: "\ i 0" + and exec: "rec_exec f (xs @ [r]) = 0" and compile: "rec_ci f = (fap, far, fft)" shows "{\nl. nl = xs @ 0 \ (max (Suc arity) fft - arity) @ anything} fap @ B - {\nl. nl = xs @ rec_eval (Mn arity f) xs # 0 \ (max (Suc arity) fft - Suc arity) @ anything}" + {\nl. nl = xs @ rec_exec (Mn arity f) xs # 0 \ (max (Suc arity) fft - Suc arity) @ anything}" proof - have a: "far = Suc arity" using len compile termi_f @@ -2117,13 +2127,13 @@ by(rule_tac mn_loop_correct, auto) moreover have "\ stp. abc_steps_l (0, xs @ r # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = - (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" + (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "\ stp. abc_steps_l (0, xs @ r # 0 \ (ft - Suc arity) @ anything) fap stp = - (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" + (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "{\nl. nl = xs @ r # 0 \ (fft - far) @ 0\(ft - fft) @ anything} fap - {\nl. nl = xs @ r # rec_eval f (xs @ [r]) # 0 \ (fft - Suc far) @ 0\(ft - fft) @ anything}" + {\nl. nl = xs @ r # rec_exec f (xs @ [r]) # 0 \ (fft - Suc far) @ 0\(ft - fft) @ anything}" using f_ind exec by simp thus "?thesis" using ft a b @@ -2131,20 +2141,20 @@ by(simp add: replicate_merge_anywhere max_absorb2) qed then obtain stp where "abc_steps_l (0, xs @ r # 0 \ (ft - Suc arity) @ anything) fap stp = - (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" .. + (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" .. thus "?thesis" by(erule_tac abc_append_frist_steps_halt_eq) qed moreover have - "\ stp. abc_steps_l (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = - (length fap + 5, xs @ r # rec_eval f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" + "\ stp. abc_steps_l (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = + (length fap + 5, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" using ft a b len B exec apply(rule_tac x = 1 in exI, auto) by(auto simp: abc_steps_l.simps B abc_step_l.simps abc_fetch.simps nth_append max_absorb2 abc_lm_v.simps abc_lm_s.simps) - moreover have "rec_eval (Mn (length xs) f) xs = r" + moreover have "rec_exec (Mn (length xs) f) xs = r" using exec exec_less - apply(auto simp: rec_eval.simps Least_def) + apply(auto simp: rec_exec.simps Least_def) thm the_equality apply(rule_tac the_equality, auto) apply(metis exec_less less_not_refl3 linorder_not_less) @@ -2158,18 +2168,18 @@ lemma compile_mn_correct: assumes len: "length xs = n" - and termi_f: "terminates f (xs @ [r])" + and termi_f: "terminate f (xs @ [r])" and f_ind: "\ap arity fp anything. rec_ci f = (ap, arity, fp) \ {\nl. nl = xs @ r # 0 \ (fp - arity) @ anything} ap {\nl. nl = xs @ r # 0 # 0 \ (fp - Suc arity) @ anything}" - and exec: "rec_eval f (xs @ [r]) = 0" + and exec: "rec_exec f (xs @ [r]) = 0" and ind_all: - "\i + "\i (\x xa xb. rec_ci f = (x, xa, xb) \ - (\xc. {\nl. nl = xs @ i # 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \ (xb - Suc xa) @ xc})) \ - 0 < rec_eval f (xs @ [i])" + (\xc. {\nl. nl = xs @ i # 0 \ (xb - xa) @ xc} x {\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (xb - Suc xa) @ xc})) \ + 0 < rec_exec f (xs @ [i])" and compile: "rec_ci (Mn n f) = (ap, arity, fp)" shows "{\nl. nl = xs @ 0 \ (fp - arity) @ anything} ap - {\nl. nl = xs @ rec_eval (Mn n f) xs # 0 \ (fp - Suc arity) @ anything}" + {\nl. nl = xs @ rec_exec (Mn n f) xs # 0 \ (fp - Suc arity) @ anything}" proof(case_tac "rec_ci f") fix fap far fft assume h: "rec_ci f = (fap, far, fft)" @@ -2179,10 +2189,10 @@ by(rule_tac f_ind, simp) have newind_all: "\i < r. (\xc. ({\nl. nl = xs @ i # 0 \ (fft - far) @ xc} fap - {\nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" + {\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc}))" using ind_all h by(auto) - have all_less: "\ i 0" + have all_less: "\ i 0" using ind_all by auto show "?thesis" using h compile f_newind newind_all all_less len termi_f exec @@ -2191,10 +2201,10 @@ qed lemma recursive_compile_correct: - "\terminates recf args; rec_ci recf = (ap, arity, fp)\ + "\terminate recf args; rec_ci recf = (ap, arity, fp)\ \ {\ nl. nl = args @ 0\(fp - arity) @ anything} ap - {\ nl. nl = args@ rec_eval recf args # 0\(fp - Suc arity) @ anything}" -apply(induct arbitrary: ap arity fp anything r rule: terminates.induct) + {\ nl. nl = args@ rec_exec recf args # 0\(fp - Suc arity) @ anything}" +apply(induct arbitrary: ap arity fp anything r rule: terminate.induct) apply(simp_all add: compile_s_correct compile_z_correct compile_id_correct compile_cn_correct compile_pr_correct compile_mn_correct) done @@ -2323,8 +2333,8 @@ lemma recursive_compile_correct_norm': "\rec_ci f = (ap, arity, ft); - terminates f args\ - \ \ stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \ abc_list_crsp (args @ [rec_eval f args]) rl" + terminate f args\ + \ \ stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \ abc_list_crsp (args @ [rec_exec f args]) rl" using recursive_compile_correct[of f args ap arity ft "[]"] apply(auto simp: abc_Hoare_halt_def) apply(rule_tac x = n in exI) @@ -2334,9 +2344,9 @@ done lemma [simp]: - assumes a: "args @ [rec_eval f args] = lm @ 0 \ n" + assumes a: "args @ [rec_exec f args] = lm @ 0 \ n" and b: "length args < length lm" - shows "\m. lm = args @ rec_eval f args # 0 \ m" + shows "\m. lm = args @ rec_exec f args # 0 \ m" using assms apply(case_tac n, simp) apply(rule_tac x = 0 in exI, simp) @@ -2344,9 +2354,9 @@ done lemma [simp]: -"\args @ [rec_eval f args] = lm @ 0 \ n; \ length args < length lm\ +"\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_eval f args # 0 \ m" + args @ rec_exec f args # 0 \ m" apply(case_tac n, simp_all add: exp_suc list_update_append list_update.simps del: replicate_Suc) apply(subgoal_tac "length args = Suc (length lm)", simp) apply(rule_tac x = "Suc (Suc 0)" in exI, simp) @@ -2355,16 +2365,16 @@ lemma compile_append_dummy_correct: assumes compile: "rec_ci f = (ap, ary, fp)" - and termi: "terminates f args" - shows "{\ nl. nl = args} (ap [+] dummy_abc (length args)) {\ nl. (\ m. nl = args @ rec_eval f args # 0\m)}" + and termi: "terminate f args" + shows "{\ nl. nl = args} (ap [+] dummy_abc (length args)) {\ nl. (\ m. nl = args @ rec_exec f args # 0\m)}" proof(rule_tac abc_Hoare_plus_halt) - show "{\nl. nl = args} ap {\ nl. abc_list_crsp (args @ [rec_eval f args]) nl}" + show "{\nl. nl = args} ap {\ nl. abc_list_crsp (args @ [rec_exec f args]) nl}" using compile termi recursive_compile_correct_norm'[of f ap ary fp args] apply(auto simp: abc_Hoare_halt_def) by(rule_tac x = stp in exI, simp) next - show "{abc_list_crsp (args @ [rec_eval f args])} dummy_abc (length args) - {\nl. \m. nl = args @ rec_eval f args # 0 \ m}" + show "{abc_list_crsp (args @ [rec_exec f args])} dummy_abc (length args) + {\nl. \m. nl = args @ rec_exec f args # 0 \ m}" apply(auto simp: dummy_abc_def abc_Hoare_halt_def) apply(rule_tac x = 3 in exI) by(auto simp: abc_steps_l.simps abc_list_crsp_def abc_step_l.simps numeral_3_eq_3 abc_fetch.simps @@ -2386,15 +2396,15 @@ and compile2: "rec_ci (gs!i) = (gap, gar, gft) \ gar = length args" and g_unhalt: "\ anything. {\ nl. nl = args @ 0\(gft - gar) @ anything} gap \" and g_ind: "\ apj arj ftj j anything. \j < i; rec_ci (gs!j) = (apj, arj, ftj)\ - \ {\ nl. nl = args @ 0\(ftj - arj) @ anything} apj {\ nl. nl = args @ rec_eval (gs!j) args # 0\(ftj - Suc arj) @ anything}" - and all_termi: "\ j {\ nl. nl = args @ 0\(ftj - arj) @ anything} apj {\ nl. nl = args @ rec_exec (gs!j) args # 0\(ftj - Suc arj) @ anything}" + and all_termi: "\ j nl. nl = args @ 0\(ft - ar) @ anything} ap \" using compile1 apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_comp_commute) proof(rule_tac abc_Hoare_plus_unhalt1) fix fap far fft let ?ft = "max (Suc (length args)) (Max (insert fft ((\(aprog, p, n). n) ` rec_ci ` set gs)))" - let ?Q = "\nl. nl = args @ 0\ (?ft - length args) @ map (\i. rec_eval i args) (take i gs) @ + let ?Q = "\nl. nl = args @ 0\ (?ft - length args) @ map (\i. rec_exec i args) (take i gs) @ 0\(length gs - i) @ 0\ Suc (length args) @ anything" have "cn_merge_gs (map rec_ci gs) ?ft = cn_merge_gs (map rec_ci (take i gs)) ?ft [+] (gap [+] @@ -2403,11 +2413,11 @@ thus "{\nl. nl = args @ 0 # 0 \ (?ft + length gs) @ anything} (cn_merge_gs (map rec_ci gs) ?ft) \" proof(simp, rule_tac abc_Hoare_plus_unhalt1, rule_tac abc_Hoare_plus_unhalt2, rule_tac abc_Hoare_plus_unhalt1) - let ?Q_tmp = "\nl. nl = args @ 0\ (gft - gar) @ 0\(?ft - (length args) - (gft -gar)) @ map (\i. rec_eval i args) (take i gs) @ + let ?Q_tmp = "\nl. nl = args @ 0\ (gft - gar) @ 0\(?ft - (length args) - (gft -gar)) @ map (\i. rec_exec i args) (take i gs) @ 0\(length gs - i) @ 0\ Suc (length args) @ anything" have a: "{?Q_tmp} gap \" using g_unhalt[of "0 \ (?ft - (length args) - (gft - gar)) @ - map (\i. rec_eval i args) (take i gs) @ 0 \ (length gs - i) @ 0 \ Suc (length args) @ anything"] + map (\i. rec_exec i args) (take i gs) @ 0 \ (length gs - i) @ 0 \ Suc (length args) @ anything"] by simp moreover have "?ft \ gft" using g compile2 @@ -2424,7 +2434,7 @@ show "{\nl. nl = args @ 0 # 0 \ (?ft + length gs) @ anything} cn_merge_gs (map rec_ci (take i gs)) ?ft {\nl. nl = args @ 0 \ (?ft - length args) @ - map (\i. rec_eval i args) (take i gs) @ 0 \ (length gs - i) @ 0 \ Suc (length args) @ anything}" + map (\i. rec_exec i args) (take i gs) @ 0 \ (length gs - i) @ 0 \ Suc (length args) @ anything}" using all_termi apply(rule_tac compile_cn_gs_correct', auto simp: set_conv_nth) by(drule_tac apj = x and arj = xa and ftj = xb and j = ia and anything = xc in g_ind, auto) @@ -2435,7 +2445,7 @@ lemma mn_unhalt_case': assumes compile: "rec_ci f = (a, b, c)" - and all_termi: "\i. terminates f (args @ [i]) \ 0 < rec_eval f (args @ [i])" + and all_termi: "\i. terminate f (args @ [i]) \ 0 < rec_exec f (args @ [i])" and B: "B = [Dec (Suc (length args)) (length a + 5), Dec (Suc (length args)) (length a + 3), Goto (Suc (length a)), Inc (length args), Goto 0]" shows "{\nl. nl = args @ 0 \ (max (Suc (length args)) c - length args) @ anything} @@ -2455,7 +2465,7 @@ proof(rule_tac mn_loop_correct', auto) fix i xc show "{\nl. nl = args @ i # 0 \ (c - Suc (length args)) @ xc} a - {\nl. nl = args @ i # rec_eval f (args @ [i]) # 0 \ (c - Suc (Suc (length args))) @ xc}" + {\nl. nl = args @ i # rec_exec f (args @ [i]) # 0 \ (c - Suc (Suc (length args))) @ xc}" using all_termi recursive_compile_correct[of f "args @ [i]" a b c xc] compile a by(simp) qed @@ -2477,7 +2487,7 @@ lemma mn_unhalt_case: assumes compile: "rec_ci (Mn n f) = (ap, ar, ft) \ length args = ar" - and all_term: "\ i. terminates f (args @ [i]) \ rec_eval f (args @ [i]) > 0" + and all_term: "\ i. terminate f (args @ [i]) \ rec_exec f (args @ [i]) > 0" shows "{\ nl. nl = args @ 0\(ft - ar) @ anything} ap \ " using assms apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_comp_commute) @@ -2490,34 +2500,34 @@ lemma recursive_compile_to_tm_correct1: assumes compile: "rec_ci recf = (ap, ary, fp)" - and termi: " terminates recf args" + and termi: " terminate recf args" and tp: "tp = tm_of (ap [+] dummy_abc (length args))" shows "\ stp m l. steps0 (Suc 0, Bk # Bk # ires, @ Bk\rn) - (tp @ shift (mopup (length args)) (length tp div 2)) stp = (0, Bk\m @ Bk # Bk # ires, Oc\Suc (rec_eval recf args) @ Bk\l)" + (tp @ shift (mopup (length args)) (length tp div 2)) stp = (0, Bk\m @ Bk # Bk # ires, Oc\Suc (rec_exec recf args) @ Bk\l)" proof - - have "{\nl. nl = args} ap [+] dummy_abc (length args) {\nl. \m. nl = args @ rec_eval recf args # 0 \ m}" + have "{\nl. nl = args} ap [+] dummy_abc (length args) {\nl. \m. nl = args @ rec_exec recf args # 0 \ m}" using compile termi compile by(rule_tac compile_append_dummy_correct, auto) then obtain stp m where h: "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) stp = - (length (ap [+] dummy_abc (length args)), args @ rec_eval recf args # 0\m) " + (length (ap [+] dummy_abc (length args)), args @ rec_exec recf args # 0\m) " apply(simp add: abc_Hoare_halt_def, auto) by(case_tac "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) n", auto) thus "?thesis" using assms tp - by(rule_tac lm = args and stp = stp and am = "args @ rec_eval recf args # 0 \ m" + by(rule_tac lm = args and stp = stp and am = "args @ rec_exec recf args # 0 \ m" in compile_correct_halt, auto simp: crsp.simps start_of.simps length_abc_comp abc_lm_v.simps) qed lemma recursive_compile_to_tm_correct2: - assumes termi: " terminates recf args" + assumes termi: " terminate recf args" shows "\ stp m l. steps0 (Suc 0, [Bk, Bk], ) (tm_of_rec recf) stp = - (0, Bk\Suc (Suc m), Oc\Suc (rec_eval recf args) @ Bk\l)" + (0, Bk\Suc (Suc m), Oc\Suc (rec_exec recf args) @ Bk\l)" proof(case_tac "rec_ci recf", simp add: tm_of_rec.simps) 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 = - (0, Bk # Bk # Bk \ m, Oc # Oc \ rec_eval recf args @ Bk \ l)" + (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, @@ -2525,9 +2535,9 @@ qed lemma recursive_compile_to_tm_correct3: - assumes termi: "terminates recf args" + assumes termi: "terminate recf args" shows "{\ tp. tp =([Bk, Bk], )} (tm_of_rec recf) - {\ tp. \ k l. tp = (Bk\ k, @ Bk \ l)}" + {\ tp. \ k l. tp = (Bk\ k, @ Bk \ l)}" using recursive_compile_to_tm_correct2[OF assms] apply(auto simp add: Hoare_halt_def) apply(rule_tac x = stp in exI) diff -r 89ed51d72e4a -r aea02b5a58d2 thys/UF.thy --- a/thys/UF.thy Thu May 02 12:49:15 2013 +0100 +++ b/thys/UF.thy Thu May 02 12:49:33 2013 +0100 @@ -5,7 +5,7 @@ header {* Construction of a Universal Function *} theory UF -imports Rec_Def GCD Abacus "~~/src/HOL/Number_Theory/Primes" +imports Rec_Def GCD Abacus begin text {* @@ -152,58 +152,93 @@ Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1) @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))" - -declare rec_eval.simps[simp del] constn.simps[simp del] - - -section {* Correctness of various recursive functions *} - - -lemma add_lemma: "rec_eval rec_add [x, y] = x + y" -by(induct_tac y, auto simp: rec_add_def rec_eval.simps) - -lemma mult_lemma: "rec_eval rec_mult [x, y] = x * y" -by(induct_tac y, auto simp: rec_mult_def rec_eval.simps add_lemma) - -lemma pred_lemma: "rec_eval rec_pred [x] = x - 1" -by(induct_tac x, auto simp: rec_pred_def rec_eval.simps) - -lemma minus_lemma: "rec_eval rec_minus [x, y] = x - y" -by(induct_tac y, auto simp: rec_eval.simps rec_minus_def pred_lemma) - -lemma sg_lemma: "rec_eval rec_sg [x] = (if x = 0 then 0 else 1)" -by(auto simp: rec_sg_def minus_lemma rec_eval.simps constn.simps) - -lemma constn_lemma: "rec_eval (constn n) [x] = n" -by(induct n, auto simp: rec_eval.simps constn.simps) - -lemma less_lemma: "rec_eval rec_less [x, y] = (if x < y then 1 else 0)" -by(induct_tac y, auto simp: rec_eval.simps - rec_less_def minus_lemma sg_lemma) - -lemma not_lemma: "rec_eval rec_not [x] = (if x = 0 then 1 else 0)" -by(induct_tac x, auto simp: rec_eval.simps rec_not_def - constn_lemma minus_lemma) - -lemma eq_lemma: "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)" -by(induct_tac y, auto simp: rec_eval.simps rec_eq_def constn_lemma add_lemma minus_lemma) - -lemma conj_lemma: "rec_eval rec_conj [x, y] = (if x = 0 \ y = 0 then 0 else 1)" -by(induct_tac y, auto simp: rec_eval.simps sg_lemma rec_conj_def mult_lemma) - -lemma disj_lemma: "rec_eval rec_disj [x, y] = (if x = 0 \ y = 0 then 0 else 1)" -by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_eval.simps) - -declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] - minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] - less_lemma[simp] not_lemma[simp] eq_lemma[simp] - conj_lemma[simp] disj_lemma[simp] +text {* + @{text "rec_exec"} is the interpreter function for + reursive functions. The function is defined such that + it always returns meaningful results for primitive recursive + functions. + *} + +declare rec_exec.simps[simp del] constn.simps[simp del] + +text {* + Correctness of @{text "rec_add"}. + *} +lemma add_lemma: "\ x y. rec_exec rec_add [x, y] = x + y" +by(induct_tac y, auto simp: rec_add_def rec_exec.simps) + +text {* + Correctness of @{text "rec_mult"}. + *} +lemma mult_lemma: "\ x y. rec_exec rec_mult [x, y] = x * y" +by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma) + +text {* + Correctness of @{text "rec_pred"}. + *} +lemma pred_lemma: "\ x. rec_exec rec_pred [x] = x - 1" +by(induct_tac x, auto simp: rec_pred_def rec_exec.simps) + +text {* + Correctness of @{text "rec_minus"}. + *} +lemma minus_lemma: "\ x y. rec_exec rec_minus [x, y] = x - y" +by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma) + +text {* + Correctness of @{text "rec_sg"}. + *} +lemma sg_lemma: "\ x. rec_exec rec_sg [x] = (if x = 0 then 0 else 1)" +by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps) text {* - @{text "primrec recf n"} is true iff @{text "recf"} is a primitive - recursive function with arity @{text "n"}. + Correctness of @{text "constn"}. + *} +lemma constn_lemma: "rec_exec (constn n) [x] = n" +by(induct n, auto simp: rec_exec.simps constn.simps) + +text {* + Correctness of @{text "rec_less"}. + *} +lemma less_lemma: "\ x y. rec_exec rec_less [x, y] = + (if x < y then 1 else 0)" +by(induct_tac y, auto simp: rec_exec.simps + rec_less_def minus_lemma sg_lemma) + +text {* + Correctness of @{text "rec_not"}. + *} +lemma not_lemma: + "\ x. rec_exec rec_not [x] = (if x = 0 then 1 else 0)" +by(induct_tac x, auto simp: rec_exec.simps rec_not_def + constn_lemma minus_lemma) + +text {* + Correctness of @{text "rec_eq"}. *} - +lemma eq_lemma: "\ x y. rec_exec rec_eq [x, y] = (if x = y then 1 else 0)" +by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma) + +text {* + Correctness of @{text "rec_conj"}. + *} +lemma conj_lemma: "\ x y. rec_exec rec_conj [x, y] = (if x = 0 \ y = 0 then 0 + else 1)" +by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma) + +text {* + Correctness of @{text "rec_disj"}. + *} +lemma disj_lemma: "\ x y. rec_exec rec_disj [x, y] = (if x = 0 \ y = 0 then 0 + else 1)" +by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps) + + +text {* + @{text "primrec recf n"} is true iff + @{text "recf"} is a primitive recursive function + with arity @{text "n"}. + *} inductive primerec :: "recf \ nat \ bool" where prime_z[intro]: "primerec z (Suc 0)" | @@ -224,7 +259,10 @@ inductive_cases prime_cn_reverse[elim]: "primerec (Cn n f gs) m" inductive_cases prime_pr_reverse[elim]: "primerec (Pr n f g) m" - +declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] + minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] + less_lemma[simp] not_lemma[simp] eq_lemma[simp] + conj_lemma[simp] disj_lemma[simp] text {* @{text "Sigma"} is the logical specification of @@ -233,41 +271,45 @@ function Sigma :: "(nat list \ nat) \ nat list \ nat" where "Sigma g xs = (if last xs = 0 then g xs - else (Sigma g (butlast xs @ [last xs - 1]) + g xs)) " + else (Sigma g (butlast xs @ [last xs - 1]) + + g xs)) " by pat_completeness auto - termination proof show "wf (measure (\ (f, xs). last xs))" by auto next fix g xs assume "last (xs::nat list) \ 0" - thus "((g, butlast xs @ [last xs - 1]), g, xs) \ measure (\(f, xs). last xs)" + thus "((g, butlast xs @ [last xs - 1]), g, xs) + \ measure (\(f, xs). last xs)" by auto qed -declare rec_eval.simps[simp del] get_fstn_args.simps[simp del] +declare rec_exec.simps[simp del] get_fstn_args.simps[simp del] arity.simps[simp del] Sigma.simps[simp del] rec_sigma.simps[simp del] lemma [simp]: "arity z = 1" - by(simp add: arity.simps) + by(simp add: arity.simps) lemma rec_pr_0_simp_rewrite: " - rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs" - by(simp add: rec_eval.simps) + rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs" +by(simp add: rec_exec.simps) lemma rec_pr_0_simp_rewrite_single_param: " - rec_eval (Pr n f g) [0] = rec_eval f []" - by(simp add: rec_eval.simps) + rec_exec (Pr n f g) [0] = rec_exec f []" +by(simp add: rec_exec.simps) lemma rec_pr_Suc_simp_rewrite: - "rec_eval (Pr n f g) (xs @ [Suc x]) = rec_eval g (xs @ [x] @ [rec_eval (Pr n f g) (xs @ [x])])" -by(simp add: rec_eval.simps) + "rec_exec (Pr n f g) (xs @ [Suc x]) = + rec_exec g (xs @ [x] @ + [rec_exec (Pr n f g) (xs @ [x])])" +by(simp add: rec_exec.simps) lemma rec_pr_Suc_simp_rewrite_single_param: - "rec_eval (Pr n f g) ([Suc x]) = rec_eval g ([x] @ [rec_eval (Pr n f g) ([x])])" -by(simp add: rec_eval.simps) + "rec_exec (Pr n f g) ([Suc x]) = + rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])" +by(simp add: rec_exec.simps) lemma Sigma_0_simp_rewrite_single_param: "Sigma f [0] = f [0]" @@ -289,13 +331,13 @@ by(simp add: nth_append) lemma get_fstn_args_take: "\length xs = m; n \ m\ \ - map (\ f. rec_eval f xs) (get_fstn_args m n)= take n xs" + map (\ f. rec_exec f xs) (get_fstn_args m n)= take n xs" proof(induct n) case 0 thus "?case" by(simp add: get_fstn_args.simps) next case (Suc n) thus "?case" - by(simp add: get_fstn_args.simps rec_eval.simps + by(simp add: get_fstn_args.simps rec_exec.simps take_Suc_conv_app_nth) qed @@ -307,11 +349,11 @@ lemma rec_sigma_Suc_simp_rewrite: "primerec f (Suc (length xs)) - \ rec_eval (rec_sigma f) (xs @ [Suc x]) = - rec_eval (rec_sigma f) (xs @ [x]) + rec_eval f (xs @ [Suc x])" + \ rec_exec (rec_sigma f) (xs @ [Suc x]) = + rec_exec (rec_sigma f) (xs @ [x]) + rec_exec f (xs @ [Suc x])" apply(induct x) apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite - rec_eval.simps get_fstn_args_take) + rec_exec.simps get_fstn_args_take) done text {* @@ -319,9 +361,9 @@ *} lemma sigma_lemma: "primerec rg (Suc (length xs)) - \ rec_eval (rec_sigma rg) (xs @ [x]) = Sigma (rec_eval rg) (xs @ [x])" + \ rec_exec (rec_sigma rg) (xs @ [x]) = Sigma (rec_exec rg) (xs @ [x])" apply(induct x) -apply(auto simp: rec_eval.simps rec_sigma.simps Let_def +apply(auto simp: rec_exec.simps rec_sigma.simps Let_def get_fstn_args_take Sigma_0_simp_rewrite Sigma_Suc_simp_rewrite) done @@ -366,11 +408,11 @@ lemma rec_accum_Suc_simp_rewrite: "primerec f (Suc (length xs)) - \ rec_eval (rec_accum f) (xs @ [Suc x]) = - rec_eval (rec_accum f) (xs @ [x]) * rec_eval f (xs @ [Suc x])" + \ rec_exec (rec_accum f) (xs @ [Suc x]) = + rec_exec (rec_accum f) (xs @ [x]) * rec_exec f (xs @ [Suc x])" apply(induct x) apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite - rec_eval.simps get_fstn_args_take) + rec_exec.simps get_fstn_args_take) done text {* @@ -378,9 +420,9 @@ *} lemma accum_lemma : "primerec rg (Suc (length xs)) - \ rec_eval (rec_accum rg) (xs @ [x]) = Accum (rec_eval rg) (xs @ [x])" + \ rec_exec (rec_accum rg) (xs @ [x]) = Accum (rec_exec rg) (xs @ [x])" apply(induct x) -apply(auto simp: rec_eval.simps rec_sigma.simps Let_def +apply(auto simp: rec_exec.simps rec_sigma.simps Let_def get_fstn_args_take) done @@ -399,10 +441,10 @@ (get_fstn_args (vl - 1) (vl - 1) @ [rt])])" lemma rec_accum_ex: "primerec rf (Suc (length xs)) \ - (rec_eval (rec_accum rf) (xs @ [x]) = 0) = - (\ t \ x. rec_eval rf (xs @ [t]) = 0)" + (rec_exec (rec_accum rf) (xs @ [x]) = 0) = + (\ t \ x. rec_exec rf (xs @ [t]) = 0)" apply(induct x, simp_all add: rec_accum_Suc_simp_rewrite) -apply(simp add: rec_eval.simps rec_accum.simps get_fstn_args_take, +apply(simp add: rec_exec.simps rec_accum.simps get_fstn_args_take, auto) apply(rule_tac x = ta in exI, simp) apply(case_tac "t = Suc x", simp_all) @@ -415,16 +457,16 @@ lemma all_lemma: "\primerec rf (Suc (length xs)); primerec rt (length xs)\ - \ rec_eval (rec_all rt rf) xs = (if (\ x \ (rec_eval rt xs). 0 < rec_eval rf (xs @ [x])) then 1 + \ rec_exec (rec_all rt rf) xs = (if (\ x \ (rec_exec rt xs). 0 < rec_exec rf (xs @ [x])) then 1 else 0)" apply(auto simp: rec_all.simps) -apply(simp add: rec_eval.simps map_append get_fstn_args_take split: if_splits) -apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex) -apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp_all) +apply(simp add: rec_exec.simps map_append get_fstn_args_take split: if_splits) +apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex) +apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp_all) apply(erule_tac exE, erule_tac x = t in allE, simp) -apply(simp add: rec_eval.simps map_append get_fstn_args_take) -apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex) -apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp, simp) +apply(simp add: rec_exec.simps map_append get_fstn_args_take) +apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex) +apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp, simp) apply(erule_tac x = x in allE, simp) done @@ -441,10 +483,10 @@ (get_fstn_args (vl - 1) (vl - 1) @ [rt])])" lemma rec_sigma_ex: "primerec rf (Suc (length xs)) - \ (rec_eval (rec_sigma rf) (xs @ [x]) = 0) = - (\ t \ x. rec_eval rf (xs @ [t]) = 0)" + \ (rec_exec (rec_sigma rf) (xs @ [x]) = 0) = + (\ t \ x. rec_exec rf (xs @ [t]) = 0)" apply(induct x, simp_all add: rec_sigma_Suc_simp_rewrite) -apply(simp add: rec_eval.simps rec_sigma.simps +apply(simp add: rec_exec.simps rec_sigma.simps get_fstn_args_take, auto) apply(case_tac "t = Suc x", simp_all) done @@ -455,13 +497,13 @@ lemma ex_lemma:" \primerec rf (Suc (length xs)); primerec rt (length xs)\ -\ (rec_eval (rec_ex rt rf) xs = - (if (\ x \ (rec_eval rt xs). 0 (rec_exec (rec_ex rt rf) xs = + (if (\ x \ (rec_exec rt xs). 0 \ Min {uu. uu \ w \ 0 < rec_eval rf (xs @ [uu])} \ w; - x \ w; 0 < rec_eval rf (xs @ [x])\ +lemma Min_false1[simp]: "\\ Min {uu. uu \ w \ 0 < rec_exec rf (xs @ [uu])} \ w; + x \ w; 0 < rec_exec rf (xs @ [x])\ \ False" -apply(subgoal_tac "finite {uu. uu \ w \ 0 < rec_eval rf (xs @ [uu])}") -apply(subgoal_tac "{uu. uu \ w \ 0 < rec_eval rf (xs @ [uu])} \ {}") +apply(subgoal_tac "finite {uu. uu \ w \ 0 < rec_exec rf (xs @ [uu])}") +apply(subgoal_tac "{uu. uu \ w \ 0 < rec_exec rf (xs @ [uu])} \ {}") apply(simp add: Min_le_iff, simp) apply(rule_tac x = x in exI, simp) apply(simp) @@ -649,12 +692,12 @@ lemma sigma_minr_lemma: assumes prrf: "primerec rf (Suc (length xs))" - shows "UF.Sigma (rec_eval (rec_all (recf.id (Suc (length xs)) (length xs)) + shows "UF.Sigma (rec_exec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])]))) (xs @ [w]) = - Minr (\args. 0 < rec_eval rf args) xs w" + Minr (\args. 0 < rec_exec rf args) xs w" proof(induct w) let ?rt = "(recf.id (Suc (length xs)) ((length xs)))" let ?rf = "(Cn (Suc (Suc (length xs))) @@ -667,11 +710,11 @@ primerec ?rt (length (xs @ [0]))" apply(auto simp: prrf nth_append)+ done - show "Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [0]) - = Minr (\args. 0 < rec_eval rf args) xs 0" + show "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [0]) + = Minr (\args. 0 < rec_exec rf args) xs 0" apply(simp add: Sigma.simps) apply(simp only: prrf all_lemma, - auto simp: rec_eval.simps get_fstn_args_take Minr.simps) + auto simp: rec_exec.simps get_fstn_args_take Minr.simps) apply(rule_tac Min_eqI, auto) done next @@ -684,17 +727,17 @@ (Suc ((length xs)))])])" let ?rq = "(rec_all ?rt ?rf)" assume ind: - "Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\args. 0 < rec_eval rf args) xs w" + "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\args. 0 < rec_exec rf args) xs w" have prrf: "primerec ?rf (Suc (length (xs @ [Suc w]))) \ primerec ?rt (length (xs @ [Suc w]))" apply(auto simp: prrf nth_append)+ done - show "UF.Sigma (rec_eval (rec_all ?rt ?rf)) + show "UF.Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [Suc w]) = - Minr (\args. 0 < rec_eval rf args) xs (Suc w)" + Minr (\args. 0 < rec_exec rf args) xs (Suc w)" apply(auto simp: Sigma_Suc_simp_rewrite ind Minr_Suc_simp) apply(simp_all only: prrf all_lemma) - apply(auto simp: rec_eval.simps get_fstn_args_take Let_def Minr.simps split: if_splits) + apply(auto simp: rec_exec.simps get_fstn_args_take Let_def Minr.simps split: if_splits) apply(drule_tac Min_false1, simp, simp, simp) apply(case_tac "x = Suc w", simp, simp) apply(drule_tac Min_false1, simp, simp, simp) @@ -705,9 +748,10 @@ text {* The correctness of @{text "rec_Minr"}. *} -lemma Minr_lemma: - assumes h: "primerec rf (Suc (length xs))" - shows "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\ args. (0 < rec_eval rf args)) xs w" +lemma Minr_lemma: " + \primerec rf (Suc (length xs))\ + \ rec_exec (rec_Minr rf) (xs @ [w]) = + Minr (\ args. (0 < rec_exec rf args)) xs w" proof - let ?rt = "(recf.id (Suc (length xs)) ((length xs)))" let ?rf = "(Cn (Suc (Suc (length xs))) @@ -716,14 +760,16 @@ [recf.id (Suc (Suc (length xs))) (Suc ((length xs)))])])" let ?rq = "(rec_all ?rt ?rf)" + assume h: "primerec rf (Suc (length xs))" have h1: "primerec ?rq (Suc (length xs))" apply(rule_tac primerec_all_iff) apply(auto simp: h nth_append)+ done moreover have "arity rf = Suc (length xs)" using h by auto - ultimately show "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\ args. (0 < rec_eval rf args)) xs w" - apply(simp add: rec_eval.simps rec_Minr.simps arity.simps Let_def + ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = + Minr (\ args. (0 < rec_exec rf args)) xs w" + apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def sigma_lemma all_lemma) apply(rule_tac sigma_minr_lemma) apply(simp add: h) @@ -743,8 +789,8 @@ The correctness of @{text "rec_le"}. *} lemma le_lemma: - "rec_eval rec_le [x, y] = (if (x \ y) then 1 else 0)" -by(auto simp: rec_le_def rec_eval.simps) + "\x y. rec_exec rec_le [x, y] = (if (x \ y) then 1 else 0)" +by(auto simp: rec_le_def rec_exec.simps) text {* Definition of @{text "Max[Rr]"} on page 77 of Boolos's book. @@ -765,12 +811,13 @@ "rec_maxr rr = (let vl = arity rr in let rt = id (Suc vl) (vl - 1) in let rf1 = Cn (Suc (Suc vl)) rec_le - [id (Suc (Suc vl)) (Suc vl), id (Suc (Suc vl)) vl] in + [id (Suc (Suc vl)) + ((Suc vl)), id (Suc (Suc vl)) (vl)] in let rf2 = Cn (Suc (Suc vl)) rec_not [Cn (Suc (Suc vl)) rr (get_fstn_args (Suc (Suc vl)) (vl - 1) @ - [id (Suc (Suc vl)) (Suc vl)])] in + [id (Suc (Suc vl)) ((Suc vl))])] in let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in let Qf = Cn (Suc vl) rec_not [rec_all rt rf] in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @ @@ -810,7 +857,8 @@ done lemma [simp]: - "length ys = Suc n \ (take n ys @ [ys ! n, ys ! n]) = ys @ [ys ! n]" + "length ys = Suc n \ (take n ys @ [ys ! n, ys ! n]) = + ys @ [ys ! n]" apply(simp) apply(subgoal_tac "\ xs y. ys = xs @ [y]", auto) apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI) @@ -818,19 +866,22 @@ done lemma Maxr_Suc_simp: - "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w else Maxr Rr xs w)" + "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(rule_tac Max_eqI, auto) done lemma [simp]: "min (Suc n) n = n" by simp -lemma Sigma_0: "\ i \ n. (f (xs @ [i]) = 0) \ Sigma f (xs @ [n]) = 0" +lemma Sigma_0: "\ i \ n. (f (xs @ [i]) = 0) \ + Sigma f (xs @ [n]) = 0" apply(induct n, simp add: Sigma.simps) apply(simp add: Sigma_Suc_simp_rewrite) done -lemma [elim]: "\k Sigma f (xs @ [w]) = Suc w" +lemma [elim]: "\k Sigma f (xs @ [w]) = Suc w" apply(induct w) apply(simp add: Sigma.simps, simp) apply(simp add: Sigma.simps) @@ -847,7 +898,7 @@ lemma Sigma_Max_lemma: assumes prrf: "primerec rf (Suc (length xs))" - shows "UF.Sigma (rec_eval (Cn (Suc (Suc (length xs))) rec_not + shows "UF.Sigma (rec_exec (Cn (Suc (Suc (length xs))) rec_not [rec_all (recf.id (Suc (Suc (length xs))) (length xs)) (Cn (Suc (Suc (Suc (length xs)))) rec_disj [Cn (Suc (Suc (Suc (length xs)))) rec_le @@ -858,7 +909,7 @@ (get_fstn_args (Suc (Suc (Suc (length xs)))) (length xs) @ [recf.id (Suc (Suc (Suc (length xs)))) (Suc (Suc (length xs)))])]])])) ((xs @ [w]) @ [w]) = - Maxr (\args. 0 < rec_eval rf args) xs w" + Maxr (\args. 0 < rec_exec rf args) xs w" proof - let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))" let ?rf1 = "Cn (Suc (Suc (Suc (length xs)))) @@ -876,7 +927,7 @@ let ?notrq = "Cn (Suc (Suc (length xs))) rec_not [?rq]" show "?thesis" proof(auto simp: Maxr.simps) - assume h: "\x\w. rec_eval rf (xs @ [x]) = 0" + assume h: "\x\w. rec_exec rf (xs @ [x]) = 0" have "primerec ?rf (Suc (length (xs @ [w, i]))) \ primerec ?rt (length (xs @ [w, i]))" using prrf @@ -884,54 +935,54 @@ apply(case_tac i, auto) apply(case_tac ia, auto simp: h nth_append) done - hence "Sigma (rec_eval ?notrq) ((xs@[w])@[w]) = 0" + hence "Sigma (rec_exec ?notrq) ((xs@[w])@[w]) = 0" apply(rule_tac Sigma_0) - apply(auto simp: rec_eval.simps all_lemma + apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append h) done - thus "UF.Sigma (rec_eval ?notrq) + thus "UF.Sigma (rec_exec ?notrq) (xs @ [w, w]) = 0" by simp next fix x - assume h: "x \ w" "0 < rec_eval rf (xs @ [x])" - hence "\ ma. Max {y. y \ w \ 0 < rec_eval rf (xs @ [y])} = ma" + assume h: "x \ w" "0 < rec_exec rf (xs @ [x])" + hence "\ ma. Max {y. y \ w \ 0 < rec_exec rf (xs @ [y])} = ma" by auto from this obtain ma where k1: - "Max {y. y \ w \ 0 < rec_eval rf (xs @ [y])} = ma" .. - hence k2: "ma \ w \ 0 < rec_eval rf (xs @ [ma])" + "Max {y. y \ w \ 0 < rec_exec rf (xs @ [y])} = ma" .. + hence k2: "ma \ w \ 0 < rec_exec rf (xs @ [ma])" using h apply(subgoal_tac - "Max {y. y \ w \ 0 < rec_eval rf (xs @ [y])} \ {y. y \ w \ 0 < rec_eval rf (xs @ [y])}") + "Max {y. y \ w \ 0 < rec_exec rf (xs @ [y])} \ {y. y \ w \ 0 < rec_exec rf (xs @ [y])}") apply(erule_tac CollectE, simp) apply(rule_tac Max_in, auto) done - hence k3: "\ k < ma. (rec_eval ?notrq (xs @ [w, k]) = 1)" + hence k3: "\ k < ma. (rec_exec ?notrq (xs @ [w, k]) = 1)" apply(auto simp: nth_append) apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \ primerec ?rt (length (xs @ [w, k]))") - apply(auto simp: rec_eval.simps all_lemma get_fstn_args_take nth_append) + apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append) using prrf apply(case_tac i, auto) apply(case_tac ia, auto simp: h nth_append) done - have k4: "\ k \ ma. (rec_eval ?notrq (xs @ [w, k]) = 0)" + have k4: "\ k \ ma. (rec_exec ?notrq (xs @ [w, k]) = 0)" apply(auto) apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \ primerec ?rt (length (xs @ [w, k]))") - apply(auto simp: rec_eval.simps all_lemma get_fstn_args_take nth_append) - apply(subgoal_tac "x \ Max {y. y \ w \ 0 < rec_eval rf (xs @ [y])}", + apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append) + apply(subgoal_tac "x \ Max {y. y \ w \ 0 < rec_exec rf (xs @ [y])}", simp add: k1) apply(rule_tac Max_ge, auto) using prrf apply(case_tac i, auto) apply(case_tac ia, auto simp: h nth_append) done - from k3 k4 k1 have "Sigma (rec_eval ?notrq) ((xs @ [w]) @ [w]) = ma" + from k3 k4 k1 have "Sigma (rec_exec ?notrq) ((xs @ [w]) @ [w]) = ma" apply(rule_tac Sigma_max_point, simp, simp, simp add: k2) done - from k1 and this show "Sigma (rec_eval ?notrq) (xs @ [w, w]) = - Max {y. y \ w \ 0 < rec_eval rf (xs @ [y])}" + from k1 and this show "Sigma (rec_exec ?notrq) (xs @ [w, w]) = + Max {y. y \ w \ 0 < rec_exec rf (xs @ [y])}" by simp qed qed @@ -941,13 +992,13 @@ *} lemma Maxr_lemma: assumes h: "primerec rf (Suc (length xs))" - shows "rec_eval (rec_maxr rf) (xs @ [w]) = - Maxr (\ args. 0 < rec_eval rf args) xs w" + shows "rec_exec (rec_maxr rf) (xs @ [w]) = + Maxr (\ args. 0 < rec_exec rf args) xs w" proof - from h have "arity rf = Suc (length xs)" by auto thus "?thesis" - proof(simp add: rec_eval.simps rec_maxr.simps nth_append get_fstn_args_take) + proof(simp add: rec_exec.simps rec_maxr.simps nth_append get_fstn_args_take) let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))" let ?rf1 = "Cn (Suc (Suc (Suc (length xs)))) rec_le [recf.id (Suc (Suc (Suc (length xs)))) @@ -976,17 +1027,17 @@ by(erule_tac primerec_all_iff, auto) hence prnotrp: "primerec ?notrq (Suc (length ((xs @ [w]))))" by(rule_tac prime_cn, auto) - have g1: "rec_eval (rec_sigma ?notrq) ((xs @ [w]) @ [w]) - = Maxr (\args. 0 < rec_eval rf args) xs w" + have g1: "rec_exec (rec_sigma ?notrq) ((xs @ [w]) @ [w]) + = Maxr (\args. 0 < rec_exec rf args) xs w" using prnotrp using sigma_lemma apply(simp only: sigma_lemma) apply(rule_tac Sigma_Max_lemma) apply(simp add: h) done - thus "rec_eval (rec_sigma ?notrq) + thus "rec_exec (rec_sigma ?notrq) (xs @ [w, w]) = - Maxr (\args. 0 < rec_eval rf args) xs w" + Maxr (\args. 0 < rec_exec rf args) xs w" apply(simp) done qed @@ -997,9 +1048,10 @@ *} fun quo :: "nat list \ nat" where - "quo [x, y] = - (let Rr = (\ zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0)) \ zs ! 0) \ zs ! Suc 0 \ 0)) - in Maxr Rr [x, y] x)" + "quo [x, y] = (let Rr = + (\ zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0)) + \ zs ! 0) \ zs ! Suc 0 \ (0::nat))) + in Maxr Rr [x, y] x)" declare quo.simps[simp del] @@ -1036,14 +1088,16 @@ definition rec_noteq:: "recf" where "rec_noteq = Cn (Suc (Suc 0)) rec_not [Cn (Suc (Suc 0)) - rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0)) ((Suc 0))]]" + rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0)) + ((Suc 0))]]" text {* The correctness of @{text "rec_noteq"}. *} lemma noteq_lemma: - "rec_eval rec_noteq [x, y] = (if x \ y then 1 else 0)" -by(simp add: rec_eval.simps rec_noteq_def) + "\ x y. rec_exec rec_noteq [x, y] = + (if x \ y then 1 else 0)" +by(simp add: rec_exec.simps rec_noteq_def) declare noteq_lemma[simp] @@ -1079,8 +1133,8 @@ done -lemma quo_lemma1: "rec_eval rec_quo [x, y] = quo [x, y]" -proof(simp add: rec_eval.simps rec_quo_def) +lemma quo_lemma1: "rec_exec rec_quo [x, y] = quo [x, y]" +proof(simp add: rec_exec.simps rec_quo_def) let ?rR = "(Cn (Suc (Suc (Suc 0))) rec_conj [Cn (Suc (Suc (Suc 0))) rec_le [Cn (Suc (Suc (Suc 0))) rec_mult @@ -1091,7 +1145,7 @@ [recf.id (Suc (Suc (Suc 0))) (Suc (0)), Cn (Suc (Suc (Suc 0))) (constn 0) [recf.id (Suc (Suc (Suc 0))) (0)]]])" - have "rec_eval (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\ args. 0 < rec_eval ?rR args) [x, y] x" + have "rec_exec (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\ args. 0 < rec_exec ?rR args) [x, y] x" proof(rule_tac Maxr_lemma, simp) show "primerec ?rR (Suc (Suc (Suc 0)))" apply(auto) @@ -1100,24 +1154,24 @@ apply(case_tac i, auto) done qed - hence g1: "rec_eval (rec_maxr ?rR) ([x, y, x]) = - Maxr (\ args. if rec_eval ?rR args = 0 then False + hence g1: "rec_exec (rec_maxr ?rR) ([x, y, x]) = + Maxr (\ args. if rec_exec ?rR args = 0 then False else True) [x, y] x" by simp - have g2: "Maxr (\ args. if rec_eval ?rR args = 0 then False + have g2: "Maxr (\ args. if rec_exec ?rR args = 0 then False else True) [x, y] x = quo [x, y]" - apply(simp add: rec_eval.simps) + apply(simp add: rec_exec.simps) apply(simp add: Maxr.simps quo.simps, auto) done from g1 and g2 show - "rec_eval (rec_maxr ?rR) ([x, y, x]) = quo [x, y]" + "rec_exec (rec_maxr ?rR) ([x, y, x]) = quo [x, y]" by simp qed text {* The correctness of @{text "quo"}. *} -lemma quo_lemma2: "rec_eval rec_quo [x, y] = x div y" +lemma quo_lemma2: "rec_exec rec_quo [x, y] = x div y" using quo_lemma1[of x y] quo_div[of x y] by simp @@ -1134,8 +1188,8 @@ text {* The correctness of @{text "rec_mod"}: *} -lemma mod_lemma: "rec_eval rec_mod [x, y] = (x mod y)" -proof(simp add: rec_eval.simps rec_mod_def quo_lemma2) +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] @@ -1143,8 +1197,7 @@ done qed -section {* Embranch Function *} - +text{* lemmas for embranch function*} type_synonym ftype = "nat list \ nat" type_synonym rtype = "nat list \ bool" @@ -1178,56 +1231,56 @@ declare Embranch.simps[simp del] rec_embranch.simps[simp del] lemma embranch_all0: - "\\ j < length rcs. rec_eval (rcs ! j) xs = 0; + "\\ j < length rcs. rec_exec (rcs ! j) xs = 0; length rgs = length rcs; rcs \ []; list_all (\ rf. primerec rf (length xs)) (rgs @ rcs)\ \ - rec_eval (rec_embranch (zip rgs rcs)) xs = 0" + rec_exec (rec_embranch (zip rgs rcs)) xs = 0" proof(induct rcs arbitrary: rgs, simp, case_tac rgs, simp) fix a rcs rgs aa list assume ind: - "\rgs. \\jrgs. \\j []; list_all (\rf. primerec rf (length xs)) (rgs @ rcs)\ \ - rec_eval (rec_embranch (zip rgs rcs)) xs = 0" - and h: "\jj []" "list_all (\rf. primerec rf (length xs)) (rgs @ a # rcs)" "rgs = aa # list" - have g: "rcs \ [] \ rec_eval (rec_embranch (zip list rcs)) xs = 0" + have g: "rcs \ [] \ rec_exec (rec_embranch (zip list rcs)) xs = 0" using h by(rule_tac ind, auto) - show "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0" + show "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0" proof(case_tac "rcs = []", simp) - show "rec_eval (rec_embranch (zip rgs [a])) xs = 0" + show "rec_exec (rec_embranch (zip rgs [a])) xs = 0" using h - apply(simp add: rec_embranch.simps rec_eval.simps) + apply(simp add: rec_embranch.simps rec_exec.simps) apply(erule_tac x = 0 in allE, simp) done next assume "rcs \ []" - hence "rec_eval (rec_embranch (zip list rcs)) xs = 0" + hence "rec_exec (rec_embranch (zip list rcs)) xs = 0" using g by simp - thus "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0" + thus "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0" using h - apply(simp add: rec_embranch.simps rec_eval.simps) + apply(simp add: rec_embranch.simps rec_exec.simps) apply(case_tac rcs, - auto simp: rec_eval.simps rec_embranch.simps) + auto simp: rec_exec.simps rec_embranch.simps) apply(case_tac list, - auto simp: rec_eval.simps rec_embranch.simps) + auto simp: rec_exec.simps rec_embranch.simps) done qed qed -lemma embranch_exec_0: "\rec_eval aa xs = 0; zip rgs list \ []; +lemma embranch_exec_0: "\rec_exec aa xs = 0; zip rgs list \ []; list_all (\ rf. primerec rf (length xs)) ([a, aa] @ rgs @ list)\ - \ rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs - = rec_eval (rec_embranch (zip rgs list)) xs" -apply(simp add: rec_eval.simps rec_embranch.simps) + \ rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs + = rec_exec (rec_embranch (zip rgs list)) xs" +apply(simp add: rec_exec.simps rec_embranch.simps) apply(case_tac "zip rgs list", simp, case_tac ab, - simp add: rec_embranch.simps rec_eval.simps) + simp add: rec_embranch.simps rec_exec.simps) apply(subgoal_tac "arity a = length xs", auto) apply(subgoal_tac "arity aaa = length xs", auto) apply(case_tac rgs, simp, case_tac list, simp, simp) @@ -1244,18 +1297,18 @@ lemma Embranch_0: "\length rgs = k; length rcs = k; k > 0; - \ j < k. rec_eval (rcs ! j) xs = 0\ \ - Embranch (zip (map rec_eval rgs) (map (\r args. 0 < rec_eval r args) rcs)) xs = 0" + \ j < k. rec_exec (rcs ! j) xs = 0\ \ + Embranch (zip (map rec_exec rgs) (map (\r args. 0 < rec_exec r args) rcs)) xs = 0" proof(induct rgs arbitrary: rcs k, simp, simp) fix a rgs rcs k assume ind: - "\rcs k. \length rgs = k; length rcs = k; 0 < k; \j - \ Embranch (zip (map rec_eval rgs) (map (\r args. 0 < rec_eval r args) rcs)) xs = 0" + "\rcs k. \length rgs = k; length rcs = k; 0 < k; \j + \ Embranch (zip (map rec_exec rgs) (map (\r args. 0 < rec_exec r args) rcs)) xs = 0" and h: "Suc (length rgs) = k" "length rcs = k" - "\jjr args. 0 < rec_eval r args) rcs)) xs = 0" + "Embranch (zip (rec_exec a # map rec_exec rgs) + (map (\r args. 0 < rec_exec r args) rcs)) xs = 0" apply(case_tac rcs, simp, case_tac "rgs = []", simp) apply(simp add: Embranch.simps) apply(erule_tac x = 0 in allE, simp) @@ -1273,51 +1326,51 @@ assumes branch_num: "length rgs = n" "length rcs = n" "n > 0" and partition: - "(\ i < n. (rec_eval (rcs ! i) xs = 1 \ (\ j < n. j \ i \ - rec_eval (rcs ! j) xs = 0)))" + "(\ i < n. (rec_exec (rcs ! i) xs = 1 \ (\ j < n. j \ i \ + rec_exec (rcs ! j) xs = 0)))" and prime_all: "list_all (\ rf. primerec rf (length xs)) (rgs @ rcs)" - shows "rec_eval (rec_embranch (zip rgs rcs)) xs = - Embranch (zip (map rec_eval rgs) - (map (\ r args. 0 < rec_eval r args) rcs)) xs" + shows "rec_exec (rec_embranch (zip rgs rcs)) xs = + Embranch (zip (map rec_exec rgs) + (map (\ r args. 0 < rec_exec r args) rcs)) xs" using branch_num partition prime_all proof(induct rgs arbitrary: rcs n, simp) fix a rgs rcs n assume ind: "\rcs n. \length rgs = n; length rcs = n; 0 < n; - \i (\j i \ rec_eval (rcs ! j) xs = 0); + \i (\j i \ rec_exec (rcs ! j) xs = 0); list_all (\rf. primerec rf (length xs)) (rgs @ rcs)\ - \ rec_eval (rec_embranch (zip rgs rcs)) xs = - Embranch (zip (map rec_eval rgs) (map (\r args. 0 < rec_eval r args) rcs)) xs" + \ rec_exec (rec_embranch (zip rgs rcs)) xs = + Embranch (zip (map rec_exec rgs) (map (\r args. 0 < rec_exec r args) rcs)) xs" and h: "length (a # rgs) = n" "length (rcs::recf list) = n" "0 < n" - " \i - (\j i \ rec_eval (rcs ! j) xs = 0)" + " \i + (\j i \ rec_exec (rcs ! j) xs = 0)" "list_all (\rf. primerec rf (length xs)) ((a # rgs) @ rcs)" - from h show "rec_eval (rec_embranch (zip (a # rgs) rcs)) xs = - Embranch (zip (map rec_eval (a # rgs)) (map (\r args. - 0 < rec_eval r args) rcs)) xs" + from h show "rec_exec (rec_embranch (zip (a # rgs) rcs)) xs = + Embranch (zip (map rec_exec (a # rgs)) (map (\r args. + 0 < rec_exec r args) rcs)) xs" apply(case_tac rcs, simp, simp) - apply(case_tac "rec_eval aa xs = 0") + apply(case_tac "rec_exec aa xs = 0") apply(case_tac [!] "zip rgs list = []", simp) - apply(subgoal_tac "rgs = [] \ list = []", simp add: Embranch.simps rec_eval.simps rec_embranch.simps) + apply(subgoal_tac "rgs = [] \ list = []", simp add: Embranch.simps rec_exec.simps rec_embranch.simps) apply(rule_tac zip_null_iff, simp, simp, simp) proof - fix aa list assume g: "Suc (length rgs) = n" "Suc (length list) = n" - "\i - (\j i \ rec_eval ((aa # list) ! j) xs = 0)" + "\i + (\j i \ rec_exec ((aa # list) ! j) xs = 0)" "primerec a (length xs) \ list_all (\rf. primerec rf (length xs)) rgs \ primerec aa (length xs) \ list_all (\rf. primerec rf (length xs)) list" - "rec_eval aa xs = 0" "rcs = aa # list" "zip rgs list \ []" - have "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs - = rec_eval (rec_embranch (zip rgs list)) xs" + "rec_exec aa xs = 0" "rcs = aa # list" "zip rgs list \ []" + have "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs + = rec_exec (rec_embranch (zip rgs list)) xs" apply(rule embranch_exec_0, simp_all add: g) done - from g and this show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs = - Embranch ((rec_eval a, \args. 0 < rec_eval aa args) # - zip (map rec_eval rgs) (map (\r args. 0 < rec_eval r args) list)) xs" + from g and this show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs = + Embranch ((rec_exec a, \args. 0 < rec_exec aa args) # + zip (map rec_exec rgs) (map (\r args. 0 < rec_exec r args) list)) xs" apply(simp add: Embranch.simps) apply(rule_tac n = "n - Suc 0" in ind) apply(case_tac n, simp, simp) @@ -1331,32 +1384,32 @@ next fix aa list assume g: "Suc (length rgs) = n" "Suc (length list) = n" - "\i - (\j i \ rec_eval ((aa # list) ! j) xs = 0)" + "\i + (\j i \ rec_exec ((aa # list) ! j) xs = 0)" "primerec a (length xs) \ list_all (\rf. primerec rf (length xs)) rgs \ primerec aa (length xs) \ list_all (\rf. primerec rf (length xs)) list" - "rcs = aa # list" "rec_eval aa xs \ 0" "zip rgs list = []" - thus "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs = - Embranch ((rec_eval a, \args. 0 < rec_eval aa args) # - zip (map rec_eval rgs) (map (\r args. 0 < rec_eval r args) list)) xs" + "rcs = aa # list" "rec_exec aa xs \ 0" "zip rgs list = []" + thus "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs = + Embranch ((rec_exec a, \args. 0 < rec_exec aa args) # + zip (map rec_exec rgs) (map (\r args. 0 < rec_exec r args) list)) xs" apply(subgoal_tac "rgs = [] \ list = []", simp) prefer 2 apply(rule_tac zip_null_iff, simp, simp, simp) - apply(simp add: rec_eval.simps rec_embranch.simps Embranch.simps, auto) + apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps, auto) done next fix aa list assume g: "Suc (length rgs) = n" "Suc (length list) = n" - "\i - (\j i \ rec_eval ((aa # list) ! j) xs = 0)" + "\i + (\j i \ rec_exec ((aa # list) ! j) xs = 0)" "primerec a (length xs) \ list_all (\rf. primerec rf (length xs)) rgs \ primerec aa (length xs) \ list_all (\rf. primerec rf (length xs)) list" - "rcs = aa # list" "rec_eval aa xs \ 0" "zip rgs list \ []" - have "rec_eval aa xs = Suc 0" + "rcs = aa # list" "rec_exec aa xs \ 0" "zip rgs list \ []" + have "rec_exec aa xs = Suc 0" using g - apply(case_tac "rec_eval aa xs", simp, auto) + apply(case_tac "rec_exec aa xs", simp, auto) done - moreover have "rec_eval (rec_embranch' (zip rgs list) (length xs)) xs = 0" + moreover have "rec_exec (rec_embranch' (zip rgs list) (length xs)) xs = 0" proof - have "rec_embranch' (zip rgs list) (length xs) = rec_embranch (zip rgs list)" using g @@ -1365,9 +1418,9 @@ apply(subgoal_tac "arity aaa = length xs", simp, auto) apply(case_tac rgs, simp, simp, case_tac list, simp, simp) done - moreover have "rec_eval (rec_embranch (zip rgs list)) xs = 0" + moreover have "rec_exec (rec_embranch (zip rgs list)) xs = 0" proof(rule embranch_all0) - show " \jjr args. 0 < rec_eval r args) list)) xs = 0" + "Embranch (zip (map rec_exec rgs) + (map (\r args. 0 < rec_exec r args) list)) xs = 0" using g apply(rule_tac k = "length rgs" in Embranch_0) apply(simp, case_tac n, simp, simp) @@ -1411,14 +1464,22 @@ using g apply(auto) done - ultimately show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs = - Embranch ((rec_eval a, \args. 0 < rec_eval aa args) # - zip (map rec_eval rgs) (map (\r args. 0 < rec_eval r args) list)) xs" - apply(simp add: rec_eval.simps rec_embranch.simps Embranch.simps) + ultimately show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs = + Embranch ((rec_exec a, \args. 0 < rec_exec aa args) # + zip (map rec_exec rgs) (map (\r args. 0 < rec_exec r args) list)) xs" + apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps) done qed qed +text{* + @{text "prime n"} means @{text "n"} is a prime number. +*} +fun Prime :: "nat \ bool" + where + "Prime x = (1 < x \ (\ u < x. (\ v < x. u * v \ x)))" + +declare Prime.simps [simp del] lemma primerec_all1: "primerec (rec_all rt rf) n \ primerec rt n" @@ -1444,10 +1505,10 @@ declare numeral_2_eq_2[simp del] numeral_3_eq_3[simp del] lemma exec_tmp: - "rec_eval (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) + "rec_exec (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])) [x, k] = - ((if (\w\rec_eval (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) ([x, k]). - 0 < rec_eval (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0]) + ((if (\w\rec_exec (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) ([x, k]). + 0 < rec_exec (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0]) ([x, k] @ [w])) then 1 else 0))" apply(rule_tac all_lemma) apply(auto) @@ -1458,8 +1519,8 @@ text {* The correctness of @{text "Prime"}. *} -lemma prime_lemma: "rec_eval rec_prime [x] = (if prime x then 1 else 0)" -proof(simp add: rec_eval.simps rec_prime_def) +lemma prime_lemma: "rec_exec rec_prime [x] = (if Prime x then 1 else 0)" +proof(simp add: rec_exec.simps rec_prime_def) let ?rt1 = "(Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]])" let ?rf1 = "(Cn 3 rec_noteq [Cn 3 rec_mult @@ -1467,8 +1528,8 @@ let ?rt2 = "(Cn (Suc 0) rec_minus [recf.id (Suc 0) 0, constn (Suc 0)])" let ?rf2 = "rec_all ?rt1 ?rf1" - have h1: "rec_eval (rec_all ?rt2 ?rf2) ([x]) = - (if (\k\rec_eval ?rt2 ([x]). 0 < rec_eval ?rf2 ([x] @ [k])) then 1 else 0)" + have h1: "rec_exec (rec_all ?rt2 ?rf2) ([x]) = + (if (\k\rec_exec ?rt2 ([x]). 0 < rec_exec ?rf2 ([x] @ [k])) then 1 else 0)" proof(rule_tac all_lemma, simp_all) show "primerec ?rf2 (Suc (Suc 0))" apply(rule_tac primerec_all_iff) @@ -1484,45 +1545,49 @@ done qed from h1 show - "(Suc 0 < x \ (rec_eval (rec_all ?rt2 ?rf2) [x] = 0 \ - \ prime x) \ - (0 < rec_eval (rec_all ?rt2 ?rf2) [x] \ prime x)) \ - (\ Suc 0 < x \ \ prime x \ (rec_eval (rec_all ?rt2 ?rf2) [x] = 0 - \ \ prime x))" - apply(auto simp:rec_eval.simps) - apply(simp add: exec_tmp rec_eval.simps) + "(Suc 0 < x \ (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \ + \ Prime x) \ + (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \ Prime x)) \ + (\ Suc 0 < x \ \ Prime x \ (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 + \ \ Prime x))" + apply(auto simp:rec_exec.simps) + apply(simp add: exec_tmp rec_exec.simps) proof - assume "\k\x - Suc 0. (0::nat) < (if \w\x - Suc 0. 0 < (if k * w \ x then 1 else (0 :: nat)) then 1 else 0)" "Suc 0 < x" - thus "prime x" - apply(simp add: rec_eval.simps split: if_splits) - apply(simp add: prime_nat_def dvd_def, auto) - apply(erule_tac x = m in allE, auto) - apply(case_tac m, simp, case_tac nat, simp, simp) - apply(case_tac k, simp, case_tac nat, simp, simp) + thus "Prime x" + apply(simp add: rec_exec.simps split: if_splits) + apply(simp add: Prime.simps, auto) + apply(erule_tac x = u in allE, auto) + apply(case_tac u, simp, case_tac nat, simp, simp) + apply(case_tac v, simp, case_tac nat, simp, simp) + done + next + assume "\ Suc 0 < x" "Prime x" + thus "False" + apply(simp add: Prime.simps) done next - assume "\ Suc 0 < x" "prime x" + fix k + assume "rec_exec (rec_all ?rt1 ?rf1) + [x, k] = 0" "k \ x - Suc 0" "Prime x" thus "False" - by (simp add: prime_nat_def) + apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits) + done next fix k - assume "rec_eval (rec_all ?rt1 ?rf1) - [x, k] = 0" "k \ x - Suc 0" "prime x" + assume "rec_exec (rec_all ?rt1 ?rf1) + [x, k] = 0" "k \ x - Suc 0" "Prime x" thus "False" - by (auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits) - next - fix k - assume "rec_eval (rec_all ?rt1 ?rf1) - [x, k] = 0" "k \ x - Suc 0" "prime x" - thus "False" - by(auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits) + apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits) + done qed qed definition rec_dummyfac :: "recf" where - "rec_dummyfac = Pr 1 (constn 1) (Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])" + "rec_dummyfac = Pr 1 (constn 1) + (Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])" text {* The recursive function used to implment factorization. @@ -1539,26 +1604,27 @@ "fac 0 = 1" | "fac (Suc x) = (Suc x) * fac x" -lemma [simp]: "rec_eval rec_dummyfac [0, 0] = Suc 0" -by(simp add: rec_dummyfac_def rec_eval.simps) - -lemma rec_cn_simp: - "rec_eval (Cn n f gs) xs = (let rgs = map (\ g. rec_eval g xs) gs in rec_eval f rgs)" -by(simp add: rec_eval.simps) - -lemma rec_id_simp: "rec_eval (id m n) xs = xs ! n" - by(simp add: rec_eval.simps) - -lemma fac_dummy: "rec_eval rec_dummyfac [x, y] = y !" +lemma [simp]: "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 = + (let rgs = map (\ g. rec_exec g xs) gs in + rec_exec f rgs)" +by(simp add: rec_exec.simps) + +lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n" + by(simp add: rec_exec.simps) + +lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !" apply(induct y) -apply(auto simp: rec_dummyfac_def rec_eval.simps) +apply(auto simp: rec_dummyfac_def rec_exec.simps) done text {* The correctness of @{text "rec_fac"}. *} -lemma fac_lemma: "rec_eval rec_fac [x] = x!" -apply(simp add: rec_fac_def rec_eval.simps fac_dummy) +lemma fac_lemma: "rec_exec rec_fac [x] = x!" +apply(simp add: rec_fac_def rec_exec.simps fac_dummy) done declare fac.simps[simp del] @@ -1568,7 +1634,7 @@ *} fun Np ::"nat \ nat" where - "Np x = Min {y. y \ Suc (x!) \ x < y \ prime y}" + "Np x = Min {y. y \ Suc (x!) \ x < y \ Prime y}" declare Np.simps[simp del] rec_Minr.simps[simp del] @@ -1589,17 +1655,15 @@ done lemma divsor_ex: -"\\ prime x; x > Suc 0\ \ (\ u > Suc 0. (\ v > Suc 0. u * v = x))" - apply(auto simp: prime_nat_def dvd_def) -by (metis Suc_lessI mult_0 nat_mult_commute neq0_conv) - - -lemma divsor_prime_ex: "\\ prime x; x > Suc 0\ \ - \ p. prime p \ p dvd x" +"\\ Prime x; x > Suc 0\ \ (\ u > Suc 0. (\ v > Suc 0. u * v = x))" + by(auto simp: Prime.simps) + +lemma divsor_prime_ex: "\\ Prime x; x > Suc 0\ \ + \ p. Prime p \ p dvd x" apply(induct x rule: wf_induct[where r = "measure (\ y. y)"], simp) apply(drule_tac divsor_ex, simp, auto) apply(erule_tac x = u in allE, simp) -apply(case_tac "prime u", simp) +apply(case_tac "Prime u", simp) apply(rule_tac x = u in exI, simp, auto) done @@ -1637,15 +1701,15 @@ by(simp add: add_mult_distrib2) qed -lemma prime_ex: "\ p. n < p \ p \ Suc (n!) \ prime p" -proof(cases "prime (n! + 1)") +lemma prime_ex: "\ p. n < p \ p \ Suc (n!) \ Prime p" +proof(cases "Prime (n! + 1)") case True thus "?thesis" by(rule_tac x = "Suc (n!)" in exI, simp) next - assume h: "\ prime (n! + 1)" - hence "\ p. prime p \ p dvd (n! + 1)" + assume h: "\ Prime (n! + 1)" + hence "\ p. Prime p \ p dvd (n! + 1)" by(erule_tac divsor_prime_ex, auto) - from this obtain q where k: "prime q \ q dvd (n! + 1)" .. + from this obtain q where k: "Prime q \ q dvd (n! + 1)" .. thus "?thesis" proof(cases "q > n") case True thus "?thesis" @@ -1658,7 +1722,7 @@ proof - assume g: "\ n < q" have j: "q > Suc 0" - using k by(case_tac q, auto simp: prime_nat_def dvd_def) + using k by(case_tac q, auto simp: Prime.simps) hence "q dvd n!" using g apply(rule_tac fac_dvd, auto) @@ -1686,25 +1750,25 @@ text {* The correctness of @{text "rec_np"}. *} -lemma np_lemma: "rec_eval rec_np [x] = Np x" -proof(auto simp: rec_np_def rec_eval.simps Let_def fac_lemma) +lemma np_lemma: "rec_exec rec_np [x] = Np x" +proof(auto simp: rec_np_def rec_exec.simps Let_def fac_lemma) let ?rr = "(Cn 2 rec_conj [Cn 2 rec_less [recf.id 2 0, recf.id 2 (Suc 0)], Cn 2 rec_prime [recf.id 2 (Suc 0)]])" - let ?R = "\ zs. zs ! 0 < zs ! 1 \ prime (zs ! 1)" - have g1: "rec_eval (rec_Minr ?rr) ([x] @ [Suc (x!)]) = - Minr (\ args. 0 < rec_eval ?rr args) [x] (Suc (x!))" - by(rule_tac Minr_lemma, auto simp: rec_eval.simps + let ?R = "\ zs. zs ! 0 < zs ! 1 \ Prime (zs ! 1)" + have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) = + Minr (\ args. 0 < rec_exec ?rr args) [x] (Suc (x!))" + by(rule_tac Minr_lemma, auto simp: rec_exec.simps prime_lemma, auto simp: numeral_2_eq_2 numeral_3_eq_3) - have g2: "Minr (\ args. 0 < rec_eval ?rr args) [x] (Suc (x!)) = Np x" + have g2: "Minr (\ args. 0 < rec_exec ?rr args) [x] (Suc (x!)) = Np x" using prime_ex[of x] - apply(auto simp: Minr.simps Np.simps rec_eval.simps) + apply(auto simp: Minr.simps Np.simps rec_exec.simps) apply(erule_tac x = p in allE, simp add: prime_lemma) apply(simp add: prime_lemma split: if_splits) apply(subgoal_tac - "{uu. (prime uu \ (x < uu \ uu \ Suc (x!)) \ x < uu) \ prime uu} - = {y. y \ Suc (x!) \ x < y \ prime y}", auto) + "{uu. (Prime uu \ (x < uu \ uu \ Suc (x!)) \ x < uu) \ Prime uu} + = {y. y \ Suc (x!) \ x < y \ Prime y}", auto) done - from g1 and g2 show "rec_eval (rec_Minr ?rr) ([x, Suc (x!)]) = Np x" + from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x" by simp qed @@ -1719,8 +1783,8 @@ text {* The correctness of @{text "rec_power"}. *} -lemma power_lemma: "rec_eval rec_power [x, y] = x^y" - by(induct y, auto simp: rec_eval.simps rec_power_def) +lemma power_lemma: "rec_exec rec_power [x, y] = x^y" + by(induct y, auto simp: rec_exec.simps rec_power_def) text{* @{text "Pi k"} returns the @{text "k"}-th prime number. @@ -1742,15 +1806,15 @@ where "rec_pi = Cn 1 rec_dummy_pi [id 1 0, id 1 0]" -lemma pi_dummy_lemma: "rec_eval rec_dummy_pi [x, y] = Pi y" +lemma pi_dummy_lemma: "rec_exec rec_dummy_pi [x, y] = Pi y" apply(induct y) -by(auto simp: rec_eval.simps rec_dummy_pi_def Pi.simps np_lemma) +by(auto simp: rec_exec.simps rec_dummy_pi_def Pi.simps np_lemma) text {* The correctness of @{text "rec_pi"}. *} -lemma pi_lemma: "rec_eval rec_pi [x] = Pi x" -apply(simp add: rec_pi_def rec_eval.simps pi_dummy_lemma) +lemma pi_lemma: "rec_exec rec_pi [x] = Pi x" +apply(simp add: rec_pi_def rec_exec.simps pi_dummy_lemma) done fun loR :: "nat list \ bool" @@ -1833,23 +1897,23 @@ lemma rec_lo_Maxr_lor: "\Suc 0 < x; Suc 0 < y\ \ - rec_eval rec_lo [x, y] = Maxr loR [x, y] x" -proof(auto simp: rec_eval.simps rec_lo_def Let_def + rec_exec rec_lo [x, y] = Maxr loR [x, y] x" +proof(auto simp: rec_exec.simps rec_lo_def Let_def numeral_2_eq_2 numeral_3_eq_3) let ?rR = "(Cn (Suc (Suc (Suc 0))) rec_eq [Cn (Suc (Suc (Suc 0))) rec_mod [recf.id (Suc (Suc (Suc 0))) 0, Cn (Suc (Suc (Suc 0))) rec_power [recf.id (Suc (Suc (Suc 0))) (Suc 0), recf.id (Suc (Suc (Suc 0))) (Suc (Suc 0))]], Cn (Suc (Suc (Suc 0))) (constn 0) [recf.id (Suc (Suc (Suc 0))) (Suc 0)]])" - have h: "rec_eval (rec_maxr ?rR) ([x, y] @ [x]) = - Maxr (\ args. 0 < rec_eval ?rR args) [x, y] x" - by(rule_tac Maxr_lemma, auto simp: rec_eval.simps + have h: "rec_exec (rec_maxr ?rR) ([x, y] @ [x]) = + Maxr (\ args. 0 < rec_exec ?rR args) [x, y] x" + by(rule_tac Maxr_lemma, auto simp: rec_exec.simps mod_lemma power_lemma, auto simp: numeral_2_eq_2 numeral_3_eq_3) - have "Maxr loR [x, y] x = Maxr (\ args. 0 < rec_eval ?rR args) [x, y] x" - apply(simp add: rec_eval.simps mod_lemma power_lemma) + have "Maxr loR [x, y] x = Maxr (\ args. 0 < rec_exec ?rR args) [x, y] x" + apply(simp add: rec_exec.simps mod_lemma power_lemma) apply(simp add: Maxr.simps loR.simps) done - from h and this show "rec_eval (rec_maxr ?rR) [x, y, x] = + from h and this show "rec_exec (rec_maxr ?rR) [x, y, x] = Maxr loR [x, y] x" apply(simp) done @@ -1901,23 +1965,23 @@ done lemma lo_lemma': "\Suc 0 < x; Suc 0 < y\ \ - rec_eval rec_lo [x, y] = lo x y" + rec_exec rec_lo [x, y] = lo x y" by(simp add: Maxr_lo rec_lo_Maxr_lor) -lemma lo_lemma'': "\\ Suc 0 < x\ \ rec_eval rec_lo [x, y] = lo x y" -apply(case_tac x, auto simp: rec_eval.simps rec_lo_def +lemma lo_lemma'': "\\ Suc 0 < x\ \ rec_exec rec_lo [x, y] = lo x y" +apply(case_tac x, auto simp: rec_exec.simps rec_lo_def Let_def lo.simps) done -lemma lo_lemma''': "\\ Suc 0 < y\ \ rec_eval rec_lo [x, y] = lo x y" -apply(case_tac y, auto simp: rec_eval.simps rec_lo_def +lemma lo_lemma''': "\\ Suc 0 < y\ \ rec_exec rec_lo [x, y] = lo x y" +apply(case_tac y, auto simp: rec_exec.simps rec_lo_def Let_def lo.simps) done text {* The correctness of @{text "rec_lo"}: *} -lemma lo_lemma: "rec_eval rec_lo [x, y] = lo x y" +lemma lo_lemma: "rec_exec rec_lo [x, y] = lo x y" apply(case_tac "Suc 0 < x \ Suc 0 < y") apply(auto simp: lo_lemma' lo_lemma'' lo_lemma''') done @@ -1944,34 +2008,38 @@ *} definition rec_lg :: "recf" where - "rec_lg = - (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in - let conR1 = Cn 2 rec_conj [Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 0], - Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 1]] in - let conR2 = Cn 2 rec_not [conR1] in - Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR) - [id 2 0, id 2 1, id 2 0]], - Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])" + "rec_lg = (let rec_lgR = Cn 3 rec_le + [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in + let conR1 = Cn 2 rec_conj [Cn 2 rec_less + [Cn 2 (constn 1) [id 2 0], id 2 0], + Cn 2 rec_less [Cn 2 (constn 1) + [id 2 0], id 2 1]] in + let conR2 = Cn 2 rec_not [conR1] in + Cn 2 rec_add [Cn 2 rec_mult + [conR1, Cn 2 (rec_maxr rec_lgR) + [id 2 0, id 2 1, id 2 0]], + Cn 2 rec_mult [conR2, Cn 2 (constn 0) + [id 2 0]]])" lemma lg_maxr: "\Suc 0 < x; Suc 0 < y\ \ - rec_eval rec_lg [x, y] = Maxr lgR [x, y] x" -proof(simp add: rec_eval.simps rec_lg_def Let_def) + rec_exec rec_lg [x, y] = Maxr lgR [x, y] x" +proof(simp add: rec_exec.simps rec_lg_def Let_def) assume h: "Suc 0 < x" "Suc 0 < y" let ?rR = "(Cn 3 rec_le [Cn 3 rec_power [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])" - have "rec_eval (rec_maxr ?rR) ([x, y] @ [x]) - = Maxr ((\ args. 0 < rec_eval ?rR args)) [x, y] x" + have "rec_exec (rec_maxr ?rR) ([x, y] @ [x]) + = Maxr ((\ args. 0 < rec_exec ?rR args)) [x, y] x" proof(rule Maxr_lemma) show "primerec (Cn 3 rec_le [Cn 3 rec_power [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0]) (Suc (length [x, y]))" apply(auto simp: numeral_3_eq_3)+ done qed - moreover have "Maxr lgR [x, y] x = Maxr ((\ args. 0 < rec_eval ?rR args)) [x, y] x" - apply(simp add: rec_eval.simps power_lemma) + moreover have "Maxr lgR [x, y] x = Maxr ((\ args. 0 < rec_exec ?rR args)) [x, y] x" + apply(simp add: rec_exec.simps power_lemma) apply(simp add: Maxr.simps lgR.simps) done - ultimately show "rec_eval (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x" + ultimately show "rec_exec (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x" by simp qed @@ -1991,22 +2059,22 @@ apply(erule_tac x = xa in allE, simp) done -lemma lg_lemma': "\Suc 0 < x; Suc 0 < y\ \ rec_eval rec_lg [x, y] = lg x y" +lemma lg_lemma': "\Suc 0 < x; Suc 0 < y\ \ rec_exec rec_lg [x, y] = lg x y" apply(simp add: maxr_lg lg_maxr) done -lemma lg_lemma'': "\ Suc 0 < x \ rec_eval rec_lg [x, y] = lg x y" -apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps) +lemma lg_lemma'': "\ Suc 0 < x \ rec_exec rec_lg [x, y] = lg x y" +apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps) done -lemma lg_lemma''': "\ Suc 0 < y \ rec_eval rec_lg [x, y] = lg x y" -apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps) +lemma lg_lemma''': "\ Suc 0 < y \ rec_exec rec_lg [x, y] = lg x y" +apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps) done text {* The correctness of @{text "rec_lg"}. *} -lemma lg_lemma: "rec_eval rec_lg [x, y] = lg x y" +lemma lg_lemma: "rec_exec rec_lg [x, y] = lg x y" apply(case_tac "Suc 0 < x \ Suc 0 < y", auto simp: lg_lemma' lg_lemma'' lg_lemma''') done @@ -2032,8 +2100,8 @@ text {* The correctness of @{text "rec_entry"}. *} -lemma entry_lemma: "rec_eval rec_entry [str, i] = Entry str i" - by(simp add: rec_entry_def rec_eval.simps lo_lemma pi_lemma) +lemma entry_lemma: "rec_exec rec_entry [str, i] = Entry str i" + by(simp add: rec_entry_def rec_exec.simps lo_lemma pi_lemma) subsection {* The construction of F *} @@ -2057,9 +2125,9 @@ declare listsum2.simps[simp del] rec_listsum2.simps[simp del] lemma listsum2_lemma: "\length xs = vl; n \ vl\ \ - rec_eval (rec_listsum2 vl n) xs = listsum2 xs n" + rec_exec (rec_listsum2 vl n) xs = listsum2 xs n" apply(induct n, simp_all) -apply(simp_all add: rec_eval.simps rec_listsum2.simps listsum2.simps) +apply(simp_all add: rec_exec.simps rec_listsum2.simps listsum2.simps) done fun strt' :: "nat list \ nat \ nat" @@ -2081,9 +2149,9 @@ declare strt'.simps[simp del] rec_strt'.simps[simp del] lemma strt'_lemma: "\length xs = vl; n \ vl\ \ - rec_eval (rec_strt' vl n) xs = strt' xs n" + rec_exec (rec_strt' vl n) xs = strt' xs n" apply(induct n) -apply(simp_all add: rec_eval.simps rec_strt'.simps strt'.simps +apply(simp_all add: rec_exec.simps rec_strt'.simps strt'.simps Let_def power_lemma listsum2_lemma) done @@ -2108,30 +2176,30 @@ "rec_strt vl = Cn vl (rec_strt' vl vl) (rec_map s vl)" lemma map_s_lemma: "length xs = vl \ - map ((\a. rec_eval a xs) \ (\i. Cn vl s [recf.id vl i])) + map ((\a. rec_exec a xs) \ (\i. Cn vl s [recf.id vl i])) [0.. ys y. xs = ys @ [y]", auto) proof - fix ys y assume ind: "\xs. length xs = length (ys::nat list) \ - map ((\a. rec_eval a xs) \ (\i. Cn (length ys) s + map ((\a. rec_exec a xs) \ (\i. Cn (length ys) s [recf.id (length ys) (i)])) [0..a. rec_eval a (ys @ [y])) \ (\i. Cn (Suc (length ys)) s + "map ((\a. rec_exec a (ys @ [y])) \ (\i. Cn (Suc (length ys)) s [recf.id (Suc (length ys)) (i)])) [0..a. rec_eval a ys) \ (\i. Cn (length ys) s + have "map ((\a. rec_exec a ys) \ (\i. Cn (length ys) s [recf.id (length ys) (i)])) [0..a. rec_eval a (ys @ [y])) \ (\i. Cn (Suc (length ys)) s + "map ((\a. rec_exec a (ys @ [y])) \ (\i. Cn (Suc (length ys)) s [recf.id (Suc (length ys)) (i)])) [0..a. rec_eval a ys) \ (\i. Cn (length ys) s + = map ((\a. rec_exec a ys) \ (\i. Cn (length ys) s [recf.id (length ys) (i)])) [0.. - rec_eval (rec_strt vl) xs = strt xs" -apply(simp add: strt.simps rec_eval.simps strt'_lemma) -apply(subgoal_tac "(map ((\a. rec_eval a xs) \ (\i. Cn vl s [recf.id vl (i)])) [0..a. rec_exec a xs) \ (\i. Cn vl s [recf.id vl (i)])) [0.. nat" where @@ -2295,7 +2363,7 @@ The correctness of @{text "rec_newleft"}. *} lemma newleft_lemma: - "rec_eval rec_newleft [p, r, a] = newleft p r a" + "rec_exec rec_newleft [p, r, a] = newleft p r a" proof(simp only: rec_newleft_def Let_def) let ?rgs = "[Cn 3 rec_newleft0 [recf.id 3 0, recf.id 3 1], Cn 3 rec_newleft2 [recf.id 3 0, recf.id 3 1], Cn 3 rec_newleft3 [recf.id 3 0, recf.id 3 1], recf.id 3 0]" @@ -2305,8 +2373,8 @@ Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]], Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]], Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]" - have k1: "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] - = Embranch (zip (map rec_eval ?rgs) (map (\r args. 0 < rec_eval r args) ?rrs)) [p, r, a]" + have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] + = Embranch (zip (map rec_exec ?rgs) (map (\r args. 0 < rec_exec r args) ?rrs)) [p, r, a]" apply(rule_tac embranch_lemma ) apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newleft0_def rec_newleft1_def rec_newleft2_def rec_newleft3_def)+ @@ -2317,17 +2385,17 @@ apply(case_tac "a = 3", rule_tac x = "2" in exI) prefer 2 apply(case_tac "a > 3", rule_tac x = "3" in exI, auto) - apply(auto simp: rec_eval.simps) - apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_eval.simps) + apply(auto simp: rec_exec.simps) + apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_exec.simps) done - have k2: "Embranch (zip (map rec_eval ?rgs) (map (\r args. 0 < rec_eval r args) ?rrs)) [p, r, a] = newleft p r a" + have k2: "Embranch (zip (map rec_exec ?rgs) (map (\r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newleft p r a" apply(simp add: Embranch.simps) - apply(simp add: rec_eval.simps) - apply(auto simp: newleft.simps rec_newleft0_def rec_eval.simps + apply(simp add: rec_exec.simps) + apply(auto simp: newleft.simps rec_newleft0_def rec_exec.simps rec_newleft1_def rec_newleft2_def rec_newleft3_def) done from k1 and k2 show - "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a" + "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a" by simp qed @@ -2384,7 +2452,7 @@ text {* The correctness of @{text "rec_newrght"}. *} -lemma newrght_lemma: "rec_eval rec_newrght [p, r, a] = newrght p r a" +lemma newrght_lemma: "rec_exec rec_newrght [p, r, a] = newrght p r a" proof(simp only: rec_newrght_def Let_def) let ?gs' = "[newrgt0, newrgt1, newrgt2, newrgt3, \ zs. zs ! 1]" let ?r0 = "\ zs. zs ! 2 = 0" @@ -2405,8 +2473,8 @@ Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]], Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]" - have k1: "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] - = Embranch (zip (map rec_eval ?rgs) (map (\r args. 0 < rec_eval r args) ?rrs)) [p, r, a]" + have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] + = Embranch (zip (map rec_exec ?rgs) (map (\r args. 0 < rec_exec r args) ?rrs)) [p, r, a]" apply(rule_tac embranch_lemma) apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newrgt0_def rec_newrgt1_def rec_newrgt2_def rec_newrgt3_def)+ @@ -2418,18 +2486,18 @@ prefer 2 apply(case_tac "a = 3", rule_tac x = "3" in exI) prefer 2 - apply(case_tac "a > 3", rule_tac x = "4" in exI, auto simp: rec_eval.simps) - apply(erule_tac [!] Suc_5_induct, auto simp: rec_eval.simps) + apply(case_tac "a > 3", rule_tac x = "4" in exI, auto simp: rec_exec.simps) + apply(erule_tac [!] Suc_5_induct, auto simp: rec_exec.simps) done - have k2: "Embranch (zip (map rec_eval ?rgs) - (map (\r args. 0 < rec_eval r args) ?rrs)) [p, r, a] = newrght p r a" - apply(auto simp:Embranch.simps rec_eval.simps) + have k2: "Embranch (zip (map rec_exec ?rgs) + (map (\r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newrght p r a" + apply(auto simp:Embranch.simps rec_exec.simps) apply(auto simp: newrght.simps rec_newrgt3_def rec_newrgt2_def - rec_newrgt1_def rec_newrgt0_def rec_eval.simps + rec_newrgt1_def rec_newrgt0_def rec_exec.simps scan_lemma) done from k1 and k2 show - "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = + "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newrght p r a" by simp qed @@ -2466,8 +2534,8 @@ text {* The correctness of @{text "actn"}. *} -lemma actn_lemma: "rec_eval rec_actn [m, q, r] = actn m q r" - by(auto simp: rec_actn_def rec_eval.simps entry_lemma scan_lemma) +lemma actn_lemma: "rec_exec rec_actn [m, q, r] = actn m q r" + by(auto simp: rec_actn_def rec_exec.simps entry_lemma scan_lemma) fun newstat :: "nat \ nat \ nat \ nat" where @@ -2486,8 +2554,8 @@ Cn 3 rec_mult [Cn 3 (constn 0) [id 3 0], Cn 3 rec_eq [id 3 1, Cn 3 (constn 0) [id 3 0]]]] " -lemma newstat_lemma: "rec_eval rec_newstat [m, q, r] = newstat m q r" -by(auto simp: rec_eval.simps entry_lemma scan_lemma rec_newstat_def) +lemma newstat_lemma: "rec_exec rec_newstat [m, q, r] = newstat m q r" +by(auto simp: rec_exec.simps entry_lemma scan_lemma rec_newstat_def) declare newstat.simps[simp del] actn.simps[simp del] @@ -2504,8 +2572,8 @@ Cn 3 rec_power [Cn 3 (constn (Pi 1)) [id 3 0], id 3 1]], Cn 3 rec_power [Cn 3 (constn (Pi 2)) [id 3 0], id 3 2]]" declare trpl.simps[simp del] -lemma trpl_lemma: "rec_eval rec_trpl [p, q, r] = trpl p q r" -by(auto simp: rec_trpl_def rec_eval.simps power_lemma trpl.simps) +lemma trpl_lemma: "rec_exec rec_trpl [p, q, r] = trpl p q r" +by(auto simp: rec_trpl_def rec_exec.simps power_lemma trpl.simps) text{*left, stat, rght: decode func*} fun left :: "nat \ nat" @@ -2555,24 +2623,24 @@ Cn vl (rec_strt (vl - 1)) (map (\ i. id vl (i)) [1..a. rec_eval a (m # xs)) \ + "(map ((\a. rec_exec a (m # xs)) \ (\i. recf.id (Suc (length xs)) (i))) [Suc 0.. i. xs ! (i - 1)) [Suc 0.. length xs \ - (map ((\a. rec_eval a (m # xs)) \ + (map ((\a. rec_exec a (m # xs)) \ (\i. recf.id (Suc (length xs)) (i))) [Suc 0..Suc (length xs) = vl\ \ - rec_eval (rec_inpt vl) (m # xs) = inpt m xs" -apply(auto simp: rec_eval.simps rec_inpt_def + rec_exec (rec_inpt vl) (m # xs) = inpt m xs" +apply(auto simp: rec_exec.simps rec_inpt_def trpl_lemma inpt.simps strt_lemma) apply(subgoal_tac - "(map ((\a. rec_eval a (m # xs)) \ + "(map ((\a. rec_exec a (m # xs)) \ (\i. recf.id (Suc (length xs)) (i))) [Suc 0.. - rec_eval rec_NSTD [c] = 0" -by(simp add: rec_eval.simps rec_NSTD_def) +lemma NSTD_lemma1: "rec_exec rec_NSTD [c] = Suc 0 \ + rec_exec rec_NSTD [c] = 0" +by(simp add: rec_exec.simps rec_NSTD_def) declare NSTD.simps[simp del] -lemma NSTD_lemma2': "(rec_eval rec_NSTD [c] = Suc 0) \ NSTD c" -apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma left_lemma +lemma NSTD_lemma2': "(rec_exec rec_NSTD [c] = Suc 0) \ NSTD c" +apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma left_lemma lg_lemma right_lemma power_lemma NSTD.simps eq_lemma) apply(auto) apply(case_tac "0 < left c", simp, simp) done lemma NSTD_lemma2'': - "NSTD c \ (rec_eval rec_NSTD [c] = Suc 0)" -apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma + "NSTD c \ (rec_exec rec_NSTD [c] = Suc 0)" +apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma left_lemma lg_lemma right_lemma power_lemma NSTD.simps) apply(auto split: if_splits) done @@ -2757,7 +2825,7 @@ text {* The correctness of @{text "NSTD"}. *} -lemma NSTD_lemma2: "(rec_eval rec_NSTD [c] = Suc 0) = NSTD c" +lemma NSTD_lemma2: "(rec_exec rec_NSTD [c] = Suc 0) = NSTD c" using NSTD_lemma1 apply(auto intro: NSTD_lemma2' NSTD_lemma2'') done @@ -2766,7 +2834,7 @@ where "nstd c = (if NSTD c then 1 else 0)" -lemma nstd_lemma: "rec_eval rec_NSTD [c] = nstd c" +lemma nstd_lemma: "rec_exec rec_NSTD [c] = nstd c" using NSTD_lemma1 apply(simp add: NSTD_lemma2, auto) done @@ -2790,8 +2858,8 @@ The correctness of @{text "rec_nonstop"}. *} lemma nonstop_lemma: - "rec_eval rec_nonstop [m, r, t] = nonstop m r t" -apply(simp add: rec_eval.simps rec_nonstop_def nstd_lemma conf_lemma) + "rec_exec rec_nonstop [m, r, t] = nonstop m r t" +apply(simp add: rec_exec.simps rec_nonstop_def nstd_lemma conf_lemma) done text{* @@ -2985,51 +3053,51 @@ @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ done -lemma primerec_terminates: - "\primerec f x; length xs = x\ \ terminates f xs" +lemma primerec_terminate: + "\primerec f x; length xs = x\ \ terminate f xs" proof(induct arbitrary: xs rule: primerec.induct) fix xs - assume "length (xs::nat list) = Suc 0" thus "terminates z xs" + assume "length (xs::nat list) = Suc 0" thus "terminate z xs" by(case_tac xs, auto intro: termi_z) next fix xs - assume "length (xs::nat list) = Suc 0" thus "terminates s xs" + assume "length (xs::nat list) = Suc 0" thus "terminate s xs" by(case_tac xs, auto intro: termi_s) next fix n m xs - assume "n < m" "length (xs::nat list) = m" thus "terminates (id m n) xs" + assume "n < m" "length (xs::nat list) = m" thus "terminate (id m n) xs" by(erule_tac termi_id, simp) next fix f k gs m n xs - assume ind: "\i (\x. length x = m \ terminates (gs ! i) x)" - and ind2: "\ xs. length xs = k \ terminates f xs" + assume ind: "\i (\x. length x = m \ terminate (gs ! i) x)" + and ind2: "\ xs. length xs = k \ terminate f xs" and h: "primerec f k" "length gs = k" "m = n" "length (xs::nat list) = m" - have "terminates f (map (\g. rec_eval g xs) gs)" - using ind2[of "(map (\g. rec_eval g xs) gs)"] h + have "terminate f (map (\g. rec_exec g xs) gs)" + using ind2[of "(map (\g. rec_exec g xs) gs)"] h by simp - moreover have "\g\set gs. terminates g xs" + moreover have "\g\set gs. terminate g xs" using ind h by(auto simp: set_conv_nth) - ultimately show "terminates (Cn n f gs) xs" + ultimately show "terminate (Cn n f gs) xs" using h by(rule_tac termi_cn, auto) next fix f n g m xs - assume ind1: "\xs. length xs = n \ terminates f xs" - and ind2: "\xs. length xs = Suc (Suc n) \ terminates g xs" + assume ind1: "\xs. length xs = n \ terminate f xs" + 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 "\yy (get_fstn_args m n ! k) = id m (k)" @@ -3101,12 +3167,12 @@ id (length ys) (k)" by(erule_tac get_fstn_args_nth) -lemma terminates_halt_lemma: - "\rec_eval rec_nonstop ([m, r] @ [t]) = 0; - \i \ terminates rec_halt [m, r]" +lemma terminate_halt_lemma: + "\rec_exec rec_nonstop ([m, r] @ [t]) = 0; + \i \ terminate rec_halt [m, r]" apply(simp add: rec_halt_def) apply(rule_tac termi_mn, auto) -apply(rule_tac [!] primerec_terminates, auto) +apply(rule_tac [!] primerec_terminate, auto) done @@ -3114,17 +3180,17 @@ The correctness of @{text "rec_F"}, halt case. *} -lemma F_lemma: "rec_eval rec_halt [m, r] = t \ rec_eval rec_F [m, r] = (valu (rght (conf m r t)))" -by(simp add: rec_F_def rec_eval.simps value_lemma right_lemma conf_lemma halt_lemma) - -lemma terminates_F_lemma: "terminates rec_halt [m, r] \ terminates rec_F [m, r]" +lemma F_lemma: "rec_exec rec_halt [m, r] = t \ rec_exec rec_F [m, r] = (valu (rght (conf m r t)))" +by(simp add: rec_F_def rec_exec.simps value_lemma right_lemma conf_lemma halt_lemma) + +lemma terminate_F_lemma: "terminate rec_halt [m, r] \ terminate rec_F [m, r]" apply(simp add: rec_F_def) apply(rule_tac termi_cn, auto) -apply(rule_tac primerec_terminates, auto) +apply(rule_tac primerec_terminate, auto) apply(rule_tac termi_cn, auto) -apply(rule_tac primerec_terminates, auto) +apply(rule_tac primerec_terminate, auto) apply(rule_tac termi_cn, auto) -apply(rule_tac primerec_terminates, auto) +apply(rule_tac primerec_terminate, auto) apply(rule_tac [!] termi_id, auto) done @@ -3211,7 +3277,7 @@ lemma Pi_gr_1[simp]: "Pi n > Suc 0" proof(induct n, auto simp: Pi.simps Np.simps) fix n - let ?setx = "{y. y \ Suc (Pi n!) \ Pi n < y \ prime y}" + let ?setx = "{y. y \ Suc (Pi n!) \ Pi n < y \ Prime y}" have "finite ?setx" by auto moreover have "?setx \ {}" using prime_ex[of "Pi n"] @@ -3219,7 +3285,7 @@ done ultimately show "Suc 0 < Min ?setx" apply(simp add: Min_gr_iff) - apply(auto simp: prime_nat_def dvd_def) + apply(auto simp: Prime.simps) done qed @@ -3248,9 +3314,49 @@ 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, + rule_tac classical, simp) + fix d k ka + assume case_ka: "\uv d * ka" + and case_k: "\uv d * k" + 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 + from this show "False" + proof(erule_tac disjE) + assume "(Suc 0::nat) < k" + hence "k < d*k \ d < d*k" + using h + by(auto) + thus "?thesis" + using case_k + apply(erule_tac x = d in allE) + apply(simp) + apply(erule_tac x = k in allE) + apply(simp) + done + next + assume "(Suc 0::nat) < ka" + hence "ka < d * ka \ d < d*ka" + using h by auto + thus "?thesis" + using case_ka + apply(erule_tac x = d in allE) + apply(simp) + apply(erule_tac x = ka in allE) + apply(simp) + done + qed +qed + lemma Pi_inc: "Pi (Suc i) > Pi i" proof(simp add: Pi.simps Np.simps) - let ?setx = "{y. y \ Suc (Pi i!) \ Pi i < y \ prime y}" + let ?setx = "{y. y \ Suc (Pi i!) \ Pi i < y \ Prime y}" have "finite ?setx" by simp moreover have "?setx \ {}" using prime_ex[of "Pi i"] @@ -3296,16 +3402,16 @@ apply(simp) done -lemma [intro]: "prime (Suc (Suc 0))" -apply(auto simp: prime_nat_def dvd_def) -apply(case_tac m, simp, case_tac k, simp, simp) +lemma [intro]: "Prime (Suc (Suc 0))" +apply(auto simp: Prime.simps) +apply(case_tac u, simp, case_tac nat, simp, simp) done -lemma Prime_Pi[intro]: "prime (Pi n)" +lemma Prime_Pi[intro]: "Prime (Pi n)" proof(induct n, auto simp: Pi.simps Np.simps) fix n - let ?setx = "{y. y \ Suc (Pi n!) \ Pi n < y \ prime y}" - show "prime (Min ?setx)" + let ?setx = "{y. y \ Suc (Pi n!) \ Pi n < y \ Prime y}" + show "Prime (Min ?setx)" proof - have "finite ?setx" by simp moreover have "?setx \ {}" @@ -3321,7 +3427,7 @@ lemma Pi_coprime: "i \ j \ coprime (Pi i) (Pi j)" using Prime_Pi[of i] using Prime_Pi[of j] -apply(rule_tac primes_coprime_nat, simp_all add: Pi_notEq) +apply(rule_tac prime_coprime, simp_all add: Pi_notEq) done lemma Pi_power_coprime: "i \ j \ coprime ((Pi i)^m) ((Pi j)^n)" @@ -3417,7 +3523,7 @@ 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 primes_coprime_nat, auto) + apply(rule_tac coprime_exp_nat, rule prime_coprime, auto) using Pi_notEq[of "Suc i" "length ps"] h by simp qed from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))" @@ -4001,7 +4107,7 @@ lemma rec_t_eq_step: "(\ (s, l, r). s \ length tp div 2) c \ trpl_code (step0 c tp) = - rec_eval rec_newconf [code tp, trpl_code c]" + rec_exec rec_newconf [code tp, trpl_code c]" apply(cases c, simp) proof(case_tac "fetch tp a (read ca)", simp add: newconf.simps trpl_code.simps step.simps) @@ -4163,8 +4269,8 @@ lemma [simp]: "trpl_code (steps0 (Suc 0, Bk\l, ) tp 0) = - rec_eval rec_conf [code tp, bl2wc (), 0]" -apply(simp add: steps.simps rec_eval.simps conf_lemma conf.simps + rec_exec rec_conf [code tp, bl2wc (), 0]" +apply(simp add: steps.simps rec_exec.simps conf_lemma conf.simps inpt.simps trpl_code.simps bl2wc.simps) done @@ -4212,7 +4318,7 @@ lemma rec_t_eq_steps: "tm_wf (tp,0) \ trpl_code (steps0 (Suc 0, Bk\l, ) tp stp) = - rec_eval rec_conf [code tp, bl2wc (), stp]" + rec_exec rec_conf [code tp, bl2wc (), stp]" proof(induct stp) case 0 thus "?case" by(simp) next @@ -4220,11 +4326,11 @@ proof - assume ind: "tm_wf (tp,0) \ trpl_code (steps0 (Suc 0, Bk\ l, ) tp n) - = rec_eval rec_conf [code tp, bl2wc (), n]" + = rec_exec rec_conf [code tp, bl2wc (), n]" and h: "tm_wf (tp, 0)" show "trpl_code (steps0 (Suc 0, Bk\ l, ) tp (Suc n)) = - rec_eval rec_conf [code tp, bl2wc (), Suc n]" + rec_exec rec_conf [code tp, bl2wc (), Suc n]" proof(case_tac "steps0 (Suc 0, Bk\ l, ) tp n", simp only: step_red conf_lemma conf.simps) fix a b c @@ -4235,7 +4341,7 @@ done moreover hence "trpl_code (step0 (a, b, c) tp) = - rec_eval rec_newconf [code tp, trpl_code (a, b, c)]" + rec_exec rec_newconf [code tp, trpl_code (a, b, c)]" apply(rule_tac rec_t_eq_step) using h g apply(simp add: state_in_range) @@ -4293,11 +4399,11 @@ "\steps0 (Suc 0, Bk\l, ) tp stp = (0, Bk\ m, Oc\ rs @ Bk\ n); tm_wf (tp, 0); rs > 0\ - \ rec_eval rec_nonstop [code tp, bl2wc (), stp] = 0" + \ rec_exec rec_nonstop [code tp, bl2wc (), stp] = 0" proof(simp add: nonstop_lemma nonstop.simps nstd.simps) assume h: "steps0 (Suc 0, Bk\l, ) tp stp = (0, Bk\ m, Oc\ rs @ Bk\ n)" and tc_t: "tm_wf (tp, 0)" "rs > 0" - have g: "rec_eval rec_conf [code tp, bl2wc (), stp] = + have g: "rec_exec rec_conf [code tp, bl2wc (), stp] = trpl_code (0, Bk\ m, Oc\ rs@Bk\ n)" using rec_t_eq_steps[of tp l lm stp] tc_t h by(simp) @@ -4487,26 +4593,26 @@ execution of of TMs. *} -lemma terminates_halt: +lemma terminate_halt: "\steps0 (Suc 0, Bk\l, ) tp stp = (0, Bk\m, Oc\rs@Bk\n); - tm_wf (tp,0); 0 \ terminates rec_halt [code tp, (bl2wc ())]" + tm_wf (tp,0); 0 \ terminate rec_halt [code tp, (bl2wc ())]" apply(frule_tac halt_least_step, auto) -thm terminates_halt_lemma -apply(rule_tac t = stpa in terminates_halt_lemma) +thm terminate_halt_lemma +apply(rule_tac t = stpa in terminate_halt_lemma) apply(simp_all add: nonstop_lemma, auto) done -lemma terminates_F: +lemma terminate_F: "\steps0 (Suc 0, Bk\l, ) tp stp = (0, Bk\m, Oc\rs@Bk\n); - tm_wf (tp,0); 0 \ terminates rec_F [code tp, (bl2wc ())]" -apply(drule_tac terminates_halt, simp_all) -apply(erule_tac terminates_F_lemma) + tm_wf (tp,0); 0 \ terminate rec_F [code tp, (bl2wc ())]" +apply(drule_tac terminate_halt, simp_all) +apply(erule_tac terminate_F_lemma) done lemma F_correct: "\steps0 (Suc 0, Bk\l, ) tp stp = (0, Bk\m, Oc\rs@Bk\n); tm_wf (tp,0); 0 - \ rec_eval rec_F [code tp, (bl2wc ())] = (rs - Suc 0)" + \ rec_exec rec_F [code tp, (bl2wc ())] = (rs - Suc 0)" apply(frule_tac halt_least_step, auto) apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) using rec_t_eq_steps[of tp l lm stp] @@ -4523,11 +4629,11 @@ using halt_state_keep[of "code tp" lm stpa stp] by(simp) moreover have g2: - "rec_eval rec_halt [code tp, (bl2wc ())] = stpa" + "rec_exec rec_halt [code tp, (bl2wc ())] = stpa" using h - by(auto simp: rec_eval.simps rec_halt_def nonstop_lemma intro!: Least_equality) + by(auto simp: rec_exec.simps rec_halt_def nonstop_lemma intro!: Least_equality) show - "rec_eval rec_F [code tp, (bl2wc ())] = (rs - Suc 0)" + "rec_exec rec_F [code tp, (bl2wc ())] = (rs - Suc 0)" proof - have "valu (rght (conf (code tp) (bl2wc ()) stpa)) = rs - Suc 0" @@ -4536,7 +4642,7 @@ bl2wc.simps bl2nat_append lg_power) done thus "?thesis" - by(simp add: rec_eval.simps F_lemma g2) + by(simp add: rec_exec.simps F_lemma g2) qed qed diff -r 89ed51d72e4a -r aea02b5a58d2 thys/UF_Rec.thy --- a/thys/UF_Rec.thy Thu May 02 12:49:15 2013 +0100 +++ b/thys/UF_Rec.thy Thu May 02 12:49:33 2013 +0100 @@ -1,40 +1,9 @@ theory UF_Rec -imports Recs +imports Recs Turing_Hoare begin section {* Universal Function *} -text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *} - -fun NextPrime ::"nat \ nat" - where - "NextPrime x = (LEAST y. y \ Suc (fact x) \ x < y \ prime y)" - -definition rec_nextprime :: "recf" - where - "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in - let conj2 = CN rec_less [Id 2 1, Id 2 0] in - let conj3 = CN rec_prime [Id 2 0] in - let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3] - in MN (CN rec_not [conjs]))" - -lemma nextprime_lemma [simp]: - "rec_eval rec_nextprime [x] = NextPrime x" -by (simp add: rec_nextprime_def Let_def) - - -fun Pi :: "nat \ nat" - where - "Pi 0 = 2" | - "Pi (Suc x) = NextPrime (Pi x)" - -definition - "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])" - -lemma pi_lemma [simp]: - "rec_eval rec_pi [x] = Pi x" -by (induct x) (simp_all add: rec_pi_def) - text{* coding of the configuration *} @@ -371,494 +340,79 @@ definition "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]" -end - - -(* - +text {* + The correctness of @{text "rec_uf"}, nonhalt case. + *} +subsection {* Coding function of TMs *} -fun mtest where - "mtest R 0 = if R 0 then 0 else 1" -| "mtest R (Suc n) = (if R n then mtest R n else (Suc n))" - +text {* + The purpose of this section is to get the coding function of Turing Machine, + which is going to be named @{text "code"}. + *} -lemma - "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX" -apply(simp only: rec_maxr2_def) -apply(case_tac x) -apply(clarify) -apply(subst rec_eval.simps) -apply(simp only: constn_lemma) -defer -apply(clarify) -apply(subst rec_eval.simps) -apply(simp only: rec_maxr2_def[symmetric]) -apply(subst rec_eval.simps) -apply(simp only: map.simps nth) -apply(subst rec_eval.simps) -apply(simp only: map.simps nth) -apply(subst rec_eval.simps) -apply(simp only: map.simps nth) -apply(subst rec_eval.simps) -apply(simp only: map.simps nth) -apply(subst rec_eval.simps) -apply(simp only: map.simps nth) -apply(subst rec_eval.simps) -apply(simp only: map.simps nth) +fun bl2nat :: "cell list \ nat \ nat" + where + "bl2nat [] n = 0" +| "bl2nat (Bk # bl) n = bl2nat bl (Suc n)" +| "bl2nat (Oc # bl) n = 2 ^ n + bl2nat bl (Suc n)" + +fun bl2wc :: "cell list \ nat" + where + "bl2wc xs = bl2nat xs 0" - -definition - "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))" - -definition - "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])" +fun trpl_code :: "config \ nat" + where + "trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)" -definition Minr :: "(nat \ nat list \ bool) \ nat \ nat list \ nat" - where "Minr R x ys = Min ({z | z. z \ x \ R z ys} \ {Suc x})" - -definition Maxr :: "(nat \ nat list \ bool) \ nat \ nat list \ nat" - where "Maxr R x ys = Max ({z | z. z \ x \ R z ys} \ {0})" - -lemma rec_minr2_le_Suc: - "rec_eval (rec_minr2 f) [x, y1, y2] \ Suc x" -apply(simp add: rec_minr2_def) -apply(auto intro!: setsum_one_le setprod_one_le) -done +fun action_map :: "action \ nat" + where + "action_map W0 = 0" +| "action_map W1 = 1" +| "action_map L = 2" +| "action_map R = 3" +| "action_map Nop = 4" -lemma rec_minr2_eq_Suc: - assumes "\z \ x. rec_eval f [z, y1, y2] = 0" - shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x" -using assms by (simp add: rec_minr2_def) - -lemma rec_minr2_le: - assumes h1: "y \ x" - and h2: "0 < rec_eval f [y, y1, y2]" - shows "rec_eval (rec_minr2 f) [x, y1, y2] \ y" -apply(simp add: rec_minr2_def) -apply(subst setsum_cut_off_le[OF h1]) -using h2 apply(auto) -apply(auto intro!: setsum_one_less setprod_one_le) -done +fun action_map_iff :: "nat \ action" + where + "action_map_iff (0::nat) = W0" +| "action_map_iff (Suc 0) = W1" +| "action_map_iff (Suc (Suc 0)) = L" +| "action_map_iff (Suc (Suc (Suc 0))) = R" +| "action_map_iff n = Nop" -(* ??? *) -lemma setsum_eq_one_le2: - fixes n::nat - assumes "\i \ n. f i \ 1" - shows "((\i \ n. f i) \ Suc n) \ (\i \ n. f i = 1)" -using assms -apply(induct n) -apply(simp add: One_nat_def) -apply(simp) -apply(auto simp add: One_nat_def) -apply(drule_tac x="Suc n" in spec) -apply(auto) -by (metis le_Suc_eq) - +fun block_map :: "cell \ nat" + where + "block_map Bk = 0" +| "block_map Oc = 1" -lemma rec_min2_not: - assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x" - shows "\z \ x. rec_eval f [z, y1, y2] = 0" -using assms -apply(simp add: rec_minr2_def) -apply(subgoal_tac "\i \ x. (\z\i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)") -apply(simp) -apply (metis atMost_iff le_refl zero_neq_one) -apply(rule setsum_eq_one_le2) -apply(auto) -apply(rule setprod_one_le) -apply(auto) -done +fun Goedel_code' :: "nat list \ nat \ nat" + where + "Goedel_code' [] n = 1" +| "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) " + +fun Goedel_code :: "nat list \ nat" + where + "Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)" -lemma disjCI2: - assumes "~P ==> Q" shows "P|Q" -apply (rule classical) -apply (iprover intro: assms disjI1 disjI2 notI elim: notE) -done +fun modify_tprog :: "instr list \ nat list" + where + "modify_tprog [] = []" +| "modify_tprog ((a, s) # nl) = action_map a # s # modify_tprog nl" -lemma minr_lemma [simp]: -shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \ x \ 0 < rec_eval f [z, y1, y2]) \ z = Suc x)" -apply(induct x) -apply(rule Least_equality[symmetric]) -apply(simp add: rec_minr2_def) -apply(erule disjE) -apply(rule rec_minr2_le) -apply(auto)[2] -apply(simp) -apply(rule rec_minr2_le_Suc) -apply(simp) +text {* @{text "Code tp"} gives the Goedel coding of TM program @{text "tp"}. *} +fun Code :: "instr list \ nat" + where + "Code tp = Goedel_code (modify_tprog tp)" -apply(rule rec_minr2_le) +subsection {* Relating interperter functions to the execution of TMs *} -apply(rule rec_minr2_le_Suc) -apply(rule disjCI) -apply(simp add: rec_minr2_def) - -apply(ru le setsum_one_less) -apply(clarify) -apply(rule setprod_one_le) -apply(auto)[1] -apply(simp) -apply(rule setsum_one_le) -apply(clarify) -apply(rule setprod_one_le) -apply(auto)[1] -thm disj_CE -apply(auto) - -lemma minr_lemma: -shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\x xs. (0 < rec_eval f (x #xs))) x [y1, y2]" -apply(simp only: Minr_def) -apply(rule sym) -apply(rule Min_eqI) -apply(auto)[1] -apply(simp) -apply(erule disjE) -apply(simp) -apply(rule rec_minr2_le_Suc) -apply(rule rec_minr2_le) -apply(auto)[2] -apply(simp) -apply(induct x) -apply(simp add: rec_minr2_def) -apply( -apply(rule disjCI) -apply(rule rec_minr2_eq_Suc) -apply(simp) -apply(auto) - -apply(rule setsum_one_le) -apply(auto)[1] -apply(rule setprod_one_le) -apply(auto)[1] -apply(subst setsum_cut_off_le) -apply(auto)[2] -apply(rule setsum_one_less) -apply(auto)[1] -apply(rule setprod_one_le) -apply(auto)[1] -apply(simp) -thm setsum_eq_one_le -apply(subgoal_tac "(\z\x. (\z\z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \ - (\ (\z\x. (\z\z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") -prefer 2 -apply(auto)[1] -apply(erule disjE) -apply(rule disjI1) -apply(rule setsum_eq_one_le) -apply(simp) -apply(rule disjI2) -apply(simp) -apply(clarify) -apply(subgoal_tac "\l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") -defer -apply metis -apply(erule exE) -apply(subgoal_tac "l \ x") -defer -apply (metis not_leE not_less_Least order_trans) -apply(subst setsum_least_eq) -apply(rotate_tac 4) -apply(assumption) -apply(auto)[1] -apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") -prefer 2 -apply(auto)[1] -apply(rotate_tac 5) -apply(drule not_less_Least) -apply(auto)[1] -apply(auto) -apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) -apply(simp) -apply (metis LeastI_ex) -apply(subst setsum_least_eq) -apply(rotate_tac 3) -apply(assumption) -apply(simp) -apply(auto)[1] -apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") -prefer 2 -apply(auto)[1] -apply (metis neq0_conv not_less_Least) -apply(auto)[1] -apply (metis (mono_tags) LeastI_ex) -by (metis LeastI_ex) - -lemma minr_lemma: -shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\x xs. (0 < rec_eval f (x #xs))) x [y1, y2]" -apply(simp only: Minr_def rec_minr2_def) -apply(simp) -apply(rule sym) -apply(rule Min_eqI) -apply(auto)[1] -apply(simp) -apply(erule disjE) -apply(simp) -apply(rule setsum_one_le) -apply(auto)[1] -apply(rule setprod_one_le) -apply(auto)[1] -apply(subst setsum_cut_off_le) -apply(auto)[2] -apply(rule setsum_one_less) -apply(auto)[1] -apply(rule setprod_one_le) -apply(auto)[1] -apply(simp) -thm setsum_eq_one_le -apply(subgoal_tac "(\z\x. (\z\z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \ - (\ (\z\x. (\z\z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") -prefer 2 -apply(auto)[1] -apply(erule disjE) -apply(rule disjI1) -apply(rule setsum_eq_one_le) -apply(simp) -apply(rule disjI2) -apply(simp) -apply(clarify) -apply(subgoal_tac "\l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") -defer -apply metis -apply(erule exE) -apply(subgoal_tac "l \ x") -defer -apply (metis not_leE not_less_Least order_trans) -apply(subst setsum_least_eq) -apply(rotate_tac 4) -apply(assumption) -apply(auto)[1] -apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") -prefer 2 -apply(auto)[1] -apply(rotate_tac 5) -apply(drule not_less_Least) -apply(auto)[1] -apply(auto) -apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) -apply(simp) -apply (metis LeastI_ex) -apply(subst setsum_least_eq) -apply(rotate_tac 3) -apply(assumption) -apply(simp) -apply(auto)[1] -apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") -prefer 2 -apply(auto)[1] -apply (metis neq0_conv not_less_Least) -apply(auto)[1] -apply (metis (mono_tags) LeastI_ex) -by (metis LeastI_ex) - -lemma disjCI2: - assumes "~P ==> Q" shows "P|Q" -apply (rule classical) -apply (iprover intro: assms disjI1 disjI2 notI elim: notE) -done +lemma F_correct: + assumes tp: "steps0 (1, Bk \ l, ) tp stp = (0, Bk \ m, Oc \ rs @ Bk \ n)" + and wf: "tm_wf0 tp" "0 < rs" + shows "rec_eval rec_uf [Code tp, bl2wc ()] = (rs - Suc 0)" -lemma minr_lemma [simp]: -shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \ x \ 0 < rec_eval f [z, y1, y2]) \ z = Suc x)" -(*apply(simp add: rec_minr2_def)*) -apply(rule Least_equality[symmetric]) -prefer 2 -apply(erule disjE) -apply(rule rec_minr2_le) -apply(auto)[2] -apply(clarify) -apply(rule rec_minr2_le_Suc) -apply(rule disjCI) -apply(simp add: rec_minr2_def) - -apply(ru le setsum_one_less) -apply(clarify) -apply(rule setprod_one_le) -apply(auto)[1] -apply(simp) -apply(rule setsum_one_le) -apply(clarify) -apply(rule setprod_one_le) -apply(auto)[1] -thm disj_CE -apply(auto) -apply(auto) -prefer 2 -apply(rule le_tran - -apply(rule le_trans) -apply(simp) -defer -apply(auto) -apply(subst setsum_cut_off_le) - - -lemma - "Minr R x ys = (LEAST z. (R z ys \ z = Suc x))" -apply(simp add: Minr_def) -apply(rule Min_eqI) -apply(auto)[1] -apply(simp) -apply(rule Least_le) -apply(auto)[1] -apply(rule LeastI2_wellorder) -apply(auto) -done - -definition (in ord) - Great :: "('a \ bool) \ 'a" (binder "GREAT " 10) where - "Great P = (THE x. P x \ (\y. P y \ y \ x))" - -(* -lemma Great_equality: - assumes "P x" - and "\y. P y \ y \ x" - shows "Great P = x" -unfolding Great_def -apply(rule the_equality) -apply(blast intro: assms) -*) - - - -lemma - "Maxr R x ys = (GREAT z. (R z ys \ z = 0))" -apply(simp add: Maxr_def) -apply(rule Max_eqI) -apply(auto)[1] -apply(simp) -thm Least_le Greatest_le -oops - -lemma - "Maxr R x ys = x - Minr (\z. R (x - z)) x ys" -apply(simp add: Maxr_def Minr_def) -apply(rule Max_eqI) -apply(auto)[1] -apply(simp) -apply(erule disjE) -apply(simp) -apply(auto)[1] -defer -apply(simp) -apply(auto)[1] -thm Min_insert -defer -oops - - - -definition quo :: "nat \ nat \ nat" - where - "quo x y = (if y = 0 then 0 else x div y)" - - -definition - "rec_quo = CN rec_mult [CN rec_sign [Id 2 1], - CN (rec_minr2 (CN rec_less [Id 3 1, CN rec_mult [CN S [Id 3 0], Id 3 2]])) - [Id 2 0, Id 2 0, Id 2 1]]" +end -lemma div_lemma [simp]: - "rec_eval rec_quo [x, y] = quo x y" -apply(simp add: rec_quo_def quo_def) -apply(rule impI) -apply(rule Min_eqI) -apply(auto)[1] -apply(simp) -apply(erule disjE) -apply(simp) -apply(auto)[1] -apply (metis div_le_dividend le_SucI) -defer -apply(simp) -apply(auto)[1] -apply (metis mult_Suc_right nat_mult_commute split_div_lemma) -apply(auto)[1] - -apply (smt div_le_dividend fst_divmod_nat) -apply(simp add: quo_def) -apply(auto)[1] - -apply(auto) - -fun Minr :: "(nat list \ bool) \ nat \ nat \ nat" - where "Minr R x y = (let setx = {z | z. z \ x \ R [z, y]} in - if (setx = {}) then (Suc x) else (Min setx))" - -definition - "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))" - -lemma minr_lemma [simp]: -shows "rec_eval (rec_minr f) [x, y] = Minr (\xs. (0 < rec_eval f xs)) x y" -apply(simp only: rec_minr_def) -apply(simp only: sigma1_lemma) -apply(simp only: accum1_lemma) -apply(subst rec_eval.simps) -apply(simp only: map.simps nth) -apply(simp only: Minr.simps Let_def) -apply(auto simp del: not_lemma) -apply(simp) -apply(simp only: not_lemma sign_lemma) -apply(rule sym) -apply(rule Min_eqI) -apply(auto)[1] -apply(simp) -apply(subst setsum_cut_off_le[where m="ya"]) -apply(simp) -apply(simp) -apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) -apply(rule setsum_one_less) -apply(default) -apply(rule impI) -apply(rule setprod_one_le) -apply(auto split: if_splits)[1] -apply(simp) -apply(rule conjI) -apply(subst setsum_cut_off_le[where m="xa"]) -apply(simp) -apply(simp) -apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) -apply(rule le_trans) -apply(rule setsum_one_less) -apply(default) -apply(rule impI) -apply(rule setprod_one_le) -apply(auto split: if_splits)[1] -apply(simp) -apply(subgoal_tac "\l. l = (LEAST z. 0 < rec_eval f [z, y])") -defer -apply metis -apply(erule exE) -apply(subgoal_tac "l \ x") -defer -apply (metis not_leE not_less_Least order_trans) -apply(subst setsum_least_eq) -apply(rotate_tac 3) -apply(assumption) -prefer 3 -apply (metis LeastI_ex) -apply(auto)[1] -apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])") -prefer 2 -apply(auto)[1] -apply(rotate_tac 5) -apply(drule not_less_Least) -apply(auto)[1] -apply(auto) -by (metis (mono_tags) LeastI_ex) - - -fun Minr2 :: "(nat list \ bool) \ nat \ nat \ nat" - where "Minr2 R x y = (let setx = {z | z. z \ x \ R [z, y]} in - Min (setx \ {Suc x}))" - -lemma Minr2_Minr: - "Minr2 R x y = Minr R x y" -apply(auto) -apply (metis (lifting, no_types) Min_singleton empty_Collect_eq) -apply(rule min_absorb2) -apply(subst Min_le_iff) -apply(auto) -done - *) \ No newline at end of file diff -r 89ed51d72e4a -r aea02b5a58d2 thys/UTM.thy --- a/thys/UTM.thy Thu May 02 12:49:15 2013 +0100 +++ b/thys/UTM.thy Thu May 02 12:49:33 2013 +0100 @@ -1216,8 +1216,8 @@ declare start_of.simps[simp del] -lemma twice_lemma: "rec_eval rec_twice [rs] = 2*rs" -by(auto simp: rec_twice_def rec_eval.simps) +lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs" +by(auto simp: rec_twice_def rec_exec.simps) lemma t_twice_correct: "\stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\(Suc rs) @ Bk\(n)) @@ -1227,13 +1227,13 @@ fix a b c assume h: "rec_ci rec_twice = (a, b, c)" have "\stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\(n)) (tm_of abc_twice @ shift (mopup (length [rs])) - (length (tm_of abc_twice) div 2)) stp = (0, Bk\(m) @ Bk # Bk # ires, Oc\(Suc (rec_eval rec_twice [rs])) @ Bk\(l))" + (length (tm_of abc_twice) div 2)) stp = (0, Bk\(m) @ Bk # Bk # ires, Oc\(Suc (rec_exec rec_twice [rs])) @ Bk\(l))" thm recursive_compile_to_tm_correct1 proof(rule_tac recursive_compile_to_tm_correct1) show "rec_ci rec_twice = (a, b, c)" by (simp add: h) next - show "terminates rec_twice [rs]" - apply(rule_tac primerec_terminates, auto) + show "terminate rec_twice [rs]" + apply(rule_tac primerec_terminate, auto) apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2) by(auto) next @@ -1242,7 +1242,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_eval.simps twice_lemma) + apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma) done qed @@ -2005,8 +2005,8 @@ apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps) by auto -lemma fourtimes_lemma: "rec_eval rec_fourtimes [rs] = 4 * rs" -by(simp add: rec_eval.simps rec_fourtimes_def) +lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs" +by(simp add: rec_exec.simps rec_fourtimes_def) lemma t_fourtimes_correct: @@ -2017,13 +2017,13 @@ fix a b c assume h: "rec_ci rec_fourtimes = (a, b, c)" have "\stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\(n)) (tm_of abc_fourtimes @ shift (mopup (length [rs])) - (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\(m) @ Bk # Bk # ires, Oc\(Suc (rec_eval rec_fourtimes [rs])) @ Bk\(l))" + (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\(m) @ Bk # Bk # ires, Oc\(Suc (rec_exec rec_fourtimes [rs])) @ Bk\(l))" thm recursive_compile_to_tm_correct1 proof(rule_tac recursive_compile_to_tm_correct1) show "rec_ci rec_fourtimes = (a, b, c)" by (simp add: h) next - show "terminates rec_fourtimes [rs]" - apply(rule_tac primerec_terminates) + show "terminate rec_fourtimes [rs]" + apply(rule_tac primerec_terminate) by auto next show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))" @@ -4729,19 +4729,19 @@ proof - obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)" by (metis prod_cases3) - moreover have b: "rec_eval rec_F [code tp, (bl2wc ())] = (rs - Suc 0)" + moreover have b: "rec_exec rec_F [code tp, (bl2wc ())] = (rs - Suc 0)" using assms apply(rule_tac F_correct, simp_all) done have "\ stp m l. steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc ()]> @ Bk\i) (F_tprog @ shift (mopup (length [code tp, bl2wc ()])) (length F_tprog div 2)) stp - = (0, Bk\m @ Bk # Bk # [], Oc\Suc (rec_eval rec_F [code tp, (bl2wc ())]) @ Bk\l)" + = (0, Bk\m @ Bk # Bk # [], Oc\Suc (rec_exec rec_F [code tp, (bl2wc ())]) @ Bk\l)" proof(rule_tac recursive_compile_to_tm_correct1) show "rec_ci rec_F = (ap, arity, fp)" using a by simp next - show "terminates rec_F [code tp, bl2wc ()]" + show "terminate rec_F [code tp, bl2wc ()]" using assms - by(rule_tac terminates_F, simp_all) + by(rule_tac terminate_F, simp_all) next show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc ()]))" using a @@ -4751,14 +4751,14 @@ then obtain stp m l where "steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc ()]> @ Bk\i) (F_tprog @ shift (mopup (length [code tp, (bl2wc ())])) (length F_tprog div 2)) stp - = (0, Bk\m @ Bk # Bk # [], Oc\Suc (rec_eval rec_F [code tp, (bl2wc ())]) @ Bk\l)" by blast + = (0, Bk\m @ Bk # Bk # [], Oc\Suc (rec_exec rec_F [code tp, (bl2wc ())]) @ Bk\l)" by blast hence "\ m. steps0 (Suc 0, [Bk], <[code tp, bl2wc ()]> @ Bk\i) (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp = (0, Bk\m, Oc\Suc (rs - 1) @ Bk\l)" proof - assume g: "steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc ()]> @ Bk \ i) (F_tprog @ shift (mopup (length [code tp, bl2wc ()])) (length F_tprog div 2)) stp = - (0, Bk \ m @ [Bk, Bk], Oc \ Suc ((rec_eval rec_F [code tp, bl2wc ()])) @ Bk \ l)" + (0, Bk \ m @ [Bk, Bk], Oc \ Suc ((rec_exec rec_F [code tp, bl2wc ()])) @ Bk \ l)" moreover have "tinres [Bk, Bk] [Bk]" apply(auto simp: tinres_def) done @@ -4936,7 +4936,7 @@ done lemma NSTD_1: "\ TSTD (a, b, c) - \ rec_eval rec_NSTD [trpl_code (a, b, c)] = Suc 0" + \ rec_exec rec_NSTD [trpl_code (a, b, c)] = Suc 0" using NSTD_lemma1[of "trpl_code (a, b, c)"] NSTD_lemma2[of "trpl_code (a, b, c)"] apply(simp add: TSTD_def) @@ -4949,10 +4949,10 @@ "\tm_wf (tp, 0); steps0 (Suc 0, Bk\(l), ) tp stp = (a, b, c); \ TSTD (a, b, c)\ - \ rec_eval rec_nonstop [code tp, bl2wc (), stp] = Suc 0" -apply(simp add: rec_nonstop_def rec_eval.simps) + \ rec_exec rec_nonstop [code tp, bl2wc (), stp] = Suc 0" +apply(simp add: rec_nonstop_def rec_exec.simps) apply(subgoal_tac - "rec_eval rec_conf [code tp, bl2wc (), stp] = + "rec_exec rec_conf [code tp, bl2wc (), stp] = trpl_code (a, b, c)", simp) apply(erule_tac NSTD_1) using rec_t_eq_steps[of tp l lm stp] @@ -4962,7 +4962,7 @@ lemma nonstop_true: "\tm_wf (tp, 0); \ stp. (\ TSTD (steps0 (Suc 0, Bk\(l), ) tp stp))\ - \ \y. rec_eval rec_nonstop ([code tp, bl2wc (), y]) = (Suc 0)" + \ \y. rec_exec rec_nonstop ([code tp, bl2wc (), y]) = (Suc 0)" apply(rule_tac allI, erule_tac x = y in allE) apply(case_tac "steps0 (Suc 0, Bk\(l), ) tp y", simp) apply(rule_tac nonstop_t_uhalt_eq, simp_all) @@ -5021,11 +5021,11 @@ using e f proof(rule_tac mn_unhalt_case, auto simp: rec_halt_def) fix i - show "terminates rec_nonstop [code tp, bl2wc (), i]" - by(rule_tac primerec_terminates, auto) + show "terminate rec_nonstop [code tp, bl2wc (), i]" + by(rule_tac primerec_terminate, auto) next fix i - show "0 < rec_eval rec_nonstop [code tp, bl2wc (), i]" + show "0 < rec_exec rec_nonstop [code tp, bl2wc (), i]" using assms by(drule_tac nonstop_true, auto) qed @@ -5035,22 +5035,22 @@ assume "j<2" "rec_ci ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) = (apj, arj, ftj)" hence "{\nl. nl = [code tp, bl2wc ()] @ 0 \ (ftj - arj) @ anything} apj {\nl. nl = [code tp, bl2wc ()] @ - rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc ()] # + rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc ()] # 0 \ (ftj - Suc arj) @ anything}" apply(rule_tac recursive_compile_correct) apply(case_tac j, auto) - apply(rule_tac [!] primerec_terminates) + apply(rule_tac [!] primerec_terminate) by(auto) thus "{\nl. nl = code tp # bl2wc () # 0 \ (ftj - arj) @ anything} apj - {\nl. nl = code tp # bl2wc () # rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) + {\nl. nl = code tp # bl2wc () # rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc ()] # 0 \ (ftj - Suc arj) @ anything}" by simp next fix j assume "(j::nat) < 2" - thus "terminates ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) + thus "terminate ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc ()]" - by(case_tac j, auto intro!: primerec_terminates) + by(case_tac j, auto intro!: primerec_terminate) qed thus "{\nl. nl = code tp # bl2wc () # 0 \ (ft2 - Suc (Suc 0)) @ anything} ap2 \" by simp