Theory Sem_Equiv

section "Constant Folding"

theory Sem_Equiv
imports Big_Step
begin

subsection "Semantic Equivalence up to a Condition"

type_synonym assn = "state ⇒ bool"

definition
  equiv_up_to :: "assn ⇒ com ⇒ com ⇒ bool" ("_ ⊨ _ ∼ _" [50,0,10] 50)
where
  "(P ⊨ c ∼ c') = (∀s s'. P s ⟶ (c,s) ⇒ s' ⟷ (c',s) ⇒ s')"

definition
  bequiv_up_to :: "assn ⇒ bexp ⇒ bexp ⇒ bool" ("_ ⊨ _ <∼> _" [50,0,10] 50)
where
  "(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)
  moreover
  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)
  moreover
  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)
  ultimately
  show ?case by blast
next
  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)
qed

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)


end