equal
deleted
inserted
replaced
48 definition validTE :: "('a, 's) ioa_temp \<Rightarrow> bool" |
48 definition validTE :: "('a, 's) ioa_temp \<Rightarrow> bool" |
49 where "validTE P \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P))" |
49 where "validTE P \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P))" |
50 |
50 |
51 definition validIOA :: "('a, 's) ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" |
51 definition validIOA :: "('a, 's) ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" |
52 where "validIOA A P \<longleftrightarrow> (\<forall>ex \<in> executions A. (ex \<TTurnstile> P))" |
52 where "validIOA A P \<longleftrightarrow> (\<forall>ex \<in> executions A. (ex \<TTurnstile> P))" |
|
53 |
|
54 |
|
55 lemma IMPLIES_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<longrightarrow> (ex \<TTurnstile> Q))" |
|
56 by (simp add: IMPLIES_def temp_sat_def satisfies_def) |
|
57 |
|
58 lemma AND_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<and> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<and> (ex \<TTurnstile> Q))" |
|
59 by (simp add: AND_def temp_sat_def satisfies_def) |
|
60 |
|
61 lemma OR_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<or> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<or> (ex \<TTurnstile> Q))" |
|
62 by (simp add: OR_def temp_sat_def satisfies_def) |
|
63 |
|
64 lemma NOT_temp_sat [simp]: "(ex \<TTurnstile> \<^bold>\<not> P) \<longleftrightarrow> (\<not> (ex \<TTurnstile> P))" |
|
65 by (simp add: NOT_def temp_sat_def satisfies_def) |
53 |
66 |
54 |
67 |
55 axiomatization |
68 axiomatization |
56 where mkfin_UU [simp]: "mkfin UU = nil" |
69 where mkfin_UU [simp]: "mkfin UU = nil" |
57 and mkfin_nil [simp]: "mkfin nil = nil" |
70 and mkfin_nil [simp]: "mkfin nil = nil" |