equal
deleted
inserted
replaced
1 (* Title: HOL/HOLCF/IOA/meta_theory/TL.thy |
1 (* Title: HOL/HOLCF/IOA/meta_theory/TL.thy |
2 Author: Olaf Müller |
2 Author: Olaf Müller |
3 *) |
3 *) |
4 |
4 |
5 section {* A General Temporal Logic *} |
5 section \<open>A General Temporal Logic\<close> |
6 |
6 |
7 theory TL |
7 theory TL |
8 imports Pred Sequence |
8 imports Pred Sequence |
9 begin |
9 begin |
10 |
10 |
145 |
145 |
146 lemma tsuffix_TL [rule_format (no_asm)]: |
146 lemma tsuffix_TL [rule_format (no_asm)]: |
147 "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s" |
147 "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s" |
148 apply (unfold tsuffix_def suffix_def) |
148 apply (unfold tsuffix_def suffix_def) |
149 apply auto |
149 apply auto |
150 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
150 apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>) |
151 apply (rule_tac x = "a\<leadsto>s1" in exI) |
151 apply (rule_tac x = "a\<leadsto>s1" in exI) |
152 apply auto |
152 apply auto |
153 done |
153 done |
154 |
154 |
155 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |
155 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |