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