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