equal
deleted
inserted
replaced
119 done |
119 done |
120 |
120 |
121 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |
121 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |
122 |
122 |
123 lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))" |
123 lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))" |
124 supply split_if [split del] |
124 supply if_split [split del] |
125 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def) |
125 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def) |
126 apply auto |
126 apply auto |
127 text \<open>\<open>\<box>F \<^bold>\<longrightarrow> F\<close>\<close> |
127 text \<open>\<open>\<box>F \<^bold>\<longrightarrow> F\<close>\<close> |
128 apply (erule_tac x = "s" in allE) |
128 apply (erule_tac x = "s" in allE) |
129 apply (simp add: tsuffix_def suffix_refl) |
129 apply (simp add: tsuffix_def suffix_refl) |
130 text \<open>\<open>\<box>F \<^bold>\<longrightarrow> Next \<box>F\<close>\<close> |
130 text \<open>\<open>\<box>F \<^bold>\<longrightarrow> Next \<box>F\<close>\<close> |
131 apply (simp split add: split_if) |
131 apply (simp split add: if_split) |
132 apply auto |
132 apply auto |
133 apply (drule tsuffix_TL2) |
133 apply (drule tsuffix_TL2) |
134 apply assumption+ |
134 apply assumption+ |
135 apply auto |
135 apply auto |
136 done |
136 done |