move stronger rules into exercise
authorkleing
Thu Feb 20 12:27:51 2014 +1100 (2014-02-20)
changeset 55598da35747597bd
parent 55597 25d7b485df81
child 55599 6535c537b243
move stronger rules into exercise
src/HOL/IMP/Sem_Equiv.thy
     1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Wed Feb 19 15:57:02 2014 +0000
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Thu Feb 20 12:27:51 2014 +1100
     1.3 @@ -75,10 +75,10 @@
     1.4    P \<Turnstile> (c;; d) \<sim> (c';; d')"
     1.5    by (clarsimp simp: equiv_up_to_def) blast
     1.6  
     1.7 -lemma equiv_up_to_while_lemma:
     1.8 +lemma equiv_up_to_while_lemma_weak:
     1.9    shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
    1.10           P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
    1.11 -         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
    1.12 +         P \<Turnstile> c \<sim> c' \<Longrightarrow>
    1.13           (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
    1.14           P s \<Longrightarrow>
    1.15           d = WHILE b DO c \<Longrightarrow>
    1.16 @@ -92,7 +92,7 @@
    1.17    have "bval b' s1" by (simp add: bequiv_up_to_def)
    1.18    moreover
    1.19    from WhileTrue.prems
    1.20 -  have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
    1.21 +  have "P \<Turnstile> c \<sim> c'" by simp
    1.22    with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
    1.23    have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
    1.24    moreover
    1.25 @@ -108,45 +108,29 @@
    1.26    thus ?case by (auto simp: bequiv_up_to_def)
    1.27  qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+
    1.28  
    1.29 -lemma bequiv_context_subst:
    1.30 -  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
    1.31 -  by (auto simp: bequiv_up_to_def)
    1.32 -
    1.33 -lemma equiv_up_to_while:
    1.34 +lemma equiv_up_to_while_weak:
    1.35    assumes b: "P \<Turnstile> b <\<sim>> b'"
    1.36 -  assumes c: "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'"
    1.37 +  assumes c: "P \<Turnstile> c \<sim> c'"
    1.38    assumes I: "\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'"
    1.39    shows "P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
    1.40  proof -
    1.41    from b have b': "P \<Turnstile> b' <\<sim>> b" by (simp add: bequiv_up_to_sym)
    1.42  
    1.43 -  from c b have c': "(\<lambda>s. P s \<and> bval b' s) \<Turnstile> c' \<sim> c"
    1.44 -    by (simp add: equiv_up_to_sym bequiv_context_subst)
    1.45 +  from c b have c': "P \<Turnstile> c' \<sim> c" by (simp add: equiv_up_to_sym)
    1.46  
    1.47    from I
    1.48    have I': "\<And>s s'. (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b' s \<Longrightarrow> P s'"
    1.49      by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])
    1.50  
    1.51 -  note equiv_up_to_while_lemma [OF _ b c]
    1.52 -       equiv_up_to_while_lemma [OF _ b' c']
    1.53 +  note equiv_up_to_while_lemma_weak [OF _ b c]
    1.54 +       equiv_up_to_while_lemma_weak [OF _ b' c']
    1.55    thus ?thesis using I I' by (auto intro!: equiv_up_toI)
    1.56  qed
    1.57  
    1.58 -lemma equiv_up_to_while_weak:
    1.59 -  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow>
    1.60 -   (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
    1.61 -   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
    1.62 -  by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken)
    1.63 -
    1.64 -lemma equiv_up_to_if:
    1.65 -  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
    1.66 -   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
    1.67 -  by (auto simp: bequiv_up_to_def equiv_up_to_def)
    1.68 -
    1.69  lemma equiv_up_to_if_weak:
    1.70    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
    1.71     P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
    1.72 -  by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken)
    1.73 +  by (auto simp: bequiv_up_to_def equiv_up_to_def)
    1.74  
    1.75  lemma equiv_up_to_if_True [intro!]:
    1.76    "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"