equal
deleted
inserted
replaced
164 "MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n-> t)" |
164 "MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n-> t)" |
165 MGTe :: "expr => state => etriple" |
165 MGTe :: "expr => state => etriple" |
166 "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)" |
166 "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)" |
167 syntax (xsymbols) |
167 syntax (xsymbols) |
168 MGTe :: "expr => state => etriple" ("MGT\<^sub>e") |
168 MGTe :: "expr => state => etriple" ("MGT\<^sub>e") |
|
169 syntax (HTML output) |
|
170 MGTe :: "expr => state => etriple" ("MGT\<^sub>e") |
169 |
171 |
170 lemma MGF_implies_complete: |
172 lemma MGF_implies_complete: |
171 "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" |
173 "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" |
172 apply (simp only: valid_def2) |
174 apply (simp only: valid_def2) |
173 apply (unfold MGT_def) |
175 apply (unfold MGT_def) |