diff -r 2363eb91d9fd -r 8c7f10b3da7b thys/uncomputable.thy --- a/thys/uncomputable.thy Wed Jan 23 20:18:40 2013 +0100 +++ b/thys/uncomputable.thy Thu Jan 24 00:20:26 2013 +0100 @@ -57,26 +57,19 @@ (* tcopy_init *) -fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" - where - "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)" - -fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" - where - "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)" - -fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" - where - "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])" - -fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" - where - "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))" - -fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" - where +fun + inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and + inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and + inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and + inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and + inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" +where "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or> (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))" +| "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)" +| "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)" +| "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])" +| "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))" fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool" where @@ -184,7 +177,7 @@ lemma init_correct: "x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}" -proof(rule_tac HoareI) +proof(rule_tac Hoare_haltI) fix l r assume h: "0 < x" "inv_init1 x (l, r)" @@ -690,7 +683,7 @@ lemma loop_correct: "x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}" -proof(rule_tac HoareI) +proof(rule_tac Hoare_haltI) fix l r assume h: "0 < x" "inv_loop1 x (l, r)" @@ -973,7 +966,7 @@ lemma end_correct: "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}" -proof(rule_tac HoareI) +proof(rule_tac Hoare_haltI) fix l r assume h: "0 < x" "inv_end1 x (l, r)" @@ -1060,7 +1053,7 @@ by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) ultimately show "{pre_tcopy n} tcopy {post_tcopy n}" - by (rule Hoare_weak) + by (rule Hoare_weaken) qed @@ -1113,7 +1106,7 @@ lemma dither_halts: shows "{dither_halt_inv} dither {dither_halt_inv}" -apply(rule HoareI) +apply(rule Hoare_haltI) using dither_halt_rs apply(auto) by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) @@ -1314,7 +1307,7 @@ where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])" using nh_newcase[of "M" "[n]" "1", OF assms] by auto then show "{pre_H_inv M n} H {post_H_halt_inv}" - unfolding Hoare_def + unfolding Hoare_halt_def apply(auto) apply(rule_tac x = stp in exI) apply(auto) @@ -1329,7 +1322,7 @@ where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])" using h_newcase[of "M" "[n]" "1", OF assms] by auto then show "{pre_H_inv M n} H {post_H_unhalt_inv}" - unfolding Hoare_def + unfolding Hoare_halt_def apply(auto) apply(rule_tac x = stp in exI) apply(auto) @@ -1387,7 +1380,7 @@ with assms show "False" unfolding P1_def P3_def unfolding haltP_def - unfolding Hoare_def + unfolding Hoare_halt_def apply(auto) apply(erule_tac x = n in allE) apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")