Theory Sem_Equiv

section "Constant Folding"

theory Sem_Equiv
imports Big_Step

subsection "Semantic Equivalence up to a Condition"

type_synonym assn = "state  bool"

  equiv_up_to :: "assn  com  com  bool" ("_  _  _" [50,0,10] 50)
  "(P  c  c') = (s s'. P s  (c,s)  s'  (c',s)  s')"

  bequiv_up_to :: "assn  bexp  bexp  bool" ("_  _ <∼> _" [50,0,10] 50)
  "(P  b <∼> b') = (s. P s  bval b s = bval b' s)"

lemma equiv_up_to_True:
  "((λ_. True)  c  c') = (c  c')"
  by (simp add: equiv_def equiv_up_to_def)

lemma equiv_up_to_weaken:
  "P  c  c'  (s. P' s  P s)  P'  c  c'"
  by (simp add: equiv_up_to_def)

lemma equiv_up_toI:
  "(s s'. P s  (c, s)  s' = (c', s)  s')  P  c  c'"
  by (unfold equiv_up_to_def) blast

lemma equiv_up_toD1:
  "P  c  c'  (c, s)  s'  P s  (c', s)  s'"
  by (unfold equiv_up_to_def) blast

lemma equiv_up_toD2:
  "P  c  c'  (c', s)  s'  P s  (c, s)  s'"
  by (unfold equiv_up_to_def) blast

lemma equiv_up_to_refl [simp, intro!]:
  "P  c  c"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_sym:
  "(P  c  c') = (P  c'  c)"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_trans:
  "P  c  c'  P  c'  c''  P  c  c''"
  by (auto simp: equiv_up_to_def)

lemma bequiv_up_to_refl [simp, intro!]:
  "P  b <∼> b"
  by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_sym:
  "(P  b <∼> b') = (P  b' <∼> b)"
  by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_trans:
  "P  b <∼> b'  P  b' <∼> b''  P  b <∼> b''"
  by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_subst:
  "P  b <∼> b'  P s  bval b s = bval b' s"
  by (simp add: bequiv_up_to_def)

lemma equiv_up_to_seq:
  "P  c  c'  Q  d  d' 
  (s s'. (c,s)  s'  P s  Q s') 
  P  (c;; d)  (c';; d')"
  by (clarsimp simp: equiv_up_to_def) blast

lemma equiv_up_to_while_lemma_weak:
  shows "(d,s)  s' 
         P  b <∼> b' 
         P  c  c' 
         (s s'. (c, s)  s'  P s  bval b s  P s') 
         P s 
         d = WHILE b DO c 
         (WHILE b' DO c', s)  s'"
proof (induction rule: big_step_induct)
  case (WhileTrue b s1 c s2 s3)
  hence IH: "P s2  (WHILE b' DO c', s2)  s3" by auto
  from WhileTrue.prems
  have "P  b <∼> b'" by simp
  with bval b s1 P s1
  have "bval b' s1" by (simp add: bequiv_up_to_def)
  from WhileTrue.prems
  have "P  c  c'" by simp
  with bval b s1 P s1 (c, s1)  s2
  have "(c', s1)  s2" by (simp add: equiv_up_to_def)
  from WhileTrue.prems
  have "s s'. (c,s)  s'  P s  bval b s  P s'" by simp
  with P s1 bval b s1 (c, s1)  s2
  have "P s2" by simp
  hence "(WHILE b' DO c', s2)  s3" by (rule IH)
  show ?case by blast
  case WhileFalse
  thus ?case by (auto simp: bequiv_up_to_def)
qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+

lemma equiv_up_to_while_weak:
  assumes b: "P  b <∼> b'"
  assumes c: "P  c  c'"
  assumes I: "s s'. (c, s)  s'  P s  bval b s  P s'"
  shows "P  WHILE b DO c  WHILE b' DO c'"
proof -
  from b have b': "P  b' <∼> b" by (simp add: bequiv_up_to_sym)

  from c b have c': "P  c'  c" by (simp add: equiv_up_to_sym)

  from I
  have I': "s s'. (c', s)  s'  P s  bval b' s  P s'"
    by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])

  note equiv_up_to_while_lemma_weak [OF _ b c]
       equiv_up_to_while_lemma_weak [OF _ b' c']
  thus ?thesis using I I' by (auto intro!: equiv_up_toI)

lemma equiv_up_to_if_weak:
  "P  b <∼> b'  P  c  c'  P  d  d' 
   P  IF b THEN c ELSE d  IF b' THEN c' ELSE d'"
  by (auto simp: bequiv_up_to_def equiv_up_to_def)

lemma equiv_up_to_if_True [intro!]:
  "(s. P s  bval b s)  P  IF b THEN c1 ELSE c2  c1"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_if_False [intro!]:
  "(s. P s  ¬ bval b s)  P  IF b THEN c1 ELSE c2  c2"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_while_False [intro!]:
  "(s. P s  ¬ bval b s)  P  WHILE b DO c  SKIP"
  by (auto simp: equiv_up_to_def)

lemma while_never: "(c, s)  u  c  WHILE (Bc True) DO c'"
 by (induct rule: big_step_induct) auto

lemma equiv_up_to_while_True [intro!,simp]:
  "P  WHILE Bc True DO c  WHILE Bc True DO SKIP"
  unfolding equiv_up_to_def
  by (blast dest: while_never)