Theory Sem_Equiv

theory Sem_Equiv
imports Big_Step
header "Semantic Equivalence up to a Condition"

theory Sem_Equiv
imports Big_Step
begin

type_synonym assn = "state => bool"

definition
equiv_up_to :: "assn => com => com => bool" ("_ \<Turnstile> _ ∼ _" [50,0,10] 50)
where
"(P \<Turnstile> c ∼ c') = (∀s s'. P s --> (c,s) => s' <-> (c',s) => s')"

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

lemma equiv_up_to_True:
"((λ_. True) \<Turnstile> c ∼ c') = (c ∼ c')"
by (simp add: equiv_def equiv_up_to_def)

lemma equiv_up_to_weaken:
"P \<Turnstile> c ∼ c' ==> (!!s. P' s ==> P s) ==> P' \<Turnstile> c ∼ c'"
by (simp add: equiv_up_to_def)

lemma equiv_up_toI:
"(!!s s'. P s ==> (c, s) => s' = (c', s) => s') ==> P \<Turnstile> c ∼ c'"
by (unfold equiv_up_to_def) blast

lemma equiv_up_toD1:
"P \<Turnstile> c ∼ c' ==> (c, s) => s' ==> P s ==> (c', s) => s'"
by (unfold equiv_up_to_def) blast

lemma equiv_up_toD2:
"P \<Turnstile> 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 \<Turnstile> c ∼ c"
by (auto simp: equiv_up_to_def)

lemma equiv_up_to_sym:
"(P \<Turnstile> c ∼ c') = (P \<Turnstile> c' ∼ c)"
by (auto simp: equiv_up_to_def)

lemma equiv_up_to_trans:
"P \<Turnstile> c ∼ c' ==> P \<Turnstile> c' ∼ c'' ==> P \<Turnstile> c ∼ c''"
by (auto simp: equiv_up_to_def)


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

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

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

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


lemma equiv_up_to_seq:
"P \<Turnstile> c ∼ c' ==> Q \<Turnstile> d ∼ d' ==>
(!!s s'. (c,s) => s' ==> P s ==> Q s') ==>
P \<Turnstile> (c;; d) ∼ (c';; d')"

by (clarsimp simp: equiv_up_to_def) blast

lemma equiv_up_to_while_lemma:
shows "(d,s) => s' ==>
P \<Turnstile> b <∼> b' ==>
(λs. P s ∧ bval b s) \<Turnstile> 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 \<Turnstile> 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 "(λs. P s ∧ bval b s) \<Turnstile> 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 bequiv_context_subst:
"P \<Turnstile> b <∼> b' ==> (P s ∧ bval b s) = (P s ∧ bval b' s)"
by (auto simp: bequiv_up_to_def)

lemma equiv_up_to_while:
assumes b: "P \<Turnstile> b <∼> b'"
assumes c: "(λs. P s ∧ bval b s) \<Turnstile> c ∼ c'"
assumes I: "!!s s'. (c, s) => s' ==> P s ==> bval b s ==> P s'"
shows "P \<Turnstile> WHILE b DO c ∼ WHILE b' DO c'"
proof -
from b have b': "P \<Turnstile> b' <∼> b" by (simp add: bequiv_up_to_sym)

from c b have c': "(λs. P s ∧ bval b' s) \<Turnstile> c' ∼ c"
by (simp add: equiv_up_to_sym bequiv_context_subst)

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 [OF _ b c]
equiv_up_to_while_lemma [OF _ b' c']
thus ?thesis using I I' by (auto intro!: equiv_up_toI)
qed

lemma equiv_up_to_while_weak:
"P \<Turnstile> b <∼> b' ==> P \<Turnstile> c ∼ c' ==>
(!!s s'. (c, s) => s' ==> P s ==> bval b s ==> P s') ==>
P \<Turnstile> WHILE b DO c ∼ WHILE b' DO c'"

by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken)

lemma equiv_up_to_if:
"P \<Turnstile> b <∼> b' ==> (λs. P s ∧ bval b s) \<Turnstile> c ∼ c' ==> (λs. P s ∧ ¬bval b s) \<Turnstile> d ∼ d' ==>
P \<Turnstile> 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_weak:
"P \<Turnstile> b <∼> b' ==> P \<Turnstile> c ∼ c' ==> P \<Turnstile> d ∼ d' ==>
P \<Turnstile> IF b THEN c ELSE d ∼ IF b' THEN c' ELSE d'"

by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken)

lemma equiv_up_to_if_True [intro!]:
"(!!s. P s ==> bval b s) ==> P \<Turnstile> 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 \<Turnstile> 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 \<Turnstile> 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 \<Turnstile> WHILE Bc True DO c ∼ WHILE Bc True DO SKIP"
unfolding equiv_up_to_def
by (blast dest: while_never)


end