src/HOL/IMP/Sem_Equiv.thy
changeset 44890 22f665a2e91c
parent 44261 e44f465c00a1
child 45015 fdac1e9880eb
     1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4  next
     1.5    case WhileFalse
     1.6    thus ?case by (auto simp: bequiv_up_to_def)
     1.7 -qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
     1.8 +qed (fastforce simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
     1.9  
    1.10  lemma bequiv_context_subst:
    1.11    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
    1.12 @@ -128,7 +128,7 @@
    1.13  lemma equiv_up_to_while_weak:
    1.14    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> 
    1.15     P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
    1.16 -  by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken 
    1.17 +  by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken 
    1.18                 simp: hoare_valid_def)
    1.19  
    1.20  lemma equiv_up_to_if:
    1.21 @@ -139,7 +139,7 @@
    1.22  lemma equiv_up_to_if_weak:
    1.23    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
    1.24     P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
    1.25 -  by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
    1.26 +  by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken)
    1.27  
    1.28  lemma equiv_up_to_if_True [intro!]:
    1.29    "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"