diff --git a/thys/LTL/Equivalence_Relations.thy b/thys/LTL/Equivalence_Relations.thy --- a/thys/LTL/Equivalence_Relations.thy +++ b/thys/LTL/Equivalence_Relations.thy @@ -1,567 +1,561 @@ (* Author: Benedikt Seidl License: BSD *) section \Equivalence Relations for LTL formulas\ theory Equivalence_Relations imports LTL begin subsection \Language Equivalence\ definition ltl_lang_equiv :: "'a ltln \ 'a ltln \ bool" (infix "\\<^sub>L" 75) where "\ \\<^sub>L \ \ \w. w \\<^sub>n \ \ w \\<^sub>n \" lemma ltl_lang_equiv_equivp: "equivp (\\<^sub>L)" unfolding ltl_lang_equiv_def by (simp add: equivpI reflp_def symp_def transp_def) lemma ltl_lang_equiv_and_true[simp]: "\\<^sub>1 and\<^sub>n \\<^sub>2 \\<^sub>L true\<^sub>n \ \\<^sub>1 \\<^sub>L true\<^sub>n \ \\<^sub>2 \\<^sub>L true\<^sub>n" unfolding ltl_lang_equiv_def by auto lemma ltl_lang_equiv_and_false[intro, simp]: "\\<^sub>1 \\<^sub>L false\<^sub>n \ \\<^sub>1 and\<^sub>n \\<^sub>2 \\<^sub>L false\<^sub>n" "\\<^sub>2 \\<^sub>L false\<^sub>n \ \\<^sub>1 and\<^sub>n \\<^sub>2 \\<^sub>L false\<^sub>n" unfolding ltl_lang_equiv_def by auto lemma ltl_lang_equiv_or_false[simp]: "\\<^sub>1 or\<^sub>n \\<^sub>2 \\<^sub>L false\<^sub>n \ \\<^sub>1 \\<^sub>L false\<^sub>n \ \\<^sub>2 \\<^sub>L false\<^sub>n" unfolding ltl_lang_equiv_def by auto lemma ltl_lang_equiv_or_const[intro, simp]: "\\<^sub>1 \\<^sub>L true\<^sub>n \ \\<^sub>1 or\<^sub>n \\<^sub>2 \\<^sub>L true\<^sub>n" "\\<^sub>2 \\<^sub>L true\<^sub>n \ \\<^sub>1 or\<^sub>n \\<^sub>2 \\<^sub>L true\<^sub>n" unfolding ltl_lang_equiv_def by auto - subsection \Propositional Equivalence\ fun ltl_prop_entailment :: "'a ltln set \ 'a ltln \ bool" (infix "\\<^sub>P" 80) where "\ \\<^sub>P true\<^sub>n = True" | "\ \\<^sub>P false\<^sub>n = False" | "\ \\<^sub>P \ and\<^sub>n \ = (\ \\<^sub>P \ \ \ \\<^sub>P \)" | "\ \\<^sub>P \ or\<^sub>n \ = (\ \\<^sub>P \ \ \ \\<^sub>P \)" | "\ \\<^sub>P \ = (\ \ \)" lemma ltl_prop_entailment_monotonI[intro]: "S \\<^sub>P \ \ S \ S' \ S' \\<^sub>P \" by (induction \) auto lemma ltl_models_equiv_prop_entailment: "w \\<^sub>n \ \ {\. w \\<^sub>n \} \\<^sub>P \" by (induction \) auto - definition ltl_prop_equiv :: "'a ltln \ 'a ltln \ bool" (infix "\\<^sub>P" 75) where "\ \\<^sub>P \ \ \\. \ \\<^sub>P \ \ \ \\<^sub>P \" definition ltl_prop_implies :: "'a ltln \ 'a ltln \ bool" (infix "\\<^sub>P" 75) where "\ \\<^sub>P \ \ \\. \ \\<^sub>P \ \ \ \\<^sub>P \" lemma ltl_prop_implies_equiv: "\ \\<^sub>P \ \ (\ \\<^sub>P \ \ \ \\<^sub>P \)" unfolding ltl_prop_equiv_def ltl_prop_implies_def by meson lemma ltl_prop_equiv_equivp: "equivp (\\<^sub>P)" by (simp add: ltl_prop_equiv_def equivpI reflp_def symp_def transp_def) lemma ltl_prop_equiv_trans[trans]: "\ \\<^sub>P \ \ \ \\<^sub>P \ \ \ \\<^sub>P \" by (simp add: ltl_prop_equiv_def) lemma ltl_prop_equiv_true: "\ \\<^sub>P true\<^sub>n \ {} \\<^sub>P \" using bot.extremum ltl_prop_entailment.simps(1) ltl_prop_equiv_def by blast lemma ltl_prop_equiv_false: "\ \\<^sub>P false\<^sub>n \ \ UNIV \\<^sub>P \" by (meson ltl_prop_entailment.simps(2) ltl_prop_entailment_monotonI ltl_prop_equiv_def top_greatest) lemma ltl_prop_equiv_true_implies_true: "x \\<^sub>P true\<^sub>n \ x \\<^sub>P y \ y \\<^sub>P true\<^sub>n" by (simp add: ltl_prop_equiv_def ltl_prop_implies_def) lemma ltl_prop_equiv_false_implied_by_false: "y \\<^sub>P false\<^sub>n \ x \\<^sub>P y \ x \\<^sub>P false\<^sub>n" by (simp add: ltl_prop_equiv_def ltl_prop_implies_def) lemma ltl_prop_implication_implies_ltl_implication: "w \\<^sub>n \ \ \ \\<^sub>P \ \ w \\<^sub>n \" using ltl_models_equiv_prop_entailment ltl_prop_implies_def by blast lemma ltl_prop_equiv_implies_ltl_lang_equiv: "\ \\<^sub>P \ \ \ \\<^sub>L \" using ltl_lang_equiv_def ltl_prop_implication_implies_ltl_implication ltl_prop_implies_equiv by blast lemma ltl_prop_equiv_lt_ltl_lang_equiv[simp]: "(\\<^sub>P) \ (\\<^sub>L)" using ltl_prop_equiv_implies_ltl_lang_equiv by blast - subsection \Constants Equivalence\ datatype tvl = Yes | No | Maybe definition eval_and :: "tvl \ tvl \ tvl" where "eval_and \ \ = (case (\, \) of (Yes, Yes) \ Yes | (No, _) \ No | (_, No) \ No | _ \ Maybe)" definition eval_or :: "tvl \ tvl \ tvl" where "eval_or \ \ = (case (\, \) of (No, No) \ No | (Yes, _) \ Yes | (_, Yes) \ Yes | _ \ Maybe)" fun eval :: "'a ltln \ tvl" where "eval true\<^sub>n = Yes" | "eval false\<^sub>n = No" | "eval (\ and\<^sub>n \) = eval_and (eval \) (eval \)" | "eval (\ or\<^sub>n \) = eval_or (eval \) (eval \)" | "eval \ = Maybe" lemma eval_and_const[simp]: "eval_and \ \ = No \ \ = No \ \ = No" "eval_and \ \ = Yes \ \ = Yes \ \ = Yes" unfolding eval_and_def by (cases \; cases \, auto)+ lemma eval_or_const[simp]: "eval_or \ \ = Yes \ \ = Yes \ \ = Yes" "eval_or \ \ = No \ \ = No \ \ = No" unfolding eval_or_def by (cases \; cases \, auto)+ lemma eval_prop_entailment: "eval \ = Yes \ {} \\<^sub>P \" "eval \ = No \ \ UNIV \\<^sub>P \" by (induction \) auto - definition ltl_const_equiv :: "'a ltln \ 'a ltln \ bool" (infix "\\<^sub>C" 75) where "\ \\<^sub>C \ \ \ = \ \ (eval \ = eval \ \ eval \ \ Maybe)" lemma ltl_const_equiv_equivp: "equivp (\\<^sub>C)" unfolding ltl_const_equiv_def by (intro equivpI reflpI sympI transpI) auto lemma ltl_const_equiv_const: "\ \\<^sub>C true\<^sub>n \ eval \ = Yes" "\ \\<^sub>C false\<^sub>n \ eval \ = No" unfolding ltl_const_equiv_def by force+ lemma ltl_const_equiv_and_const[simp]: "\\<^sub>1 and\<^sub>n \\<^sub>2 \\<^sub>C true\<^sub>n \ \\<^sub>1 \\<^sub>C true\<^sub>n \ \\<^sub>2 \\<^sub>C true\<^sub>n" "\\<^sub>1 and\<^sub>n \\<^sub>2 \\<^sub>C false\<^sub>n \ \\<^sub>1 \\<^sub>C false\<^sub>n \ \\<^sub>2 \\<^sub>C false\<^sub>n" unfolding ltl_const_equiv_const by force+ lemma ltl_const_equiv_or_const[simp]: "\\<^sub>1 or\<^sub>n \\<^sub>2 \\<^sub>C true\<^sub>n \ \\<^sub>1 \\<^sub>C true\<^sub>n \ \\<^sub>2 \\<^sub>C true\<^sub>n" "\\<^sub>1 or\<^sub>n \\<^sub>2 \\<^sub>C false\<^sub>n \ \\<^sub>1 \\<^sub>C false\<^sub>n \ \\<^sub>2 \\<^sub>C false\<^sub>n" unfolding ltl_const_equiv_const by force+ lemma ltl_const_equiv_other[simp]: "\ \\<^sub>C prop\<^sub>n(a) \ \ = prop\<^sub>n(a)" "\ \\<^sub>C nprop\<^sub>n(a) \ \ = nprop\<^sub>n(a)" "\ \\<^sub>C X\<^sub>n \ \ \ = X\<^sub>n \" "\ \\<^sub>C \\<^sub>1 U\<^sub>n \\<^sub>2 \ \ = \\<^sub>1 U\<^sub>n \\<^sub>2" "\ \\<^sub>C \\<^sub>1 R\<^sub>n \\<^sub>2 \ \ = \\<^sub>1 R\<^sub>n \\<^sub>2" "\ \\<^sub>C \\<^sub>1 W\<^sub>n \\<^sub>2 \ \ = \\<^sub>1 W\<^sub>n \\<^sub>2" "\ \\<^sub>C \\<^sub>1 M\<^sub>n \\<^sub>2 \ \ = \\<^sub>1 M\<^sub>n \\<^sub>2" using ltl_const_equiv_def by fastforce+ lemma ltl_const_equiv_no_const_singleton: "eval \ = Maybe \ \ \\<^sub>C \ \ \ = \" unfolding ltl_const_equiv_def by fastforce - lemma ltl_const_equiv_implies_prop_equiv: "\ \\<^sub>C true\<^sub>n \ \ \\<^sub>P true\<^sub>n" "\ \\<^sub>C false\<^sub>n \ \ \\<^sub>P false\<^sub>n" unfolding ltl_const_equiv_const eval_prop_entailment ltl_prop_equiv_def by auto lemma ltl_const_equiv_no_const_prop_equiv: "eval \ = Maybe \ \ \\<^sub>C \ \ \ \\<^sub>P \" using ltl_const_equiv_no_const_singleton equivp_reflp[OF ltl_prop_equiv_equivp] by blast lemma ltl_const_equiv_implies_ltl_prop_equiv: "\ \\<^sub>C \ \ \ \\<^sub>P \" proof (induction \) case (And_ltln \1 \2) show ?case proof (cases "eval (\1 and\<^sub>n \2)") case Yes then have "\ \\<^sub>C true\<^sub>n" by (meson And_ltln.prems equivp_transp ltl_const_equiv_const(1) ltl_const_equiv_equivp) then show ?thesis by (metis (full_types) Yes ltl_const_equiv_const(1) ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_trans ltl_prop_implies_equiv) next case No then have "\ \\<^sub>C false\<^sub>n" by (meson And_ltln.prems equivp_transp ltl_const_equiv_const(2) ltl_const_equiv_equivp) then show ?thesis by (metis (full_types) No ltl_const_equiv_const(2) ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_trans ltl_prop_implies_equiv) next case Maybe then show ?thesis using And_ltln.prems ltl_const_equiv_no_const_prop_equiv by force qed next case (Or_ltln \1 \2) then show ?case proof (cases "eval (\1 or\<^sub>n \2)") case Yes then have "\ \\<^sub>C true\<^sub>n" by (meson Or_ltln.prems equivp_transp ltl_const_equiv_const(1) ltl_const_equiv_equivp) then show ?thesis by (metis (full_types) Yes ltl_const_equiv_const(1) ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_trans ltl_prop_implies_equiv) next case No then have "\ \\<^sub>C false\<^sub>n" by (meson Or_ltln.prems equivp_transp ltl_const_equiv_const(2) ltl_const_equiv_equivp) then show ?thesis by (metis (full_types) No ltl_const_equiv_const(2) ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_trans ltl_prop_implies_equiv) next case Maybe then show ?thesis using Or_ltln.prems ltl_const_equiv_no_const_prop_equiv by force qed qed (simp_all add: ltl_const_equiv_implies_prop_equiv equivp_reflp[OF ltl_prop_equiv_equivp]) lemma ltl_const_equiv_lt_ltl_prop_equiv[simp]: "(\\<^sub>C) \ (\\<^sub>P)" using ltl_const_equiv_implies_ltl_prop_equiv by blast - subsection \Quotient types\ quotient_type 'a ltln\<^sub>L = "'a ltln" / "(\\<^sub>L)" by (rule ltl_lang_equiv_equivp) instantiation ltln\<^sub>L :: (type) equal begin lift_definition ltln\<^sub>L_eq_test :: "'a ltln\<^sub>L \ 'a ltln\<^sub>L \ bool" is "\x y. x \\<^sub>L y" by (metis ltln\<^sub>L.abs_eq_iff) definition eq\<^sub>L: "equal_class.equal \ ltln\<^sub>L_eq_test" instance by (standard; simp add: eq\<^sub>L ltln\<^sub>L_eq_test.rep_eq, metis Quotient_ltln\<^sub>L Quotient_rel_rep) end quotient_type 'a ltln\<^sub>P = "'a ltln" / "(\\<^sub>P)" by (rule ltl_prop_equiv_equivp) instantiation ltln\<^sub>P :: (type) equal begin lift_definition ltln\<^sub>P_eq_test :: "'a ltln\<^sub>P \ 'a ltln\<^sub>P \ bool" is "\x y. x \\<^sub>P y" by (metis ltln\<^sub>P.abs_eq_iff) definition eq\<^sub>P: "equal_class.equal \ ltln\<^sub>P_eq_test" instance by (standard; simp add: eq\<^sub>P ltln\<^sub>P_eq_test.rep_eq, metis Quotient_ltln\<^sub>P Quotient_rel_rep) end quotient_type 'a ltln\<^sub>C = "'a ltln" / "(\\<^sub>C)" by (rule ltl_const_equiv_equivp) instantiation ltln\<^sub>C :: (type) equal begin lift_definition ltln\<^sub>C_eq_test :: "'a ltln\<^sub>C \ 'a ltln\<^sub>C \ bool" is "\x y. x \\<^sub>C y" by (metis ltln\<^sub>C.abs_eq_iff) definition eq\<^sub>C: "equal_class.equal \ ltln\<^sub>C_eq_test" instance by (standard; simp add: eq\<^sub>C ltln\<^sub>C_eq_test.rep_eq, metis Quotient_ltln\<^sub>C Quotient_rel_rep) end subsection \Cardinality of propositional quotient sets\ definition sat_models :: "'a ltln\<^sub>P \ 'a ltln set set" where "sat_models \ = {\. \ \\<^sub>P rep_ltln\<^sub>P \}" lemma Rep_Abs_prop_entailment[simp]: "\ \\<^sub>P rep_ltln\<^sub>P (abs_ltln\<^sub>P \) = \ \\<^sub>P \" by (metis Quotient3_ltln\<^sub>P Quotient3_rep_abs ltl_prop_equiv_def) lemma sat_models_Abs: "\ \ sat_models (abs_ltln\<^sub>P \) = \ \\<^sub>P \" by (simp add: sat_models_def) lemma sat_models_inj: "inj sat_models" proof (rule injI) fix \ \ :: "'a ltln\<^sub>P" assume "sat_models \ = sat_models \" then have "rep_ltln\<^sub>P \ \\<^sub>P rep_ltln\<^sub>P \" unfolding sat_models_def ltl_prop_equiv_def by force then show "\ = \" by (meson Quotient3_ltln\<^sub>P Quotient3_rel_rep) qed fun prop_atoms :: "'a ltln \ 'a ltln set" where "prop_atoms true\<^sub>n = {}" | "prop_atoms false\<^sub>n = {}" | "prop_atoms (\ and\<^sub>n \) = prop_atoms \ \ prop_atoms \" | "prop_atoms (\ or\<^sub>n \) = prop_atoms \ \ prop_atoms \" | "prop_atoms \ = {\}" fun nested_prop_atoms :: "'a ltln \ 'a ltln set" where "nested_prop_atoms true\<^sub>n = {}" | "nested_prop_atoms false\<^sub>n = {}" | "nested_prop_atoms (\ and\<^sub>n \) = nested_prop_atoms \ \ nested_prop_atoms \" | "nested_prop_atoms (\ or\<^sub>n \) = nested_prop_atoms \ \ nested_prop_atoms \" | "nested_prop_atoms (X\<^sub>n \) = {X\<^sub>n \} \ nested_prop_atoms \" | "nested_prop_atoms (\ U\<^sub>n \) = {\ U\<^sub>n \} \ nested_prop_atoms \ \ nested_prop_atoms \" | "nested_prop_atoms (\ R\<^sub>n \) = {\ R\<^sub>n \} \ nested_prop_atoms \ \ nested_prop_atoms \" | "nested_prop_atoms (\ W\<^sub>n \) = {\ W\<^sub>n \} \ nested_prop_atoms \ \ nested_prop_atoms \" | "nested_prop_atoms (\ M\<^sub>n \) = {\ M\<^sub>n \} \ nested_prop_atoms \ \ nested_prop_atoms \" | "nested_prop_atoms \ = {\}" lemma prop_atoms_nested_prop_atoms: "prop_atoms \ \ nested_prop_atoms \" by (induction \) auto lemma prop_atoms_subfrmlsn: "prop_atoms \ \ subfrmlsn \" by (induction \) auto lemma nested_prop_atoms_subfrmlsn: "nested_prop_atoms \ \ subfrmlsn \" by (induction \) auto lemma prop_atoms_notin[simp]: "true\<^sub>n \ prop_atoms \" "false\<^sub>n \ prop_atoms \" "\\<^sub>1 and\<^sub>n \\<^sub>2 \ prop_atoms \" "\\<^sub>1 or\<^sub>n \\<^sub>2 \ prop_atoms \" by (induction \) auto lemma nested_prop_atoms_notin[simp]: "true\<^sub>n \ nested_prop_atoms \" "false\<^sub>n \ nested_prop_atoms \" "\\<^sub>1 and\<^sub>n \\<^sub>2 \ nested_prop_atoms \" "\\<^sub>1 or\<^sub>n \\<^sub>2 \ nested_prop_atoms \" by (induction \) auto lemma prop_atoms_finite: "finite (prop_atoms \)" by (induction \) auto lemma nested_prop_atoms_finite: "finite (nested_prop_atoms \)" by (induction \) auto lemma prop_atoms_entailment_iff: "\ \ prop_atoms \ \ \ \\<^sub>P \ \ \ \ \" by (induction \) auto lemma prop_atoms_entailment_inter: "prop_atoms \ \ P \ (\ \ P) \\<^sub>P \ = \ \\<^sub>P \" by (induction \) auto lemma nested_prop_atoms_entailment_inter: "nested_prop_atoms \ \ P \ (\ \ P) \\<^sub>P \ = \ \\<^sub>P \" by (induction \) auto lemma sat_models_inter_inj_helper: assumes "prop_atoms \ \ P" and "prop_atoms \ \ P" and "sat_models (abs_ltln\<^sub>P \) \ Pow P = sat_models (abs_ltln\<^sub>P \) \ Pow P" shows "\ \\<^sub>P \" proof - from assms have "\\. (\ \ P) \\<^sub>P \ \ (\ \ P) \\<^sub>P \" by (auto simp: sat_models_Abs) with assms show "\ \\<^sub>P \" by (simp add: prop_atoms_entailment_inter ltl_prop_equiv_def) qed lemma sat_models_inter_inj: "inj_on (\\. sat_models \ \ Pow P) {abs_ltln\<^sub>P \ |\. prop_atoms \ \ P}" by (auto simp: inj_on_def sat_models_inter_inj_helper ltln\<^sub>P.abs_eq_iff) lemma sat_models_pow_pow: "{sat_models (abs_ltln\<^sub>P \) \ Pow P | \. prop_atoms \ \ P} \ Pow (Pow P)" by (auto simp: sat_models_def) lemma sat_models_finite: "finite P \ finite {sat_models (abs_ltln\<^sub>P \) \ Pow P | \. prop_atoms \ \ P}" using sat_models_pow_pow finite_subset by fastforce lemma sat_models_card: "finite P \ card ({sat_models (abs_ltln\<^sub>P \) \ Pow P | \. prop_atoms \ \ P}) \ 2 ^ 2 ^ card P" by (metis (mono_tags, lifting) sat_models_pow_pow Pow_def card_Pow card_mono finite_Collect_subsets) lemma image_filter: "f ` {g a | a. P a} = {f (g a) | a. P a}" by blast lemma prop_equiv_finite: "finite P \ finite {abs_ltln\<^sub>P \ | \. prop_atoms \ \ P}" by (auto simp: image_filter sat_models_finite finite_imageD[OF _ sat_models_inter_inj]) lemma prop_equiv_card: "finite P \ card {abs_ltln\<^sub>P \ | \. prop_atoms \ \ P} \ 2 ^ 2 ^ card P" by (auto simp: image_filter sat_models_card card_image[OF sat_models_inter_inj, symmetric]) lemma prop_equiv_subset: "{abs_ltln\<^sub>P \ |\. nested_prop_atoms \ \ P} \ {abs_ltln\<^sub>P \ |\. prop_atoms \ \ P}" using prop_atoms_nested_prop_atoms by blast lemma prop_equiv_finite': "finite P \ finite {abs_ltln\<^sub>P \ | \. nested_prop_atoms \ \ P}" using prop_equiv_finite prop_equiv_subset finite_subset by fast lemma prop_equiv_card': "finite P \ card {abs_ltln\<^sub>P \ | \. nested_prop_atoms \ \ P} \ 2 ^ 2 ^ card P" by (metis (mono_tags, lifting) prop_equiv_card prop_equiv_subset prop_equiv_finite card_mono le_trans) subsection \Substitution\ fun subst :: "'a ltln \ ('a ltln \ 'a ltln) \ 'a ltln" where "subst true\<^sub>n m = true\<^sub>n" | "subst false\<^sub>n m = false\<^sub>n" | "subst (\ and\<^sub>n \) m = subst \ m and\<^sub>n subst \ m" | "subst (\ or\<^sub>n \) m = subst \ m or\<^sub>n subst \ m" | "subst \ m = (case m \ of Some \ \ \ | None \ \)" text \Based on Uwe Schoening's Translation Lemma (Logic for CS, p. 54)\ lemma ltl_prop_equiv_subst_S: "S \\<^sub>P subst \ m = ((S - dom m) \ {\ | \ \'. \ \ dom m \ m \ = Some \' \ S \\<^sub>P \'}) \\<^sub>P \" by (induction \) (auto split: option.split) lemma subst_respects_ltl_prop_entailment: "\ \\<^sub>P \ \ subst \ m \\<^sub>P subst \ m" "\ \\<^sub>P \ \ subst \ m \\<^sub>P subst \ m" unfolding ltl_prop_equiv_def ltl_prop_implies_def ltl_prop_equiv_subst_S by blast+ lemma eval_subst: "eval \ = Yes \ eval (subst \ m) = Yes" "eval \ = No \ eval (subst \ m) = No" by (meson empty_subsetI eval_prop_entailment ltl_prop_entailment_monotonI ltl_prop_equiv_subst_S subset_UNIV)+ lemma subst_respects_ltl_const_entailment: "\ \\<^sub>C \ \ subst \ m \\<^sub>C subst \ m" unfolding ltl_const_equiv_def by (cases "eval \") (metis eval_subst(1), metis eval_subst(2), blast) subsection \Order of Equivalence Relations\ locale ltl_equivalence = fixes eq :: "'a ltln \ 'a ltln \ bool" (infix "\" 75) assumes eq_equivp: "equivp (\)" and ge_const_equiv: "(\\<^sub>C) \ (\)" and le_lang_equiv: "(\) \ (\\<^sub>L)" begin lemma eq_implies_ltl_equiv: "\ \ \ \ w \\<^sub>n \ = w \\<^sub>n \" using le_lang_equiv ltl_lang_equiv_def by blast lemma const_implies_eq: "\ \\<^sub>C \ \ \ \ \" using ge_const_equiv by blast lemma eq_implies_lang: "\ \ \ \ \ \\<^sub>L \" using le_lang_equiv by blast lemma eq_refl[simp]: "\ \ \" by (meson eq_equivp equivp_reflp) lemma eq_sym[sym]: "\ \ \ \ \ \ \" by (meson eq_equivp equivp_symp) lemma eq_trans[trans]: "\ \ \ \ \ \ \ \ \ \ \" by (meson eq_equivp equivp_transp) end interpretation ltl_lang_equivalence: ltl_equivalence "(\\<^sub>L)" using ltl_lang_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv by unfold_locales blast+ interpretation ltl_prop_equivalence: ltl_equivalence "(\\<^sub>P)" using ltl_prop_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv by unfold_locales blast+ interpretation ltl_const_equivalence: ltl_equivalence "(\\<^sub>C)" using ltl_const_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv by unfold_locales blast+ end diff --git a/thys/LTL/LTL.thy b/thys/LTL/LTL.thy --- a/thys/LTL/LTL.thy +++ b/thys/LTL/LTL.thy @@ -1,1185 +1,1189 @@ (* Author: Salomon Sickert Author: Benedikt Seidl Author: Alexander Schimpf (original entry: CAVA/LTL.thy) Author: Stephan Merz (original entry: Stuttering_Equivalence/PLTL.thy) License: BSD *) section \Linear Temporal Logic\ theory LTL imports Main "HOL-Library.Omega_Words_Fun" begin text \This theory provides a formalisation of linear temporal logic. It provides three variants: \begin{enumerate} \item LTL with syntactic sugar. This variant is the semantic reference and the included parser generates ASTs of this datatype. \item LTL in negation normal form without syntactic sugar. This variant is used by the included rewriting engine and is used for the translation to automata (implemented in other entries). \item LTL in restricted negation normal form without the rather uncommon operators ``weak until'' and ``strong release''. It is used by the formalization of Gerth's algorithm. \item PLTL. A variant with a reduced set of operators. \end{enumerate} This theory subsumes (and partly reuses) the existing formalisation found in LTL\_to\_GBA and Stuttering\_Equivalence and unifies them.\ subsection \LTL with Syntactic Sugar\ text \In this section, we provide a formulation of LTL with explicit syntactic sugar deeply embedded. This formalization serves as a reference semantics.\ subsubsection \Syntax\ datatype (atoms_ltlc: 'a) ltlc = True_ltlc ("true\<^sub>c") | False_ltlc ("false\<^sub>c") | Prop_ltlc 'a ("prop\<^sub>c'(_')") | Not_ltlc "'a ltlc" ("not\<^sub>c _" [85] 85) | And_ltlc "'a ltlc" "'a ltlc" ("_ and\<^sub>c _" [82,82] 81) | Or_ltlc "'a ltlc" "'a ltlc" ("_ or\<^sub>c _" [81,81] 80) | Implies_ltlc "'a ltlc" "'a ltlc" ("_ implies\<^sub>c _" [81,81] 80) | Next_ltlc "'a ltlc" ("X\<^sub>c _" [88] 87) | Final_ltlc "'a ltlc" ("F\<^sub>c _" [88] 87) | Global_ltlc "'a ltlc" ("G\<^sub>c _" [88] 87) | Until_ltlc "'a ltlc" "'a ltlc" ("_ U\<^sub>c _" [84,84] 83) | Release_ltlc "'a ltlc" "'a ltlc" ("_ R\<^sub>c _" [84,84] 83) | WeakUntil_ltlc "'a ltlc" "'a ltlc" ("_ W\<^sub>c _" [84,84] 83) | StrongRelease_ltlc "'a ltlc" "'a ltlc" ("_ M\<^sub>c _" [84,84] 83) definition Iff_ltlc ("_ iff\<^sub>c _" [81,81] 80) where "\ iff\<^sub>c \ \ (\ implies\<^sub>c \) and\<^sub>c (\ implies\<^sub>c \)" subsubsection \Semantics\ primrec semantics_ltlc :: "['a set word, 'a ltlc] \ bool" ("_ \\<^sub>c _" [80,80] 80) where "\ \\<^sub>c true\<^sub>c = True" | "\ \\<^sub>c false\<^sub>c = False" | "\ \\<^sub>c prop\<^sub>c(q) = (q\\ 0)" | "\ \\<^sub>c not\<^sub>c \ = (\ \ \\<^sub>c \)" | "\ \\<^sub>c \ and\<^sub>c \ = (\ \\<^sub>c \ \ \ \\<^sub>c \)" | "\ \\<^sub>c \ or\<^sub>c \ = (\ \\<^sub>c \ \ \ \\<^sub>c \)" | "\ \\<^sub>c \ implies\<^sub>c \ = (\ \\<^sub>c \ \ \ \\<^sub>c \)" | "\ \\<^sub>c X\<^sub>c \ = (suffix 1 \ \\<^sub>c \)" | "\ \\<^sub>c F\<^sub>c \ = (\i. suffix i \ \\<^sub>c \)" | "\ \\<^sub>c G\<^sub>c \ = (\i. suffix i \ \\<^sub>c \)" | "\ \\<^sub>c \ U\<^sub>c \ = (\i. suffix i \ \\<^sub>c \ \ (\j \\<^sub>c \))" | "\ \\<^sub>c \ R\<^sub>c \ = (\i. suffix i \ \\<^sub>c \ \ (\j \\<^sub>c \))" | "\ \\<^sub>c \ W\<^sub>c \ = (\i. suffix i \ \\<^sub>c \ \ (\j\i. suffix j \ \\<^sub>c \))" | "\ \\<^sub>c \ M\<^sub>c \ = (\i. suffix i \ \\<^sub>c \ \ (\j\i. suffix j \ \\<^sub>c \))" lemma semantics_ltlc_sugar [simp]: "\ \\<^sub>c \ iff\<^sub>c \ = (\ \\<^sub>c \ \ \ \\<^sub>c \)" "\ \\<^sub>c F\<^sub>c \ = \ \\<^sub>c (true\<^sub>c U\<^sub>c \)" "\ \\<^sub>c G\<^sub>c \ = \ \\<^sub>c (false\<^sub>c R\<^sub>c \)" by (auto simp add: Iff_ltlc_def) definition "language_ltlc \ \ {\. \ \\<^sub>c \}" lemma language_ltlc_negate[simp]: "language_ltlc (not\<^sub>c \) = - language_ltlc \" unfolding language_ltlc_def by auto lemma ltl_true_or_con[simp]: "\ \\<^sub>c prop\<^sub>c(p) or\<^sub>c (not\<^sub>c prop\<^sub>c(p))" by auto lemma ltl_false_true_con[simp]: "\ \\<^sub>c not\<^sub>c true\<^sub>c \ \ \\<^sub>c false\<^sub>c" by auto lemma ltl_Next_Neg_con[simp]: "\ \\<^sub>c X\<^sub>c (not\<^sub>c \) \ \ \\<^sub>c not\<^sub>c X\<^sub>c \" by auto \ \The connection between dual operators\ lemma ltl_Until_Release_con: "\ \\<^sub>c \ R\<^sub>c \ \ (\ \ \\<^sub>c (not\<^sub>c \) U\<^sub>c (not\<^sub>c \))" "\ \\<^sub>c \ U\<^sub>c \ \ (\ \ \\<^sub>c (not\<^sub>c \) R\<^sub>c (not\<^sub>c \))" by auto lemma ltl_WeakUntil_StrongRelease_con: "\ \\<^sub>c \ W\<^sub>c \ \ (\ \ \\<^sub>c (not\<^sub>c \) M\<^sub>c (not\<^sub>c \))" "\ \\<^sub>c \ M\<^sub>c \ \ (\ \ \\<^sub>c (not\<^sub>c \) W\<^sub>c (not\<^sub>c \))" by auto \ \The connection between weak and strong operators\ lemma ltl_Release_StrongRelease_con: "\ \\<^sub>c \ R\<^sub>c \ \ \ \\<^sub>c (\ M\<^sub>c \) or\<^sub>c (G\<^sub>c \)" "\ \\<^sub>c \ M\<^sub>c \ \ \ \\<^sub>c (\ R\<^sub>c \) and\<^sub>c (F\<^sub>c \)" proof safe assume asm: "\ \\<^sub>c \ R\<^sub>c \" show "\ \\<^sub>c (\ M\<^sub>c \) or\<^sub>c (G\<^sub>c \)" proof (cases "\ \\<^sub>c G\<^sub>c \") case False then obtain i where "\ suffix i \ \\<^sub>c \" and "\j \\<^sub>c \" using exists_least_iff[of "\i. \ suffix i \ \\<^sub>c \"] by force then show ?thesis using asm by force qed simp next assume asm: "\ \\<^sub>c (\ R\<^sub>c \) and\<^sub>c (F\<^sub>c \)" then show "\ \\<^sub>c \ M\<^sub>c \" proof (cases "\ \\<^sub>c F\<^sub>c \") case True then obtain i where "suffix i \ \\<^sub>c \" and "\j suffix j \ \\<^sub>c \" using exists_least_iff[of "\i. suffix i \ \\<^sub>c \"] by force then show ?thesis using asm by force qed simp qed (unfold semantics_ltlc.simps; insert not_less, blast)+ lemma ltl_Until_WeakUntil_con: "\ \\<^sub>c \ U\<^sub>c \ \ \ \\<^sub>c (\ W\<^sub>c \) and\<^sub>c (F\<^sub>c \)" "\ \\<^sub>c \ W\<^sub>c \ \ \ \\<^sub>c (\ U\<^sub>c \) or\<^sub>c (G\<^sub>c \)" proof safe assume asm: "\ \\<^sub>c (\ W\<^sub>c \) and\<^sub>c (F\<^sub>c \)" then show "\ \\<^sub>c \ U\<^sub>c \" proof (cases "\ \\<^sub>c F\<^sub>c \") case True then obtain i where "suffix i \ \\<^sub>c \" and "\j suffix j \ \\<^sub>c \" using exists_least_iff[of "\i. suffix i \ \\<^sub>c \"] by force then show ?thesis using asm by force qed simp next assume asm: "\ \\<^sub>c \ W\<^sub>c \" then show "\ \\<^sub>c (\ U\<^sub>c \) or\<^sub>c (G\<^sub>c \)" proof (cases "\ \\<^sub>c G\<^sub>c \") case False then obtain i where "\ suffix i \ \\<^sub>c \" and "\j \\<^sub>c \" using exists_least_iff[of "\i. \ suffix i \ \\<^sub>c \"] by force then show ?thesis using asm by force qed simp qed (unfold semantics_ltlc.simps; insert not_less, blast)+ lemma ltl_StrongRelease_Until_con: "\ \\<^sub>c \ M\<^sub>c \ \ \ \\<^sub>c \ U\<^sub>c (\ and\<^sub>c \)" using order.order_iff_strict by auto lemma ltl_WeakUntil_Release_con: "\ \\<^sub>c \ R\<^sub>c \ \ \ \\<^sub>c \ W\<^sub>c (\ and\<^sub>c \)" by (meson ltl_Release_StrongRelease_con(1) ltl_StrongRelease_Until_con ltl_Until_WeakUntil_con(2) semantics_ltlc.simps(6)) definition "pw_eq_on S w w' \ \i. w i \ S = w' i \ S" lemma pw_eq_on_refl[simp]: "pw_eq_on S w w" and pw_eq_on_sym: "pw_eq_on S w w' \ pw_eq_on S w' w" and pw_eq_on_trans[trans]: "\pw_eq_on S w w'; pw_eq_on S w' w''\ \ pw_eq_on S w w''" unfolding pw_eq_on_def by auto lemma pw_eq_on_suffix: "pw_eq_on S w w' \ pw_eq_on S (suffix k w) (suffix k w')" by (simp add: pw_eq_on_def) lemma pw_eq_on_subset: "S \ S' \ pw_eq_on S' w w' \ pw_eq_on S w w'" by (auto simp add: pw_eq_on_def) lemma ltlc_eq_on_aux: "pw_eq_on (atoms_ltlc \) w w' \ w \\<^sub>c \ \ w' \\<^sub>c \" proof (induction \ arbitrary: w w') case Until_ltlc thus ?case by simp (meson Un_upper1 Un_upper2 pw_eq_on_subset pw_eq_on_suffix) next case Release_ltlc thus ?case by simp (metis Un_upper1 pw_eq_on_subset pw_eq_on_suffix sup_commute) next case WeakUntil_ltlc thus ?case by simp (meson pw_eq_on_subset pw_eq_on_suffix sup.cobounded1 sup_ge2) next case StrongRelease_ltlc thus ?case by simp (metis Un_upper1 pw_eq_on_subset pw_eq_on_suffix pw_eq_on_sym sup_ge2) next case (And_ltlc \ \) thus ?case by simp (meson Un_upper1 inf_sup_ord(4) pw_eq_on_subset) next case (Or_ltlc \ \) thus ?case by simp (meson Un_upper2 pw_eq_on_subset sup_ge1) next case (Implies_ltlc \ \) thus ?case by simp (meson Un_upper1 Un_upper2 pw_eq_on_subset[of "atoms_ltlc _" "atoms_ltlc \ \ atoms_ltlc \"] pw_eq_on_sym) qed (auto simp add: pw_eq_on_def; metis suffix_nth)+ lemma ltlc_eq_on: "pw_eq_on (atoms_ltlc \) w w' \ w \\<^sub>c \ \ w' \\<^sub>c \" using ltlc_eq_on_aux pw_eq_on_sym by blast lemma suffix_comp: "(\i. f (suffix k w i)) = suffix k (f o w)" by auto lemma suffix_range: "\(range \) \ APs \ \(range (suffix k \)) \ APs" by auto lemma map_semantics_ltlc_aux: assumes "inj_on f APs" assumes "\(range w) \ APs" assumes "atoms_ltlc \ \ APs" shows "w \\<^sub>c \ \ (\i. f ` w i) \\<^sub>c map_ltlc f \" using assms(2,3) proof (induction \ arbitrary: w) case (Prop_ltlc x) thus ?case using assms(1) by (simp add: SUP_le_iff inj_on_image_mem_iff) next case (Next_ltlc \) show ?case using Next_ltlc(1)[of "suffix 1 w", unfolded suffix_comp comp_def] Next_ltlc(2,3) apply simp by (metis Next_ltlc.prems(1) One_nat_def \\\(range (suffix 1 w)) \ APs; atoms_ltlc \ \ APs\ \ suffix 1 w \\<^sub>c \ = suffix 1 (\x. f ` w x) \\<^sub>c map_ltlc f \\ suffix_range) next case (Final_ltlc \) thus ?case using Final_ltlc(1)[of "suffix _ _", unfolded suffix_comp comp_def, OF suffix_range] by fastforce next case (Global_ltlc) thus ?case using Global_ltlc(1)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce next case (Until_ltlc) thus ?case using Until_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce next case (Release_ltlc) thus ?case using Release_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce next case (WeakUntil_ltlc) thus ?case using WeakUntil_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce next case (StrongRelease_ltlc) thus ?case using StrongRelease_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce qed simp+ definition "map_props f APs \ {i. \p\APs. f p = Some i}" lemma map_semantics_ltlc: assumes INJ: "inj_on f (dom f)" and DOM: "atoms_ltlc \ \ dom f" shows "\ \\<^sub>c \ \ (map_props f o \) \\<^sub>c map_ltlc (the o f) \" proof - let ?\r = "\i. \ i \ atoms_ltlc \" let ?\r' = "\i. \ i \ dom f" have 1: "\(range ?\r) \ atoms_ltlc \" by auto have INJ_the_dom: "inj_on (the o f) (dom f)" using assms by (auto simp: inj_on_def domIff) note 2 = subset_inj_on[OF this DOM] have 3: "(\i. (the o f) ` ?\r' i) = map_props f o \" using DOM INJ apply (auto intro!: ext simp: map_props_def domIff image_iff) by (metis Int_iff domI option.sel) have "\ \\<^sub>c \ \ ?\r \\<^sub>c \" apply (rule ltlc_eq_on) apply (auto simp: pw_eq_on_def) done also from map_semantics_ltlc_aux[OF 2 1 subset_refl] have "\ \ (\i. (the o f) ` ?\r i) \\<^sub>c map_ltlc (the o f) \" . also have "\ \ (\i. (the o f) ` ?\r' i) \\<^sub>c map_ltlc (the o f) \" apply (rule ltlc_eq_on) using DOM INJ apply (auto simp: pw_eq_on_def ltlc.set_map domIff image_iff) by (metis Int_iff contra_subsetD domD domI inj_on_eq_iff option.sel) also note 3 finally show ?thesis . qed lemma map_semantics_ltlc_inv: assumes INJ: "inj_on f (dom f)" and DOM: "atoms_ltlc \ \ dom f" shows "\ \\<^sub>c map_ltlc (the o f) \ \ (\i. (the o f) -` \ i) \\<^sub>c \" using map_semantics_ltlc[OF assms] apply simp apply (intro ltlc_eq_on) apply (auto simp add: pw_eq_on_def ltlc.set_map map_props_def) by (metis DOM comp_apply contra_subsetD domD option.sel vimage_eq) subsection \LTL in Negation Normal Form\ text \We define a type of LTL formula in negation normal form (NNF).\ subsubsection \Syntax\ datatype (atoms_ltln: 'a) ltln = True_ltln ("true\<^sub>n") | False_ltln ("false\<^sub>n") | Prop_ltln 'a ("prop\<^sub>n'(_')") | Nprop_ltln 'a ("nprop\<^sub>n'(_')") | And_ltln "'a ltln" "'a ltln" ("_ and\<^sub>n _" [82,82] 81) | Or_ltln "'a ltln" "'a ltln" ("_ or\<^sub>n _" [84,84] 83) | Next_ltln "'a ltln" ("X\<^sub>n _" [88] 87) | Until_ltln "'a ltln" "'a ltln" ("_ U\<^sub>n _" [84,84] 83) | Release_ltln "'a ltln" "'a ltln" ("_ R\<^sub>n _" [84,84] 83) | WeakUntil_ltln "'a ltln" "'a ltln" ("_ W\<^sub>n _" [84,84] 83) | StrongRelease_ltln "'a ltln" "'a ltln" ("_ M\<^sub>n _" [84,84] 83) abbreviation finally\<^sub>n :: "'a ltln \ 'a ltln" ("F\<^sub>n _" [88] 87) where "F\<^sub>n \ \ true\<^sub>n U\<^sub>n \" notation (input) finally\<^sub>n ("\\<^sub>n _" [88] 87) abbreviation globally\<^sub>n :: "'a ltln \ 'a ltln" ("G\<^sub>n _" [88] 87) where "G\<^sub>n \ \ false\<^sub>n R\<^sub>n \" notation (input) globally\<^sub>n ("\\<^sub>n _" [88] 87) subsubsection \Semantics\ primrec semantics_ltln :: "['a set word, 'a ltln] \ bool" ("_ \\<^sub>n _" [80,80] 80) where "\ \\<^sub>n true\<^sub>n = True" | "\ \\<^sub>n false\<^sub>n = False" | "\ \\<^sub>n prop\<^sub>n(q) = (q \ \ 0)" | "\ \\<^sub>n nprop\<^sub>n(q) = (q \ \ 0)" | "\ \\<^sub>n \ and\<^sub>n \ = (\ \\<^sub>n \ \ \ \\<^sub>n \)" | "\ \\<^sub>n \ or\<^sub>n \ = (\ \\<^sub>n \ \ \ \\<^sub>n \)" | "\ \\<^sub>n X\<^sub>n \ = (suffix 1 \ \\<^sub>n \)" | "\ \\<^sub>n \ U\<^sub>n \ = (\i. suffix i \ \\<^sub>n \ \ (\j \\<^sub>n \))" | "\ \\<^sub>n \ R\<^sub>n \ = (\i. suffix i \ \\<^sub>n \ \ (\j \\<^sub>n \))" | "\ \\<^sub>n \ W\<^sub>n \ = (\i. suffix i \ \\<^sub>n \ \ (\j\i. suffix j \ \\<^sub>n \))" | "\ \\<^sub>n \ M\<^sub>n \ = (\i. suffix i \ \\<^sub>n \ \ (\j\i. suffix j \ \\<^sub>n \))" definition "language_ltln \ \ {\. \ \\<^sub>n \}" +lemma semantics_ltln_ite_simps[simp]: + "w \\<^sub>n (if P then true\<^sub>n else false\<^sub>n) = P" + "w \\<^sub>n (if P then false\<^sub>n else true\<^sub>n) = (\P)" + by simp_all + subsubsection \Conversion\ fun ltlc_to_ltln' :: "bool \ 'a ltlc \ 'a ltln" where "ltlc_to_ltln' False true\<^sub>c = true\<^sub>n" | "ltlc_to_ltln' False false\<^sub>c = false\<^sub>n" | "ltlc_to_ltln' False prop\<^sub>c(q) = prop\<^sub>n(q)" | "ltlc_to_ltln' False (\ and\<^sub>c \) = (ltlc_to_ltln' False \) and\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (\ or\<^sub>c \) = (ltlc_to_ltln' False \) or\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (\ implies\<^sub>c \) = (ltlc_to_ltln' True \) or\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (F\<^sub>c \) = true\<^sub>n U\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (G\<^sub>c \) = false\<^sub>n R\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (\ U\<^sub>c \) = (ltlc_to_ltln' False \) U\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (\ R\<^sub>c \) = (ltlc_to_ltln' False \) R\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (\ W\<^sub>c \) = (ltlc_to_ltln' False \) W\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' False (\ M\<^sub>c \) = (ltlc_to_ltln' False \) M\<^sub>n (ltlc_to_ltln' False \)" | "ltlc_to_ltln' True true\<^sub>c = false\<^sub>n" | "ltlc_to_ltln' True false\<^sub>c = true\<^sub>n" | "ltlc_to_ltln' True prop\<^sub>c(q) = nprop\<^sub>n(q)" | "ltlc_to_ltln' True (\ and\<^sub>c \) = (ltlc_to_ltln' True \) or\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (\ or\<^sub>c \) = (ltlc_to_ltln' True \) and\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (\ implies\<^sub>c \) = (ltlc_to_ltln' False \) and\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (F\<^sub>c \) = false\<^sub>n R\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (G\<^sub>c \) = true\<^sub>n U\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (\ U\<^sub>c \) = (ltlc_to_ltln' True \) R\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (\ R\<^sub>c \) = (ltlc_to_ltln' True \) U\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (\ W\<^sub>c \) = (ltlc_to_ltln' True \) M\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' True (\ M\<^sub>c \) = (ltlc_to_ltln' True \) W\<^sub>n (ltlc_to_ltln' True \)" | "ltlc_to_ltln' b (not\<^sub>c \) = ltlc_to_ltln' (\ b) \" | "ltlc_to_ltln' b (X\<^sub>c \) = X\<^sub>n (ltlc_to_ltln' b \)" fun ltlc_to_ltln :: "'a ltlc \ 'a ltln" where "ltlc_to_ltln \ = ltlc_to_ltln' False \" fun ltln_to_ltlc :: "'a ltln \ 'a ltlc" where "ltln_to_ltlc true\<^sub>n = true\<^sub>c" | "ltln_to_ltlc false\<^sub>n = false\<^sub>c" | "ltln_to_ltlc prop\<^sub>n(q) = prop\<^sub>c(q)" | "ltln_to_ltlc nprop\<^sub>n(q) = not\<^sub>c (prop\<^sub>c(q))" | "ltln_to_ltlc (\ and\<^sub>n \) = (ltln_to_ltlc \ and\<^sub>c ltln_to_ltlc \)" | "ltln_to_ltlc (\ or\<^sub>n \) = (ltln_to_ltlc \ or\<^sub>c ltln_to_ltlc \)" | "ltln_to_ltlc (X\<^sub>n \) = (X\<^sub>c ltln_to_ltlc \)" | "ltln_to_ltlc (\ U\<^sub>n \) = (ltln_to_ltlc \ U\<^sub>c ltln_to_ltlc \)" | "ltln_to_ltlc (\ R\<^sub>n \) = (ltln_to_ltlc \ R\<^sub>c ltln_to_ltlc \)" | "ltln_to_ltlc (\ W\<^sub>n \) = (ltln_to_ltlc \ W\<^sub>c ltln_to_ltlc \)" | "ltln_to_ltlc (\ M\<^sub>n \) = (ltln_to_ltlc \ M\<^sub>c ltln_to_ltlc \)" lemma ltlc_to_ltln'_correct: "w \\<^sub>n (ltlc_to_ltln' True \) \ \ w \\<^sub>c \" "w \\<^sub>n (ltlc_to_ltln' False \) \ w \\<^sub>c \" "size (ltlc_to_ltln' True \) \ 2 * size \" "size (ltlc_to_ltln' False \) \ 2 * size \" by (induction \ arbitrary: w) simp+ lemma ltlc_to_ltln_semantics [simp]: "w \\<^sub>n ltlc_to_ltln \ \ w \\<^sub>c \" using ltlc_to_ltln'_correct by auto lemma ltlc_to_ltln_size: "size (ltlc_to_ltln \) \ 2 * size \" using ltlc_to_ltln'_correct by simp lemma ltln_to_ltlc_semantics [simp]: "w \\<^sub>c ltln_to_ltlc \ \ w \\<^sub>n \" by (induction \ arbitrary: w) simp+ lemma ltlc_to_ltln_atoms: "atoms_ltln (ltlc_to_ltln \) = atoms_ltlc \" proof - have "atoms_ltln (ltlc_to_ltln' True \) = atoms_ltlc \" "atoms_ltln (ltlc_to_ltln' False \) = atoms_ltlc \" by (induction \) simp+ thus ?thesis by simp qed subsubsection \Negation\ fun not\<^sub>n where "not\<^sub>n true\<^sub>n = false\<^sub>n" | "not\<^sub>n false\<^sub>n = true\<^sub>n" | "not\<^sub>n prop\<^sub>n(a) = nprop\<^sub>n(a)" | "not\<^sub>n nprop\<^sub>n(a) = prop\<^sub>n(a)" | "not\<^sub>n (\ and\<^sub>n \) = (not\<^sub>n \) or\<^sub>n (not\<^sub>n \)" | "not\<^sub>n (\ or\<^sub>n \) = (not\<^sub>n \) and\<^sub>n (not\<^sub>n \)" | "not\<^sub>n (X\<^sub>n \) = X\<^sub>n (not\<^sub>n \)" | "not\<^sub>n (\ U\<^sub>n \) = (not\<^sub>n \) R\<^sub>n (not\<^sub>n \)" | "not\<^sub>n (\ R\<^sub>n \) = (not\<^sub>n \) U\<^sub>n (not\<^sub>n \)" | "not\<^sub>n (\ W\<^sub>n \) = (not\<^sub>n \) M\<^sub>n (not\<^sub>n \)" | "not\<^sub>n (\ M\<^sub>n \) = (not\<^sub>n \) W\<^sub>n (not\<^sub>n \)" lemma not\<^sub>n_semantics[simp]: "w \\<^sub>n not\<^sub>n \ \ \ w \\<^sub>n \" by (induction \ arbitrary: w) auto lemma not\<^sub>n_size: "size (not\<^sub>n \) = size \" by (induction \) auto subsubsection \Subformulas\ fun subfrmlsn :: "'a ltln \ 'a ltln set" where "subfrmlsn (\ and\<^sub>n \) = {\ and\<^sub>n \} \ subfrmlsn \ \ subfrmlsn \" | "subfrmlsn (\ or\<^sub>n \) = {\ or\<^sub>n \} \ subfrmlsn \ \ subfrmlsn \" | "subfrmlsn (X\<^sub>n \) = {X\<^sub>n \} \ subfrmlsn \" | "subfrmlsn (\ U\<^sub>n \) = {\ U\<^sub>n \} \ subfrmlsn \ \ subfrmlsn \" | "subfrmlsn (\ R\<^sub>n \) = {\ R\<^sub>n \} \ subfrmlsn \ \ subfrmlsn \" | "subfrmlsn (\ W\<^sub>n \) = {\ W\<^sub>n \} \ subfrmlsn \ \ subfrmlsn \" | "subfrmlsn (\ M\<^sub>n \) = {\ M\<^sub>n \} \ subfrmlsn \ \ subfrmlsn \" | "subfrmlsn \ = {\}" lemma subfrmlsn_id[simp]: "\ \ subfrmlsn \" by (induction \) auto lemma subfrmlsn_finite: "finite (subfrmlsn \)" by (induction \) auto lemma subfrmlsn_card: "card (subfrmlsn \) \ size \" by (induction \) (simp_all add: card_insert_if subfrmlsn_finite, (meson add_le_mono card_Un_le dual_order.trans le_SucI)+) lemma subfrmlsn_subset: "\ \ subfrmlsn \ \ subfrmlsn \ \ subfrmlsn \" by (induction \) auto lemma subfrmlsn_size: "\ \ subfrmlsn \ \ size \ < size \ \ \ = \" by (induction \) auto abbreviation "size_set S \ sum (\x. 2 * size x + 1) S" lemma size_set_diff: "finite S \ S' \ S \ size_set (S - S') = size_set S - size_set S'" using sum_diff_nat finite_subset by metis subsubsection \Constant Folding\ lemma U_consts[intro, simp]: "w \\<^sub>n \ U\<^sub>n true\<^sub>n" "\ (w \\<^sub>n \ U\<^sub>n false\<^sub>n)" "(w \\<^sub>n false\<^sub>n U\<^sub>n \) = (w \\<^sub>n \)" by force+ lemma R_consts[intro, simp]: "w \\<^sub>n \ R\<^sub>n true\<^sub>n" "\ (w \\<^sub>n \ R\<^sub>n false\<^sub>n)" "(w \\<^sub>n true\<^sub>n R\<^sub>n \) = (w \\<^sub>n \)" by force+ lemma W_consts[intro, simp]: "w \\<^sub>n true\<^sub>n W\<^sub>n \" "w \\<^sub>n \ W\<^sub>n true\<^sub>n" "(w \\<^sub>n false\<^sub>n W\<^sub>n \) = (w \\<^sub>n \)" "(w \\<^sub>n \ W\<^sub>n false\<^sub>n) = (w \\<^sub>n G\<^sub>n \)" by force+ lemma M_consts[intro, simp]: "\ (w \\<^sub>n false\<^sub>n M\<^sub>n \)" "\ (w \\<^sub>n \ M\<^sub>n false\<^sub>n)" "(w \\<^sub>n true\<^sub>n M\<^sub>n \) = (w \\<^sub>n \)" "(w \\<^sub>n \ M\<^sub>n true\<^sub>n) = (w \\<^sub>n F\<^sub>n \)" by force+ subsubsection \Distributivity\ lemma until_and_left_distrib: "w \\<^sub>n (\\<^sub>1 and\<^sub>n \\<^sub>2) U\<^sub>n \ \ w \\<^sub>n (\\<^sub>1 U\<^sub>n \) and\<^sub>n (\\<^sub>2 U\<^sub>n \)" proof assume "w \\<^sub>n \\<^sub>1 U\<^sub>n \ and\<^sub>n \\<^sub>2 U\<^sub>n \" then obtain i1 i2 where "suffix i1 w \\<^sub>n \ \ (\j\<^sub>n \\<^sub>1)" and "suffix i2 w \\<^sub>n \ \ (\j\<^sub>n \\<^sub>2)" by auto then have "suffix (min i1 i2) w \\<^sub>n \ \ (\j\<^sub>n \\<^sub>1 and\<^sub>n \\<^sub>2)" by (simp add: min_def) then show "w \\<^sub>n (\\<^sub>1 and\<^sub>n \\<^sub>2) U\<^sub>n \" by force qed auto lemma until_or_right_distrib: "w \\<^sub>n \ U\<^sub>n (\\<^sub>1 or\<^sub>n \\<^sub>2) \ w \\<^sub>n (\ U\<^sub>n \\<^sub>1) or\<^sub>n (\ U\<^sub>n \\<^sub>2)" by auto lemma release_and_right_distrib: "w \\<^sub>n \ R\<^sub>n (\\<^sub>1 and\<^sub>n \\<^sub>2) \ w \\<^sub>n (\ R\<^sub>n \\<^sub>1) and\<^sub>n (\ R\<^sub>n \\<^sub>2)" by auto lemma release_or_left_distrib: "w \\<^sub>n (\\<^sub>1 or\<^sub>n \\<^sub>2) R\<^sub>n \ \ w \\<^sub>n (\\<^sub>1 R\<^sub>n \) or\<^sub>n (\\<^sub>2 R\<^sub>n \)" by (metis not\<^sub>n.simps(6) not\<^sub>n.simps(9) not\<^sub>n_semantics until_and_left_distrib) lemma strong_release_and_right_distrib: "w \\<^sub>n \ M\<^sub>n (\\<^sub>1 and\<^sub>n \\<^sub>2) \ w \\<^sub>n (\ M\<^sub>n \\<^sub>1) and\<^sub>n (\ M\<^sub>n \\<^sub>2)" proof assume "w \\<^sub>n (\ M\<^sub>n \\<^sub>1) and\<^sub>n (\ M\<^sub>n \\<^sub>2)" then obtain i1 i2 where "suffix i1 w \\<^sub>n \ \ (\j\i1. suffix j w \\<^sub>n \\<^sub>1)" and "suffix i2 w \\<^sub>n \ \ (\j\i2. suffix j w \\<^sub>n \\<^sub>2)" by auto then have "suffix (min i1 i2) w \\<^sub>n \ \ (\j\min i1 i2. suffix j w \\<^sub>n \\<^sub>1 and\<^sub>n \\<^sub>2)" by (simp add: min_def) then show "w \\<^sub>n \ M\<^sub>n (\\<^sub>1 and\<^sub>n \\<^sub>2)" by force qed auto lemma strong_release_or_left_distrib: "w \\<^sub>n (\\<^sub>1 or\<^sub>n \\<^sub>2) M\<^sub>n \ \ w \\<^sub>n (\\<^sub>1 M\<^sub>n \) or\<^sub>n (\\<^sub>2 M\<^sub>n \)" by auto lemma weak_until_and_left_distrib: "w \\<^sub>n (\\<^sub>1 and\<^sub>n \\<^sub>2) W\<^sub>n \ \ w \\<^sub>n (\\<^sub>1 W\<^sub>n \) and\<^sub>n (\\<^sub>2 W\<^sub>n \)" by auto lemma weak_until_or_right_distrib: "w \\<^sub>n \ W\<^sub>n (\\<^sub>1 or\<^sub>n \\<^sub>2) \ w \\<^sub>n (\ W\<^sub>n \\<^sub>1) or\<^sub>n (\ W\<^sub>n \\<^sub>2)" by (metis not\<^sub>n.simps(10) not\<^sub>n.simps(6) not\<^sub>n_semantics strong_release_and_right_distrib) lemma next_until_distrib: "w \\<^sub>n X\<^sub>n (\ U\<^sub>n \) \ w \\<^sub>n (X\<^sub>n \) U\<^sub>n (X\<^sub>n \)" by auto lemma next_release_distrib: "w \\<^sub>n X\<^sub>n (\ R\<^sub>n \) \ w \\<^sub>n (X\<^sub>n \) R\<^sub>n (X\<^sub>n \)" by auto lemma next_weak_until_distrib: "w \\<^sub>n X\<^sub>n (\ W\<^sub>n \) \ w \\<^sub>n (X\<^sub>n \) W\<^sub>n (X\<^sub>n \)" by auto lemma next_strong_release_distrib: "w \\<^sub>n X\<^sub>n (\ M\<^sub>n \) \ w \\<^sub>n (X\<^sub>n \) M\<^sub>n (X\<^sub>n \)" by auto subsubsection \Nested operators\ lemma finally_until[simp]: "w \\<^sub>n F\<^sub>n (\ U\<^sub>n \) \ w \\<^sub>n F\<^sub>n \" by auto force lemma globally_release[simp]: "w \\<^sub>n G\<^sub>n (\ R\<^sub>n \) \ w \\<^sub>n G\<^sub>n \" by auto force lemma globally_weak_until[simp]: "w \\<^sub>n G\<^sub>n (\ W\<^sub>n \) \ w \\<^sub>n G\<^sub>n (\ or\<^sub>n \)" by auto force lemma finally_strong_release[simp]: "w \\<^sub>n F\<^sub>n (\ M\<^sub>n \) \ w \\<^sub>n F\<^sub>n (\ and\<^sub>n \)" by auto force subsubsection \Weak and strong operators\ lemma ltln_weak_strong: "w \\<^sub>n \ W\<^sub>n \ \ w \\<^sub>n (G\<^sub>n \) or\<^sub>n (\ U\<^sub>n \)" "w \\<^sub>n \ R\<^sub>n \ \ w \\<^sub>n (G\<^sub>n \) or\<^sub>n (\ M\<^sub>n \)" proof auto fix i assume "\i. suffix i w \\<^sub>n \ \ (\j\i. suffix j w \\<^sub>n \)" and "\i. suffix i w \\<^sub>n \ \ (\j suffix j w \\<^sub>n \)" then show "suffix i w \\<^sub>n \" by (induction i rule: less_induct) force next fix i k assume "\j\i. \ suffix j w \\<^sub>n \" and "suffix k w \\<^sub>n \" and "\j\<^sub>n \" then show "suffix i w \\<^sub>n \" by (cases "i < k") simp_all next fix i assume "\i. suffix i w \\<^sub>n \ \ (\j\<^sub>n \)" and "\i. suffix i w \\<^sub>n \ \ (\j\i. \ suffix j w \\<^sub>n \)" then show "suffix i w \\<^sub>n \" by (induction i rule: less_induct) force next fix i k assume "\j suffix j w \\<^sub>n \" and "suffix k w \\<^sub>n \" and "\j\k. suffix j w \\<^sub>n \" then show "suffix i w \\<^sub>n \" by (cases "i \ k") simp_all qed lemma ltln_strong_weak: "w \\<^sub>n \ U\<^sub>n \ \ w \\<^sub>n (F\<^sub>n \) and\<^sub>n (\ W\<^sub>n \)" "w \\<^sub>n \ M\<^sub>n \ \ w \\<^sub>n (F\<^sub>n \) and\<^sub>n (\ R\<^sub>n \)" by (metis ltln_weak_strong not\<^sub>n.simps(1,5,8-11) not\<^sub>n_semantics)+ lemma ltln_strong_to_weak: "w \\<^sub>n \ U\<^sub>n \ \ w \\<^sub>n \ W\<^sub>n \" "w \\<^sub>n \ M\<^sub>n \ \ w \\<^sub>n \ R\<^sub>n \" using ltln_weak_strong by simp_all blast+ lemma ltln_weak_to_strong: "\w \\<^sub>n \ W\<^sub>n \; \ w \\<^sub>n G\<^sub>n \\ \ w \\<^sub>n \ U\<^sub>n \" "\w \\<^sub>n \ W\<^sub>n \; w \\<^sub>n F\<^sub>n \\ \ w \\<^sub>n \ U\<^sub>n \" "\w \\<^sub>n \ R\<^sub>n \; \ w \\<^sub>n G\<^sub>n \\ \ w \\<^sub>n \ M\<^sub>n \" "\w \\<^sub>n \ R\<^sub>n \; w \\<^sub>n F\<^sub>n \\ \ w \\<^sub>n \ M\<^sub>n \" unfolding ltln_weak_strong[of w \ \] by auto lemma ltln_StrongRelease_to_Until: "w \\<^sub>n \ M\<^sub>n \ \ w \\<^sub>n \ U\<^sub>n (\ and\<^sub>n \)" using order.order_iff_strict by auto lemma ltln_Release_to_WeakUntil: "w \\<^sub>n \ R\<^sub>n \ \ w \\<^sub>n \ W\<^sub>n (\ and\<^sub>n \)" by (meson ltln_StrongRelease_to_Until ltln_weak_strong semantics_ltln.simps(6)) lemma ltln_WeakUntil_to_Release: "w \\<^sub>n \ W\<^sub>n \ \ w \\<^sub>n \ R\<^sub>n (\ or\<^sub>n \)" by (metis ltln_StrongRelease_to_Until not\<^sub>n.simps(6,9,10) not\<^sub>n_semantics) lemma ltln_Until_to_StrongRelease: "w \\<^sub>n \ U\<^sub>n \ \ w \\<^sub>n \ M\<^sub>n (\ or\<^sub>n \)" by (metis ltln_Release_to_WeakUntil not\<^sub>n.simps(6,8,11) not\<^sub>n_semantics) subsubsection \GF and FG semantics\ lemma GF_suffix: - "w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \)" - by simp + "suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ w \\<^sub>n G\<^sub>n (F\<^sub>n \)" + by auto (metis ab_semigroup_add_class.add_ac(1) add.left_commute) lemma FG_suffix: - "w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \)" - by (auto simp: algebra_simps) - + "suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ w \\<^sub>n F\<^sub>n (G\<^sub>n \)" + by (auto simp: algebra_simps) (metis add.commute add.left_commute) lemma GF_Inf_many: "w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ (\\<^sub>\ i. suffix i w \\<^sub>n \)" unfolding INFM_nat_le by simp (blast dest: le_Suc_ex intro: le_add1) lemma FG_Alm_all: "w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ (\\<^sub>\ i. suffix i w \\<^sub>n \)" unfolding MOST_nat_le by simp (blast dest: le_Suc_ex intro: le_add1) (* TODO: move to Infinite_Set.thy ?? *) lemma MOST_nat_add: "(\\<^sub>\i::nat. P i) \ (\\<^sub>\i. P (i + j))" by (simp add: cofinite_eq_sequentially) lemma INFM_nat_add: "(\\<^sub>\i::nat. P i) \ (\\<^sub>\i. P (i + j))" using MOST_nat_add not_MOST not_INFM by blast lemma FG_suffix_G: "w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ \\<^sub>\i. suffix i w \\<^sub>n G\<^sub>n \" proof - assume "w \\<^sub>n F\<^sub>n (G\<^sub>n \)" then have "w \\<^sub>n F\<^sub>n (G\<^sub>n (G\<^sub>n \))" by (meson globally_release semantics_ltln.simps(8)) then show "\\<^sub>\i. suffix i w \\<^sub>n G\<^sub>n \" unfolding FG_Alm_all . qed lemma Alm_all_GF_F: "\\<^sub>\i. suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ suffix i w \\<^sub>n F\<^sub>n \" unfolding MOST_nat proof standard+ fix i :: nat assume "suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \)" then show "suffix i w \\<^sub>n F\<^sub>n \" unfolding GF_Inf_many INFM_nat by fastforce next fix i :: nat assume suffix: "suffix i w \\<^sub>n F\<^sub>n \" assume max: "i > Max {i. suffix i w \\<^sub>n \}" with suffix obtain j where "j \ i" and j_suffix: "suffix j w \\<^sub>n \" by simp (blast intro: le_add1) with max have j_max: "j > Max {i. suffix i w \\<^sub>n \}" by fastforce show "suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \)" proof (cases "w \\<^sub>n G\<^sub>n (F\<^sub>n \)") case False then have "\ (\\<^sub>\i. suffix i w \\<^sub>n \)" unfolding GF_Inf_many by simp then have "finite {i. suffix i w \\<^sub>n \}" by (simp add: INFM_iff_infinite) then have "\i>Max {i. suffix i w \\<^sub>n \}. \ suffix i w \\<^sub>n \" using Max_ge not_le by auto then show ?thesis using j_suffix j_max by blast qed force qed lemma Alm_all_FG_G: "\\<^sub>\i. suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ suffix i w \\<^sub>n G\<^sub>n \" unfolding MOST_nat proof standard+ fix i :: nat assume "suffix i w \\<^sub>n G\<^sub>n \" then show "suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \)" unfolding FG_Alm_all INFM_nat by fastforce next fix i :: nat assume suffix: "suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \)" assume max: "i > Max {i. \ suffix i w \\<^sub>n G\<^sub>n \}" with suffix have "\\<^sub>\j. suffix (i + j) w \\<^sub>n G\<^sub>n \" using FG_suffix_G[of "suffix i w"] suffix_suffix by fastforce then have "\ (\\<^sub>\j. \ suffix j w \\<^sub>n G\<^sub>n \)" using MOST_nat_add[of "\i. suffix i w \\<^sub>n G\<^sub>n \" i] by (simp add: algebra_simps) then have "finite {i. \ suffix i w \\<^sub>n G\<^sub>n \}" by (simp add: INFM_iff_infinite) with max show "suffix i w \\<^sub>n G\<^sub>n \" using Max_ge leD by blast qed subsubsection \Expansion\ lemma ltln_expand_Until: "\ \\<^sub>n \ U\<^sub>n \ \ (\ \\<^sub>n \ or\<^sub>n (\ and\<^sub>n (X\<^sub>n (\ U\<^sub>n \))))" (is "?lhs = ?rhs") proof assume ?lhs then obtain i where "suffix i \ \\<^sub>n \" and "\j \\<^sub>n \" by auto thus ?rhs by (cases i) auto next assume ?rhs show ?lhs proof (cases "\ \\<^sub>n \") case False then have "\ \\<^sub>n \" and "\ \\<^sub>n X\<^sub>n (\ U\<^sub>n \)" using `?rhs` by auto thus ?lhs using less_Suc_eq_0_disj suffix_singleton_suffix by force qed force qed lemma ltln_expand_Release: "\ \\<^sub>n \ R\<^sub>n \ \ (\ \\<^sub>n \ and\<^sub>n (\ or\<^sub>n (X\<^sub>n (\ R\<^sub>n \))))" (is "?lhs = ?rhs") proof assume ?lhs thus ?rhs using less_Suc_eq_0_disj by force next assume ?rhs { fix i assume "\ suffix i \ \\<^sub>n \" then have "\j \\<^sub>n \" using `?rhs` by (cases i) force+ } thus ?lhs by auto qed lemma ltln_expand_WeakUntil: "\ \\<^sub>n \ W\<^sub>n \ \ (\ \\<^sub>n \ or\<^sub>n (\ and\<^sub>n (X\<^sub>n (\ W\<^sub>n \))))" (is "?lhs = ?rhs") proof assume ?lhs thus ?rhs by (metis ltln_expand_Release ltln_expand_Until ltln_weak_strong(1) semantics_ltln.simps(2,5,6,7)) next assume ?rhs { fix i assume "\ suffix i \ \\<^sub>n \" then have "\j\i. suffix j \ \\<^sub>n \" using `?rhs` by (cases i) force+ } thus ?lhs by auto qed lemma ltln_expand_StrongRelease: "\ \\<^sub>n \ M\<^sub>n \ \ (\ \\<^sub>n \ and\<^sub>n (\ or\<^sub>n (X\<^sub>n (\ M\<^sub>n \))))" (is "?lhs = ?rhs") proof assume ?lhs then obtain i where "suffix i \ \\<^sub>n \" and "\j\i. suffix j \ \\<^sub>n \" by auto thus ?rhs by (cases i) auto next assume ?rhs show ?lhs proof (cases "\ \\<^sub>n \") case True thus ?lhs using `?rhs` ltln_expand_WeakUntil by fastforce next case False thus ?lhs by (metis `?rhs` ltln_expand_WeakUntil not\<^sub>n.simps(5,6,7,11) not\<^sub>n_semantics) qed qed lemma ltln_Release_alterdef: "w \\<^sub>n \ R\<^sub>n \ \ w \\<^sub>n (G\<^sub>n \) or\<^sub>n (\ U\<^sub>n (\ and\<^sub>n \))" proof (cases "\i. \suffix i w \\<^sub>n \") case True define i where "i \ Least (\i. \suffix i w \\<^sub>n \)" have "\j. j < i \ suffix j w \\<^sub>n \" and "\ suffix i w \\<^sub>n \" using True LeastI not_less_Least unfolding i_def by fast+ hence *: "\i. suffix i w \\<^sub>n \ \ (\j\<^sub>n \) \ (\i. (suffix i w \\<^sub>n \ \ suffix i w \\<^sub>n \) \ (\j\<^sub>n \))" by fastforce hence "\i. (suffix i w \\<^sub>n \ \ suffix i w \\<^sub>n \) \ (\j\<^sub>n \) \ (\i. suffix i w \\<^sub>n \ \ (\j\<^sub>n \))" using linorder_cases by blast thus ?thesis using True * by auto qed auto subsection \LTL in restricted Negation Normal Form\ text \Some algorithms do not handle the operators W and M, hence we also provide a datatype without these two operators.\ subsubsection \Syntax\ datatype (atoms_ltlr: 'a) ltlr = True_ltlr ("true\<^sub>r") | False_ltlr ("false\<^sub>r") | Prop_ltlr 'a ("prop\<^sub>r'(_')") | Nprop_ltlr 'a ("nprop\<^sub>r'(_')") | And_ltlr "'a ltlr" "'a ltlr" ("_ and\<^sub>r _" [82,82] 81) | Or_ltlr "'a ltlr" "'a ltlr" ("_ or\<^sub>r _" [84,84] 83) | Next_ltlr "'a ltlr" ("X\<^sub>r _" [88] 87) | Until_ltlr "'a ltlr" "'a ltlr" ("_ U\<^sub>r _" [84,84] 83) | Release_ltlr "'a ltlr" "'a ltlr" ("_ R\<^sub>r _" [84,84] 83) subsubsection \Semantics\ primrec semantics_ltlr :: "['a set word, 'a ltlr] \ bool" ("_ \\<^sub>r _" [80,80] 80) where "\ \\<^sub>r true\<^sub>r = True" | "\ \\<^sub>r false\<^sub>r = False" | "\ \\<^sub>r prop\<^sub>r(q) = (q \ \ 0)" | "\ \\<^sub>r nprop\<^sub>r(q) = (q \ \ 0)" | "\ \\<^sub>r \ and\<^sub>r \ = (\ \\<^sub>r \ \ \ \\<^sub>r \)" | "\ \\<^sub>r \ or\<^sub>r \ = (\ \\<^sub>r \ \ \ \\<^sub>r \)" | "\ \\<^sub>r X\<^sub>r \ = (suffix 1 \ \\<^sub>r \)" | "\ \\<^sub>r \ U\<^sub>r \ = (\i. suffix i \ \\<^sub>r \ \ (\j \\<^sub>r \))" | "\ \\<^sub>r \ R\<^sub>r \ = (\i. suffix i \ \\<^sub>r \ \ (\j \\<^sub>r \))" subsubsection \Conversion\ fun ltln_to_ltlr :: "'a ltln \ 'a ltlr" where "ltln_to_ltlr true\<^sub>n = true\<^sub>r" | "ltln_to_ltlr false\<^sub>n = false\<^sub>r" | "ltln_to_ltlr prop\<^sub>n(a) = prop\<^sub>r(a)" | "ltln_to_ltlr nprop\<^sub>n(a) = nprop\<^sub>r(a)" | "ltln_to_ltlr (\ and\<^sub>n \) = (ltln_to_ltlr \) and\<^sub>r (ltln_to_ltlr \)" | "ltln_to_ltlr (\ or\<^sub>n \) = (ltln_to_ltlr \) or\<^sub>r (ltln_to_ltlr \)" | "ltln_to_ltlr (X\<^sub>n \) = X\<^sub>r (ltln_to_ltlr \)" | "ltln_to_ltlr (\ U\<^sub>n \) = (ltln_to_ltlr \) U\<^sub>r (ltln_to_ltlr \)" | "ltln_to_ltlr (\ R\<^sub>n \) = (ltln_to_ltlr \) R\<^sub>r (ltln_to_ltlr \)" | "ltln_to_ltlr (\ W\<^sub>n \) = (ltln_to_ltlr \) R\<^sub>r ((ltln_to_ltlr \) or\<^sub>r (ltln_to_ltlr \))" | "ltln_to_ltlr (\ M\<^sub>n \) = (ltln_to_ltlr \) U\<^sub>r ((ltln_to_ltlr \) and\<^sub>r (ltln_to_ltlr \))" fun ltlr_to_ltln :: "'a ltlr \ 'a ltln" where "ltlr_to_ltln true\<^sub>r = true\<^sub>n" | "ltlr_to_ltln false\<^sub>r = false\<^sub>n" | "ltlr_to_ltln prop\<^sub>r(a) = prop\<^sub>n(a)" | "ltlr_to_ltln nprop\<^sub>r(a) = nprop\<^sub>n(a)" | "ltlr_to_ltln (\ and\<^sub>r \) = (ltlr_to_ltln \) and\<^sub>n (ltlr_to_ltln \)" | "ltlr_to_ltln (\ or\<^sub>r \) = (ltlr_to_ltln \) or\<^sub>n (ltlr_to_ltln \)" | "ltlr_to_ltln (X\<^sub>r \) = X\<^sub>n (ltlr_to_ltln \)" | "ltlr_to_ltln (\ U\<^sub>r \) = (ltlr_to_ltln \) U\<^sub>n (ltlr_to_ltln \)" | "ltlr_to_ltln (\ R\<^sub>r \) = (ltlr_to_ltln \) R\<^sub>n (ltlr_to_ltln \)" lemma ltln_to_ltlr_semantics: "w \\<^sub>r ltln_to_ltlr \ \ w \\<^sub>n \" by (induction \ arbitrary: w) (unfold ltln_WeakUntil_to_Release ltln_StrongRelease_to_Until, simp_all) lemma ltlr_to_ltln_semantics: "w \\<^sub>n ltlr_to_ltln \ \ w \\<^sub>r \" by (induction \ arbitrary: w) simp_all subsubsection \Negation\ fun not\<^sub>r where "not\<^sub>r true\<^sub>r = false\<^sub>r" | "not\<^sub>r false\<^sub>r = true\<^sub>r" | "not\<^sub>r prop\<^sub>r(a) = nprop\<^sub>r(a)" | "not\<^sub>r nprop\<^sub>r(a) = prop\<^sub>r(a)" | "not\<^sub>r (\ and\<^sub>r \) = (not\<^sub>r \) or\<^sub>r (not\<^sub>r \)" | "not\<^sub>r (\ or\<^sub>r \) = (not\<^sub>r \) and\<^sub>r (not\<^sub>r \)" | "not\<^sub>r (X\<^sub>r \) = X\<^sub>r (not\<^sub>r \)" | "not\<^sub>r (\ U\<^sub>r \) = (not\<^sub>r \) R\<^sub>r (not\<^sub>r \)" | "not\<^sub>r (\ R\<^sub>r \) = (not\<^sub>r \) U\<^sub>r (not\<^sub>r \)" lemma not\<^sub>r_semantics [simp]: "w \\<^sub>r not\<^sub>r \ \ \ w \\<^sub>r \" by (induction \ arbitrary: w) auto subsubsection \Subformulas\ fun subfrmlsr :: "'a ltlr \ 'a ltlr set" where "subfrmlsr (\ and\<^sub>r \) = {\ and\<^sub>r \} \ subfrmlsr \ \ subfrmlsr \" | "subfrmlsr (\ or\<^sub>r \) = {\ or\<^sub>r \} \ subfrmlsr \ \ subfrmlsr \" | "subfrmlsr (\ U\<^sub>r \) = {\ U\<^sub>r \} \ subfrmlsr \ \ subfrmlsr \" | "subfrmlsr (\ R\<^sub>r \) = {\ R\<^sub>r \} \ subfrmlsr \ \ subfrmlsr \" | "subfrmlsr (X\<^sub>r \) = {X\<^sub>r \} \ subfrmlsr \" | "subfrmlsr x = {x}" lemma subfrmlsr_id[simp]: "\ \ subfrmlsr \" by (induction \) auto lemma subfrmlsr_finite: "finite (subfrmlsr \)" by (induction \) auto lemma subfrmlsr_subset: "\ \ subfrmlsr \ \ subfrmlsr \ \ subfrmlsr \" by (induction \) auto lemma subfrmlsr_size: "\ \ subfrmlsr \ \ size \ < size \ \ \ = \" by (induction \) auto subsubsection \Expansion lemmas\ lemma ltlr_expand_Until: "\ \\<^sub>r \ U\<^sub>r \ \ (\ \\<^sub>r \ or\<^sub>r (\ and\<^sub>r (X\<^sub>r (\ U\<^sub>r \))))" by (metis ltln_expand_Until ltlr_to_ltln.simps(5-8) ltlr_to_ltln_semantics) lemma ltlr_expand_Release: "\ \\<^sub>r \ R\<^sub>r \ \ (\ \\<^sub>r \ and\<^sub>r (\ or\<^sub>r (X\<^sub>r (\ R\<^sub>r \))))" by (metis ltln_expand_Release ltlr_to_ltln.simps(5-7,9) ltlr_to_ltln_semantics) subsection \Propositional LTL\ text \We define the syntax and semantics of propositional linear-time temporal logic PLTL. PLTL formulas are built from atomic formulas, propositional connectives, and the temporal operators ``next'' and ``until''. The following data type definition is parameterized by the type of states over which formulas are evaluated.\ subsubsection \Syntax\ datatype 'a pltl = False_ltlp ("false\<^sub>p") | Atom_ltlp "'a \ bool" ("atom\<^sub>p'(_')") | Implies_ltlp "'a pltl" "'a pltl" ("_ implies\<^sub>p _" [81,81] 80) | Next_ltlp "'a pltl" ("X\<^sub>p _" [88] 87) | Until_ltlp "'a pltl" "'a pltl" ("_ U\<^sub>p _" [84,84] 83) \ \Further connectives of PLTL can be defined in terms of the existing syntax.\ definition Not_ltlp ("not\<^sub>p _" [85] 85) where "not\<^sub>p \ \ \ implies\<^sub>p false\<^sub>p" definition True_ltlp ("true\<^sub>p") where "true\<^sub>p \ not\<^sub>p false\<^sub>p" definition Or_ltlp ("_ or\<^sub>p _" [81,81] 80) where "\ or\<^sub>p \ \ (not\<^sub>p \) implies\<^sub>p \" definition And_ltlp ("_ and\<^sub>p _" [82,82] 81) where "\ and\<^sub>p \ \ not\<^sub>p ((not\<^sub>p \) or\<^sub>p (not\<^sub>p \))" definition Eventually_ltlp ("F\<^sub>p _" [88] 87) where "F\<^sub>p \ \ true\<^sub>p U\<^sub>p \" definition Always_ltlp ("G\<^sub>p _" [88] 87) where "G\<^sub>p \ \ not\<^sub>p (F\<^sub>p (not\<^sub>p \))" definition Release_ltlp ("_ R\<^sub>p _" [84,84] 83) where "\ R\<^sub>p \ \ not\<^sub>p ((not\<^sub>p \) U\<^sub>p (not\<^sub>p \))" definition WeakUntil_ltlp ("_ W\<^sub>p _" [84,84] 83) where "\ W\<^sub>p \ \ \ R\<^sub>p (\ or\<^sub>p \)" definition StrongRelease_ltlp ("_ M\<^sub>p _" [84,84] 83) where "\ M\<^sub>p \ \ \ U\<^sub>p (\ and\<^sub>p \)" subsubsection \Semantics\ fun semantics_pltl :: "['a word, 'a pltl] \ bool" ("_ \\<^sub>p _" [80,80] 80) where "w \\<^sub>p false\<^sub>p = False" | "w \\<^sub>p atom\<^sub>p(p) = (p (w 0))" | "w \\<^sub>p \ implies\<^sub>p \ = (w \\<^sub>p \ \ w \\<^sub>p \)" | "w \\<^sub>p X\<^sub>p \ = (suffix 1 w \\<^sub>p \)" | "w \\<^sub>p \ U\<^sub>p \ = (\i. suffix i w \\<^sub>p \ \ (\j\<^sub>p \))" lemma semantics_pltl_sugar [simp]: "w \\<^sub>p not\<^sub>p \ = (\w \\<^sub>p \)" "w \\<^sub>p true\<^sub>p = True" "w \\<^sub>p \ or\<^sub>p \ = (w \\<^sub>p \ \ w \\<^sub>p \)" "w \\<^sub>p \ and\<^sub>p \ = (w \\<^sub>p \ \ w \\<^sub>p \)" "w \\<^sub>p F\<^sub>p \ = (\i. suffix i w \\<^sub>p \)" "w \\<^sub>p G\<^sub>p \ = (\i. suffix i w \\<^sub>p \)" "w \\<^sub>p \ R\<^sub>p \ = (\i. suffix i w \\<^sub>p \ \ (\j\<^sub>p \))" "w \\<^sub>p \ W\<^sub>p \ = (\i. suffix i w \\<^sub>p \ \ (\j\i. suffix j w \\<^sub>p \))" "w \\<^sub>p \ M\<^sub>p \ = (\i. suffix i w \\<^sub>p \ \ (\j\i. suffix j w \\<^sub>p \))" by (auto simp: Not_ltlp_def True_ltlp_def Or_ltlp_def And_ltlp_def Eventually_ltlp_def Always_ltlp_def Release_ltlp_def WeakUntil_ltlp_def StrongRelease_ltlp_def) (insert le_neq_implies_less, blast)+ definition "language_ltlp \ \ {\. \ \\<^sub>p \}" subsubsection \Conversion\ fun ltlc_to_pltl :: "'a ltlc \ 'a set pltl" where "ltlc_to_pltl true\<^sub>c = true\<^sub>p" | "ltlc_to_pltl false\<^sub>c = false\<^sub>p" | "ltlc_to_pltl (prop\<^sub>c(q)) = atom\<^sub>p((\) q)" | "ltlc_to_pltl (not\<^sub>c \) = not\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (\ and\<^sub>c \) = (ltlc_to_pltl \) and\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (\ or\<^sub>c \) = (ltlc_to_pltl \) or\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (\ implies\<^sub>c \) = (ltlc_to_pltl \) implies\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (X\<^sub>c \) = X\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (F\<^sub>c \) = F\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (G\<^sub>c \) = G\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (\ U\<^sub>c \) = (ltlc_to_pltl \) U\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (\ R\<^sub>c \) = (ltlc_to_pltl \) R\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (\ W\<^sub>c \) = (ltlc_to_pltl \) W\<^sub>p (ltlc_to_pltl \)" | "ltlc_to_pltl (\ M\<^sub>c \) = (ltlc_to_pltl \) M\<^sub>p (ltlc_to_pltl \)" lemma ltlc_to_pltl_semantics [simp]: "w \\<^sub>p (ltlc_to_pltl \) \ w \\<^sub>c \" by (induction \ arbitrary: w) simp_all subsubsection \Atoms\ fun atoms_pltl :: "'a pltl \ ('a \ bool) set" where "atoms_pltl false\<^sub>p = {}" | "atoms_pltl atom\<^sub>p(p) = {p}" | "atoms_pltl (\ implies\<^sub>p \) = atoms_pltl \ \ atoms_pltl \" | "atoms_pltl (X\<^sub>p \) = atoms_pltl \" | "atoms_pltl (\ U\<^sub>p \) = atoms_pltl \ \ atoms_pltl \" lemma atoms_finite [iff]: "finite (atoms_pltl \)" by (induct \) auto lemma atoms_pltl_sugar [simp]: "atoms_pltl (not\<^sub>p \) = atoms_pltl \" "atoms_pltl true\<^sub>p = {}" "atoms_pltl (\ or\<^sub>p \) = atoms_pltl \ \ atoms_pltl \" "atoms_pltl (\ and\<^sub>p \) = atoms_pltl \ \ atoms_pltl \" "atoms_pltl (F\<^sub>p \) = atoms_pltl \" "atoms_pltl (G\<^sub>p \) = atoms_pltl \" by (auto simp: Not_ltlp_def True_ltlp_def Or_ltlp_def And_ltlp_def Eventually_ltlp_def Always_ltlp_def) end diff --git a/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy b/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy --- a/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy +++ b/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy @@ -1,539 +1,996 @@ (* Author: Benedikt Seidl + Author: Salomon Sickert License: BSD *) section \Advice functions\ theory Advice imports LTL.LTL LTL.Equivalence_Relations Syntactic_Fragments_and_Stability After begin subsection \The GF and FG Advice Functions\ fun GF_advice :: "'a ltln \ 'a ltln set \ 'a ltln" ("_[_]\<^sub>\" [90,60] 89) where "(X\<^sub>n \)[X]\<^sub>\ = X\<^sub>n (\[X]\<^sub>\)" | "(\\<^sub>1 and\<^sub>n \\<^sub>2)[X]\<^sub>\ = (\\<^sub>1[X]\<^sub>\) and\<^sub>n (\\<^sub>2[X]\<^sub>\)" | "(\\<^sub>1 or\<^sub>n \\<^sub>2)[X]\<^sub>\ = (\\<^sub>1[X]\<^sub>\) or\<^sub>n (\\<^sub>2[X]\<^sub>\)" | "(\\<^sub>1 W\<^sub>n \\<^sub>2)[X]\<^sub>\ = (\\<^sub>1[X]\<^sub>\) W\<^sub>n (\\<^sub>2[X]\<^sub>\)" | "(\\<^sub>1 R\<^sub>n \\<^sub>2)[X]\<^sub>\ = (\\<^sub>1[X]\<^sub>\) R\<^sub>n (\\<^sub>2[X]\<^sub>\)" | "(\\<^sub>1 U\<^sub>n \\<^sub>2)[X]\<^sub>\ = (if (\\<^sub>1 U\<^sub>n \\<^sub>2) \ X then (\\<^sub>1[X]\<^sub>\) W\<^sub>n (\\<^sub>2[X]\<^sub>\) else false\<^sub>n)" | "(\\<^sub>1 M\<^sub>n \\<^sub>2)[X]\<^sub>\ = (if (\\<^sub>1 M\<^sub>n \\<^sub>2) \ X then (\\<^sub>1[X]\<^sub>\) R\<^sub>n (\\<^sub>2[X]\<^sub>\) else false\<^sub>n)" | "\[_]\<^sub>\ = \" fun FG_advice :: "'a ltln \ 'a ltln set \ 'a ltln" ("_[_]\<^sub>\" [90,60] 89) where "(X\<^sub>n \)[Y]\<^sub>\ = X\<^sub>n (\[Y]\<^sub>\)" | "(\\<^sub>1 and\<^sub>n \\<^sub>2)[Y]\<^sub>\ = (\\<^sub>1[Y]\<^sub>\) and\<^sub>n (\\<^sub>2[Y]\<^sub>\)" | "(\\<^sub>1 or\<^sub>n \\<^sub>2)[Y]\<^sub>\ = (\\<^sub>1[Y]\<^sub>\) or\<^sub>n (\\<^sub>2[Y]\<^sub>\)" | "(\\<^sub>1 U\<^sub>n \\<^sub>2)[Y]\<^sub>\ = (\\<^sub>1[Y]\<^sub>\) U\<^sub>n (\\<^sub>2[Y]\<^sub>\)" | "(\\<^sub>1 M\<^sub>n \\<^sub>2)[Y]\<^sub>\ = (\\<^sub>1[Y]\<^sub>\) M\<^sub>n (\\<^sub>2[Y]\<^sub>\)" | "(\\<^sub>1 W\<^sub>n \\<^sub>2)[Y]\<^sub>\ = (if (\\<^sub>1 W\<^sub>n \\<^sub>2) \ Y then true\<^sub>n else (\\<^sub>1[Y]\<^sub>\) U\<^sub>n (\\<^sub>2[Y]\<^sub>\))" | "(\\<^sub>1 R\<^sub>n \\<^sub>2)[Y]\<^sub>\ = (if (\\<^sub>1 R\<^sub>n \\<^sub>2) \ Y then true\<^sub>n else (\\<^sub>1[Y]\<^sub>\) M\<^sub>n (\\<^sub>2[Y]\<^sub>\))" | "\[_]\<^sub>\ = \" lemma GF_advice_\LTL: "\[X]\<^sub>\ \ \LTL" "\ \ \LTL \ \[X]\<^sub>\ = \" by (induction \) auto lemma FG_advice_\LTL: "\[X]\<^sub>\ \ \LTL" "\ \ \LTL \ \[X]\<^sub>\ = \" by (induction \) auto lemma GF_advice_subfrmlsn: "subfrmlsn (\[X]\<^sub>\) \ {\[X]\<^sub>\ | \. \ \ subfrmlsn \}" by (induction \) force+ lemma FG_advice_subfrmlsn: "subfrmlsn (\[Y]\<^sub>\) \ {\[Y]\<^sub>\ | \. \ \ subfrmlsn \}" by (induction \) force+ lemma GF_advice_subfrmlsn_card: "card (subfrmlsn (\[X]\<^sub>\)) \ card (subfrmlsn \)" proof - have "card (subfrmlsn (\[X]\<^sub>\)) \ card {\[X]\<^sub>\ | \. \ \ subfrmlsn \}" by (simp add: subfrmlsn_finite GF_advice_subfrmlsn card_mono) also have "\ \ card (subfrmlsn \)" by (metis Collect_mem_eq card_image_le image_Collect subfrmlsn_finite) finally show ?thesis . qed lemma FG_advice_subfrmlsn_card: "card (subfrmlsn (\[Y]\<^sub>\)) \ card (subfrmlsn \)" proof - have "card (subfrmlsn (\[Y]\<^sub>\)) \ card {\[Y]\<^sub>\ | \. \ \ subfrmlsn \}" by (simp add: subfrmlsn_finite FG_advice_subfrmlsn card_mono) also have "\ \ card (subfrmlsn \)" by (metis Collect_mem_eq card_image_le image_Collect subfrmlsn_finite) finally show ?thesis . qed +lemma GF_advice_monotone: + "X \ Y \ w \\<^sub>n \[X]\<^sub>\ \ w \\<^sub>n \[Y]\<^sub>\" +proof (induction \ arbitrary: w) + case (Until_ltln \ \) + then show ?case + by (cases "\ U\<^sub>n \ \ X") (simp_all, blast) +next + case (Release_ltln \ \) + then show ?case by (simp, blast) +next + case (WeakUntil_ltln \ \) + then show ?case by (simp, blast) +next + case (StrongRelease_ltln \ \) + then show ?case + by (cases "\ M\<^sub>n \ \ X") (simp_all, blast) +qed auto +lemma FG_advice_monotone: + "X \ Y \ w \\<^sub>n \[X]\<^sub>\ \ w \\<^sub>n \[Y]\<^sub>\" +proof (induction \ arbitrary: w) + case (Until_ltln \ \) + then show ?case by (simp, blast) +next + case (Release_ltln \ \) + then show ?case + by (cases "\ R\<^sub>n \ \ X") (auto, blast) +next + case (WeakUntil_ltln \ \) + then show ?case + by (cases "\ W\<^sub>n \ \ X") (auto, blast) +next + case (StrongRelease_ltln \ \) + then show ?case by (simp, blast) +qed auto + +lemma GF_advice_ite_simps[simp]: + "(if P then true\<^sub>n else false\<^sub>n)[X]\<^sub>\ = (if P then true\<^sub>n else false\<^sub>n)" + "(if P then false\<^sub>n else true\<^sub>n)[X]\<^sub>\ = (if P then false\<^sub>n else true\<^sub>n)" + by simp_all + +lemma FG_advice_ite_simps[simp]: + "(if P then true\<^sub>n else false\<^sub>n)[Y]\<^sub>\ = (if P then true\<^sub>n else false\<^sub>n)" + "(if P then false\<^sub>n else true\<^sub>n)[Y]\<^sub>\ = (if P then false\<^sub>n else true\<^sub>n)" + by simp_all subsection \Advice Functions on Nested Propositions\ definition nested_prop_atoms\<^sub>\ :: "'a ltln \ 'a ltln set \ 'a ltln set" where "nested_prop_atoms\<^sub>\ \ X = {\[X]\<^sub>\ | \. \ \ nested_prop_atoms \}" definition nested_prop_atoms\<^sub>\ :: "'a ltln \ 'a ltln set \ 'a ltln set" where "nested_prop_atoms\<^sub>\ \ X = {\[X]\<^sub>\ | \. \ \ nested_prop_atoms \}" lemma nested_prop_atoms\<^sub>\_finite: "finite (nested_prop_atoms\<^sub>\ \ X)" by (simp add: nested_prop_atoms\<^sub>\_def nested_prop_atoms_finite) lemma nested_prop_atoms\<^sub>\_finite: "finite (nested_prop_atoms\<^sub>\ \ X)" by (simp add: nested_prop_atoms\<^sub>\_def nested_prop_atoms_finite) lemma nested_prop_atoms\<^sub>\_card: "card (nested_prop_atoms\<^sub>\ \ X) \ card (nested_prop_atoms \)" unfolding nested_prop_atoms\<^sub>\_def by (metis Collect_mem_eq card_image_le image_Collect nested_prop_atoms_finite) lemma nested_prop_atoms\<^sub>\_card: "card (nested_prop_atoms\<^sub>\ \ X) \ card (nested_prop_atoms \)" unfolding nested_prop_atoms\<^sub>\_def by (metis Collect_mem_eq card_image_le image_Collect nested_prop_atoms_finite) lemma GF_advice_nested_prop_atoms\<^sub>\: "nested_prop_atoms (\[X]\<^sub>\) \ nested_prop_atoms\<^sub>\ \ X" by (induction \) (unfold nested_prop_atoms\<^sub>\_def, force+) lemma FG_advice_nested_prop_atoms\<^sub>\: "nested_prop_atoms (\[Y]\<^sub>\) \ nested_prop_atoms\<^sub>\ \ Y" by (induction \) (unfold nested_prop_atoms\<^sub>\_def, force+) +lemma nested_prop_atoms\<^sub>\_subset: + "nested_prop_atoms \ \ nested_prop_atoms \ \ nested_prop_atoms\<^sub>\ \ X \ nested_prop_atoms\<^sub>\ \ X" + unfolding nested_prop_atoms\<^sub>\_def by blast + +lemma nested_prop_atoms\<^sub>\_subset: + "nested_prop_atoms \ \ nested_prop_atoms \ \ nested_prop_atoms\<^sub>\ \ Y \ nested_prop_atoms\<^sub>\ \ Y" + unfolding nested_prop_atoms\<^sub>\_def by blast + lemma GF_advice_nested_prop_atoms_card: "card (nested_prop_atoms (\[X]\<^sub>\)) \ card (nested_prop_atoms \)" proof - have "card (nested_prop_atoms (\[X]\<^sub>\)) \ card (nested_prop_atoms\<^sub>\ \ X)" by (simp add: nested_prop_atoms\<^sub>\_finite GF_advice_nested_prop_atoms\<^sub>\ card_mono) then show ?thesis using nested_prop_atoms\<^sub>\_card le_trans by blast qed lemma FG_advice_nested_prop_atoms_card: "card (nested_prop_atoms (\[Y]\<^sub>\)) \ card (nested_prop_atoms \)" proof - have "card (nested_prop_atoms (\[Y]\<^sub>\)) \ card (nested_prop_atoms\<^sub>\ \ Y)" by (simp add: nested_prop_atoms\<^sub>\_finite FG_advice_nested_prop_atoms\<^sub>\ card_mono) then show ?thesis using nested_prop_atoms\<^sub>\_card le_trans by blast qed subsection \Intersecting the Advice Set\ lemma GF_advice_inter: "X \ subformulas\<^sub>\ \ \ S \ \[X \ S]\<^sub>\ = \[X]\<^sub>\" by (induction \) auto lemma GF_advice_inter_subformulas: "\[X \ subformulas\<^sub>\ \]\<^sub>\ = \[X]\<^sub>\" using GF_advice_inter by blast lemma GF_advice_minus_subformulas: "\ \ subformulas\<^sub>\ \ \ \[X - {\}]\<^sub>\ = \[X]\<^sub>\" proof - assume "\ \ subformulas\<^sub>\ \" then have "subformulas\<^sub>\ \ \ X \ X - {\}" by blast then show "\[X - {\}]\<^sub>\ = \[X]\<^sub>\" by (metis GF_advice_inter Diff_subset Int_absorb1 inf.commute) qed lemma GF_advice_minus_size: "\size \ \ size \; \ \ \\ \ \[X - {\}]\<^sub>\ = \[X]\<^sub>\" using subfrmlsn_size subformulas\<^sub>\_subfrmlsn GF_advice_minus_subformulas by fastforce lemma FG_advice_inter: "Y \ subformulas\<^sub>\ \ \ S \ \[Y \ S]\<^sub>\ = \[Y]\<^sub>\" by (induction \) auto lemma FG_advice_inter_subformulas: "\[Y \ subformulas\<^sub>\ \]\<^sub>\ = \[Y]\<^sub>\" using FG_advice_inter by blast lemma FG_advice_minus_subformulas: "\ \ subformulas\<^sub>\ \ \ \[Y - {\}]\<^sub>\ = \[Y]\<^sub>\" proof - assume "\ \ subformulas\<^sub>\ \" then have "subformulas\<^sub>\ \ \ Y \ Y - {\}" by blast then show "\[Y - {\}]\<^sub>\ = \[Y]\<^sub>\" by (metis FG_advice_inter Diff_subset Int_absorb1 inf.commute) qed lemma FG_advice_minus_size: "\size \ \ size \; \ \ \\ \ \[Y - {\}]\<^sub>\ = \[Y]\<^sub>\" using subfrmlsn_size subformulas\<^sub>\_subfrmlsn FG_advice_minus_subformulas by fastforce lemma FG_advice_insert: "\\ \ Y; size \ < size \\ \ \[insert \ Y]\<^sub>\ = \[Y]\<^sub>\" by (metis FG_advice_minus_size Diff_insert_absorb less_imp_le neq_iff) subsection \Correctness GF-advice function\ lemma GF_advice_a1: "\\ \ w \ X; w \\<^sub>n \\ \ w \\<^sub>n \[X]\<^sub>\" proof (induction \ arbitrary: w) case (Next_ltln \) then show ?case using \_suffix by simp blast next case (Until_ltln \1 \2) have "\ (\1 W\<^sub>n \2) w \ \ (\1 U\<^sub>n \2) w" by fastforce then have "\ (\1 W\<^sub>n \2) w \ X" and "w \\<^sub>n \1 W\<^sub>n \2" using Until_ltln.prems ltln_strong_to_weak by blast+ then have "w \\<^sub>n \1[X]\<^sub>\ W\<^sub>n \2[X]\<^sub>\" using Until_ltln.IH by simp (meson \_suffix subset_trans sup.boundedE) moreover have "w \\<^sub>n \1 U\<^sub>n \2" using Until_ltln.prems by simp then have "\1 U\<^sub>n \2 \ \ (\1 U\<^sub>n \2) w" by force then have "\1 U\<^sub>n \2 \ X" using Until_ltln.prems by fast ultimately show ?case by auto next case (Release_ltln \1 \2) then show ?case by simp (meson \_suffix subset_trans sup.boundedE) next case (WeakUntil_ltln \1 \2) then show ?case by simp (meson \_suffix subset_trans sup.boundedE) next case (StrongRelease_ltln \1 \2) have "\ (\1 R\<^sub>n \2) w \ \ (\1 M\<^sub>n \2) w" by fastforce then have "\ (\1 R\<^sub>n \2) w \ X" and "w \\<^sub>n \1 R\<^sub>n \2" using StrongRelease_ltln.prems ltln_strong_to_weak by blast+ then have "w \\<^sub>n \1[X]\<^sub>\ R\<^sub>n \2[X]\<^sub>\" using StrongRelease_ltln.IH by simp (meson \_suffix subset_trans sup.boundedE) moreover have "w \\<^sub>n \1 M\<^sub>n \2" using StrongRelease_ltln.prems by simp then have "\1 M\<^sub>n \2 \ \ (\1 M\<^sub>n \2) w" by force then have "\1 M\<^sub>n \2 \ X" using StrongRelease_ltln.prems by fast ultimately show ?case by auto qed auto lemma GF_advice_a2_helper: "\\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \); w \\<^sub>n \[X]\<^sub>\\ \ w \\<^sub>n \" proof (induction \ arbitrary: w) case (Next_ltln \) then show ?case unfolding GF_advice.simps semantics_ltln.simps(7) using GF_suffix by blast next case (Until_ltln \1 \2) then have "\1 U\<^sub>n \2 \ X" using ccontr[of "\1 U\<^sub>n \2 \ X"] by force then have "w \\<^sub>n F\<^sub>n \2" using Until_ltln.prems by fastforce moreover have "w \\<^sub>n (\1 U\<^sub>n \2)[X]\<^sub>\" using Until_ltln.prems by simp then have "w \\<^sub>n (\1[X]\<^sub>\) W\<^sub>n (\2[X]\<^sub>\)" unfolding GF_advice.simps using `\1 U\<^sub>n \2 \ X` by simp then have "w \\<^sub>n \1 W\<^sub>n \2" unfolding GF_advice.simps semantics_ltln.simps(10) by (metis GF_suffix Until_ltln.IH Until_ltln.prems(1)) ultimately show ?case using ltln_weak_to_strong by blast next case (Release_ltln \1 \2) then show ?case unfolding GF_advice.simps semantics_ltln.simps(9) by (metis GF_suffix Release_ltln.IH Release_ltln.prems(1)) next case (WeakUntil_ltln \1 \2) then show ?case unfolding GF_advice.simps semantics_ltln.simps(10) by (metis GF_suffix) next case (StrongRelease_ltln \1 \2) then have "\1 M\<^sub>n \2 \ X" using ccontr[of "\1 M\<^sub>n \2 \ X"] by force then have "w \\<^sub>n F\<^sub>n \1" using StrongRelease_ltln.prems by fastforce moreover have "w \\<^sub>n (\1 M\<^sub>n \2)[X]\<^sub>\" using StrongRelease_ltln.prems by simp then have "w \\<^sub>n (\1[X]\<^sub>\) R\<^sub>n (\2[X]\<^sub>\)" unfolding GF_advice.simps using `\1 M\<^sub>n \2 \ X` by simp then have "w \\<^sub>n \1 R\<^sub>n \2" unfolding GF_advice.simps semantics_ltln.simps(9) by (metis GF_suffix StrongRelease_ltln.IH StrongRelease_ltln.prems(1)) ultimately show ?case using ltln_weak_to_strong by blast qed auto lemma GF_advice_a2: "\X \ \\ \ w; w \\<^sub>n \[X]\<^sub>\\ \ w \\<^sub>n \" by (metis GF_advice_a2_helper \\_elim subset_eq) lemma GF_advice_a3: "\X = \ \ w; X = \\ \ w\ \ w \\<^sub>n \ \ w \\<^sub>n \[X]\<^sub>\" using GF_advice_a1 GF_advice_a2 by fastforce subsection \Correctness FG-advice function\ lemma FG_advice_b1: "\\\ \ w \ Y; w \\<^sub>n \\ \ w \\<^sub>n \[Y]\<^sub>\" proof (induction \ arbitrary: w) case (Next_ltln \) then show ?case using \\_suffix by simp blast next case (Until_ltln \1 \2) then show ?case by simp (metis \\_suffix) next case (Release_ltln \1 \2) show ?case proof (cases "\1 R\<^sub>n \2 \ Y") case False then have "\1 R\<^sub>n \2 \ \\ (\1 R\<^sub>n \2) w" using Release_ltln.prems by blast then have "\ w \\<^sub>n G\<^sub>n \2" by fastforce then have "w \\<^sub>n \1 M\<^sub>n \2" using Release_ltln.prems ltln_weak_to_strong by blast moreover have "\\ (\1 M\<^sub>n \2) w \ \\ (\1 R\<^sub>n \2) w" by fastforce then have "\\ (\1 M\<^sub>n \2) w \ Y" using Release_ltln.prems by blast ultimately show ?thesis using Release_ltln.IH by simp (metis \\_suffix) qed simp next case (WeakUntil_ltln \1 \2) show ?case proof (cases "\1 W\<^sub>n \2 \ Y") case False then have "\1 W\<^sub>n \2 \ \\ (\1 W\<^sub>n \2) w" using WeakUntil_ltln.prems by blast then have "\ w \\<^sub>n G\<^sub>n \1" by fastforce then have "w \\<^sub>n \1 U\<^sub>n \2" using WeakUntil_ltln.prems ltln_weak_to_strong by blast moreover have "\\ (\1 U\<^sub>n \2) w \ \\ (\1 W\<^sub>n \2) w" by fastforce then have "\\ (\1 U\<^sub>n \2) w \ Y" using WeakUntil_ltln.prems by blast ultimately show ?thesis using WeakUntil_ltln.IH by simp (metis \\_suffix) qed simp next case (StrongRelease_ltln \1 \2) then show ?case by simp (metis \\_suffix) qed auto lemma FG_advice_b2_helper: "\\\ \ Y. w \\<^sub>n G\<^sub>n \; w \\<^sub>n \[Y]\<^sub>\\ \ w \\<^sub>n \" proof (induction \ arbitrary: w) case (Until_ltln \1 \2) then show ?case by simp (metis (no_types, lifting) suffix_suffix) next case (Release_ltln \1 \2) then show ?case proof (cases "\1 R\<^sub>n \2 \ Y") case True then show ?thesis using Release_ltln.prems by force next case False then have "w \\<^sub>n (\1[Y]\<^sub>\) M\<^sub>n (\2[Y]\<^sub>\)" using Release_ltln.prems by simp then have "w \\<^sub>n \1 M\<^sub>n \2" using Release_ltln by simp (metis (no_types, lifting) suffix_suffix) then show ?thesis using ltln_strong_to_weak by fast qed next case (WeakUntil_ltln \1 \2) then show ?case proof (cases "\1 W\<^sub>n \2 \ Y") case True then show ?thesis using WeakUntil_ltln.prems by force next case False then have "w \\<^sub>n (\1[Y]\<^sub>\) U\<^sub>n (\2[Y]\<^sub>\)" using WeakUntil_ltln.prems by simp then have "w \\<^sub>n \1 U\<^sub>n \2" using WeakUntil_ltln by simp (metis (no_types, lifting) suffix_suffix) then show ?thesis using ltln_strong_to_weak by fast qed next case (StrongRelease_ltln \1 \2) then show ?case by simp (metis (no_types, lifting) suffix_suffix) qed auto lemma FG_advice_b2: "\Y \ \ \ w; w \\<^sub>n \[Y]\<^sub>\\ \ w \\<^sub>n \" by (metis FG_advice_b2_helper \_elim subset_eq) lemma FG_advice_b3: "\Y = \\ \ w; Y = \ \ w\ \ w \\<^sub>n \ \ w \\<^sub>n \[Y]\<^sub>\" using FG_advice_b1 FG_advice_b2 by fastforce -subsection \Advice functions and the after function\ +subsection \Advice Functions and the ``after'' Function\ lemma GF_advice_af_letter: "(x ## w) \\<^sub>n \[X]\<^sub>\ \ w \\<^sub>n (af_letter \ x)[X]\<^sub>\" proof (induction \) case (Until_ltln \1 \2) then have "w \\<^sub>n af_letter ((\1 U\<^sub>n \2)[X]\<^sub>\) x" using af_letter_build by blast then show ?case using Until_ltln.IH af_letter_build by fastforce next case (Release_ltln \1 \2) then have "w \\<^sub>n af_letter ((\1 R\<^sub>n \2)[X]\<^sub>\) x" using af_letter_build by blast then show ?case using Release_ltln.IH af_letter_build by auto next case (WeakUntil_ltln \1 \2) then have "w \\<^sub>n af_letter ((\1 W\<^sub>n \2)[X]\<^sub>\) x" using af_letter_build by blast then show ?case using WeakUntil_ltln.IH af_letter_build by auto next case (StrongRelease_ltln \1 \2) then have "w \\<^sub>n af_letter ((\1 M\<^sub>n \2)[X]\<^sub>\) x" using af_letter_build by blast then show ?case using StrongRelease_ltln.IH af_letter_build by force qed auto +lemma FG_advice_af_letter: + "w \\<^sub>n (af_letter \ x)[Y]\<^sub>\ \ (x ## w) \\<^sub>n \[Y]\<^sub>\" +proof (induction \) + case (Prop_ltln a) + then show ?case + using semantics_ltln.simps(3) by fastforce +next + case (Until_ltln \1 \2) + then show ?case + unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6) + using af_letter_build apply (cases "w \\<^sub>n af_letter \2 x[Y]\<^sub>\") apply force + by (metis af_letter.simps(8) semantics_ltln.simps(5) semantics_ltln.simps(6)) +next + case (Release_ltln \1 \2) + then show ?case + apply (cases "\1 R\<^sub>n \2 \ Y") + apply simp + unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6) + using af_letter_build apply (cases "w \\<^sub>n af_letter \1 x[Y]\<^sub>\") apply force + by (metis (full_types) af_letter.simps(11) semantics_ltln.simps(5) semantics_ltln.simps(6)) +next + case (WeakUntil_ltln \1 \2) + then show ?case + apply (cases "\1 W\<^sub>n \2 \ Y") + apply simp + unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6) + using af_letter_build apply (cases "w \\<^sub>n af_letter \2 x[Y]\<^sub>\") apply force + by (metis (full_types) af_letter.simps(8) semantics_ltln.simps(5) semantics_ltln.simps(6)) +next + case (StrongRelease_ltln \1 \2) + then show ?case + unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6) + using af_letter_build apply (cases "w \\<^sub>n af_letter \1 x[Y]\<^sub>\") apply force + by (metis af_letter.simps(11) semantics_ltln.simps(5) semantics_ltln.simps(6)) +qed auto + lemma GF_advice_af: "(w \ w') \\<^sub>n \[X]\<^sub>\ \ w' \\<^sub>n (af \ w)[X]\<^sub>\" by (induction w arbitrary: \) (simp, insert GF_advice_af_letter, fastforce) +lemma FG_advice_af: + "w' \\<^sub>n (af \ w)[X]\<^sub>\ \ (w \ w') \\<^sub>n \[X]\<^sub>\" + by (induction w arbitrary: \) (simp, insert FG_advice_af_letter, fastforce) + +lemma GF_advice_af_2: + "w \\<^sub>n \[X]\<^sub>\ \ suffix i w \\<^sub>n (af \ (prefix i w))[X]\<^sub>\" + using GF_advice_af by force + +lemma FG_advice_af_2: + "suffix i w \\<^sub>n (af \ (prefix i w))[X]\<^sub>\ \ w \\<^sub>n \[X]\<^sub>\" + using FG_advice_af by force + +(* TODO move to Omega_Words_Fun.thy ?? *) +lemma prefix_suffix_subsequence: "prefix i (suffix j w) = (w [j \ i + j])" + by (simp add: add.commute) + +text \We show this generic lemma to prove the following theorems:\ + +lemma GF_advice_sync: + fixes index :: "nat \ nat" + fixes formula :: "nat \ 'a ltln" + assumes "\i. i < n \ \j. suffix ((index i) + j) w \\<^sub>n af (formula i) (w [index i \ (index i) + j])[X]\<^sub>\" + shows "\k. (\i < n. k \ index i \ suffix k w \\<^sub>n af (formula i) (w [index i \ k])[X]\<^sub>\)" + using assms +proof (induction n) + case (Suc n) + + obtain k1 where leq1: "\i. i < n \ k1 \ index i" + and suffix1: "\i. i < n \ suffix k1 w \\<^sub>n af (formula i) (w [(index i) \ k1])[X]\<^sub>\" + using Suc less_SucI by blast + + obtain k2 where leq2: "k2 \ index n" + and suffix2: "suffix k2 w \\<^sub>n af (formula n) (w [index n \ k2])[X]\<^sub>\" + using le_add1 Suc.prems by blast + + define k where "k \ k1 + k2" + + have "\i. i < Suc n \ k \ index i" + unfolding k_def by (metis leq1 leq2 less_SucE trans_le_add1 trans_le_add2) + + moreover + + { + have "\i. i < n \ suffix k w \\<^sub>n af (formula i) (w [(index i) \ k])[X]\<^sub>\" + unfolding k_def + by (metis GF_advice_af_2[OF suffix1, unfolded suffix_suffix prefix_suffix_subsequence] af_subsequence_append leq1 add.commute le_add1) + + moreover + + have "suffix k w \\<^sub>n af (formula n) (w [index n \ k])[X]\<^sub>\" + unfolding k_def + by (metis GF_advice_af_2[OF suffix2, unfolded suffix_suffix prefix_suffix_subsequence] af_subsequence_append leq2 add.commute le_add1) + + ultimately + + have "\i. i \ n \ suffix k w \\<^sub>n af (formula i) (w [(index i) \ k])[X]\<^sub>\" + using nat_less_le by blast + } + + ultimately + + show ?case + by (meson less_Suc_eq_le) +qed simp + +lemma GF_advice_sync_and: + assumes "\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" + assumes "\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" + shows "\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\ \ suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" +proof - + let ?formula = "\i :: nat. (if (i = 0) then \ else \)" + + have assms: "\i. i < 2 \ \j. suffix j w \\<^sub>n af (?formula i) (w [0 \ j])[X]\<^sub>\" + using assms by simp + obtain k where k_def: "\i :: nat. i < 2 \ suffix k w \\<^sub>n af (if i = 0 then \ else \) (prefix k w)[X]\<^sub>\" + using GF_advice_sync[of "2" "\i. 0" w ?formula, simplified, OF assms, simplified] by blast + show ?thesis + using k_def[of 0] k_def[of 1] by auto +qed + +lemma GF_advice_sync_less: + assumes "\i. i < n \ \j. suffix (i + j) w \\<^sub>n af \ (w [i \ j + i])[X]\<^sub>\" + assumes "\j. suffix (n + j) w \\<^sub>n af \ (w [n \ j + n])[X]\<^sub>\" + shows "\k \ n. (\j < n. suffix k w \\<^sub>n af \ (w [j \ k])[X]\<^sub>\) \ suffix k w \\<^sub>n af \ (w [n \ k])[X]\<^sub>\" +proof - + let ?index = "\i. min i n" + let ?formula = "\i. if (i < n) then \ else \" + + { + fix i + assume "i < Suc n" + then have min_def: "min i n = i" + by simp + have "\j. suffix ((?index i) + j) w \\<^sub>n af (?formula i) (w [?index i \ (?index i) + j])[X]\<^sub>\" + unfolding min_def + by (cases "i < n") + (metis (full_types) assms(1) add.commute, metis (full_types) assms(2) \i < Suc n\ add.commute less_SucE) + } + + then obtain k where leq: "(\i. i < Suc n \ min i n \ k)" + and suffix: "\i. i < Suc n \ suffix k w \\<^sub>n af (if i < n then \ else \) (w [min i n \ k])[X]\<^sub>\" + using GF_advice_sync[of "Suc n" ?index w ?formula X] by metis + + have "\j < n. suffix k w \\<^sub>n af \ (w [j \ k])[X]\<^sub>\" + using suffix by (metis (full_types) less_SucI min.strict_order_iff) + + moreover + + have "suffix k w \\<^sub>n af \ (w [n \ k])[X]\<^sub>\" + using suffix[of n, simplified] by blast + + moreover + + have "k \ n" + using leq by presburger + + ultimately + show ?thesis + by auto +qed + +lemma GF_advice_sync_lesseq: + assumes "\i. i \ n \ \j. suffix (i + j) w \\<^sub>n af \ (w [i \ j + i])[X]\<^sub>\" + assumes "\j. suffix (n + j) w \\<^sub>n af \ (w [n \ j + n])[X]\<^sub>\" + shows "\k \ n. (\j \ n. suffix k w \\<^sub>n af \ (w [j \ k])[X]\<^sub>\) \ suffix k w \\<^sub>n af \ (w [n \ k])[X]\<^sub>\" +proof - + let ?index = "\i. min i n" + let ?formula = "\i. if (i \ n) then \ else \" + + { + fix i + assume "i < Suc (Suc n)" + hence "\j. suffix ((?index i) + j) w \\<^sub>n af (?formula i) (w [?index i \ (?index i) + j])[X]\<^sub>\" + proof (cases "i < Suc n") + case True + then have min_def: "min i n = i" + by simp + show ?thesis + unfolding min_def by (metis (full_types) assms(1) Suc_leI Suc_le_mono True add.commute) + next + case False + then have i_def: "i = Suc n" + using \i < Suc (Suc n)\ less_antisym by blast + have min_def: "min i n = n" + unfolding i_def by simp + show ?thesis + using assms(2) False + by (simp add: min_def add.commute) + qed + } + + then obtain k where leq: "(\i. i \ Suc n \ min i n \ k)" + and suffix: "\i :: nat. i < Suc (Suc n) \ suffix k w \\<^sub>n af (if i \ n then \ else \) (w [min i n \ k])[X]\<^sub>\" + using GF_advice_sync[of "Suc (Suc n)" ?index w ?formula X] + by (metis (no_types, hide_lams) less_Suc_eq min_le_iff_disj) + + have "\j \ n. suffix k w \\<^sub>n af \ (w [j \ k])[X]\<^sub>\" + using suffix by (metis (full_types) le_SucI less_Suc_eq_le min.orderE) + + moreover + + have "suffix k w \\<^sub>n af \ (w [n \ k])[X]\<^sub>\" + using suffix[of "Suc n", simplified] by linarith + + moreover + + have "k \ n" + using leq by presburger + + ultimately + show ?thesis + by auto +qed + +lemma af_subsequence_U_GF_advice: + assumes "i \ n" + assumes "suffix n w \\<^sub>n ((af \ (w [i \ n]))[X]\<^sub>\)" + assumes "\j. j < i \ suffix n w \\<^sub>n ((af \ (w [j \ n]))[X]\<^sub>\)" + shows "suffix (Suc n) w \\<^sub>n (af (\ U\<^sub>n \) (prefix (Suc n) w))[X]\<^sub>\" + using assms +proof (induction i arbitrary: w n) + case 0 + then have A: "suffix n w \\<^sub>n ((af \ (w [0 \ n]))[X]\<^sub>\)" + by blast + then have "suffix (Suc n) w \\<^sub>n (af \ (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF A, of 1] by simp + then show ?case + unfolding GF_advice.simps af_subsequence_U semantics_ltln.simps by blast +next + case (Suc i) + have "suffix (Suc n) w \\<^sub>n (af \ (prefix (Suc n) w))[X]\<^sub>\" + using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1] + by simp + moreover + have B: "(Suc (n - 1)) = n" + using Suc by simp + note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems + then have "suffix (Suc n) w \\<^sub>n (af (\ U\<^sub>n \) (w [1 \ (Suc n)]))[X]\<^sub>\" + by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift) + ultimately + show ?case + unfolding af_subsequence_U semantics_ltln.simps GF_advice.simps by blast +qed + +lemma af_subsequence_M_GF_advice: + assumes "i \ n" + assumes "suffix n w \\<^sub>n ((af \ (w [i \ n]))[X]\<^sub>\)" + assumes "\j. j \ i \ suffix n w \\<^sub>n ((af \ (w [j \ n]))[X]\<^sub>\)" + shows "suffix (Suc n) w \\<^sub>n (af (\ M\<^sub>n \) (prefix (Suc n) w))[X]\<^sub>\" + using assms +proof (induction i arbitrary: w n) + case 0 + then have A: "suffix n w \\<^sub>n ((af \ (w [0 \ n]))[X]\<^sub>\)" + by blast + have "suffix (Suc n) w \\<^sub>n (af \ (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF A, of 1] by simp + moreover + have "suffix (Suc n) w \\<^sub>n (af \ (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by auto + ultimately + show ?case + unfolding af_subsequence_M GF_advice.simps semantics_ltln.simps by blast +next + case (Suc i) + have "suffix 1 (suffix n w) \\<^sub>n af (af \ (prefix n w)) [suffix n w 0][X]\<^sub>\" + by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le) + then have "suffix (Suc n) w \\<^sub>n (af \ (prefix (Suc n) w))[X]\<^sub>\" + using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp + moreover + have B: "(Suc (n - 1)) = n" + using Suc by simp + note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix] + then have "suffix (Suc n) w \\<^sub>n (af (\ M\<^sub>n \) (w [1 \ (Suc n)]))[X]\<^sub>\" + by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems) + ultimately + show ?case + unfolding af_subsequence_M semantics_ltln.simps GF_advice.simps by blast +qed + +lemma af_subsequence_R_GF_advice: + assumes "i \ n" + assumes "suffix n w \\<^sub>n ((af \ (w [i \ n]))[X]\<^sub>\)" + assumes "\j. j \ i \ suffix n w \\<^sub>n ((af \ (w [j \ n]))[X]\<^sub>\)" + shows "suffix (Suc n) w \\<^sub>n (af (\ R\<^sub>n \) (prefix (Suc n) w))[X]\<^sub>\" + using assms +proof (induction i arbitrary: w n) + case 0 + then have A: "suffix n w \\<^sub>n ((af \ (w [0 \ n]))[X]\<^sub>\)" + by blast + have "suffix (Suc n) w \\<^sub>n (af \ (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF A, of 1] by simp + moreover + have "suffix (Suc n) w \\<^sub>n (af \ (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by auto + ultimately + show ?case + unfolding af_subsequence_R GF_advice.simps semantics_ltln.simps by blast +next + case (Suc i) + have "suffix 1 (suffix n w) \\<^sub>n af (af \ (prefix n w)) [suffix n w 0][X]\<^sub>\" + by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le) + then have "suffix (Suc n) w \\<^sub>n (af \ (prefix (Suc n) w))[X]\<^sub>\" + using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp + moreover + have B: "(Suc (n - 1)) = n" + using Suc by simp + note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix] + then have "suffix (Suc n) w \\<^sub>n (af (\ R\<^sub>n \) (w [1 \ (Suc n)]))[X]\<^sub>\" + by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems) + ultimately + show ?case + unfolding af_subsequence_R semantics_ltln.simps GF_advice.simps by blast +qed + +lemma af_subsequence_W_GF_advice: + assumes "i \ n" + assumes "suffix n w \\<^sub>n ((af \ (w [i \ n]))[X]\<^sub>\)" + assumes "\j. j < i \ suffix n w \\<^sub>n ((af \ (w [j \ n]))[X]\<^sub>\)" + shows "suffix (Suc n) w \\<^sub>n (af (\ W\<^sub>n \) (prefix (Suc n) w))[X]\<^sub>\" + using assms +proof (induction i arbitrary: w n) + case 0 + then have A: "suffix n w \\<^sub>n ((af \ (w [0 \ n]))[X]\<^sub>\)" + by blast + have "suffix (Suc n) w \\<^sub>n (af \ (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF A, of 1] by simp + then show ?case + unfolding af_subsequence_W GF_advice.simps semantics_ltln.simps by blast +next + case (Suc i) + have "suffix (Suc n) w \\<^sub>n (af \ (prefix (Suc n) w))[X]\<^sub>\" + using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1] + by simp + moreover + have B: "(Suc (n - 1)) = n" + using Suc by simp + note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems + then have "suffix (Suc n) w \\<^sub>n (af (\ W\<^sub>n \) (w [1 \ (Suc n)]))[X]\<^sub>\" + by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift) + ultimately + show ?case + unfolding af_subsequence_W unfolding semantics_ltln.simps GF_advice.simps by simp +qed + +lemma af_subsequence_R_GF_advice_connect: + assumes "i \ n" + assumes "suffix n w \\<^sub>n af (\ R\<^sub>n \) (w [i \ n])[X]\<^sub>\" + assumes "\j. j \ i \ suffix n w \\<^sub>n ((af \ (w [j \ n]))[X]\<^sub>\)" + shows "suffix (Suc n) w \\<^sub>n (af (\ R\<^sub>n \) (prefix (Suc n) w))[X]\<^sub>\" + using assms +proof (induction i arbitrary: w n) + case 0 + then have A: "suffix n w \\<^sub>n ((af \ (w [0 \ n]))[X]\<^sub>\)" + by blast + have "suffix (Suc n) w \\<^sub>n (af \ (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF A, of 1] by simp + moreover + have "suffix (Suc n) w \\<^sub>n (af (\ R\<^sub>n \) (w [0 \ Suc n]))[X]\<^sub>\" + using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by simp + ultimately + show ?case + unfolding af_subsequence_R GF_advice.simps semantics_ltln.simps by blast +next + case (Suc i) + have "suffix 1 (suffix n w) \\<^sub>n af (af \ (prefix n w)) [suffix n w 0][X]\<^sub>\" + by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le) + then have "suffix (Suc n) w \\<^sub>n (af \ (prefix (Suc n) w))[X]\<^sub>\" + using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp + moreover + have B: "(Suc (n - 1)) = n" + using Suc by simp + note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix] + then have "suffix (Suc n) w \\<^sub>n (af (\ R\<^sub>n \) (w [1 \ (Suc n)]))[X]\<^sub>\" + by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems) + ultimately + show ?case + unfolding af_subsequence_R semantics_ltln.simps GF_advice.simps by blast +qed + +lemma af_subsequence_W_GF_advice_connect: + assumes "i \ n" + assumes "suffix n w \\<^sub>n af (\ W\<^sub>n \) (w [i \ n])[X]\<^sub>\" + assumes "\j. j < i \ suffix n w \\<^sub>n ((af \ (w [j \ n]))[X]\<^sub>\)" + shows "suffix (Suc n) w \\<^sub>n (af (\ W\<^sub>n \) (prefix (Suc n) w))[X]\<^sub>\" + using assms +proof (induction i arbitrary: w n) + case 0 + have "suffix (Suc n) w \\<^sub>n af_letter (af (\ W\<^sub>n \) (prefix n w)) (w n)[X]\<^sub>\" + by (simp add: "0.prems"(2) GF_advice_af_letter) + moreover + have "prefix (Suc n) w = prefix n w @ [w n]" + using subseq_to_Suc by blast + ultimately show ?case + by (metis (no_types) foldl.simps(1) foldl.simps(2) foldl_append) +next + case (Suc i) + have "suffix (Suc n) w \\<^sub>n (af \ (prefix (Suc n) w))[X]\<^sub>\" + using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp + moreover + have "n > 0" and B: "(Suc (n - 1)) = n" + using Suc by simp+ + note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems + then have "suffix (Suc n) w \\<^sub>n (af (\ W\<^sub>n \) (w [1 \ (Suc n)]))[X]\<^sub>\" + by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift) + ultimately + show ?case + unfolding af_subsequence_W unfolding semantics_ltln.simps GF_advice.simps by simp +qed subsection \Advice Functions and Propositional Entailment\ lemma GF_advice_prop_entailment: "\ \\<^sub>P \[X]\<^sub>\ \ {\. \[X]\<^sub>\ \ \} \\<^sub>P \" "false\<^sub>n \ \ \ {\. \[X]\<^sub>\ \ \} \\<^sub>P \ \ \ \\<^sub>P \[X]\<^sub>\" by (induction \) (auto, meson, meson) lemma GF_advice_iff_prop_entailment: "false\<^sub>n \ \ \ \ \\<^sub>P \[X]\<^sub>\ \ {\. \[X]\<^sub>\ \ \} \\<^sub>P \" by (metis GF_advice_prop_entailment) lemma FG_advice_prop_entailment: "true\<^sub>n \ \ \ \ \\<^sub>P \[Y]\<^sub>\ \ {\. \[Y]\<^sub>\ \ \} \\<^sub>P \" "{\. \[Y]\<^sub>\ \ \} \\<^sub>P \ \ \ \\<^sub>P \[Y]\<^sub>\" by (induction \) auto lemma FG_advice_iff_prop_entailment: "true\<^sub>n \ \ \ \ \\<^sub>P \[X]\<^sub>\ \ {\. \[X]\<^sub>\ \ \} \\<^sub>P \" by (metis FG_advice_prop_entailment) lemma GF_advice_subst: "\[X]\<^sub>\ = subst \ (\\. Some (\[X]\<^sub>\))" by (induction \) auto lemma FG_advice_subst: "\[X]\<^sub>\ = subst \ (\\. Some (\[X]\<^sub>\))" by (induction \) auto lemma GF_advice_prop_congruent: "\ \\<^sub>P \ \ \[X]\<^sub>\ \\<^sub>P \[X]\<^sub>\" "\ \\<^sub>P \ \ \[X]\<^sub>\ \\<^sub>P \[X]\<^sub>\" by (metis GF_advice_subst subst_respects_ltl_prop_entailment)+ lemma FG_advice_prop_congruent: "\ \\<^sub>P \ \ \[X]\<^sub>\ \\<^sub>P \[X]\<^sub>\" "\ \\<^sub>P \ \ \[X]\<^sub>\ \\<^sub>P \[X]\<^sub>\" by (metis FG_advice_subst subst_respects_ltl_prop_entailment)+ locale GF_advice_congruent = ltl_equivalence + assumes GF_advice_congruent: "\ \ \ \ \[X]\<^sub>\ \ \[X]\<^sub>\" begin end interpretation prop_GF_advice_compatible: GF_advice_congruent "(\\<^sub>P)" by unfold_locales (simp add: GF_advice_prop_congruent(2)) end diff --git a/thys/LTL_Master_Theorem/Logical_Characterization/After.thy b/thys/LTL_Master_Theorem/Logical_Characterization/After.thy --- a/thys/LTL_Master_Theorem/Logical_Characterization/After.thy +++ b/thys/LTL_Master_Theorem/Logical_Characterization/After.thy @@ -1,695 +1,719 @@ (* Author: Benedikt Seidl License: BSD *) section \The ``after''-Function\ theory After -imports +imports LTL.LTL LTL.Equivalence_Relations Syntactic_Fragments_and_Stability begin subsection \Definition of af\ primrec af_letter :: "'a ltln \ 'a set \ 'a ltln" where "af_letter true\<^sub>n \ = true\<^sub>n" | "af_letter false\<^sub>n \ = false\<^sub>n" | "af_letter prop\<^sub>n(a) \ = (if a \ \ then true\<^sub>n else false\<^sub>n)" | "af_letter nprop\<^sub>n(a) \ = (if a \ \ then true\<^sub>n else false\<^sub>n)" | "af_letter (\ and\<^sub>n \) \ = (af_letter \ \) and\<^sub>n (af_letter \ \)" | "af_letter (\ or\<^sub>n \) \ = (af_letter \ \) or\<^sub>n (af_letter \ \)" | "af_letter (X\<^sub>n \) \ = \" | "af_letter (\ U\<^sub>n \) \ = (af_letter \ \) or\<^sub>n ((af_letter \ \) and\<^sub>n (\ U\<^sub>n \))" | "af_letter (\ R\<^sub>n \) \ = (af_letter \ \) and\<^sub>n ((af_letter \ \) or\<^sub>n (\ R\<^sub>n \))" | "af_letter (\ W\<^sub>n \) \ = (af_letter \ \) or\<^sub>n ((af_letter \ \) and\<^sub>n (\ W\<^sub>n \))" | "af_letter (\ M\<^sub>n \) \ = (af_letter \ \) and\<^sub>n ((af_letter \ \) or\<^sub>n (\ M\<^sub>n \))" abbreviation af :: "'a ltln \ 'a set list \ 'a ltln" where "af \ w \ foldl af_letter \ w" lemma af_decompose: "af (\ and\<^sub>n \) w = (af \ w) and\<^sub>n (af \ w)" "af (\ or\<^sub>n \) w = (af \ w) or\<^sub>n (af \ w)" by (induction w rule: rev_induct) simp_all lemma af_simps[simp]: "af true\<^sub>n w = true\<^sub>n" "af false\<^sub>n w = false\<^sub>n" "af (X\<^sub>n \) (x # xs) = af \ xs" by (induction w) simp_all +lemma af_ite_simps[simp]: + "af (if P then true\<^sub>n else false\<^sub>n) w = (if P then true\<^sub>n else false\<^sub>n)" + "af (if P then false\<^sub>n else true\<^sub>n) w = (if P then false\<^sub>n else true\<^sub>n)" + by simp_all + +lemma af_subsequence_append: + "i \ j \ j \ k \ af (af \ (w [i \ j])) (w [j \ k]) = af \ (w [i \ k])" + by (metis foldl_append le_Suc_ex map_append subsequence_def upt_add_eq_append) + lemma af_subsequence_U: "af (\ U\<^sub>n \) (w [0 \ Suc n]) = (af \ (w [0 \ Suc n])) or\<^sub>n ((af \ (w [0 \ Suc n])) and\<^sub>n af (\ U\<^sub>n \) (w [1 \ Suc n]))" by (induction n) fastforce+ +lemma af_subsequence_U': + "af (\ U\<^sub>n \) (a # xs) = (af \ (a # xs)) or\<^sub>n ((af \ (a # xs)) and\<^sub>n af (\ U\<^sub>n \) xs)" + by (simp add: af_decompose) + lemma af_subsequence_R: "af (\ R\<^sub>n \) (w [0 \ Suc n]) = (af \ (w [0 \ Suc n])) and\<^sub>n ((af \ (w [0 \ Suc n])) or\<^sub>n af (\ R\<^sub>n \) (w [1 \ Suc n]))" by (induction n) fastforce+ +lemma af_subsequence_R': + "af (\ R\<^sub>n \) (a # xs) = (af \ (a # xs)) and\<^sub>n ((af \ (a # xs)) or\<^sub>n af (\ R\<^sub>n \) xs)" + by (simp add: af_decompose) + lemma af_subsequence_W: "af (\ W\<^sub>n \) (w [0 \ Suc n]) = (af \ (w [0 \ Suc n])) or\<^sub>n ((af \ (w [0 \ Suc n])) and\<^sub>n af (\ W\<^sub>n \) (w [1 \ Suc n]))" by (induction n) fastforce+ +lemma af_subsequence_W': + "af (\ W\<^sub>n \) (a # xs) = (af \ (a # xs)) or\<^sub>n ((af \ (a # xs)) and\<^sub>n af (\ W\<^sub>n \) xs)" + by (simp add: af_decompose) + lemma af_subsequence_M: "af (\ M\<^sub>n \) (w [0 \ Suc n]) = (af \ (w [0 \ Suc n])) and\<^sub>n ((af \ (w [0 \ Suc n])) or\<^sub>n af (\ M\<^sub>n \) (w [1 \ Suc n]))" by (induction n) fastforce+ +lemma af_subsequence_M': + "af (\ M\<^sub>n \) (a # xs) = (af \ (a # xs)) and\<^sub>n ((af \ (a # xs)) or\<^sub>n af (\ M\<^sub>n \) xs)" + by (simp add: af_decompose) lemma suffix_build[simp]: "suffix (Suc n) (x ## xs) = suffix n xs" by fastforce lemma af_letter_build: "(x ## w) \\<^sub>n \ \ w \\<^sub>n af_letter \ x" proof (induction \ arbitrary: x w) case (Until_ltln \ \) then show ?case unfolding ltln_expand_Until by force next case (Release_ltln \ \) then show ?case unfolding ltln_expand_Release by force next case (WeakUntil_ltln \ \) then show ?case unfolding ltln_expand_WeakUntil by force next case (StrongRelease_ltln \ \) then show ?case unfolding ltln_expand_StrongRelease by force qed simp+ lemma af_ltl_continuation: "(w \ w') \\<^sub>n \ \ w' \\<^sub>n af \ w" proof (induction w arbitrary: \ w') case (Cons x xs) then show ?case using af_letter_build by fastforce qed simp subsection \Range of the after function\ lemma af_letter_atoms: "atoms_ltln (af_letter \ \) \ atoms_ltln \" by (induction \) auto lemma af_atoms: "atoms_ltln (af \ w) \ atoms_ltln \" by (induction w rule: rev_induct) (simp, insert af_letter_atoms, fastforce) lemma af_letter_nested_prop_atoms: "nested_prop_atoms (af_letter \ \) \ nested_prop_atoms \" by (induction \) auto lemma af_nested_prop_atoms: "nested_prop_atoms (af \ w) \ nested_prop_atoms \" by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atoms, blast) lemma af_letter_range: "range (af_letter \) \ {\. nested_prop_atoms \ \ nested_prop_atoms \}" using af_letter_nested_prop_atoms by blast lemma af_range: "range (af \) \ {\. nested_prop_atoms \ \ nested_prop_atoms \}" using af_nested_prop_atoms by blast subsection \Subformulas of the after function\ lemma af_letter_subformulas\<^sub>\: "subformulas\<^sub>\ (af_letter \ \) = subformulas\<^sub>\ \" by (induction \) auto lemma af_subformulas\<^sub>\: "subformulas\<^sub>\ (af \ w) = subformulas\<^sub>\ \" using af_letter_subformulas\<^sub>\ by (induction w arbitrary: \ rule: rev_induct) (simp, fastforce) lemma af_letter_subformulas\<^sub>\: "subformulas\<^sub>\ (af_letter \ \) = subformulas\<^sub>\ \" by (induction \) auto lemma af_subformulas\<^sub>\: "subformulas\<^sub>\ (af \ w) = subformulas\<^sub>\ \" using af_letter_subformulas\<^sub>\ by (induction w arbitrary: \ rule: rev_induct) (simp, fastforce) subsection \Stability and the after function\ lemma \\_af: "\\ (af \ (prefix i w)) (suffix i w) = \\ \ (suffix i w)" unfolding \\_semantics' af_subformulas\<^sub>\ by blast lemma \_af: "\ (af \ (prefix i w)) (suffix i w) = \ \ (suffix i w)" unfolding \_semantics' af_subformulas\<^sub>\ by blast lemma \\_af: "\\ (af \ (prefix i w)) (suffix i w) = \\ \ (suffix i w)" unfolding \\_semantics' af_subformulas\<^sub>\ by blast lemma \_af: "\ (af \ (prefix i w)) (suffix i w) = \ \ (suffix i w)" unfolding \_semantics' af_subformulas\<^sub>\ by blast subsection \Congruence\ lemma af_letter_lang_congruent: "\ \\<^sub>L \ \ af_letter \ \ \\<^sub>L af_letter \ \" unfolding ltl_lang_equiv_def using af_letter_build by blast lemma af_lang_congruent: "\ \\<^sub>L \ \ af \ w \\<^sub>L af \ w" unfolding ltl_lang_equiv_def using af_ltl_continuation by (induction \) blast+ lemma af_letter_subst: "af_letter \ \ = subst \ (\\. Some (af_letter \ \))" by (induction \) auto lemma af_letter_prop_congruent: "\ \\<^sub>P \ \ af_letter \ \ \\<^sub>P af_letter \ \" "\ \\<^sub>P \ \ af_letter \ \ \\<^sub>P af_letter \ \" by (metis af_letter_subst subst_respects_ltl_prop_entailment)+ lemma af_prop_congruent: "\ \\<^sub>P \ \ af \ w \\<^sub>P af \ w" "\ \\<^sub>P \ \ af \ w \\<^sub>P af \ w" by (induction w arbitrary: \ \) (insert af_letter_prop_congruent, fastforce+) lemma af_letter_const_congruent: "\ \\<^sub>C \ \ af_letter \ \ \\<^sub>C af_letter \ \" by (metis af_letter_subst subst_respects_ltl_const_entailment) lemma af_const_congruent: "\ \\<^sub>C \ \ af \ w \\<^sub>C af \ w" by (induction w arbitrary: \ \) (insert af_letter_const_congruent, fastforce+) lemma af_letter_one_step_back: "{x. \ \\<^sub>P af_letter x \} \\<^sub>P \ \ \ \\<^sub>P af_letter \ \" by (induction \) simp_all subsection \Implications\ lemma af_F_prefix_prop: "af (F\<^sub>n \) w \\<^sub>P af (F\<^sub>n \) (w' @ w)" by (induction w') (simp add: ltl_prop_implies_def af_decompose(1,2))+ lemma af_G_prefix_prop: "af (G\<^sub>n \) (w' @ w) \\<^sub>P af (G\<^sub>n \) w" by (induction w') (simp add: ltl_prop_implies_def af_decompose(1,2))+ lemma af_F_prefix_lang: "w \\<^sub>n af (F\<^sub>n \) ys \ w \\<^sub>n af (F\<^sub>n \) (xs @ ys)" using af_F_prefix_prop ltl_prop_implication_implies_ltl_implication by blast lemma af_G_prefix_lang: "w \\<^sub>n af (G\<^sub>n \) (xs @ ys) \ w \\<^sub>n af (G\<^sub>n \) ys" using af_G_prefix_prop ltl_prop_implication_implies_ltl_implication by blast lemma af_F_prefix_const_equiv_true: "af (F\<^sub>n \) w \\<^sub>C true\<^sub>n \ af (F\<^sub>n \) (w' @ w) \\<^sub>C true\<^sub>n" using af_F_prefix_prop ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_true_implies_true by blast lemma af_G_prefix_const_equiv_false: "af (G\<^sub>n \) w \\<^sub>C false\<^sub>n \ af (G\<^sub>n \) (w' @ w) \\<^sub>C false\<^sub>n" using af_G_prefix_prop ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_false_implied_by_false by blast lemma af_F_prefix_lang_equiv_true: "af (F\<^sub>n \) w \\<^sub>L true\<^sub>n \ af (F\<^sub>n \) (w' @ w) \\<^sub>L true\<^sub>n" unfolding ltl_lang_equiv_def using af_F_prefix_lang by fastforce lemma af_G_prefix_lang_equiv_false: "af (G\<^sub>n \) w \\<^sub>L false\<^sub>n \ af (G\<^sub>n \) (w' @ w) \\<^sub>L false\<^sub>n" unfolding ltl_lang_equiv_def using af_G_prefix_lang by fastforce locale af_congruent = ltl_equivalence + assumes af_letter_congruent: "\ \ \ \ af_letter \ \ \ af_letter \ \" begin lemma af_congruentness: "\ \ \ \ af \ xs \ af \ xs" by (induction xs arbitrary: \ \) (insert af_letter_congruent, fastforce+) lemma af_append_congruent: "af \ w \ af \ w \ af \ (w @ w') \ af \ (w @ w')" by (simp add: af_congruentness) lemma af_append_true: "af \ w \ true\<^sub>n \ af \ (w @ w') \ true\<^sub>n" using af_congruentness by fastforce lemma af_append_false: "af \ w \ false\<^sub>n \ af \ (w @ w') \ false\<^sub>n" using af_congruentness by fastforce lemma prefix_append_subsequence: "i \ j \ (prefix i w) @ (w [i \ j]) = prefix j w" by (metis le_add_diff_inverse subsequence_append) lemma af_prefix_congruent: "i \ j \ af \ (prefix i w) \ af \ (prefix i w) \ af \ (prefix j w) \ af \ (prefix j w)" by (metis af_congruentness foldl_append prefix_append_subsequence)+ lemma af_prefix_true: "i \ j \ af \ (prefix i w) \ true\<^sub>n \ af \ (prefix j w) \ true\<^sub>n" by (metis af_append_true prefix_append_subsequence) lemma af_prefix_false: "i \ j \ af \ (prefix i w) \ false\<^sub>n \ af \ (prefix j w) \ false\<^sub>n" by (metis af_append_false prefix_append_subsequence) end interpretation lang_af_congruent: af_congruent "(\\<^sub>L)" by unfold_locales (rule af_letter_lang_congruent) interpretation prop_af_congruent: af_congruent "(\\<^sub>P)" by unfold_locales (rule af_letter_prop_congruent) interpretation const_af_congruent: af_congruent "(\\<^sub>C)" by unfold_locales (rule af_letter_const_congruent) subsection \After in @{term \LTL} and @{term \LTL}\ lemma valid_prefix_implies_ltl: "af \ (prefix i w) \\<^sub>L true\<^sub>n \ w \\<^sub>n \" proof - assume "af \ (prefix i w) \\<^sub>L true\<^sub>n" then have "suffix i w \\<^sub>n af \ (prefix i w)" unfolding ltl_lang_equiv_def using semantics_ltln.simps(1) by blast then show "w \\<^sub>n \" using af_ltl_continuation by force qed lemma ltl_implies_satisfiable_prefix: "w \\<^sub>n \ \ \ (af \ (prefix i w) \\<^sub>L false\<^sub>n)" proof - assume "w \\<^sub>n \" then have "suffix i w \\<^sub>n af \ (prefix i w)" using af_ltl_continuation by fastforce then show "\ (af \ (prefix i w) \\<^sub>L false\<^sub>n)" unfolding ltl_lang_equiv_def using semantics_ltln.simps(2) by blast qed lemma \LTL_implies_valid_prefix: "\ \ \LTL \ w \\<^sub>n \ \ \i. af \ (prefix i w) \\<^sub>C true\<^sub>n" proof (induction \ arbitrary: w) case True_ltln then show ?case using ltl_const_equiv_equivp equivp_reflp by fastforce next case (Prop_ltln x) then show ?case by (metis af_letter.simps(3) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(3) subsequence_singleton) next case (Nprop_ltln x) then show ?case by (metis af_letter.simps(4) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(4) subsequence_singleton) next case (And_ltln \1 \2) then obtain i1 i2 where "af \1 (prefix i1 w) \\<^sub>C true\<^sub>n" and "af \2 (prefix i2 w) \\<^sub>C true\<^sub>n" by fastforce then have "af \1 (prefix (i1 + i2) w) \\<^sub>C true\<^sub>n" and "af \2 (prefix (i2 + i1) w) \\<^sub>C true\<^sub>n" using const_af_congruent.af_prefix_true le_add1 by blast+ then have "af (\1 and\<^sub>n \2) (prefix (i1 + i2) w) \\<^sub>C true\<^sub>n" unfolding af_decompose by (simp add: add.commute) then show ?case by blast next case (Or_ltln \1 \2) then obtain i where "af \1 (prefix i w) \\<^sub>C true\<^sub>n \ af \2 (prefix i w) \\<^sub>C true\<^sub>n" by auto then show ?case unfolding af_decompose by auto next case (Next_ltln \) then obtain i where "af \ (prefix i (suffix 1 w)) \\<^sub>C true\<^sub>n" by fastforce then show ?case by (metis (no_types, lifting) One_nat_def add.right_neutral af_simps(3) foldl_Nil foldl_append subsequence_append subsequence_shift subsequence_singleton) next case (Until_ltln \1 \2) then obtain k where "suffix k w \\<^sub>n \2" and "\j\<^sub>n \1" by fastforce then show ?case proof (induction k arbitrary: w) case 0 then obtain i where "af \2 (prefix i w) \\<^sub>C true\<^sub>n" using Until_ltln by fastforce then have "af \2 (prefix (Suc i) w) \\<^sub>C true\<^sub>n" using const_af_congruent.af_prefix_true le_SucI by blast then have "af (\1 U\<^sub>n \2) (prefix (Suc i) w) \\<^sub>C true\<^sub>n" unfolding af_subsequence_U by simp then show ?case by blast next case (Suc k) then have "suffix k (suffix 1 w) \\<^sub>n \2" and "\j\<^sub>n \1" by (simp add: Suc.prems)+ then obtain i where i_def: "af (\1 U\<^sub>n \2) (prefix i (suffix 1 w)) \\<^sub>C true\<^sub>n" using Suc.IH by blast obtain j where "af \1 (prefix j w) \\<^sub>C true\<^sub>n" using Until_ltln Suc by fastforce then have "af \1 (prefix (Suc (j + i)) w) \\<^sub>C true\<^sub>n" using const_af_congruent.af_prefix_true le_SucI le_add1 by blast moreover from i_def have "af (\1 U\<^sub>n \2) (w [1 \ Suc (j + i)]) \\<^sub>C true\<^sub>n" by (metis One_nat_def const_af_congruent.af_prefix_true le_add2 plus_1_eq_Suc subsequence_shift) ultimately have "af (\1 U\<^sub>n \2) (prefix (Suc (j + i)) w) \\<^sub>C true\<^sub>n" unfolding af_subsequence_U by simp then show ?case by blast qed next case (StrongRelease_ltln \1 \2) then obtain k where "suffix k w \\<^sub>n \1" and "\j\k. suffix j w \\<^sub>n \2" by fastforce then show ?case proof (induction k arbitrary: w) case 0 then obtain i1 i2 where "af \1 (prefix i1 w) \\<^sub>C true\<^sub>n" and "af \2 (prefix i2 w) \\<^sub>C true\<^sub>n" using StrongRelease_ltln by fastforce then have "af \1 (prefix (Suc (i1 + i2)) w) \\<^sub>C true\<^sub>n" and "af \2 (prefix (Suc (i2 + i1)) w) \\<^sub>C true\<^sub>n" using const_af_congruent.af_prefix_true le_SucI le_add1 by blast+ then have "af (\1 M\<^sub>n \2) (prefix (Suc (i1 + i2)) w) \\<^sub>C true\<^sub>n" unfolding af_subsequence_M by (simp add: add.commute) then show ?case by blast next case (Suc k) then have "suffix k (suffix 1 w) \\<^sub>n \1" and "\j\k. suffix j (suffix 1 w) \\<^sub>n \2" by (simp add: Suc.prems)+ then obtain i where i_def: "af (\1 M\<^sub>n \2) (prefix i (suffix 1 w)) \\<^sub>C true\<^sub>n" using Suc.IH by blast obtain j where "af \2 (prefix j w) \\<^sub>C true\<^sub>n" using StrongRelease_ltln Suc by fastforce then have "af \2 (prefix (Suc (j + i)) w) \\<^sub>C true\<^sub>n" using const_af_congruent.af_prefix_true le_SucI le_add1 by blast moreover from i_def have "af (\1 M\<^sub>n \2) (w [1 \ Suc (j + i)]) \\<^sub>C true\<^sub>n" by (metis One_nat_def const_af_congruent.af_prefix_true le_add2 plus_1_eq_Suc subsequence_shift) ultimately have "af (\1 M\<^sub>n \2) (prefix (Suc (j + i)) w) \\<^sub>C true\<^sub>n" unfolding af_subsequence_M by simp then show ?case by blast qed qed force+ lemma satisfiable_prefix_implies_\LTL: "\ \ \LTL \ \i. af \ (prefix i w) \\<^sub>C false\<^sub>n \ w \\<^sub>n \" proof (erule contrapos_np, induction \ arbitrary: w) case False_ltln then show ?case using ltl_const_equiv_equivp equivp_reflp by fastforce next case (Prop_ltln x) then show ?case by (metis af_letter.simps(3) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(3) subsequence_singleton) next case (Nprop_ltln x) then show ?case by (metis af_letter.simps(4) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(4) subsequence_singleton) next case (And_ltln \1 \2) then obtain i where "af \1 (prefix i w) \\<^sub>C false\<^sub>n \ af \2 (prefix i w) \\<^sub>C false\<^sub>n" by auto then show ?case unfolding af_decompose by auto next case (Or_ltln \1 \2) then obtain i1 i2 where "af \1 (prefix i1 w) \\<^sub>C false\<^sub>n" and "af \2 (prefix i2 w) \\<^sub>C false\<^sub>n" by fastforce then have "af \1 (prefix (i1 + i2) w) \\<^sub>C false\<^sub>n" and "af \2 (prefix (i2 + i1) w) \\<^sub>C false\<^sub>n" using const_af_congruent.af_prefix_false le_add1 by blast+ then have "af (\1 or\<^sub>n \2) (prefix (i1 + i2) w) \\<^sub>C false\<^sub>n" unfolding af_decompose by (simp add: add.commute) then show ?case by blast next case (Next_ltln \) then obtain i where "af \ (prefix i (suffix 1 w)) \\<^sub>C false\<^sub>n" by fastforce then show ?case by (metis (no_types, lifting) One_nat_def add.right_neutral af_simps(3) foldl_Nil foldl_append subsequence_append subsequence_shift subsequence_singleton) next case (Release_ltln \1 \2) then obtain k where "\ suffix k w \\<^sub>n \2" and "\j suffix j w \\<^sub>n \1" by fastforce then show ?case proof (induction k arbitrary: w) case 0 then obtain i where "af \2 (prefix i w) \\<^sub>C false\<^sub>n" using Release_ltln by fastforce then have "af \2 (prefix (Suc i) w) \\<^sub>C false\<^sub>n" using const_af_congruent.af_prefix_false le_SucI by blast then have "af (\1 R\<^sub>n \2) (prefix (Suc i) w) \\<^sub>C false\<^sub>n" unfolding af_subsequence_R by simp then show ?case by blast next case (Suc k) then have "\ suffix k (suffix 1 w) \\<^sub>n \2" and "\j suffix j (suffix 1 w) \\<^sub>n \1" by (simp add: Suc.prems)+ then obtain i where i_def: "af (\1 R\<^sub>n \2) (prefix i (suffix 1 w)) \\<^sub>C false\<^sub>n" using Suc.IH by blast obtain j where "af \1 (prefix j w) \\<^sub>C false\<^sub>n" using Release_ltln Suc by fastforce then have "af \1 (prefix (Suc (j + i)) w) \\<^sub>C false\<^sub>n" using const_af_congruent.af_prefix_false le_SucI le_add1 by blast moreover from i_def have "af (\1 R\<^sub>n \2) (w [1 \ Suc (j + i)]) \\<^sub>C false\<^sub>n" by (metis One_nat_def const_af_congruent.af_prefix_false le_add2 plus_1_eq_Suc subsequence_shift) ultimately have "af (\1 R\<^sub>n \2) (prefix (Suc (j + i)) w) \\<^sub>C false\<^sub>n" unfolding af_subsequence_R by auto then show ?case by blast qed next case (WeakUntil_ltln \1 \2) then obtain k where "\ suffix k w \\<^sub>n \1" and "\j\k. \ suffix j w \\<^sub>n \2" by fastforce then show ?case proof (induction k arbitrary: w) case 0 then obtain i1 i2 where "af \1 (prefix i1 w) \\<^sub>C false\<^sub>n" and "af \2 (prefix i2 w) \\<^sub>C false\<^sub>n" using WeakUntil_ltln by fastforce then have "af \1 (prefix (Suc (i1 + i2)) w) \\<^sub>C false\<^sub>n" and "af \2 (prefix (Suc (i2 + i1)) w) \\<^sub>C false\<^sub>n" using const_af_congruent.af_prefix_false le_SucI le_add1 by blast+ then have "af (\1 W\<^sub>n \2) (prefix (Suc (i1 + i2)) w) \\<^sub>C false\<^sub>n" unfolding af_subsequence_W by (simp add: add.commute) then show ?case by blast next case (Suc k) then have "\ suffix k (suffix 1 w) \\<^sub>n \1" and "\j\k. \ suffix j (suffix 1 w) \\<^sub>n \2" by (simp add: Suc.prems)+ then obtain i where i_def: "af (\1 W\<^sub>n \2) (prefix i (suffix 1 w)) \\<^sub>C false\<^sub>n" using Suc.IH by blast obtain j where "af \2 (prefix j w) \\<^sub>C false\<^sub>n" using WeakUntil_ltln Suc by fastforce then have "af \2 (prefix (Suc (j + i)) w) \\<^sub>C false\<^sub>n" using const_af_congruent.af_prefix_false le_SucI le_add1 by blast moreover from i_def have "af (\1 W\<^sub>n \2) (w [1 \ Suc (j + i)]) \\<^sub>C false\<^sub>n" by (metis One_nat_def const_af_congruent.af_prefix_false le_add2 plus_1_eq_Suc subsequence_shift) ultimately have "af (\1 W\<^sub>n \2) (prefix (Suc (j + i)) w) \\<^sub>C false\<^sub>n" unfolding af_subsequence_W by simp then show ?case by blast qed qed force+ context ltl_equivalence begin lemma valid_prefix_implies_ltl: "af \ (prefix i w) \ true\<^sub>n \ w \\<^sub>n \" using valid_prefix_implies_ltl eq_implies_lang by blast lemma ltl_implies_satisfiable_prefix: "w \\<^sub>n \ \ \ (af \ (prefix i w) \ false\<^sub>n)" using ltl_implies_satisfiable_prefix eq_implies_lang by blast lemma \LTL_implies_valid_prefix: "\ \ \LTL \ w \\<^sub>n \ \ \i. af \ (prefix i w) \ true\<^sub>n" using \LTL_implies_valid_prefix const_implies_eq by blast lemma satisfiable_prefix_implies_\LTL: "\ \ \LTL \ \i. af \ (prefix i w) \ false\<^sub>n \ w \\<^sub>n \" using satisfiable_prefix_implies_\LTL const_implies_eq by blast lemma af_\LTL: "\ \ \LTL \ w \\<^sub>n \ \ (\i. af \ (prefix i w) \ true\<^sub>n)" using valid_prefix_implies_ltl \LTL_implies_valid_prefix by blast lemma af_\LTL: "\ \ \LTL \ w \\<^sub>n \ \ (\i. \ (af \ (prefix i w) \ false\<^sub>n))" using ltl_implies_satisfiable_prefix satisfiable_prefix_implies_\LTL by blast lemma af_\LTL_GF: "\ \ \LTL \ w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ (\i. \j. af (F\<^sub>n \) (w[i \ j]) \ true\<^sub>n)" proof - assume "\ \ \LTL" then have "F\<^sub>n \ \ \LTL" by simp have "w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ (\i. suffix i w \\<^sub>n F\<^sub>n \)" by simp also have "\ \ (\i. \j. af (F\<^sub>n \) (prefix j (suffix i w)) \ true\<^sub>n)" using af_\LTL[OF `F\<^sub>n \ \ \LTL`] by blast also have "\ \ (\i. \j. af (F\<^sub>n \) (prefix (j - i) (suffix i w)) \ true\<^sub>n)" by (metis diff_add_inverse) also have "\ \ (\i. \j. af (F\<^sub>n \) (w[i \ j]) \ true\<^sub>n)" unfolding subsequence_prefix_suffix .. finally show ?thesis by blast qed lemma af_\LTL_FG: "\ \ \LTL \ w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ (\i. \j. \ (af (G\<^sub>n \) (w[i \ j]) \ false\<^sub>n))" proof - assume "\ \ \LTL" then have "G\<^sub>n \ \ \LTL" by simp have "w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ (\i. suffix i w \\<^sub>n G\<^sub>n \)" by force also have "\ \ (\i. \j. \ (af (G\<^sub>n \) (prefix j (suffix i w)) \ false\<^sub>n))" using af_\LTL[OF `G\<^sub>n \ \ \LTL`] by blast also have "\ \ (\i. \j. \ (af (G\<^sub>n \) (prefix (j - i) (suffix i w)) \ false\<^sub>n))" by (metis diff_add_inverse) also have "\ \ (\i. \j. \ (af (G\<^sub>n \) (w[i \ j]) \ false\<^sub>n))" unfolding subsequence_prefix_suffix .. finally show ?thesis by blast qed end text \Bring Propositional Equivalence into scope\ interpretation af_congruent "(\\<^sub>P)" by unfold_locales (rule af_letter_prop_congruent) end diff --git a/thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy b/thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy --- a/thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy +++ b/thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy @@ -1,351 +1,352 @@ (* Author: Benedikt Seidl License: BSD *) section \The Master Theorem\ theory Master_Theorem imports Advice After begin subsection \Checking @{term "X \ \\ \ w"} and @{term "Y \ \\ \ w"}\ lemma X_\\_Y_\\: assumes X_\: "X \ subformulas\<^sub>\ \" and Y_\: "Y \ subformulas\<^sub>\ \" and X_GF: "\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)" and Y_FG: "\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)" shows "X \ \\ \ w \ Y \ \\ \ w" proof - \ \Custom induction rule with @{term size} as a partial order\ note induct = finite_ranking_induct[where f = size] have "finite (X \ Y)" using subformulas\<^sub>\_finite subformulas\<^sub>\_finite X_\ Y_\ finite_subset by blast+ then show ?thesis using assms proof (induction "X \ Y" arbitrary: X Y \ rule: induct) case (insert \ S) note IH = insert(3) note insert_S = `insert \ S = X \ Y` note X_\ = `X \ subformulas\<^sub>\ \` note Y_\ = `Y \ subformulas\<^sub>\ \` note X_GF = `\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)` note Y_FG = `\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)` from X_\ Y_\ have "X \ Y = {}" using subformulas\<^sub>\\<^sub>\_disjoint by fast from insert_S X_\ Y_\ have "\ \ subfrmlsn \" using subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subfrmlsn by blast show ?case proof (cases "\ \ S", cases "\ \ X") assume "\ \ S" and "\ \ X" { \ \Show @{term "X - {\} \ \\ \ w"} and @{term "Y \ \\ \ w"}\ then have "\ \ Y" using `X \ Y = {}` by auto then have "S = (X - {\}) \ Y" using insert_S `\ \ S` by fast moreover have "\\' \ Y. \'[X - {\}]\<^sub>\ = \'[X]\<^sub>\" using GF_advice_minus_size insert(1,2,4) `\ \ Y` by fast ultimately have "X - {\} \ \\ \ w" and "Y \ \\ \ w" using IH[of "X - {\}" Y \] X_\ Y_\ X_GF Y_FG by auto } moreover { \ \Show @{term "\ \ \\ \ w"}\ have "w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)" using X_GF `\ \ X` by simp then have "\\<^sub>\i. suffix i w \\<^sub>n \[Y]\<^sub>\" unfolding GF_Inf_many by simp moreover from Y_\ have "finite Y" using subformulas\<^sub>\_finite finite_subset by auto have "\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \)" using `Y \ \\ \ w` by (blast dest: \\_elim) then have "\\ \ Y. \\<^sub>\i. suffix i w \\<^sub>n G\<^sub>n \" using FG_suffix_G by blast then have "\\<^sub>\i. \\ \ Y. suffix i w \\<^sub>n G\<^sub>n \" using `finite Y` eventually_ball_finite by fast ultimately have "\\<^sub>\i. suffix i w \\<^sub>n \[Y]\<^sub>\ \ (\\ \ Y. suffix i w \\<^sub>n G\<^sub>n \)" using INFM_conjI by auto then have "\\<^sub>\i. suffix i w \\<^sub>n \" by (elim frequently_elim1) (metis FG_advice_b2_helper) then have "w \\<^sub>n G\<^sub>n (F\<^sub>n \)" unfolding GF_Inf_many by simp then have "\ \ \\ \ w" unfolding \\_semantics using `\ \ X` X_\ by auto } ultimately show ?thesis by auto next assume "\ \ S" and "\ \ X" then have "\ \ Y" using insert by fast { \ \Show @{term "X \ \\ \ w"} and @{term "Y - {\} \ \\ \ w"}\ then have "S \ X = X" using insert `\ \ X` by fast then have "S = X \ (Y - {\})" using insert_S `\ \ S` by fast moreover have "\\' \ X. \'[Y - {\}]\<^sub>\ = \'[Y]\<^sub>\" using FG_advice_minus_size insert(1,2,4) `\ \ X` by fast ultimately have "X \ \\ \ w" and "Y - {\} \ \\ \ w" using IH[of X "Y - {\}" \] X_\ Y_\ X_GF Y_FG by auto } moreover { \ \Show @{term "\ \ \\ \ w"}\ have "w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)" using Y_FG `\ \ Y` by simp then have "\\<^sub>\i. suffix i w \\<^sub>n \[X]\<^sub>\" unfolding FG_Alm_all by simp moreover have "\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \)" using `X \ \\ \ w` by (blast dest: \\_elim) then have "\\<^sub>\i. \\ \ X. suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \)" by simp ultimately have "\\<^sub>\i. suffix i w \\<^sub>n \[X]\<^sub>\ \ (\\ \ X. suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \))" using MOST_conjI by auto then have "\\<^sub>\i. suffix i w \\<^sub>n \" by (elim MOST_mono) (metis GF_advice_a2_helper) then have "w \\<^sub>n F\<^sub>n (G\<^sub>n \)" unfolding FG_Alm_all by simp then have "\ \ \\ \ w" unfolding \\_semantics using `\ \ Y` Y_\ by auto } ultimately show ?thesis by auto next assume "\ \ \ S" then have "S = X \ Y" using insert by fast then show ?thesis using insert by auto qed qed fast qed lemma \\_implies_GF: "\\ \ \\ \ w. w \\<^sub>n G\<^sub>n (F\<^sub>n \[\\ \ w]\<^sub>\)" proof safe fix \ assume "\ \ \\ \ w" then have "\\<^sub>\i. suffix i w \\<^sub>n \" using \\_elim GF_Inf_many by blast moreover have "\ \ subfrmlsn \" using `\ \ \\ \ w` \\_subfrmlsn by blast then have "\i w. \\ \ (suffix i w) \ \\ \ w" using \\_suffix \\_subset by blast ultimately have "\\<^sub>\i. suffix i w \\<^sub>n \[\\ \ w]\<^sub>\" by (elim frequently_elim1) (metis FG_advice_b1) then show "w \\<^sub>n G\<^sub>n (F\<^sub>n \[\\ \ w]\<^sub>\)" unfolding GF_Inf_many by simp qed lemma \\_implies_FG: "\\ \ \\ \ w. w \\<^sub>n F\<^sub>n (G\<^sub>n \[\\ \ w]\<^sub>\)" proof safe fix \ assume "\ \ \\ \ w" then have "\\<^sub>\i. suffix i w \\<^sub>n \" using \\_elim FG_Alm_all by blast moreover { have "\ \ subfrmlsn \" using `\ \ \\ \ w` \\_subfrmlsn by blast moreover have "\\<^sub>\i. \\ \ (suffix i w) = \ \ (suffix i w)" using suffix_\_stable unfolding \_stable_def by blast ultimately have "\\<^sub>\i. \ \ (suffix i w) \ \\ \ w" unfolding MOST_nat_le by (metis \\_subset \\_suffix) } ultimately have "\\<^sub>\i. \ \ (suffix i w) \ \\ \ w \ suffix i w \\<^sub>n \" using eventually_conj by auto then have "\\<^sub>\i. suffix i w \\<^sub>n \[\\ \ w]\<^sub>\" using GF_advice_a1 by (elim eventually_mono) auto then show "w \\<^sub>n F\<^sub>n (G\<^sub>n \[\\ \ w]\<^sub>\)" unfolding FG_Alm_all by simp qed subsection \Putting the pieces together: The Master Theorem\ theorem master_theorem_ltr: assumes "w \\<^sub>n \" obtains X and Y where "X \ subformulas\<^sub>\ \" and "Y \ subformulas\<^sub>\ \" and "\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" and "\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)" and "\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)" proof show "\\ \ w \ subformulas\<^sub>\ \" by (rule \\_subformulas\<^sub>\) next show "\\ \ w \ subformulas\<^sub>\ \" by (rule \\_subformulas\<^sub>\) next obtain i where "\\ \ (suffix i w) = \ \ (suffix i w)" using suffix_\_stable unfolding MOST_nat \_stable_def by fast then have "\ (af \ (prefix i w)) (suffix i w) \ \\ \ w" using \\_af \_af \\_suffix by fast moreover have "suffix i w \\<^sub>n af \ (prefix i w)" using af_ltl_continuation `w \\<^sub>n \` by fastforce ultimately show "\i. suffix i w \\<^sub>n af \ (prefix i w)[\\ \ w]\<^sub>\" using GF_advice_a1 by blast next show "\\ \ \\ \ w. w \\<^sub>n G\<^sub>n (F\<^sub>n \[\\ \ w]\<^sub>\)" by (rule \\_implies_GF) next show "\\ \ \\ \ w. w \\<^sub>n F\<^sub>n (G\<^sub>n \[\\ \ w]\<^sub>\)" by (rule \\_implies_FG) qed theorem master_theorem_rtl: assumes "X \ subformulas\<^sub>\ \" and "Y \ subformulas\<^sub>\ \" and 1: "\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" and 2: "\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)" and 3: "\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)" shows "w \\<^sub>n \" proof - from 1 obtain i where "suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" by blast moreover from assms have "X \ \\ \ w" using X_\\_Y_\\ by blast then have "X \ \\ \ (suffix i w)" using \\_suffix by fast ultimately have "suffix i w \\<^sub>n af \ (prefix i w)" using GF_advice_a2 \\_af by metis then show "w \\<^sub>n \" using af_ltl_continuation by force qed theorem master_theorem: "w \\<^sub>n \ \ - (\X \ subformulas\<^sub>\ \. \Y \ subformulas\<^sub>\ \. - (\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\) - \ (\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)) - \ (\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)))" + (\X \ subformulas\<^sub>\ \. + (\Y \ subformulas\<^sub>\ \. + (\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\) + \ (\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)) + \ (\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\))))" by (metis master_theorem_ltr master_theorem_rtl) subsection \The Master Theorem on Languages\ definition "L\<^sub>1 \ X = {w. \i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\}" definition "L\<^sub>2 X Y = {w. \\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)}" definition "L\<^sub>3 X Y = {w. \\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)}" corollary master_theorem_language: "language_ltln \ = \ {L\<^sub>1 \ X \ L\<^sub>2 X Y \ L\<^sub>3 X Y | X Y. X \ subformulas\<^sub>\ \ \ Y \ subformulas\<^sub>\ \}" proof safe fix w assume "w \ language_ltln \" then have "w \\<^sub>n \" unfolding language_ltln_def by simp then obtain X Y where "X \ subformulas\<^sub>\ \" and "Y \ subformulas\<^sub>\ \" and "\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" and "\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)" and "\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)" using master_theorem_ltr by metis then have "w \ L\<^sub>1 \ X" and "w \ L\<^sub>2 X Y" and "w \ L\<^sub>3 X Y" unfolding L\<^sub>1_def L\<^sub>2_def L\<^sub>3_def by simp+ then show "w \ \ {L\<^sub>1 \ X \ L\<^sub>2 X Y \ L\<^sub>3 X Y | X Y. X \ subformulas\<^sub>\ \ \ Y \ subformulas\<^sub>\ \}" using `X \ subformulas\<^sub>\ \` `Y \ subformulas\<^sub>\ \` by blast next fix w X Y assume "X \ subformulas\<^sub>\ \" and "Y \ subformulas\<^sub>\ \" and "w \ L\<^sub>1 \ X" and "w \ L\<^sub>2 X Y" and "w \ L\<^sub>3 X Y" then show "w \ language_ltln \" unfolding language_ltln_def L\<^sub>1_def L\<^sub>2_def L\<^sub>3_def using master_theorem_rtl by blast qed end diff --git a/thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy b/thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy new file mode 100644 --- /dev/null +++ b/thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy @@ -0,0 +1,558 @@ +(* + Author: Salomon Sickert + Author: Benedikt Seidl + License: BSD +*) + +section \Master Theorem with Reduced Subformulas\ + +theory Restricted_Master_Theorem +imports + Master_Theorem +begin + +subsection \Restricted Set of Subformulas\ + +fun restricted_subformulas_inner :: "'a ltln \ 'a ltln set" +where + "restricted_subformulas_inner (\ and\<^sub>n \) = restricted_subformulas_inner \ \ restricted_subformulas_inner \" +| "restricted_subformulas_inner (\ or\<^sub>n \) = restricted_subformulas_inner \ \ restricted_subformulas_inner \" +| "restricted_subformulas_inner (X\<^sub>n \) = restricted_subformulas_inner \" +| "restricted_subformulas_inner (\ U\<^sub>n \) = subformulas\<^sub>\ (\ U\<^sub>n \) \ subformulas\<^sub>\ (\ U\<^sub>n \)" +| "restricted_subformulas_inner (\ R\<^sub>n \) = restricted_subformulas_inner \ \ restricted_subformulas_inner \" +| "restricted_subformulas_inner (\ W\<^sub>n \) = restricted_subformulas_inner \ \ restricted_subformulas_inner \" +| "restricted_subformulas_inner (\ M\<^sub>n \) = subformulas\<^sub>\ (\ M\<^sub>n \) \ subformulas\<^sub>\ (\ M\<^sub>n \)" +| "restricted_subformulas_inner _ = {}" + +fun restricted_subformulas :: "'a ltln \ 'a ltln set" +where + "restricted_subformulas (\ and\<^sub>n \) = restricted_subformulas \ \ restricted_subformulas \" +| "restricted_subformulas (\ or\<^sub>n \) = restricted_subformulas \ \ restricted_subformulas \" +| "restricted_subformulas (X\<^sub>n \) = restricted_subformulas \" +| "restricted_subformulas (\ U\<^sub>n \) = restricted_subformulas \ \ restricted_subformulas \" +| "restricted_subformulas (\ R\<^sub>n \) = restricted_subformulas \ \ restricted_subformulas_inner \" +| "restricted_subformulas (\ W\<^sub>n \) = restricted_subformulas_inner \ \ restricted_subformulas \" +| "restricted_subformulas (\ M\<^sub>n \) = restricted_subformulas \ \ restricted_subformulas \" +| "restricted_subformulas _ = {}" + +lemma GF_advice_restricted_subformulas_inner: + "restricted_subformulas_inner (\[X]\<^sub>\) = {}" + by (induction \) simp_all + +lemma GF_advice_restricted_subformulas: + "restricted_subformulas (\[X]\<^sub>\) = {}" + by (induction \) (simp_all add: GF_advice_restricted_subformulas_inner) + +lemma restricted_subformulas_inner_subset: + "restricted_subformulas_inner \ \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" + by (induction \) auto + +lemma restricted_subformulas_subset': + "restricted_subformulas \ \ restricted_subformulas_inner \" + by (induction \) (insert restricted_subformulas_inner_subset, auto) + +lemma restricted_subformulas_subset: + "restricted_subformulas \ \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" + using restricted_subformulas_inner_subset restricted_subformulas_subset' by auto + +lemma restricted_subformulas_size: + "\ \ restricted_subformulas \ \ size \ < size \" +proof - + have "\\. restricted_subformulas_inner \ \ subfrmlsn \" + using restricted_subformulas_inner_subset subformulas\<^sub>\\<^sub>\_subfrmlsn by blast + + then have inner: "\\ \. \ \ restricted_subformulas_inner \ \ size \ \ size \" + using subfrmlsn_size dual_order.strict_implies_order + by blast + + show "\ \ restricted_subformulas \ \ size \ < size \" + by (induction \ arbitrary: \) (fastforce dest: inner)+ +qed + +lemma restricted_subformulas_notin: + "\ \ restricted_subformulas \" + using restricted_subformulas_size by auto + +lemma restricted_subformulas_superset: + "\ \ restricted_subformulas \ \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \ \ restricted_subformulas \" +proof - + assume "\ \ restricted_subformulas \" + + then obtain \ x where + "\ \ restricted_subformulas_inner \" and "(x R\<^sub>n \) \ subformulas\<^sub>\ \ \ (\ W\<^sub>n x) \ subformulas\<^sub>\ \ " + by (induction \) auto + + moreover + + have "\\\<^sub>1 \\<^sub>2. (\\<^sub>1 R\<^sub>n \\<^sub>2) \ subformulas\<^sub>\ \ \ restricted_subformulas_inner \\<^sub>2 \ restricted_subformulas \" + "\\\<^sub>1 \\<^sub>2. (\\<^sub>1 W\<^sub>n \\<^sub>2) \ subformulas\<^sub>\ \ \ restricted_subformulas_inner \\<^sub>1 \ restricted_subformulas \" + by (induction \) (simp_all; insert restricted_subformulas_subset', blast)+ + + moreover + + have "subformulas\<^sub>\ \ \ subformulas\<^sub>\ \ \ restricted_subformulas_inner \" + using `\ \ restricted_subformulas_inner \` + proof (induction \) + case (Until_ltln \1 \2) + then show ?case + apply (cases "\ = \1 U\<^sub>n \2") + apply auto[1] + apply simp + apply (cases "\ \ subformulas\<^sub>\ \1") + apply (meson le_supI1 le_supI2 subformulas\<^sub>\_subset subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subset_eq subset_insertI2) + apply (cases "\ \ subformulas\<^sub>\ \2") + apply (meson le_supI1 le_supI2 subformulas\<^sub>\_subset subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subset_eq subset_insertI2) + apply (cases "\ \ subformulas\<^sub>\ \1") + apply (metis (no_types, hide_lams) Un_insert_right subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subformulas\<^sub>\_subset subsetD sup.coboundedI2 sup_commute) + apply simp + by (metis (no_types, hide_lams) Un_insert_right subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subformulas\<^sub>\_subset subsetD sup.coboundedI2 sup_commute) + next + case (Release_ltln \1 \2) + then show ?case by simp blast + next + case (WeakUntil_ltln \1 \2) + then show ?case by simp blast + next + case (StrongRelease_ltln \1 \2) + then show ?case + apply (cases "\ = \1 M\<^sub>n \2") + apply auto[1] + apply simp + apply (cases "\ \ subformulas\<^sub>\ \1") + apply (meson le_supI1 le_supI2 subformulas\<^sub>\_subset subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subset_eq subset_insertI2) + apply (cases "\ \ subformulas\<^sub>\ \2") + apply (meson le_supI1 le_supI2 subformulas\<^sub>\_subset subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subset_eq subset_insertI2) + apply (cases "\ \ subformulas\<^sub>\ \1") + apply (metis (no_types, hide_lams) Un_insert_right subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subformulas\<^sub>\_subset subsetD sup.coboundedI2 sup_commute) + apply simp + by (metis (no_types, hide_lams) Un_insert_right subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subset subformulas\<^sub>\_subset subsetD sup.coboundedI2 sup_commute) + qed auto + + ultimately + + show "subformulas\<^sub>\ \ \ subformulas\<^sub>\ \ \ restricted_subformulas \" + by blast +qed + +lemma restricted_subformulas_W_\: + "subformulas\<^sub>\ \ \ restricted_subformulas (\ W\<^sub>n \)" + by (induction \) auto + +lemma restricted_subformulas_R_\: + "subformulas\<^sub>\ \ \ restricted_subformulas (\ R\<^sub>n \)" + by (induction \) auto + +lemma restrict_af_letter: + "restricted_subformulas (af_letter \ \) = restricted_subformulas \" +proof (induction \) + case (Release_ltln \1 \2) + then show ?case + using restricted_subformulas_subset' by simp blast +next + case (WeakUntil_ltln \1 \2) + then show ?case + using restricted_subformulas_subset' by simp blast +qed auto + +lemma restrict_af: + "restricted_subformulas (af \ w) = restricted_subformulas \" + by (induction w rule: rev_induct) (auto simp: restrict_af_letter) + + +subsection \Restricted Master Theorem / Lemmas\ + +lemma delay_2: + assumes "\_stable \ w" + assumes "w \\<^sub>n \" + shows "\i. suffix i w \\<^sub>n af \ (prefix i w)[{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \]\<^sub>\" + using assms +proof (induction \ arbitrary: w) + case (Prop_ltln x) + then show ?case + by (metis GF_advice.simps(10) GF_advice_af prefix_suffix) +next + case (Nprop_ltln x) + then show ?case + by (metis GF_advice.simps(11) GF_advice_af prefix_suffix) +next + case (And_ltln \1 \2) + + let ?X = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas (\1 and\<^sub>n \2)" + let ?X1 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \1" + let ?X2 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \2" + + have "?X1 \ ?X" and "?X2 \ ?X" + by auto + + moreover + + obtain i j where "suffix i w \\<^sub>n af \1 (prefix i w)[?X1]\<^sub>\" + and "suffix j w \\<^sub>n af \2 (prefix j w)[?X2]\<^sub>\" + using \_stable_subfrmlsn[OF \\_stable (\1 and\<^sub>n \2) w\] And_ltln by fastforce + + ultimately + + obtain k where "suffix k w \\<^sub>n af \1 (prefix k w)[?X]\<^sub>\" + and "suffix k w \\<^sub>n af \2 (prefix k w)[?X]\<^sub>\" + using GF_advice_sync_and GF_advice_monotone by blast + + thus ?case + unfolding af_decompose semantics_ltln.simps(5) GF_advice.simps by blast +next + case (Or_ltln \1 \2) + let ?X = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas (\1 and\<^sub>n \2)" + let ?X1 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \1" + let ?X2 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \2" + + have "?X1 \ ?X" and "?X2 \ ?X" + by auto + + moreover + + obtain i j where "suffix i w \\<^sub>n af \1 (prefix i w)[?X1]\<^sub>\ \ suffix j w \\<^sub>n af \2 (prefix j w)[?X2]\<^sub>\" + using \_stable_subfrmlsn[OF \\_stable (\1 or\<^sub>n \2) w\] Or_ltln by fastforce + + ultimately + + obtain k where "suffix k w \\<^sub>n af \1 (prefix k w)[?X]\<^sub>\ \ suffix k w \\<^sub>n af \2 (prefix k w)[?X]\<^sub>\" + using GF_advice_monotone by blast + + thus ?case + unfolding af_decompose semantics_ltln.simps(6) GF_advice.simps by auto +next + case (Next_ltln \) + then have stable: "\_stable \ (suffix 1 w)" + and suffix: "suffix 1 w \\<^sub>n \" + using \_suffix \\_\_subset \\_suffix + by (simp_all add: \_stable_def) fast + show ?case + by (metis (no_types, lifting) Next_ltln.IH[OF stable suffix, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] One_nat_def add.commute af_simps(3) foldl_Nil foldl_append restricted_subformulas.simps(3) subsequence_append subsequence_singleton) +next + case (Until_ltln \1 \2) + let ?X = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas (\1 U\<^sub>n \2)" + let ?X1 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \1" + let ?X2 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \2" + + have stable_1: "\i. \_stable \1 (suffix i w)" + and stable_2: "\i. \_stable \2 (suffix i w)" + using \_stable_subfrmlsn[OF Until_ltln.prems(1)] by (simp add: \_stable_suffix)+ + + obtain i where "\j. j < i \ suffix j w \\<^sub>n \1" and "suffix i w \\<^sub>n \2" + using Until_ltln by auto + + then have "\j. j < i \ \k. suffix (j + k) w \\<^sub>n af \1 (w [j \ k + j])[?X1]\<^sub>\" + and "\k. suffix (i + k) w \\<^sub>n af \2 (w [i \ k + i])[?X2]\<^sub>\" + using Until_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + using Until_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + by blast+ + + moreover + + have "?X1 \ ?X" + and "?X2 \ ?X" + by auto + + ultimately + + obtain k where "k \ i" + and "suffix k w \\<^sub>n af \2 (w [i \ k])[?X]\<^sub>\" + and "\j. j < i \ suffix k w \\<^sub>n af \1 (w [j \ k])[?X]\<^sub>\" + using GF_advice_sync_less[of i w \1 ?X \2] GF_advice_monotone[of _ ?X] by meson + + hence "suffix (Suc k) w \\<^sub>n af (\1 U\<^sub>n \2) (prefix (Suc k) w)[?X]\<^sub>\" + by (rule af_subsequence_U_GF_advice) + + then show ?case + by blast +next + case (WeakUntil_ltln \1 \2) + + let ?X = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas (\1 W\<^sub>n \2)" + let ?X1 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \1" + let ?X2 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \2" + + have stable_1: "\i. \_stable \1 (suffix i w)" + and stable_2: "\i. \_stable \2 (suffix i w)" + using \_stable_subfrmlsn[OF WeakUntil_ltln.prems(1)] by (simp add: \_stable_suffix)+ + + { + assume Until_ltln: "w \\<^sub>n \1 U\<^sub>n \2" + then obtain i where "\j. j < i \ suffix j w \\<^sub>n \1" and "suffix i w \\<^sub>n \2" + by auto + + then have "\j. j < i \ \k. suffix (j + k) w \\<^sub>n af \1 (w [j \ k + j])[?X1]\<^sub>\" + and "\k. suffix (i + k) w \\<^sub>n af \2 (w [i \ k + i])[?X2]\<^sub>\" + using WeakUntil_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + using WeakUntil_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + by blast+ + + moreover + + have "?X1 \ ?X" + and "?X2 \ ?X" + using restricted_subformulas_subset' by force+ + + ultimately + + obtain k where "k \ i" + and "suffix k w \\<^sub>n af \2 (w [i \ k])[?X]\<^sub>\" + and "\j. j < i \ suffix k w \\<^sub>n af \1 (w [j \ k])[?X]\<^sub>\" + using GF_advice_sync_less[of i w \1 ?X \2] GF_advice_monotone[of _ ?X] by meson + + hence "suffix (Suc k) w \\<^sub>n af (\1 W\<^sub>n \2) (prefix (Suc k) w)[?X]\<^sub>\" + by (rule af_subsequence_W_GF_advice) + hence ?case + by blast + } + moreover + { + assume Globally_ltln: "w \\<^sub>n G\<^sub>n \1" + + { + fix j + have "suffix j w \\<^sub>n \1" + using Globally_ltln by simp + then have "suffix j w \\<^sub>n \1[{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)}]\<^sub>\" + by (metis stable_1 GF_advice_a1 \\_suffix \_stable_def \\_elim mem_Collect_eq subsetI) + then have "suffix j w \\<^sub>n \1[?X]\<^sub>\" + by (metis GF_advice_inter restricted_subformulas_W_\ le_infI2) + } + + then have "w \\<^sub>n (\1 W\<^sub>n \2)[?X]\<^sub>\" + by simp + then have ?case + using GF_advice_af_2 by blast + } + ultimately + show ?case + using WeakUntil_ltln.prems(2) ltln_weak_to_strong(1) by blast +next + case (Release_ltln \1 \2) + + let ?X = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas (\1 R\<^sub>n \2)" + let ?X1 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \1" + let ?X2 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \2" + + have stable_1: "\i. \_stable \1 (suffix i w)" + and stable_2: "\i. \_stable \2 (suffix i w)" + using \_stable_subfrmlsn[OF Release_ltln.prems(1)] by (simp add: \_stable_suffix)+ + + { + assume Until_ltln: "w \\<^sub>n \1 M\<^sub>n \2" + then obtain i where "\j. j \ i \ suffix j w \\<^sub>n \2" and "suffix i w \\<^sub>n \1" + by auto + + then have "\j. j \ i \ \k. suffix (j + k) w \\<^sub>n af \2 (w [j \ k + j])[?X2]\<^sub>\" + and "\k. suffix (i + k) w \\<^sub>n af \1 (w [i \ k + i])[?X1]\<^sub>\" + using Release_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + using Release_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + by blast+ + + moreover + + have "?X1 \ ?X" + and "?X2 \ ?X" + using restricted_subformulas_subset' by force+ + + ultimately + + obtain k where "k \ i" + and "suffix k w \\<^sub>n af \1 (w [i \ k])[?X]\<^sub>\" + and "\j. j \ i \ suffix k w \\<^sub>n af \2 (w [j \ k])[?X]\<^sub>\" + using GF_advice_sync_lesseq[of i w \2 ?X \1] GF_advice_monotone[of _ ?X] by meson + + hence "suffix (Suc k) w \\<^sub>n af (\1 R\<^sub>n \2) (prefix (Suc k) w)[?X]\<^sub>\" + by (rule af_subsequence_R_GF_advice) + hence ?case + by blast + } + moreover + { + assume Globally_ltln: "w \\<^sub>n G\<^sub>n \2" + + { + fix j + have "suffix j w \\<^sub>n \2" + using Globally_ltln by simp + then have "suffix j w \\<^sub>n \2[{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)}]\<^sub>\" + by (metis stable_2 GF_advice_a1 \\_suffix \_stable_def \\_elim mem_Collect_eq subsetI) + then have "suffix j w \\<^sub>n \2[?X]\<^sub>\" + by (metis GF_advice_inter restricted_subformulas_R_\ le_infI2) + } + + then have "w \\<^sub>n (\1 R\<^sub>n \2)[?X]\<^sub>\" + by simp + then have ?case + using GF_advice_af_2 by blast + } + ultimately + show ?case + using Release_ltln.prems(2) ltln_weak_to_strong(3) by blast +next + case (StrongRelease_ltln \1 \2) + + let ?X = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas (\1 M\<^sub>n \2)" + let ?X1 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \1" + let ?X2 = "{\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)} \ restricted_subformulas \2" + + have stable_1: "\i. \_stable \1 (suffix i w)" + and stable_2: "\i. \_stable \2 (suffix i w)" + using \_stable_subfrmlsn[OF StrongRelease_ltln.prems(1)] by (simp add: \_stable_suffix)+ + + obtain i where "\j. j \ i \ suffix j w \\<^sub>n \2" and "suffix i w \\<^sub>n \1" + using StrongRelease_ltln by auto + + then have "\j. j \ i \ \k. suffix (j + k) w \\<^sub>n af \2 (w [j \ k + j])[?X2]\<^sub>\" + and "\k. suffix (i + k) w \\<^sub>n af \1 (w [i \ k + i])[?X1]\<^sub>\" + using StrongRelease_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + using StrongRelease_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] + by blast+ + + moreover + + have "?X1 \ ?X" + and "?X2 \ ?X" + by auto + + ultimately + + obtain k where "k \ i" + and "suffix k w \\<^sub>n af \1 (w [i \ k])[?X]\<^sub>\" + and "\j. j \ i \ suffix k w \\<^sub>n af \2 (w [j \ k])[?X]\<^sub>\" + using GF_advice_sync_lesseq[of i w \2 ?X \1] GF_advice_monotone[of _ ?X] by meson + + hence "suffix (Suc k) w \\<^sub>n af (\1 M\<^sub>n \2) (prefix (Suc k) w)[?X]\<^sub>\" + by (rule af_subsequence_M_GF_advice) + + then show ?case + by blast +qed simp+ + +theorem master_theorem_restricted: + "w \\<^sub>n \ \ + (\X \ subformulas\<^sub>\ \ \ restricted_subformulas \. + (\Y \ subformulas\<^sub>\ \ \ restricted_subformulas \. + (\i. (suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\) + \ (\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)) + \ (\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)))))" + (is "?lhs \ ?rhs") +proof + assume ?lhs + + obtain i where "\_stable \ (suffix i w)" + by (metis MOST_nat less_Suc_eq suffix_\_stable) + + hence stable: "\_stable (af \ (prefix i w)) (suffix i w)" + by (simp add: \_af \\_af \_stable_def) + + let ?\' = "af \ (prefix i w)" + let ?X' = "\\ \ w \ restricted_subformulas \" + let ?Y' = "\\ \ w \ restricted_subformulas \" + + have 1: "suffix i w \\<^sub>n ?\'" + using `?lhs` af_ltl_continuation by force + + have 2: "\j. af (af \ (prefix i w)) (prefix j (suffix i w)) = af \ (prefix (i + j) w)" + by (simp add: subsequence_append) + + have 3: "\\ \ w = \\ \ (suffix i w)" + using \\_af \\_suffix by blast + + have "\j. suffix (i + j) w \\<^sub>n af (?\') (prefix j (suffix i w))[?X']\<^sub>\" + using delay_2[OF stable 1] unfolding suffix_suffix 2 restrict_af 3 unfolding \\_semantics' + by (metis (no_types, lifting) GF_advice_inter_subformulas af_subformulas\<^sub>\ inf_assoc inf_commute) + + hence "\i. suffix i w \\<^sub>n af \ (prefix i w)[?X']\<^sub>\" + using 2 by auto + + moreover + + { + fix \ + have "\X. \ \ restricted_subformulas \ \ \[X \ restricted_subformulas \]\<^sub>\ = \[X]\<^sub>\" + by (metis le_supE restricted_subformulas_superset FG_advice_inter inf.coboundedI2) + hence "\ \ ?X' \ w \\<^sub>n G\<^sub>n (F\<^sub>n \[?Y']\<^sub>\)" + using \\_implies_GF by force + } + + moreover + + { + fix \ + have "\X. \ \ restricted_subformulas \ \ \[X \ restricted_subformulas \]\<^sub>\ = \[X]\<^sub>\" + by (metis le_supE restricted_subformulas_superset GF_advice_inter inf.coboundedI2) + hence "\ \ ?Y' \ w \\<^sub>n F\<^sub>n (G\<^sub>n \[?X']\<^sub>\)" + using \\_implies_FG by force + } + + moreover + + have "?X' \ subformulas\<^sub>\ \ \ restricted_subformulas \" + using \\_subformulas\<^sub>\ by blast + + moreover + + have "?Y' \ subformulas\<^sub>\ \ \ restricted_subformulas \" + using \\_subformulas\<^sub>\ by blast + + ultimately show ?rhs + by meson +qed (insert master_theorem, fast) + + +corollary master_theorem_restricted_language: + "language_ltln \ = \ {L\<^sub>1 \ X \ L\<^sub>2 X Y \ L\<^sub>3 X Y | X Y. X \ subformulas\<^sub>\ \ \ restricted_subformulas \ \ Y \ subformulas\<^sub>\ \ \ restricted_subformulas \}" +proof safe + fix w + assume "w \ language_ltln \" + + then have "w \\<^sub>n \" + unfolding language_ltln_def by simp + + then obtain X Y where + 1: "X \ subformulas\<^sub>\ \ \ restricted_subformulas \" + and 2: "Y \ subformulas\<^sub>\ \ \ restricted_subformulas \" + and "\i. suffix i w \\<^sub>n af \ (prefix i w)[X]\<^sub>\" + and "\\ \ X. w \\<^sub>n G\<^sub>n (F\<^sub>n \[Y]\<^sub>\)" + and "\\ \ Y. w \\<^sub>n F\<^sub>n (G\<^sub>n \[X]\<^sub>\)" + using master_theorem_restricted by metis + + then have "w \ L\<^sub>1 \ X" and "w \ L\<^sub>2 X Y" and "w \ L\<^sub>3 X Y" + unfolding L\<^sub>1_def L\<^sub>2_def L\<^sub>3_def by simp+ + + then show "w \ \ {L\<^sub>1 \ X \ L\<^sub>2 X Y \ L\<^sub>3 X Y | X Y. X \ subformulas\<^sub>\ \ \ restricted_subformulas \ \ Y \ subformulas\<^sub>\ \ \ restricted_subformulas \}" + using 1 2 by blast +next + fix w X Y + assume "X \ subformulas\<^sub>\ \ \ restricted_subformulas \" and "Y \ subformulas\<^sub>\ \ \ restricted_subformulas \" + and "w \ L\<^sub>1 \ X" and "w \ L\<^sub>2 X Y" and "w \ L\<^sub>3 X Y" + + then show "w \ language_ltln \" + unfolding language_ltln_def L\<^sub>1_def L\<^sub>2_def L\<^sub>3_def + using master_theorem_restricted by blast +qed + + +subsection \Definitions with Lists for Code Export\ + +definition restricted_advice_sets :: "'a ltln \ ('a ltln list \ 'a ltln list) list" +where + "restricted_advice_sets \ = List.product (subseqs (List.filter (\x. x \ restricted_subformulas \) (subformulas\<^sub>\_list \))) (subseqs (List.filter (\x. x \ restricted_subformulas \) (subformulas\<^sub>\_list \)))" + +lemma subseqs_subformulas\<^sub>\_restricted_list: + "X \ subformulas\<^sub>\ \ \ restricted_subformulas \ \ (\xs. X = set xs \ xs \ set (subseqs (List.filter (\x. x \ restricted_subformulas \) (subformulas\<^sub>\_list \))))" + by (metis in_set_subseqs inf_commute inter_set_filter subformulas\<^sub>\_list_set subset_subseq) + +lemma subseqs_subformulas\<^sub>\_restricted_list: + "Y \ subformulas\<^sub>\ \ \ restricted_subformulas \ \ (\ys. Y = set ys \ ys \ set (subseqs (List.filter (\x. x \ restricted_subformulas \) (subformulas\<^sub>\_list \))))" + by (metis in_set_subseqs inf_commute inter_set_filter subformulas\<^sub>\_list_set subset_subseq) + +lemma restricted_advice_sets_subformulas: + "X \ subformulas\<^sub>\ \ \ restricted_subformulas \ \ Y \ subformulas\<^sub>\ \ \ restricted_subformulas \ \ (\xs ys. X = set xs \ Y = set ys \ (xs, ys) \ set (restricted_advice_sets \))" + unfolding restricted_advice_sets_def set_product subseqs_subformulas\<^sub>\_restricted_list subseqs_subformulas\<^sub>\_restricted_list by blast + +lemma restricted_advice_sets_not_empty: + "restricted_advice_sets \ \ []" + unfolding restricted_advice_sets_def using subseqs_not_empty product_not_empty by blast + +end diff --git a/thys/LTL_Master_Theorem/Logical_Characterization/Syntactic_Fragments_and_Stability.thy b/thys/LTL_Master_Theorem/Logical_Characterization/Syntactic_Fragments_and_Stability.thy --- a/thys/LTL_Master_Theorem/Logical_Characterization/Syntactic_Fragments_and_Stability.thy +++ b/thys/LTL_Master_Theorem/Logical_Characterization/Syntactic_Fragments_and_Stability.thy @@ -1,516 +1,548 @@ (* Author: Benedikt Seidl License: BSD *) section \Syntactic Fragments and Stability\ theory Syntactic_Fragments_and_Stability imports LTL.LTL "HOL-Library.Sublist" begin \ \We use prefix and suffix on infinite words.\ hide_const Sublist.prefix Sublist.suffix subsection \The fragments @{term \LTL} and @{term \LTL}\ fun is_\LTL :: "'a ltln \ bool" where "is_\LTL true\<^sub>n = True" | "is_\LTL false\<^sub>n = True" | "is_\LTL prop\<^sub>n(_) = True" | "is_\LTL nprop\<^sub>n(_) = True" | "is_\LTL (\ and\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL (\ or\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL (X\<^sub>n \) = is_\LTL \" | "is_\LTL (\ U\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL (\ M\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL _ = False" fun is_\LTL :: "'a ltln \ bool" where "is_\LTL true\<^sub>n = True" | "is_\LTL false\<^sub>n = True" | "is_\LTL prop\<^sub>n(_) = True" | "is_\LTL nprop\<^sub>n(_) = True" | "is_\LTL (\ and\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL (\ or\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL (X\<^sub>n \) = is_\LTL \" | "is_\LTL (\ W\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL (\ R\<^sub>n \) = (is_\LTL \ \ is_\LTL \)" | "is_\LTL _ = False" definition \LTL :: "'a ltln set" where "\LTL = {\. is_\LTL \}" definition \LTL :: "'a ltln set" where "\LTL = {\. is_\LTL \}" lemma \LTL_simp[simp]: "\ \ \LTL \ is_\LTL \" unfolding \LTL_def by simp lemma \LTL_simp[simp]: "\ \ \LTL \ is_\LTL \" unfolding \LTL_def by simp subsubsection \Subformulas in @{term \LTL} and @{term \LTL}\ fun subformulas\<^sub>\ :: "'a ltln \ 'a ltln set" where "subformulas\<^sub>\ (\ and\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ or\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (X\<^sub>n \) = subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ U\<^sub>n \) = {\ U\<^sub>n \} \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ R\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ W\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ M\<^sub>n \) = {\ M\<^sub>n \} \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ _ = {}" fun subformulas\<^sub>\ :: "'a ltln \ 'a ltln set" where "subformulas\<^sub>\ (\ and\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ or\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (X\<^sub>n \) = subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ U\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ R\<^sub>n \) = {\ R\<^sub>n \} \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ W\<^sub>n \) = {\ W\<^sub>n \} \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ (\ M\<^sub>n \) = subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" | "subformulas\<^sub>\ _ = {}" -abbreviation "ltln_U \ {\ U\<^sub>n \ | \ \. True}" -abbreviation "ltln_R \ {\ R\<^sub>n \ | \ \. True}" -abbreviation "ltln_W \ {\ W\<^sub>n \ | \ \. True}" -abbreviation "ltln_M \ {\ M\<^sub>n \ | \ \. True}" - lemma subformulas\<^sub>\_semantics: - "subformulas\<^sub>\ \ = subfrmlsn \ \ (ltln_U \ ltln_M)" + "subformulas\<^sub>\ \ = {\ \ subfrmlsn \. \\\<^sub>1 \\<^sub>2. \ = \\<^sub>1 U\<^sub>n \\<^sub>2 \ \ = \\<^sub>1 M\<^sub>n \\<^sub>2}" by (induction \) auto lemma subformulas\<^sub>\_semantics: - "subformulas\<^sub>\ \ = subfrmlsn \ \ (ltln_R \ ltln_W)" + "subformulas\<^sub>\ \ = {\ \ subfrmlsn \. \\\<^sub>1 \\<^sub>2. \ = \\<^sub>1 R\<^sub>n \\<^sub>2 \ \ = \\<^sub>1 W\<^sub>n \\<^sub>2}" by (induction \) auto lemma subformulas\<^sub>\_subfrmlsn: "subformulas\<^sub>\ \ \ subfrmlsn \" by (induction \) auto lemma subformulas\<^sub>\_subfrmlsn: "subformulas\<^sub>\ \ \ subfrmlsn \" by (induction \) auto lemma subformulas\<^sub>\_finite: "finite (subformulas\<^sub>\ \)" by (induction \) auto lemma subformulas\<^sub>\_finite: "finite (subformulas\<^sub>\ \)" by (induction \) auto lemma subformulas\<^sub>\_subset: "\ \ subfrmlsn \ \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" by (induction \) auto lemma subformulas\<^sub>\_subset: "\ \ subfrmlsn \ \ subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" by (induction \) auto lemma subfrmlsn_\LTL: "\ \ \LTL \ subfrmlsn \ \ \LTL" by (induction \) auto lemma subfrmlsn_\LTL: "\ \ \LTL \ subfrmlsn \ \ \LTL" by (induction \) auto lemma subformulas\<^sub>\\<^sub>\_disjoint: "subformulas\<^sub>\ \ \ subformulas\<^sub>\ \ = {}" unfolding subformulas\<^sub>\_semantics subformulas\<^sub>\_semantics by fastforce lemma subformulas\<^sub>\\<^sub>\_subfrmlsn: "subformulas\<^sub>\ \ \ subformulas\<^sub>\ \ \ subfrmlsn \" using subformulas\<^sub>\_subfrmlsn subformulas\<^sub>\_subfrmlsn by blast lemma subformulas\<^sub>\\<^sub>\_card: "card (subformulas\<^sub>\ \ \ subformulas\<^sub>\ \) = card (subformulas\<^sub>\ \) + card (subformulas\<^sub>\ \)" by (simp add: subformulas\<^sub>\\<^sub>\_disjoint subformulas\<^sub>\_finite subformulas\<^sub>\_finite card_Un_disjoint) -text \The $\mu$- and $\nu$-subformulas as lists:\ - -fun subformulas\<^sub>\_list :: "'a ltln \ 'a ltln list" -where - "subformulas\<^sub>\_list (\ and\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list (\ or\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list (X\<^sub>n \) = subformulas\<^sub>\_list \" -| "subformulas\<^sub>\_list (\ U\<^sub>n \) = List.insert (\ U\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" -| "subformulas\<^sub>\_list (\ R\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list (\ W\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list (\ M\<^sub>n \) = List.insert (\ M\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" -| "subformulas\<^sub>\_list _ = []" - -fun subformulas\<^sub>\_list :: "'a ltln \ 'a ltln list" -where - "subformulas\<^sub>\_list (\ and\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list (\ or\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list (X\<^sub>n \) = subformulas\<^sub>\_list \" -| "subformulas\<^sub>\_list (\ U\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list (\ R\<^sub>n \) = List.insert (\ R\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" -| "subformulas\<^sub>\_list (\ W\<^sub>n \) = List.insert (\ W\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" -| "subformulas\<^sub>\_list (\ M\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" -| "subformulas\<^sub>\_list _ = []" - -lemma subformulas\<^sub>\_list_set: - "set (subformulas\<^sub>\_list \) = subformulas\<^sub>\ \" - by (induction \) auto - -lemma subformulas\<^sub>\_list_set: - "set (subformulas\<^sub>\_list \) = subformulas\<^sub>\ \" - by (induction \) auto - -lemma subformulas\<^sub>\_list_distinct: - "distinct (subformulas\<^sub>\_list \)" - by (induction \) auto - -lemma subformulas\<^sub>\_list_distinct: - "distinct (subformulas\<^sub>\_list \)" - by (induction \) auto - -lemma subformulas\<^sub>\_list_length: - "length (subformulas\<^sub>\_list \) = card (subformulas\<^sub>\ \)" - by (metis subformulas\<^sub>\_list_set subformulas\<^sub>\_list_distinct distinct_card) - -lemma subformulas\<^sub>\_list_length: - "length (subformulas\<^sub>\_list \) = card (subformulas\<^sub>\ \)" - by (metis subformulas\<^sub>\_list_set subformulas\<^sub>\_list_distinct distinct_card) - - - -subsection \List of Advice Sets\ - -definition advice_sets :: "'a ltln \ ('a ltln list \ 'a ltln list) list" -where - "advice_sets \ = List.product (subseqs (subformulas\<^sub>\_list \)) (subseqs (subformulas\<^sub>\_list \))" - -lemma subset_subseq: - "X \ set ys \ (\xs. X = set xs \ subseq xs ys)" - by (metis (no_types, lifting) Pow_iff image_iff in_set_subseqs subseqs_powset) - -lemma subseqs_subformulas\<^sub>\_list: - "X \ subformulas\<^sub>\ \ \ (\xs. X = set xs \ xs \ set (subseqs (subformulas\<^sub>\_list \)))" - by (metis subset_subseq subformulas\<^sub>\_list_set in_set_subseqs) - -lemma subseqs_subformulas\<^sub>\_list: - "Y \ subformulas\<^sub>\ \ \ (\ys. Y = set ys \ ys \ set (subseqs (subformulas\<^sub>\_list \)))" - by (metis subset_subseq subformulas\<^sub>\_list_set in_set_subseqs) - -lemma advice_sets_subformulas: - "X \ subformulas\<^sub>\ \ \ Y \ subformulas\<^sub>\ \ \ (\xs ys. X = set xs \ Y = set ys \ (xs, ys) \ set (advice_sets \))" - unfolding advice_sets_def set_product subseqs_subformulas\<^sub>\_list subseqs_subformulas\<^sub>\_list by blast - -(* TODO add to HOL/List.thy *) -lemma subseqs_not_empty: - "subseqs xs \ []" - by (metis empty_iff list.set(1) subseqs_refl) - -(* TODO add to HOL/List.thy *) -lemma product_not_empty: - "xs \ [] \ ys \ [] \ List.product xs ys \ []" - by (induction xs) simp_all - -lemma advice_sets_not_empty: - "advice_sets \ \ []" - unfolding advice_sets_def using subseqs_not_empty product_not_empty by blast - -lemma advice_sets_length: - "length (advice_sets \) \ 2 ^ card (subfrmlsn \)" - unfolding advice_sets_def length_product length_subseqs subformulas\<^sub>\_list_length subformulas\<^sub>\_list_length power_add[symmetric] - by (metis Suc_1 card_mono lessI power_increasing_iff subformulas\<^sub>\\<^sub>\_card subformulas\<^sub>\\<^sub>\_subfrmlsn subfrmlsn_finite) - -lemma advice_sets_element_length: - "(xs, ys) \ set (advice_sets \) \ length xs \ card (subfrmlsn \)" - "(xs, ys) \ set (advice_sets \) \ length ys \ card (subfrmlsn \)" - unfolding advice_sets_def set_product - by (metis SigmaD1 card_mono in_set_subseqs list_emb_length order_trans subformulas\<^sub>\_list_length subformulas\<^sub>\_subfrmlsn subfrmlsn_finite) - (metis SigmaD2 card_mono in_set_subseqs list_emb_length order_trans subformulas\<^sub>\_list_length subformulas\<^sub>\_subfrmlsn subfrmlsn_finite) - -lemma advice_sets_element_subfrmlsn: - "(xs, ys) \ set (advice_sets \) \ set xs \ subformulas\<^sub>\ \" - "(xs, ys) \ set (advice_sets \) \ set ys \ subformulas\<^sub>\ \" - unfolding advice_sets_def set_product - by (meson SigmaD1 subseqs_subformulas\<^sub>\_list) - (meson SigmaD2 subseqs_subformulas\<^sub>\_list) - - - subsection \Stability\ definition "GF_singleton w \ \ if w \\<^sub>n G\<^sub>n (F\<^sub>n \) then {\} else {}" definition "F_singleton w \ \ if w \\<^sub>n F\<^sub>n \ then {\} else {}" declare GF_singleton_def [simp] F_singleton_def [simp] fun \\ :: "'a ltln \ 'a set word \ 'a ltln set" where "\\ (\ and\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ (\ or\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ (X\<^sub>n \) w = \\ \ w" | "\\ (\ U\<^sub>n \) w = GF_singleton w (\ U\<^sub>n \) \ \\ \ w \ \\ \ w" | "\\ (\ R\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ (\ W\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ (\ M\<^sub>n \) w = GF_singleton w (\ M\<^sub>n \) \ \\ \ w \ \\ \ w" | "\\ _ _ = {}" fun \ :: "'a ltln \ 'a set word \ 'a ltln set" where "\ (\ and\<^sub>n \) w = \ \ w \ \ \ w" | "\ (\ or\<^sub>n \) w = \ \ w \ \ \ w" | "\ (X\<^sub>n \) w = \ \ w" | "\ (\ U\<^sub>n \) w = F_singleton w (\ U\<^sub>n \) \ \ \ w \ \ \ w" | "\ (\ R\<^sub>n \) w = \ \ w \ \ \ w" | "\ (\ W\<^sub>n \) w = \ \ w \ \ \ w" | "\ (\ M\<^sub>n \) w = F_singleton w (\ M\<^sub>n \) \ \ \ w \ \ \ w" | "\ _ _ = {}" lemma \\_semantics: "\\ \ w = {\. \ \ subformulas\<^sub>\ \ \ w \\<^sub>n G\<^sub>n (F\<^sub>n \)}" by (induction \) force+ lemma \_semantics: "\ \ w = {\. \ \ subformulas\<^sub>\ \ \ w \\<^sub>n F\<^sub>n \}" by (induction \) force+ lemma \\_semantics': "\\ \ w = subformulas\<^sub>\ \ \ {\. w \\<^sub>n G\<^sub>n (F\<^sub>n \)}" unfolding \\_semantics by auto lemma \_semantics': "\ \ w = subformulas\<^sub>\ \ \ {\. w \\<^sub>n F\<^sub>n \}" unfolding \_semantics by auto lemma \\_\_subset: "\\ \ w \ \ \ w" unfolding \\_semantics \_semantics by force lemma \\_finite: "finite (\\ \ w)" by (induction \) auto lemma \\_subformulas\<^sub>\: "\\ \ w \ subformulas\<^sub>\ \" unfolding \\_semantics by force lemma \\_subfrmlsn: "\\ \ w \ subfrmlsn \" using \\_subformulas\<^sub>\ subformulas\<^sub>\_subfrmlsn by blast lemma \\_elim: "\ \ \\ \ w \ w \\<^sub>n G\<^sub>n (F\<^sub>n \)" unfolding \\_semantics by simp lemma \\_suffix(* [simp] *): "\\ \ (suffix i w) = \\ \ w" proof show "\\ \ w \ \\ \ (suffix i w)" unfolding \\_semantics by auto next show "\\ \ (suffix i w) \ \\ \ w" unfolding \\_semantics GF_Inf_many proof auto fix \ assume "\\<^sub>\j. suffix (i + j) w \\<^sub>n \" then have "\\<^sub>\j. suffix (j + i) w \\<^sub>n \" by (simp add: algebra_simps) then show "\\<^sub>\j. suffix j w \\<^sub>n \" using INFM_nat_add by blast qed qed lemma \\_subset: "\ \ subfrmlsn \ \ \\ \ w \ \\ \ w" unfolding \\_semantics using subformulas\<^sub>\_subset by blast lemma \_finite: "finite (\ \ w)" by (induction \) auto lemma \_subformulas\<^sub>\: "\ \ w \ subformulas\<^sub>\ \" unfolding \_semantics by force lemma \_subfrmlsn: "\ \ w \ subfrmlsn \" using \_subformulas\<^sub>\ subformulas\<^sub>\_subfrmlsn by blast lemma \_elim: "\ \ \ \ w \ w \\<^sub>n F\<^sub>n \" unfolding \_semantics by simp lemma \_suffix: "\ \ (suffix i w) \ \ \ w" unfolding \_semantics by auto lemma \_subset: "\ \ subfrmlsn \ \ \ \ w \ \ \ w" unfolding \_semantics using subformulas\<^sub>\_subset by blast definition "\_stable \ w \ \\ \ w = \ \ w" lemma suffix_\_stable: "\\<^sub>\i. \_stable \ (suffix i w)" proof - have "\\ \ subformulas\<^sub>\ \. \\<^sub>\i. suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ suffix i w \\<^sub>n F\<^sub>n \" using Alm_all_GF_F by blast then have "\\<^sub>\i. \\ \ subformulas\<^sub>\ \. suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \) \ suffix i w \\<^sub>n F\<^sub>n \" using subformulas\<^sub>\_finite eventually_ball_finite by fast then have "\\<^sub>\i. {\ \ subformulas\<^sub>\ \. suffix i w \\<^sub>n G\<^sub>n (F\<^sub>n \)} = {\ \ subformulas\<^sub>\ \. suffix i w \\<^sub>n F\<^sub>n \}" by (rule MOST_mono) (blast intro: Collect_cong) then show ?thesis unfolding \_stable_def \\_semantics \_semantics by (rule MOST_mono) simp qed +lemma \_stable_subfrmlsn: + "\_stable \ w \ \ \ subfrmlsn \ \ \_stable \ w" +proof - + assume a1: "\ \ subfrmlsn \" and a2: "\_stable \ w" + have "subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" + using a1 by (simp add: subformulas\<^sub>\_subset) + moreover + have "\\ \ w = \ \ w" + using a2 by (meson \_stable_def) + ultimately show ?thesis + by (metis (no_types) Un_commute \_semantics' \\_semantics' \_stable_def inf_left_commute inf_sup_absorb sup.orderE) +qed + +lemma \_stable_suffix: + "\_stable \ w \ \_stable \ (suffix i w)" + by (metis \_suffix \\_\_subset \\_suffix \_stable_def subset_antisym) + definition "FG_singleton w \ \ if w \\<^sub>n F\<^sub>n (G\<^sub>n \) then {\} else {}" definition "G_singleton w \ \ if w \\<^sub>n G\<^sub>n \ then {\} else {}" declare FG_singleton_def [simp] G_singleton_def [simp] fun \\ :: "'a ltln \ 'a set word \ 'a ltln set" where "\\ (\ and\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ (\ or\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ (X\<^sub>n \) w = \\ \ w" | "\\ (\ U\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ (\ R\<^sub>n \) w = FG_singleton w (\ R\<^sub>n \) \ \\ \ w \ \\ \ w" | "\\ (\ W\<^sub>n \) w = FG_singleton w (\ W\<^sub>n \) \ \\ \ w \ \\ \ w" | "\\ (\ M\<^sub>n \) w = \\ \ w \ \\ \ w" | "\\ _ _ = {}" fun \ :: "'a ltln \ 'a set word \ 'a ltln set" where "\ (\ and\<^sub>n \) w = \ \ w \ \ \ w" | "\ (\ or\<^sub>n \) w = \ \ w \ \ \ w" | "\ (X\<^sub>n \) w = \ \ w" | "\ (\ U\<^sub>n \) w = \ \ w \ \ \ w" | "\ (\ R\<^sub>n \) w = G_singleton w (\ R\<^sub>n \) \ \ \ w \ \ \ w" | "\ (\ W\<^sub>n \) w = G_singleton w (\ W\<^sub>n \) \ \ \ w \ \ \ w" | "\ (\ M\<^sub>n \) w = \ \ w \ \ \ w" | "\ _ _ = {}" lemma \\_semantics: "\\ \ w = {\ \ subformulas\<^sub>\ \. w \\<^sub>n F\<^sub>n (G\<^sub>n \)}" by (induction \) force+ lemma \_semantics: "\ \ w \ {\ \ subformulas\<^sub>\ \. w \\<^sub>n G\<^sub>n \}" by (induction \) force+ lemma \\_semantics': "\\ \ w = subformulas\<^sub>\ \ \ {\. w \\<^sub>n F\<^sub>n (G\<^sub>n \)}" unfolding \\_semantics by auto lemma \_semantics': "\ \ w = subformulas\<^sub>\ \ \ {\. w \\<^sub>n G\<^sub>n \}" unfolding \_semantics by auto lemma \_\\_subset: "\ \ w \ \\ \ w" unfolding \_semantics \\_semantics by force lemma \\_finite: "finite (\\ \ w)" by (induction \) auto lemma \\_subformulas\<^sub>\: "\\ \ w \ subformulas\<^sub>\ \" unfolding \\_semantics by force lemma \\_subfrmlsn: "\\ \ w \ subfrmlsn \" using \\_subformulas\<^sub>\ subformulas\<^sub>\_subfrmlsn by blast lemma \\_elim: "\ \ \\ \ w \ w \\<^sub>n F\<^sub>n (G\<^sub>n \)" unfolding \\_semantics by simp lemma \\_suffix: "\\ \ (suffix i w) = \\ \ w" proof show "\\ \ (suffix i w) \ \\ \ w" unfolding \\_semantics by auto next show "\\ \ w \ \\ \ (suffix i w)" unfolding \\_semantics FG_Alm_all proof auto fix \ assume "\\<^sub>\j. suffix j w \\<^sub>n \" then have "\\<^sub>\j. suffix (j + i) w \\<^sub>n \" using MOST_nat_add by meson then show "\\<^sub>\j. suffix (i + j) w \\<^sub>n \" by (simp add: algebra_simps) qed qed lemma \\_subset: "\ \ subfrmlsn \ \ \\ \ w \ \\ \ w" unfolding \\_semantics using subformulas\<^sub>\_subset by blast lemma \_finite: "finite (\ \ w)" by (induction \) auto lemma \_subformulas\<^sub>\: "\ \ w \ subformulas\<^sub>\ \" unfolding \_semantics by force lemma \_subfrmlsn: "\ \ w \ subfrmlsn \" using \_subformulas\<^sub>\ subformulas\<^sub>\_subfrmlsn by blast lemma \_elim: "\ \ \ \ w \ w \\<^sub>n G\<^sub>n \" unfolding \_semantics by simp lemma \_suffix: "\ \ w \ \ \ (suffix i w)" unfolding \_semantics by auto lemma \_subset: "\ \ subfrmlsn \ \ \ \ w \ \ \ w" unfolding \_semantics using subformulas\<^sub>\_subset by blast definition "\_stable \ w \ \\ \ w = \ \ w" lemma suffix_\_stable: "\\<^sub>\j. \_stable \ (suffix j w)" proof - have "\\ \ subformulas\<^sub>\ \. \\<^sub>\i. suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ suffix i w \\<^sub>n G\<^sub>n \" using Alm_all_FG_G by blast then have "\\<^sub>\i. \\ \ subformulas\<^sub>\ \. suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \) \ suffix i w \\<^sub>n G\<^sub>n \" using subformulas\<^sub>\_finite eventually_ball_finite by fast then have "\\<^sub>\i. {\ \ subformulas\<^sub>\ \. suffix i w \\<^sub>n F\<^sub>n (G\<^sub>n \)} = {\ \ subformulas\<^sub>\ \. suffix i w \\<^sub>n G\<^sub>n \}" by (rule MOST_mono) (blast intro: Collect_cong) then show ?thesis unfolding \_stable_def \\_semantics \_semantics by (rule MOST_mono) simp qed +lemma \_stable_subfrmlsn: + "\_stable \ w \ \ \ subfrmlsn \ \ \_stable \ w" +proof - + assume a1: "\ \ subfrmlsn \" and a2: "\_stable \ w" + have "subformulas\<^sub>\ \ \ subformulas\<^sub>\ \" + using a1 by (simp add: subformulas\<^sub>\_subset) + moreover + have "\\ \ w = \ \ w" + using a2 by (meson \_stable_def) + ultimately show ?thesis + by (metis (no_types) Un_commute \_semantics' \\_semantics' \_stable_def inf_left_commute inf_sup_absorb sup.orderE) +qed + +lemma \_stable_suffix: + "\_stable \ w \ \_stable \ (suffix i w)" + by (metis \\_suffix \_\\_subset \_suffix \_stable_def antisym_conv) + + +subsection \Definitions with Lists for Code Export\ + +text \The \\\- and \\\-subformulas as lists:\ + +fun subformulas\<^sub>\_list :: "'a ltln \ 'a ltln list" +where + "subformulas\<^sub>\_list (\ and\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list (\ or\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list (X\<^sub>n \) = subformulas\<^sub>\_list \" +| "subformulas\<^sub>\_list (\ U\<^sub>n \) = List.insert (\ U\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" +| "subformulas\<^sub>\_list (\ R\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list (\ W\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list (\ M\<^sub>n \) = List.insert (\ M\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" +| "subformulas\<^sub>\_list _ = []" + +fun subformulas\<^sub>\_list :: "'a ltln \ 'a ltln list" +where + "subformulas\<^sub>\_list (\ and\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list (\ or\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list (X\<^sub>n \) = subformulas\<^sub>\_list \" +| "subformulas\<^sub>\_list (\ U\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list (\ R\<^sub>n \) = List.insert (\ R\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" +| "subformulas\<^sub>\_list (\ W\<^sub>n \) = List.insert (\ W\<^sub>n \) (List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \))" +| "subformulas\<^sub>\_list (\ M\<^sub>n \) = List.union (subformulas\<^sub>\_list \) (subformulas\<^sub>\_list \)" +| "subformulas\<^sub>\_list _ = []" + +lemma subformulas\<^sub>\_list_set: + "set (subformulas\<^sub>\_list \) = subformulas\<^sub>\ \" + by (induction \) auto + +lemma subformulas\<^sub>\_list_set: + "set (subformulas\<^sub>\_list \) = subformulas\<^sub>\ \" + by (induction \) auto + +lemma subformulas\<^sub>\_list_distinct: + "distinct (subformulas\<^sub>\_list \)" + by (induction \) auto + +lemma subformulas\<^sub>\_list_distinct: + "distinct (subformulas\<^sub>\_list \)" + by (induction \) auto + +lemma subformulas\<^sub>\_list_length: + "length (subformulas\<^sub>\_list \) = card (subformulas\<^sub>\ \)" + by (metis subformulas\<^sub>\_list_set subformulas\<^sub>\_list_distinct distinct_card) + +lemma subformulas\<^sub>\_list_length: + "length (subformulas\<^sub>\_list \) = card (subformulas\<^sub>\ \)" + by (metis subformulas\<^sub>\_list_set subformulas\<^sub>\_list_distinct distinct_card) + + +text \ + We define the list of advice sets as the product of all subsequences + of the \\\- and \\\-subformulas of a formula. +\ + +definition advice_sets :: "'a ltln \ ('a ltln list \ 'a ltln list) list" +where + "advice_sets \ = List.product (subseqs (subformulas\<^sub>\_list \)) (subseqs (subformulas\<^sub>\_list \))" + +lemma subset_subseq: + "X \ set ys \ (\xs. X = set xs \ subseq xs ys)" + by (metis (no_types, lifting) Pow_iff image_iff in_set_subseqs subseqs_powset) + +lemma subseqs_subformulas\<^sub>\_list: + "X \ subformulas\<^sub>\ \ \ (\xs. X = set xs \ xs \ set (subseqs (subformulas\<^sub>\_list \)))" + by (metis subset_subseq subformulas\<^sub>\_list_set in_set_subseqs) + +lemma subseqs_subformulas\<^sub>\_list: + "Y \ subformulas\<^sub>\ \ \ (\ys. Y = set ys \ ys \ set (subseqs (subformulas\<^sub>\_list \)))" + by (metis subset_subseq subformulas\<^sub>\_list_set in_set_subseqs) + +lemma advice_sets_subformulas: + "X \ subformulas\<^sub>\ \ \ Y \ subformulas\<^sub>\ \ \ (\xs ys. X = set xs \ Y = set ys \ (xs, ys) \ set (advice_sets \))" + unfolding advice_sets_def set_product subseqs_subformulas\<^sub>\_list subseqs_subformulas\<^sub>\_list by blast + +(* TODO add to HOL/List.thy *) +lemma subseqs_not_empty: + "subseqs xs \ []" + by (metis empty_iff list.set(1) subseqs_refl) + +(* TODO add to HOL/List.thy *) +lemma product_not_empty: + "xs \ [] \ ys \ [] \ List.product xs ys \ []" + by (induction xs) simp_all + +lemma advice_sets_not_empty: + "advice_sets \ \ []" + unfolding advice_sets_def using subseqs_not_empty product_not_empty by blast + +lemma advice_sets_length: + "length (advice_sets \) \ 2 ^ card (subfrmlsn \)" + unfolding advice_sets_def length_product length_subseqs subformulas\<^sub>\_list_length subformulas\<^sub>\_list_length power_add[symmetric] + by (metis Suc_1 card_mono lessI power_increasing_iff subformulas\<^sub>\\<^sub>\_card subformulas\<^sub>\\<^sub>\_subfrmlsn subfrmlsn_finite) + +lemma advice_sets_element_length: + "(xs, ys) \ set (advice_sets \) \ length xs \ card (subfrmlsn \)" + "(xs, ys) \ set (advice_sets \) \ length ys \ card (subfrmlsn \)" + unfolding advice_sets_def set_product + by (metis SigmaD1 card_mono in_set_subseqs list_emb_length order_trans subformulas\<^sub>\_list_length subformulas\<^sub>\_subfrmlsn subfrmlsn_finite) + (metis SigmaD2 card_mono in_set_subseqs list_emb_length order_trans subformulas\<^sub>\_list_length subformulas\<^sub>\_subfrmlsn subfrmlsn_finite) + +lemma advice_sets_element_subfrmlsn: + "(xs, ys) \ set (advice_sets \) \ set xs \ subformulas\<^sub>\ \" + "(xs, ys) \ set (advice_sets \) \ set ys \ subformulas\<^sub>\ \" + unfolding advice_sets_def set_product + by (meson SigmaD1 subseqs_subformulas\<^sub>\_list) + (meson SigmaD2 subseqs_subformulas\<^sub>\_list) + end diff --git a/thys/LTL_Master_Theorem/ROOT b/thys/LTL_Master_Theorem/ROOT --- a/thys/LTL_Master_Theorem/ROOT +++ b/thys/LTL_Master_Theorem/ROOT @@ -1,24 +1,25 @@ chapter AFP session LTL_Master_Theorem (AFP) = "Transition_Systems_and_Automata" + options [timeout = 600] sessions LTL Deriving directories "Logical_Characterization" "LTL_to_DRA" theories "Logical_Characterization/Master_Theorem" "Logical_Characterization/Asymmetric_Master_Theorem" + "Logical_Characterization/Restricted_Master_Theorem" "LTL_to_DRA/DRA_Construction" "LTL_to_DRA/DRA_Instantiation" "LTL_to_DRA/DRA_Implementation" Code_Export document_files "root.tex" "root.bib" export_files (in ".") [1] "LTL_Master_Theorem.Code_Export:**"