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