src/HOL/IMP/Sem_Equiv.thy
author Gerwin Klein <gerwin.klein@nicta.com.au>
Thu Aug 23 15:32:22 2012 +0200 (2012-08-23)
changeset 48909 b2dea007e55e
parent 47818 151d137f1095
child 52021 59963cda805a
permissions -rw-r--r--
remove Hoare dependency from Fold.thy
     1 header "Semantic Equivalence up to a Condition"
     2 
     3 theory Sem_Equiv
     4 imports Big_Step
     5 begin
     6 
     7 type_synonym assn = "state \<Rightarrow> bool"
     8 
     9 definition
    10   equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
    11 where
    12   "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
    13 
    14 definition
    15   bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
    16 where
    17   "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
    18 
    19 lemma equiv_up_to_True:
    20   "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')"
    21   by (simp add: equiv_def equiv_up_to_def)
    22 
    23 lemma equiv_up_to_weaken:
    24   "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'"
    25   by (simp add: equiv_up_to_def)
    26 
    27 lemma equiv_up_toI:
    28   "(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'"
    29   by (unfold equiv_up_to_def) blast
    30 
    31 lemma equiv_up_toD1:
    32   "P \<Turnstile> c \<sim> c' \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s'"
    33   by (unfold equiv_up_to_def) blast
    34 
    35 lemma equiv_up_toD2:
    36   "P \<Turnstile> c \<sim> c' \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s'"
    37   by (unfold equiv_up_to_def) blast
    38 
    39 
    40 lemma equiv_up_to_refl [simp, intro!]:
    41   "P \<Turnstile> c \<sim> c"
    42   by (auto simp: equiv_up_to_def)
    43 
    44 lemma equiv_up_to_sym:
    45   "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
    46   by (auto simp: equiv_up_to_def)
    47 
    48 lemma equiv_up_to_trans:
    49   "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
    50   by (auto simp: equiv_up_to_def)
    51 
    52 
    53 lemma bequiv_up_to_refl [simp, intro!]:
    54   "P \<Turnstile> b <\<sim>> b"
    55   by (auto simp: bequiv_up_to_def)
    56 
    57 lemma bequiv_up_to_sym:
    58   "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
    59   by (auto simp: bequiv_up_to_def)
    60 
    61 lemma bequiv_up_to_trans:
    62   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
    63   by (auto simp: bequiv_up_to_def)
    64 
    65 lemma bequiv_up_to_subst:
    66   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P s \<Longrightarrow> bval b s = bval b' s"
    67   by (simp add: bequiv_up_to_def)
    68 
    69 
    70 lemma equiv_up_to_seq:
    71   "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow>
    72   (\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
    73   P \<Turnstile> (c; d) \<sim> (c'; d')"
    74   by (clarsimp simp: equiv_up_to_def) blast
    75 
    76 lemma equiv_up_to_while_lemma:
    77   shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
    78          P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
    79          (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
    80          (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
    81          P s \<Longrightarrow>
    82          d = WHILE b DO c \<Longrightarrow>
    83          (WHILE b' DO c', s) \<Rightarrow> s'"
    84 proof (induction rule: big_step_induct)
    85   case (WhileTrue b s1 c s2 s3)
    86   hence IH: "P s2 \<Longrightarrow> (WHILE b' DO c', s2) \<Rightarrow> s3" by auto
    87   from WhileTrue.prems
    88   have "P \<Turnstile> b <\<sim>> b'" by simp
    89   with `bval b s1` `P s1`
    90   have "bval b' s1" by (simp add: bequiv_up_to_def)
    91   moreover
    92   from WhileTrue.prems
    93   have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
    94   with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
    95   have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
    96   moreover
    97   from WhileTrue.prems
    98   have "\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'" by simp
    99   with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
   100   have "P s2" by simp
   101   hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
   102   ultimately
   103   show ?case by blast
   104 next
   105   case WhileFalse
   106   thus ?case by (auto simp: bequiv_up_to_def)
   107 qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+
   108 
   109 lemma bequiv_context_subst:
   110   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
   111   by (auto simp: bequiv_up_to_def)
   112 
   113 lemma equiv_up_to_while:
   114   assumes b: "P \<Turnstile> b <\<sim>> b'"
   115   assumes c: "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'"
   116   assumes I: "\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'"
   117   shows "P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
   118 proof -
   119   from b have b': "P \<Turnstile> b' <\<sim>> b" by (simp add: bequiv_up_to_sym)
   120 
   121   from c b have c': "(\<lambda>s. P s \<and> bval b' s) \<Turnstile> c' \<sim> c"
   122     by (simp add: equiv_up_to_sym bequiv_context_subst)
   123 
   124   from I
   125   have I': "\<And>s s'. (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b' s \<Longrightarrow> P s'"
   126     by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])
   127 
   128   note equiv_up_to_while_lemma [OF _ b c]
   129        equiv_up_to_while_lemma [OF _ b' c']
   130   thus ?thesis using I I' by (auto intro!: equiv_up_toI)
   131 qed
   132 
   133 lemma equiv_up_to_while_weak:
   134   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow>
   135    (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
   136    P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
   137   by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken)
   138 
   139 lemma equiv_up_to_if:
   140   "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>
   141    P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
   142   by (auto simp: bequiv_up_to_def equiv_up_to_def)
   143 
   144 lemma equiv_up_to_if_weak:
   145   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
   146    P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
   147   by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken)
   148 
   149 lemma equiv_up_to_if_True [intro!]:
   150   "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
   151   by (auto simp: equiv_up_to_def)
   152 
   153 lemma equiv_up_to_if_False [intro!]:
   154   "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
   155   by (auto simp: equiv_up_to_def)
   156 
   157 lemma equiv_up_to_while_False [intro!]:
   158   "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
   159   by (auto simp: equiv_up_to_def)
   160 
   161 lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'"
   162  by (induct rule: big_step_induct) auto
   163 
   164 lemma equiv_up_to_while_True [intro!,simp]:
   165   "P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP"
   166   unfolding equiv_up_to_def
   167   by (blast dest: while_never)
   168 
   169 
   170 end