equal
deleted
inserted
replaced
149 |
149 |
150 lemma Thin_lemma: |
150 lemma Thin_lemma: |
151 "(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and> |
151 "(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and> |
152 (A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))" |
152 (A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))" |
153 apply (rule hoare_ehoare.induct) |
153 apply (rule hoare_ehoare.induct) |
154 apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])") |
154 apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])") |
155 apply (blast intro: hoare_ehoare.Skip) |
155 apply (blast intro: hoare_ehoare.Skip) |
156 apply (blast intro: hoare_ehoare.Comp) |
156 apply (blast intro: hoare_ehoare.Comp) |
157 apply (blast intro: hoare_ehoare.Cond) |
157 apply (blast intro: hoare_ehoare.Cond) |
158 apply (blast intro: hoare_ehoare.Loop) |
158 apply (blast intro: hoare_ehoare.Loop) |
159 apply (blast intro: hoare_ehoare.LAcc) |
159 apply (blast intro: hoare_ehoare.LAcc) |