1 theory turing_hoare

     1 theory turing_hoare

     2 imports turing_basic

     2 imports turing_basic

     3 begin

     3 begin

     6 

     4 

     7 type_synonym assert = "tape \<Rightarrow> bool"

     5 type_synonym assert = "tape \<Rightarrow> bool"

     8 

     6 

     9 definition 

     7 definition 

    10   assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)

     8   assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)

    11 where

     9 where

    12   "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)"

    10   "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)"

    15 

    11 

    16 fun 

    12 fun 

    17   holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100)

    13   holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100)

    18 where

    14 where

    19   "P holds_for (s, l, r) = P (l, r)"  

    15   "P holds_for (s, l, r) = P (l, r)"  

    46   shows "{P} p {Q}"

    42   shows "{P} p {Q}"

    47 unfolding Hoare_def using assms by auto

    43 unfolding Hoare_def using assms by auto

    48 

    44 

    49 

    45 

    50 text {*

    46 text {*

    53   {P1} A |+| B {Q2}

    49   {P1} A |+| B {Q2}

    54 *}

    50 *}

    55 

    51 

    56 

    52 

    57 lemma Hoare_plus_halt: 

    53 lemma Hoare_plus_halt: 

    77   then have "P2 (l', r')" by auto

    73   then have "P2 (l', r')" by auto

    78   then obtain n2 

    74   then obtain n2 

    79     where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)"

    75     where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)"

    80     using B_halt unfolding Hoare_def by auto

    76     using B_halt unfolding Hoare_def by auto

    81   then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"

    77   then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"

    83   then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n2 = (0, l'', r'')"

    79   then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n2 = (0, l'', r'')"

    84     by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf)

    80     by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf)

    85   ultimately show 

    81   ultimately show 

    86     "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"

    82     "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"

    88     apply(rule_tac x = "stpa + n2" in exI)

    84     apply(rule_tac x = "stpa + n2" in exI)

    89     apply(simp add: steps_add)

    85     apply(simp add: steps_add)

    90     done

    86     done

    91 qed

    87 qed

    92 

    88 

    93 definition

    89 definition

    94   Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50)

    90   Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50)

    95 where

    91 where

    98 

    93 

    99 lemma Hoare_unhalt_I:

    94 lemma Hoare_unhalt_I:

   100   assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)"

    95   assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)"

   101   shows "{P} p"

    96   shows "{P} p"

   102 unfolding Hoare_unhalt_def using assms by auto

    97 unfolding Hoare_unhalt_def using assms by auto