tm: comparison thys/uncomputable.thy

equal deleted inserted replaced

-:f2bda6ba4952
+:aeaf1374dc67
 apply(induct stp, simp add: steps.simps)
 apply(auto simp: step_red)
 apply(rule_tac inv_begin_step, simp_all)
 done
-fun init_state :: "config \<Rightarrow> nat"
+fun begin_state :: "config \<Rightarrow> nat"
 where
-"init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
+"begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
-fun init_step :: "config \<Rightarrow> nat"
+fun begin_step :: "config \<Rightarrow> nat"
 where
-"init_step (s, l, r) =
+"begin_step (s, l, r) =
 (if s = 2 then length r else
 if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
 if s = 4 then length l
 else 0)"
-fun init_measure :: "config \<Rightarrow> nat \<times> nat"
+fun begin_measure :: "config \<Rightarrow> nat \<times> nat"
 where
-"init_measure c = (init_state c, init_step c)"
+"begin_measure c = (begin_state c, begin_step c)"
 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
 where
 "lex_pair \<equiv> less_than <*lex*> less_than"
-definition init_LE :: "(config \<times> config) set"
+definition begin_LE :: "(config \<times> config) set"
 where
-"init_LE \<equiv> (inv_image lex_pair init_measure)"
+"begin_LE \<equiv> (inv_image lex_pair begin_measure)"
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
 by (case_tac r, auto, case_tac a, auto)
-lemma wf_begin_le: "wf init_LE"
+lemma wf_begin_le: "wf begin_LE"
-by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
+by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
-lemma init_halt:
+lemma begin_halt:
 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
-proof(rule_tac LE = init_LE in halt_lemma)
+proof(rule_tac LE = begin_LE in halt_lemma)
-show "wf init_LE" by(simp add: wf_begin_le)
+show "wf begin_LE" by(simp add: wf_begin_le)
 next
 assume h: "0 < x"
 show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
 (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
-steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
 proof(rule_tac allI, rule_tac impI)
 fix n
 assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
 have b: "inv_begin x (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
 apply(rule_tac inv_begin_steps)
 apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
 done
 moreover hence "inv_begin x (s, l, r)"
 using c b by simp
 ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
-steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
 using a
 proof(simp del: inv_begin.simps)
 assume "inv_begin x (s, l, r)" "0 < s"
-thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> init_LE"
+thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE"
-apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
+apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
 apply(case_tac r, auto, case_tac a, auto)
 done
 qed
 qed
 qed
-lemma init_correct:
+lemma begin_correct:
 "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
 proof(rule_tac Hoare_haltI)
 fix l r
 assume h: "0 < x" "inv_begin1 x (l, r)"
 hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"
-by (rule_tac init_halt)
+by (rule_tac begin_halt)
 then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
 moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
 apply(rule_tac inv_begin_steps)
 using h by(simp_all add: inv_begin.simps)
 ultimately show
 lemma tcopy_correct1:
 assumes "0 < x"
 shows "{inv_begin1 x} tcopy {inv_end0 x}"
 proof -
 have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
-by (metis assms init_correct)
+by (metis assms begin_correct)
 moreover
 have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
 by (metis assms loop_correct)
 moreover
 have "inv_begin0 x \<mapsto> inv_loop1 x"
 definition dither :: "instr list"
 where
 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
 (* invariants of dither *)
-abbreviation
+abbreviation (input)
 "dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
-abbreviation
+abbreviation (input)
 "dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 lemma dither_loops_aux:
 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
 shows "False"
 proof -
 (* invariants *)
 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-def P3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
+def P3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
 (*
 {P1} tcopy {P2}  {P2} H {P3}
 ----------------------------
 {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
 shows "False"
 proof -
 (* invariants *)
 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-def Q3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
+def Q3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)"
 (*
 {P1} tcopy {P2}  {P2} H {Q3}
 ----------------------------
 {P1} (tcopy |+| H) {Q3}     {Q3} dither loops

changeset 94	aeaf1374dc67
parent 93	f2bda6ba4952
child 95	5317c92ff2a7