(* File: Partial_Total_Correctness_As_Fixed_Points.thy Author: John Wickerson Last updated: 21-Jan-2015 This file must be processed by Isabelle2013-2 with the Z3 prover enabled. *) theory Partial_Total_Correctness_As_Fixed_Points imports "~~/src/HOL/Library/Continuity" begin typedecl command typedecl state type_synonym assertion = "state set" type_synonym config = "command \ state" consts reduce :: "config \ config set" abbreviation reduces :: "config \ config \ bool" (infix "\" 50) where "C1 \ C2 \ C2 \ reduce C1" abbreviation reduces_many :: "config \ config \ bool" (infix "\*" 50) where "C1 \* C2 \ (op \)^** C1 C2" abbreviation stuck :: "config \ bool" where "stuck C \ reduce C = {}" definition Next :: "config \ config set" where "Next C \ reduce C" (*****************************) (* Modal-\ calculus formulae *) (*****************************) definition Box :: "config set \ config set" ("\") where "\ p \ {C. \C'. C \ C' \ C' \ p}" abbreviation Lfp :: "(config set \ config set) \ config set" (binder "\" 10) where "\ X. p X \ lfp p" abbreviation Gfp :: "(config set \ config set) \ config set" (binder "\" 10) where "\ X. p X \ gfp p" (*******************************) (* Possibly-infinite sequences *) (*******************************) type_synonym 'a seq = "nat \ 'a option" definition infinite_seq :: "'a seq \ bool" where "infinite_seq \ \ \i. \ i \ None" definition seq_hd :: "'a seq \ 'a option" where "seq_hd \ \ \ 0" definition seq_tl :: "'a seq \ 'a seq" where "seq_tl \ \ \i. \ (Suc i)" fun seq_cons :: "'a option \ 'a seq \ 'a seq" (infixr "##" 65) where "(x ## \) 0 = x" | "(x ## \) (Suc i) = \ i" lemma seq_hd_cons_tl: "seq_hd \ ## seq_tl \ = \" apply (rule ext) apply (induct_tac x) apply (auto simp add: seq_hd_def seq_tl_def) done lemma seq_tl_cons: "seq_tl (x ## \) = \" apply (rule ext) apply (induct_tac x) apply (auto simp add: seq_tl_def) done lemma seq_hd_cons: "seq_hd (x ## \) = x" apply (induct_tac x) apply (auto simp add: seq_hd_def) done fun finite_seq :: "nat \ 'a seq \ bool" where "finite_seq 0 \ = (\i. \ i = None)" | "finite_seq (Suc i) \ = (seq_hd \ \ None \ finite_seq i (seq_tl \))" lemma finite_seq_cons: "finite_seq i \ = (\x. finite_seq (Suc i) (Some x ## \))" apply (induct_tac i) apply (auto simp add: seq_hd_def seq_tl_def) done lemma finite_seq_unique': "finite_seq j1 \ \ finite_seq j2 \ \ j1 < j2 \ False" proof (induct j2 arbitrary: j1 \) case 0 thus ?case by auto next case (Suc j2) note Suc' = Suc show ?case proof (cases j1) case 0 with Suc' show ?thesis by (auto simp add: seq_hd_def) next case (Suc j1') with Suc'(2) and Suc'(4) have "finite_seq (Suc j1') \" and "j1' < j2" by auto with Suc'(3) have "finite_seq j1' (seq_tl \)" and "finite_seq j2 (seq_tl \)" by auto from Suc'(1)[OF this `j1' < j2`] show ?thesis by assumption qed qed lemma finite_seq_unique: "finite_seq j1 \ \ finite_seq j2 \ \ j1 = j2" by (metis (full_types) nat_neq_iff finite_seq_unique') (**************) (* Executions *) (**************) definition traces :: "config \ config seq set" where "traces C \ {\. \ 0 = Some C \ (\i. case \ i of None \ \ (i+1) = None | Some C \ if stuck C then \ (i+1) = None else \ (i+1) \ Some ` Next C)}" fun first_trace :: "config \ config seq" where "first_trace C 0 = Some C" | "first_trace C (Suc i) = (case first_trace C i of None \ None | Some C' \ if stuck C' then None else Some (SOME C''. C' \ C''))" lemma exists_trace: "traces C \ {}" apply (unfold traces_def) apply simp apply (rule_tac x="first_trace C" in exI) apply simp apply (intro allI) apply (case_tac "first_trace C i") apply (auto simp add: Next_def) apply (metis (lifting) image_iff someI_ex) done lemma trace_non_empty: assumes "\ \ traces C" and "finite_seq j \" shows "j > 0" proof - { assume "j=0" with assms have False by (auto simp add: traces_def) } thus ?thesis by auto qed lemma traces_mono_None: assumes "\ \ traces C" shows "\ i = None \ \ (Suc i) = None" proof (induct i) case 0 hence False using assms by (auto simp add: traces_def) thus ?case by auto next case (Suc i) from assms have "\ ((Suc i) + 1) = None" unfolding traces_def by (metis (lifting, mono_tags) Suc.prems mem_Collect_eq option.simps(4)) thus ?case by auto qed lemma trace_hd: assumes "\ \ traces C" shows "seq_hd \ = Some C" using assms by (auto simp add: traces_def seq_hd_def) lemma singleton_trace_imp_stuck: assumes "(\x. if x=0 then Some C else None) \ traces C" shows "stuck C" using assms apply (unfold traces_def) apply simp apply (frule_tac x=0 in spec) apply (cases "stuck C") apply auto done lemma traces_of_stuck_config: assumes "stuck C" shows "traces C = {\x. if x=0 then Some C else None}" proof (intro iffI equalityI subsetI) fix \ :: "config seq" assume "\ \ traces C" thus "\ \ {\x. if x = 0 then Some C else None}" apply simp apply (rule ext) apply (rename_tac i) apply (unfold atomize_imp) apply (induct_tac i) apply (auto simp add: traces_def)[2] apply (case_tac "n=0") apply (drule_tac x=0 in spec) apply (auto simp add: assms) apply (drule_tac x=n in spec) apply auto done next fix \ :: "config seq" assume "\ \ {\x. if x = 0 then Some C else None}" thus "\ \ traces C" by (auto simp add: assms traces_def) qed lemma traces_of_nonstuck_config: assumes "\ stuck C" shows "traces C = op ## (Some C) ` \(traces ` Next C)" proof (intro iffI equalityI subsetI) fix \ :: "config seq" assume "\ \ traces C" hence "\ 0 = Some C" and 1: "\i. case \ i of None \ \ (i + 1) = None | Some C \ if stuck C then \ (i + 1) = None else \ (i + 1) \ Some ` Next C" by (auto simp add: traces_def) from this(2)[of 0] and this(1) and assms have "\ 1 \ Some ` Next C" by auto then obtain C' where "\ 1 = Some C'" and "C \ C'" by (metis Next_def imageE) show "\ \ op ## (Some C) ` \(traces ` Next C)" apply (auto simp add: traces_def image_iff) apply (rule_tac x=C' in bexI) apply (rule_tac x="seq_tl \" in exI) apply (intro conjI allI) apply (metis One_nat_def `\ 1 = Some C'` seq_tl_def) apply (metis Nat.add_0_right One_nat_def 1 add_Suc_right seq_tl_def) apply (metis `\ \ traces C` trace_hd seq_hd_cons_tl) apply (metis Next_def `C \ C'`) done next fix \ :: "config seq" assume "\ \ op ## (Some C) ` \(traces ` Next C)" then obtain \' C' where "C' \ Next C" and "\ = Some C ## \'" and "\' \ traces C'" by (auto simp add: image_iff) hence "\' 0 = Some C'" and 1: "\i. case \' i of None \ \' (i + 1) = None | Some C \ if stuck C then \' (i + 1) = None else \' (i + 1) \ Some ` Next C" by (auto simp add: traces_def) show "\ \ traces C" proof (auto simp add: traces_def) show "\ 0 = Some C" by (auto simp add: `\ = Some C ## \'`) next fix i show "case \ i of None \ \ (i + 1) = None | Some C \ (stuck C \ \ (i + 1) = None) \ (reduce C \ {} \ \ (i + 1) \ Some ` Next C)" proof (induct i) case 0 thus ?case by (smt Next_def `C' \ Next C` `\ = Some C ## \'` `\' 0 = Some C'` 1 assms seq_cons.simps option.simps(5) rev_image_eqI) next case (Suc i) thus ?case apply (unfold `\ = Some C ## \'`) apply auto apply (cases "(Some C ## \') i") apply auto apply (drule_tac traces_mono_None[OF `\' \ traces C'`]) apply auto[2] prefer 3 apply (drule_tac traces_mono_None[OF `\' \ traces C'`]) apply auto[2] proof - fix c c' \ \' assume 2: "\' (Suc i) = Some (c', \')" assume "\' i = Some (c, \)" and "stuck (c, \)" with 1[of "i"] have "\' (Suc i) = None" by auto with 2 show False by auto next fix c \ c' \' assume "(c, \) \ (c', \')" hence 2: "\ stuck (c,\)" by auto assume "\' i = Some (c, \)" with 1[of "i"] have 3: "\' (i + 1) \ Some ` Next (c, \) " apply auto apply (subst (asm) if_not_P) apply (auto simp add: 2) done assume "\' (Suc i) \ Some ` Next (c, \)" with 3 show False by auto qed qed qed qed lemma trace_from_reduces_many: assumes "stuck C'" shows "(op \ ^^ n) C C' \ \\\traces C. finite_seq (n + 1) \ \ \ n = Some C'" proof (induct n arbitrary: C) case 0 hence "C = C'" by auto with traces_of_stuck_config[OF assms] show ?case apply (rule_tac x="\x. if x = 0 then Some C' else None" in bexI) apply (auto simp add: seq_hd_def seq_tl_def) done next case (Suc n) from this(2) obtain C'' where "C \ C''" and "(op \ ^^ n) C'' C'" by (rule relpowp_Suc_E2, blast) from Suc(1)[OF this(2)] obtain \' where "\'\traces C''" and "finite_seq (n + 1) \'" and "\' n = Some C'" by auto have "\ stuck C" using `C \ C''` by auto note 1 = traces_of_nonstuck_config[OF this] show ?case apply (rule_tac x="Some C ## \'" in bexI) apply (metis Suc_eq_plus1 `\' n = Some C'` `finite_seq (n + 1) \'` finite_seq.simps(2) option.distinct(1) seq_cons.simps seq_hd_def seq_tl_cons) apply (unfold 1) apply (intro imageI UnionI[of "traces C''"]) apply (auto simp add: Next_def `C \ C''` `\'\traces C''`) done qed lemma reduces_many_from_trace': "\ \ traces C \ finite_seq (n + 1) \ \ \C'. \ n = Some C' \ (op \ ^^ n) C C' \ stuck C'" proof (induct n arbitrary: \ C) case 0 thus ?case apply (rule_tac x=C in exI) apply (intro conjI) apply (drule trace_hd, simp add: seq_hd_def) apply auto[1] apply (rule ccontr) apply (drule traces_of_nonstuck_config) apply (auto simp add: seq_tl_def seq_hd_def) apply (subgoal_tac "seq_hd x = None") apply (auto simp add: trace_hd)[1] apply (auto simp add: seq_hd_def) done next case (Suc n) have "\ stuck C" proof (rule ccontr, auto) assume "stuck C" note traces_of_stuck_config[OF this] with Suc.prems(1) have "\ 1 = None" by auto with Suc.prems(2) show False by (auto simp add: seq_hd_def seq_tl_def) qed note traces_of_nonstuck_config[OF `\ stuck C`] with Suc.prems(1) have "seq_tl \ \ \(traces ` Next C)" by (auto simp add: seq_tl_def) then obtain C'' where 1: "seq_tl \ \ traces C''" and "C \ C''" by (auto simp add: Next_def) from Suc.prems(2) have "finite_seq (n + 1) (seq_tl \)" by auto note Suc.hyps[OF 1 this] then obtain C' where 2: "seq_tl \ n = Some C'" and 3: "(op \ ^^ n) C'' C'" and "stuck C'" by auto show ?case apply (rule_tac x=C' in exI) apply (intro conjI) apply (metis 2 seq_tl_def) apply (metis (mono_tags) 3 Next_def `C \ C''` relpowp_Suc_I2) apply (rule `stuck C'`) done qed lemma reduces_many_from_trace: "\ \ traces C \ finite_seq (n + 1) \ \ \C'. \ n = Some C' \ C \* C' \ stuck C'" by (metis (lifting, no_types) reduces_many_from_trace' relpowp_imp_rtranclp) (*************************************) (* Always-terminating configurations *) (*************************************) definition always_terminates :: "config set" where "always_terminates \ {C. \\ \ traces C. \i > 0. finite_seq i \}" lemma always_terminates_stuck: assumes "stuck C" shows "C \ always_terminates" apply (unfold always_terminates_def) apply (rule CollectI) apply (intro ballI) apply (rule_tac x=1 in exI) apply (intro conjI, simp) apply (subst (asm) traces_of_stuck_config) apply (rule assms) apply (auto simp add: seq_hd_def seq_tl_def) done lemma always_terminates_step: "(\C'. C \ C' \ C' \ always_terminates) \ C \ always_terminates" apply (case_tac "stuck C") apply (rule always_terminates_stuck, assumption) apply (unfold always_terminates_def) apply (intro CollectI) apply (subst (asm) mem_Collect_eq) apply (intro ballI) apply (frule traces_of_nonstuck_config) proof - fix \ assume 1: "\C'. C \ C' \ \\\traces C'. \i>0. finite_seq i \" assume "reduce C \ {}" note 2 = traces_of_nonstuck_config[OF this] assume "\ \ traces C" with 2 obtain C' where "C \ C'" and "seq_tl \ \ traces C'" by (auto simp add: seq_tl_def Next_def) with 1 obtain i where "i>0" and "finite_seq i (seq_tl \)" by metis from this(2) show "\i>0. finite_seq i \" apply (rule_tac x="i+1" in exI) apply auto apply (metis `\ \ traces C` seq_hd_def surj_pair trace_hd) done qed lemma trace_bound: assumes "\C. finite (Next C)" assumes "C \ always_terminates" shows "\max > 0. \\\traces C. \j \ max. finite_seq j \" sorry (***********************) (* Safe configurations *) (***********************) definition safe :: "assertion \ config set" where "safe Q \ {C. \c' \'. C \* (c',\') \ stuck(c',\') \ \' \ Q}" lemma safe_step: "(\C'. C \ C' \ C' \ safe Q) = (C \ safe Q \ stuck C)" proof (rule iffI) assume "\C'. C \ C' \ C' \ safe Q" thus "C \ safe Q \ stuck C" apply (unfold safe_def) apply (case_tac "stuck C") apply auto apply (drule rtranclpD) apply (elim disjE) apply auto[1] apply (elim conjE) apply (drule tranclpD) apply auto done next assume "C \ safe Q \ stuck C" thus "\C'. C \ C' \ C' \ safe Q" apply (auto simp add: safe_def) apply (subgoal_tac "C \* (c', \')") apply auto[1] apply (rule transitive_closurep_trans', assumption, assumption) done qed lemma safe_step_forward: "C \ safe Q \ C \ C' \ C' \ safe Q" by (metis safe_step) lemma safe_step_back: "(\C'. C \ C' \ C' \ safe Q) \ \ stuck C \ C \ safe Q" by (metis safe_step) lemma safe_stuck: "\ \ Q \ stuck (c, \) \ (c, \) \ safe Q " apply (auto simp add: safe_def) apply (erule Transitive_Closure.converse_rtranclpE) apply (metis Pair_inject) apply auto done (*******************************************************) (* Partial and total correctness: original definitions *) (*******************************************************) definition pc :: "assertion \ command \ assertion \ bool" where "pc P c Q \ \\. \ \ P \ (c,\) \ safe Q " definition tc :: "assertion \ command \ assertion \ bool" where "tc P c Q \ \\. \ \ P \ ((c,\) \ always_terminates \ (c,\) \ safe Q )" (**************************************************) (* Partial and total correctness: as fixed points *) (**************************************************) definition post_if_stuck :: "assertion \ config set" where "post_if_stuck Q \ {(c,\). stuck (c,\) \ \ \ Q}" definition safe1 :: "assertion \ config set \ config set" where "safe1 Q X \ post_if_stuck Q \ \X" definition pc_fixed :: "assertion \ command \ assertion \ bool" where "pc_fixed P c Q \ {c} \ P \ (\ X. safe1 Q X)" definition tc_fixed :: "assertion \ command \ assertion \ bool" where "tc_fixed P c Q \ {c} \ P \ (\ X. safe1 Q X)" (******************************************************************************************) (* Fixed point characterisation of partial correctness coincides with original definition *) (******************************************************************************************) (* "The (k+1)th approximant of the gfp contains configurations for which every stuck configuration reachable in k steps satisfies the postcondition." *) lemma pc_helper: assumes "C \ (safe1 Q ^^ (k + 1)) UNIV" shows "(op \ ^^ k) C C' \ stuck C' \ snd C' \ Q" using assms proof (induct k arbitrary: C) case 0 thus ?case by (auto simp add: safe1_def post_if_stuck_def) next case (Suc k) hence "C \ safe1 Q ((safe1 Q ^^ Suc k) UNIV)" by auto hence 1: "\C'. C \ C' \ C' \ (safe1 Q ^^ Suc k) UNIV" unfolding safe1_def Box_def by auto from Suc(2) obtain C'' where "C \ C''" and 2: "(op \ ^^ k) C'' C'" by (erule relpowp_Suc_E2) from Suc(1)[OF 2 Suc(3)] 1[OF this(1)] show ?case by auto qed lemma downward_continuous_Box: "(\d. \ (F d)) \ \ (\d. F d)" by (auto simp add: Box_def) lemma downward_continuous_safe1: "down_cont (safe1 Q)" apply (intro down_contI) apply (thin_tac "?x") apply (rule equalityI) apply (auto simp add: safe1_def Box_def)[1] apply simp apply (unfold safe1_def) apply (subst INT_simps(2)) apply (subst if_not_P, simp) apply (rule Int_mono, simp) apply (rule downward_continuous_Box) done theorem "pc P c Q = pc_fixed P c Q" proof - have "safe Q = gfp (safe1 Q)" proof (rule equalityI) show "safe Q \ gfp (safe1 Q)" apply (rule gfp_upperbound) apply auto apply (rename_tac c \) apply (unfold safe1_def) apply (auto simp add: Box_def post_if_stuck_def) apply (case_tac "stuck (c,\)") apply (auto simp add: safe_step_forward) apply (auto simp add: safe_def) done next show "gfp (safe1 Q) \ safe Q" apply (subst INTER_down_iterate_is_gfp) apply (rule downward_continuous_safe1) apply (auto simp add: down_iterate_def) apply (unfold safe_def) apply auto apply (subst (asm) rtranclp_power) apply auto apply (erule_tac x="n + 1" in allE) apply (drule pc_helper) apply (auto simp add: snd_def) done qed thus ?thesis by (auto simp add: pc_def pc_fixed_def) qed (****************************************************************************************) (* Fixed point characterisation of total correctness coincides with original definition *) (****************************************************************************************) (* "The kth approximant of the lfp contains all configurations for which every trace terminates in fewer than k steps and satisfies the postcondition when it does so." *) lemma tc_helper: assumes "\\ \ traces C. \j \ k. finite_seq j \ \ snd (the (\ (j - 1))) \ Q" shows "C \ (safe1 Q ^^ k) {}" using assms proof (induct k arbitrary: C) case 0 hence "\\. \ \ traces C \ \ 0 = None" by simp hence "\\. \ \ traces C \ False" by (metis seq_hd_def option.distinct(1) trace_hd) with exists_trace have False by fast thus ?case by auto next case (Suc k) hence 1: "\C'. (\\'. \' \ traces C' \ \j' \ k. finite_seq j' \' \ snd (the (\' (j' - 1))) \ Q) \ C' \ (safe1 Q ^^ k) {}" and 2: "\\. \ \ traces C \ \j \ Suc k. finite_seq j \ \ snd (the (\ (j - 1))) \ Q" by auto show ?case apply auto proof (cases "stuck C") case True from traces_of_stuck_config[OF this] have "traces C = {\x. if x = 0 then Some C else None}" by auto with 2 have "\j \ Suc k. finite_seq j (\x. if x = 0 then Some C else None) \ snd (the ((\x. if x = 0 then Some C else None) (j - 1))) \ Q" by auto then obtain j where "j \ Suc k" and "finite_seq j (\x. if x = 0 then Some C else None)" and 3: "snd (the (if (j - 1) = 0 then Some C else None)) \ Q" by auto from this(2) have "j = 1" apply (case_tac "j") apply (auto simp add: seq_hd_def seq_tl_def) apply (metis option.distinct(1)) apply (metis finite_seq.elims(2) seq_hd_def) done from 3 have "snd C \ Q" unfolding `j=1` by (metis (full_types) diff_self_eq_0 the.simps) show "C \ safe1 Q ((safe1 Q ^^ k) {})" apply (unfold safe1_def Box_def) apply auto apply (insert `snd C \ Q`)[1] apply (auto simp add: post_if_stuck_def True) done next case False hence 3: "C \ post_if_stuck Q" by (cases C, auto simp add: post_if_stuck_def) from traces_of_nonstuck_config[OF False] have 5: "traces C = op ## (Some C) ` \(traces ` Next C)" by auto have 4: "\C'. C \ C' \ C' \ (safe1 Q ^^ k) {}" proof - fix C' assume "C \ C'" show "C' \ (safe1 Q ^^ k) {}" proof (rule 1) fix \' assume "\' \ traces C'" with 5 `C \ C'` have "Some C ## \' \ traces C" by (auto simp add: Next_def) from 2[OF this] obtain j where "j \ Suc k" and 6: "finite_seq j (Some C ## \')" and 7: "snd (the ((Some C ## \') (j - 1))) \ Q" by auto from 6 have "j > 0" apply (case_tac j) apply auto apply (metis option.distinct(1) seq_cons.simps(1)) done with 6 have 8: "finite_seq (j - 1) \'" by (metis diff_Suc_1 finite_seq_cons gr0_implies_Suc) show "\j'\k. finite_seq j' \' \ snd (the (\' (j' - 1))) \ Q" apply (rule_tac x="j - 1" in exI) apply (intro conjI) apply (metis `j \ Suc k` diff_Suc_eq_diff_pred diff_diff_left diff_is_0_eq) apply (rule 8) apply (smt `\' \ traces C'` 8 7 seq_cons.simps(2) trace_non_empty) done qed qed show "C \ safe1 Q ((safe1 Q ^^ k) {})" apply (unfold safe1_def Box_def) apply (auto simp add: 3 4) done qed qed lemma upward_continuous_Box: assumes "\C. finite (Next C)" assumes "up_chain F" shows "\ (\d. F d) \ (\d. \ (F d))" proof fix C assume "C \ \ (\d. F d)" hence 1: "\C' \ Next C. \d. C' \ F d" by (auto simp add: Box_def Next_def) note finite_C = assms(1)[of C] from finite_set_choice[OF finite_C 1] have "\f. \C' \ Next C. C' \ F (f C')" by auto then obtain f where 2: "\C'. C' \ Next C \ C' \ F (f C')" by auto have "\d. \C'. C \ C' \ C' \ F d" proof (cases "stuck C") case True thus ?thesis by auto next case False show ?thesis apply (rule_tac x="Max (f ` Next C)" in exI) apply (intro allI impI) proof - fix C' assume "C \ C'" hence "C' \ Next C" by (auto simp add: Next_def) from 2[OF this] have "C' \ F (f C')" by auto show "C' \ F (Max (f ` Next C))" apply (rule set_rev_mp[OF `C' \ F (f C')`]) apply (rule up_chain_mono[OF assms(2)]) apply (rule Max_ge) apply (rule finite_imageI) apply (rule finite_C) apply (rule rev_image_eqI[OF `C' \ Next C`]) apply auto done qed qed thus "C \ (\d. \ (F d))" by (auto simp add: Box_def) qed lemma upward_continuous_safe1: assumes "\C. finite (Next C)" shows "up_cont (safe1 Q)" apply (intro up_contI) apply (rule equalityI[symmetric]) apply (auto simp add: safe1_def Box_def)[1] apply simp apply (unfold safe1_def) apply (subst UN_simps(5)) apply (rule Int_mono, simp) apply (rule upward_continuous_Box[OF assms], assumption) done theorem "tc_fixed P c Q \ tc P c Q" proof - have "always_terminates \ safe Q \ lfp (safe1 Q)" proof (rule Int_greatest) show "lfp (safe1 Q) \ always_terminates" apply (rule lfp_lowerbound) apply auto apply (rename_tac c \) apply (unfold safe1_def) apply (auto simp add: Box_def) apply (case_tac "stuck (c,\)") apply (rule always_terminates_stuck, assumption) apply (rule always_terminates_step) apply auto done next show "lfp (safe1 Q) \ safe Q" apply (rule lfp_lowerbound) apply auto apply (rename_tac c \) apply (unfold safe1_def) apply (auto simp add: Box_def post_if_stuck_def) defer 1 apply (case_tac "stuck (c,\)") apply auto[1] apply (rule safe_stuck, assumption, assumption) apply (rule safe_step_back) apply auto[2] apply (metis (full_types) equals0D safe_step_back surj_pair) done qed thus ?thesis by (auto simp add: tc_def tc_fixed_def) qed theorem assumes "\C. finite (Next C)" shows "tc P c Q \ tc_fixed P c Q" proof - have "always_terminates \ safe Q \ lfp (safe1 Q)" apply (subst UNION_up_iterate_is_lfp) apply (rule upward_continuous_safe1) apply (auto simp add: up_iterate_def) apply (rename_tac c \) apply (unfold safe_def) apply (auto simp add: assms) proof - fix c \ assume "(c, \) \ always_terminates" from trace_bound[OF assms this] obtain m where 1: "\\. \ \ traces (c, \) \ \j\m. finite_seq j \" by auto assume 2: "\c' \'. (c, \) \* (c', \') \ stuck (c', \') \ \' \ Q" show "\n. (c, \) \ (safe1 Q ^^ n) {}" apply (rule_tac x="m" in exI) thm tc_helper apply (rule_tac tc_helper) apply (intro ballI) proof - fix \ assume "\ \ traces (c, \)" from 1[OF this] obtain j where "j \ m" and "finite_seq j \" by auto with trace_non_empty[OF `\ \ traces (c, \)` this(2)] have "j > 0" by auto then obtain j' where "j' + 1 = j" by (metis Suc_eq_plus1 less_not_refl3 not0_implies_Suc) with reduces_many_from_trace[OF `\ \ traces (c, \)`] `finite_seq j \` obtain C' where "\ j' = Some C'" and "(c, \) \* C' \ stuck C'" by blast with 2 have "snd (the (\ j')) \ Q" by (metis prod.exhaust snd_conv the.simps) with `j' + 1 = j` have 3: "snd (the (\ (j - Suc 0))) \ Q" by auto show "\j\m. finite_seq j \ \ snd (the (\ (j - 1))) \ Q" apply (rule_tac x="j" in exI) apply (auto simp add: `j > 0` `j \ m` `finite_seq j \` 3) done qed qed thus ?thesis by (auto simp add: tc_def tc_fixed_def) qed end