(* Tested with Isabelle2023, 15-Feb-2024 *)

theory Correctness_Incorrectness imports
  Main
begin

typedecl var
type_synonym state = "var \<Rightarrow> int"

type_synonym assertion = "state set"
type_synonym command = "(state \<times> state) set"

definition skip where [simp]:
  "skip \<equiv> { (\<sigma>,\<sigma>') | \<sigma> \<sigma>'. \<sigma> = \<sigma>' }"

definition diverge :: "command" where
  "diverge \<equiv> {}"

definition FALSE :: "assertion" where
  "FALSE \<equiv> {}"

fun NOT :: "assertion \<Rightarrow> assertion" where
  "NOT P = {\<sigma>. \<sigma> \<notin> P}"

definition TRUE :: "assertion" where [simp]:
  "TRUE \<equiv> UNIV"

fun determ :: "command \<Rightarrow> state set" where 
  "determ c = {\<sigma>. \<forall>\<sigma>1 \<sigma>2. (\<sigma>, \<sigma>1) \<in> c \<and> (\<sigma>, \<sigma>2) \<in> c \<longrightarrow> \<sigma>1 = \<sigma>2}"

fun diverges :: "command \<Rightarrow> state set" where
  "diverges c = {\<sigma>. \<forall>\<sigma>'. (\<sigma>, \<sigma>') \<notin> c}"

(* The set of all states that c can reach if it starts executing in a P state. *)
(* Same as strongest post *)
fun may_reach :: "(assertion \<times> command) \<Rightarrow> assertion" where
  "may_reach (P, c) = {\<sigma>'. \<exists>\<sigma>. (\<sigma>,\<sigma>') \<in> c \<and> \<sigma> \<in> P}"

(* The set of all states from which c is guaranteed only to reach Q states (if 
   it reaches any final state at all). *)
(* Same as weakest pre *)
fun must_reach :: "(command \<times> assertion) \<Rightarrow> assertion" where
  "must_reach (c, Q) = {\<sigma>. \<forall>\<sigma>'. (\<sigma>,\<sigma>') \<in> c \<longrightarrow> \<sigma>' \<in> Q}"

lemma "may_reach (P, c) = NOT (must_reach (c^-1, NOT P))" by simp

(* weakest liberal pre *)
(* The set of all states from which c can only reach Q states. *)
fun wlp :: "(command \<times> assertion) \<Rightarrow> assertion" where
  "wlp (c, Q) = {\<sigma>. \<forall>\<sigma>'. (\<sigma>,\<sigma>') \<in> c \<longrightarrow> \<sigma>' \<in> Q}"

(* weakest pre *)
fun wp :: "(command \<times> assertion) \<Rightarrow> assertion" where
  "wp (c, Q) = {\<sigma>. (\<exists>\<sigma>'. (\<sigma>,\<sigma>') \<in> c) \<and> (\<forall>\<sigma>'. (\<sigma>,\<sigma>') \<in> c \<longrightarrow> \<sigma>' \<in> Q)}"

lemma "wp (c, Q) \<subseteq> wlp (c, Q)" by auto
lemma "diverges c = {} \<Longrightarrow> wlp (c, Q) \<subseteq> wp (c, Q)" by auto


(* weakest possible pre *)
(* The set of all states from which c can reach Q states. *)
(* Note that Zhang and Kaminsky OOPSLA 2022 call this "weakest precondition" *)
fun wpp :: "(command \<times> assertion) \<Rightarrow> assertion" where
  "wpp (c, Q) = {\<sigma>. \<exists>\<sigma>' \<in> Q. (\<sigma>,\<sigma>') \<in> c}"

lemma "\<lbrakk> diverges c = {}; determ c = TRUE \<rbrakk> \<Longrightarrow> wpp (c, Q) = wlp (c, Q)" by fastforce
lemma "\<lbrakk> determ c = TRUE \<rbrakk> \<Longrightarrow> wpp (c, Q) \<subseteq> wlp (c, Q)" by fastforce
lemma "\<lbrakk> diverges c = {} \<rbrakk> \<Longrightarrow> wlp (c, Q) \<subseteq> wpp (c, Q)" by fastforce

lemma "determ c = TRUE \<Longrightarrow> wpp (c, Q) = wp (c, Q)" by fastforce
lemma "determ c = TRUE \<Longrightarrow> wpp (c, Q) \<subseteq> wp (c, Q)" by fastforce
lemma "wp (c, Q) \<subseteq> wpp (c, Q)" by fastforce

(* strongest post *)
(* The set of all states that c can reach if it starts executing in a P state. *)
fun sp :: "(assertion \<times> command) \<Rightarrow> assertion" where
  "sp (P, c) = {\<sigma>'. \<exists>\<sigma>. (\<sigma>,\<sigma>') \<in> c \<and> \<sigma> \<in> P}"

(* strongest liberal post *)
(* The set of all states that c can only reach if it starts executing in a P state. *)
fun slp :: "(assertion \<times> command) \<Rightarrow> assertion" where
  "slp (P, c) = {\<sigma>'. \<forall>\<sigma>. (\<sigma>,\<sigma>') \<in> c \<longrightarrow> \<sigma> \<in> P}"

lemma "wpp (c, Q) = may_reach (Q, c^-1)" by auto
lemma "may_reach (P, c) = NOT (wlp (c^-1, NOT P))" by simp
lemma "wpp (c, Q) = NOT (wlp (c, NOT Q))" by auto
lemma "wpp (c, Q) = sp (Q, c^-1)" by auto
lemma "must_reach (c, Q) = wlp (c, Q)" by simp
lemma "may_reach (P, c) = sp (P, c)" by simp
lemma "slp (P, c) = NOT (sp (NOT P, c))" by simp
lemma "slp (P, c) = must_reach (c^-1, P)" by simp
lemma "slp (P, c) = wlp (c^-1, P)" by simp
lemma "P \<subseteq> diverges c \<Longrightarrow> sp (P, c) = {}" by auto

(* Galois connections observed by Zhang and Kaminski OOPSLA 2022 *)
lemma "(P \<subseteq> wlp (c, Q)) \<longleftrightarrow> (sp (P, c) \<subseteq> Q)" by auto
lemma "(P \<subseteq> slp (Q, c)) \<longleftrightarrow> (wpp (c, P) \<subseteq> Q)" by auto


(* Partial correctness *)
fun pc :: "(assertion \<times> command \<times> assertion) \<Rightarrow> bool" where
(* If command c is executed from a state that satisfies the precondition 
   P, then any state it reaches satisfies the postcondition Q. *)
(* "P is sufficient for ensuring that c either reaches Q or diverges." *)
(* If P holds, c can only reach states where Q holds. *)
  "pc (P, c, Q) = (\<forall>\<sigma> \<sigma>'. \<sigma> \<in> P \<and> (\<sigma>,\<sigma>') \<in> c \<longrightarrow> \<sigma>' \<in> Q)"

(* Incorrectness logic *)
fun il :: "(assertion \<times> command \<times> assertion) \<Rightarrow> bool" where
(* "Every state that satisfies the postcondition Q can be reached by 
   executing command c from a state that satisfies the precondition P." *)
  "il (P, c, Q) = (\<forall>\<sigma>'\<in> Q. \<exists>\<sigma> \<in> P. (\<sigma>, \<sigma>') \<in> c)"

(* "Sufficient incorrectness logic" *)
(* AKA backwards underapproximate Hoare logic *)
(* AKA Lisbon triples *)
fun sil :: "(assertion \<times> command \<times> assertion) \<Rightarrow> bool" where
  "sil (P, c, Q) = (\<forall>\<sigma> \<in> P. \<exists>\<sigma>' \<in> Q. (\<sigma>, \<sigma>') \<in> c)"

(* "New triple" *)
fun nt :: "(assertion \<times> command \<times> assertion) \<Rightarrow> bool" where
(* "Every state from which c always reaches a state that satisfies Q, must satisfy P." *)
(* "If executing c from state \<sigma> can only reach states that satisfy Q, then \<sigma> must satisfy P."*)
(* "P contains all states from which command c can only reach states that satisfy Q." *)
(* "If a state forces c to reach Q or diverge, then P must hold." *)
(* "P is necessary for ensuring that c either reaches Q or diverges." *)
(* If P _doesn't_ hold, c can reach a state where Q _doesn't_ hold. *)
  "nt (P, c, Q) = (\<forall>\<sigma>. (\<forall>\<sigma>'. (\<sigma>, \<sigma>') \<in> c \<longrightarrow> \<sigma>' \<in> Q) \<longrightarrow> \<sigma> \<in> P)"

(* si and nt have equivalent power *)
theorem "sil (P, c, Q) \<longleftrightarrow> nt (NOT P, c, NOT Q)" by auto

(* Necessary conditions logic *)
(* As formalised by Ascari et al in their SIL paper *)
fun nc :: "(assertion \<times> command \<times> assertion) \<Rightarrow> bool" where
  "nc (P, c, Q) = (\<forall>\<sigma>. (\<exists>\<sigma>'. (\<sigma>, \<sigma>') \<in> c \<and> \<sigma>' \<in> Q) \<longrightarrow> \<sigma> \<in> P)"

(* ht and nc have equivalent power *)
theorem "pc (P, c, Q) \<longleftrightarrow> nc (NOT P, c, NOT Q)" by auto
theorem "pc (P, c, Q) \<longleftrightarrow> nc (Q, c^-1, P)" by auto

(* Yet another kind of triple *)
fun yt :: "(assertion \<times> command \<times> assertion) \<Rightarrow> bool" where
  "yt (P, c, Q) = (\<forall>\<sigma>'. (\<forall>\<sigma>. (\<sigma>, \<sigma>') \<in> c \<longrightarrow> \<sigma> \<in> P) \<longrightarrow> \<sigma>' \<in> Q)"

(* yt and it have equivalent power *)
theorem "yt (P, c, Q) \<longleftrightarrow> il (NOT P, c, NOT Q)" by auto

(* may = what may happen if execution starts (or ends) in a particular state *)
(* must = what must happen if execution starts (or ends) in a particular state *)
(* forward = considering the executions of a command from a particular start state *)
(* backward = considering the executions of a command that end in a particular final state *)
(* over = if we add behaviours to c, the triple remains valid *)
(* under = if we remove behaviours from c, the triple remains valid *)

lemma "pc (P, c, Q) \<longleftrightarrow> (sp(P, c) \<subseteq> Q)" by auto    (* (may, forward, over) *)
lemma "il (P, c, Q) \<longleftrightarrow> (sp(P, c) \<supseteq> Q)" by auto    (* (may, forward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (wpp(c, Q) \<subseteq> P)" by auto   (* (may, backward, over) *)
lemma "sil (P, c, Q) \<longleftrightarrow> (wpp(c, Q) \<supseteq> P)" by auto   (* (may, backward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (Q \<subseteq> slp(P, c))" by auto   (* (must, forward, over) *)
lemma "yt (P, c, Q) \<longleftrightarrow> (Q \<supseteq> slp(P, c))" by auto   (* (must, forward, under) *)
lemma "pc (P, c, Q) \<longleftrightarrow> (P \<subseteq> wlp(c, Q))" by auto    (* (must, backward, over) *)
lemma "nt (P, c, Q) \<longleftrightarrow> (P \<supseteq> wlp(c, Q))" by auto    (* (must, backward, under) *)

lemma "pc (P, c, Q) \<longleftrightarrow> (sp(P, c) \<subseteq> Q)" by auto     (* (may, forward, over) *)
lemma "il (P, c, Q) \<longleftrightarrow> (sp(P, c) \<supseteq> Q)" by auto     (* (may, forward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (sp(Q, c\<inverse>) \<subseteq> P)" by auto  (* (may, backward, over) *)
lemma "sil (P, c, Q) \<longleftrightarrow> (sp(Q, c\<inverse>) \<supseteq> P)" by auto  (* (may, backward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (Q \<subseteq> slp(P, c))" by auto    (* (must, forward, over) *)
lemma "yt (P, c, Q) \<longleftrightarrow> (Q \<supseteq> slp(P, c))" by auto    (* (must, forward, under) *)
lemma "pc (P, c, Q) \<longleftrightarrow> (P \<subseteq> slp(Q, c\<inverse>))" by auto (* (must, backward, over) *)
lemma "nt (P, c, Q) \<longleftrightarrow> (P \<supseteq> slp(Q, c\<inverse>))" by auto (* (must, backward, under) *)

lemma "pc (P, c, Q) \<longleftrightarrow> (sp(P, c) \<subseteq> Q)" by auto            
(* (may, forward, over) *)
lemma "il (P, c, Q) \<longleftrightarrow> (sp(P, c) \<supseteq> Q)" by auto            
(* (may, forward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (sp(Q, c\<inverse>) \<subseteq> P)" by auto         
(* (may, backward, over) *)
lemma "sil (P, c, Q) \<longleftrightarrow> (sp(Q, c\<inverse>) \<supseteq> P)" by auto         
(* (may, backward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (sp(NOT P, c) \<subseteq> NOT Q)" by auto    
(* (must, forward, over) *)
lemma "yt (P, c, Q) \<longleftrightarrow> (sp(NOT P, c) \<supseteq> NOT Q)" by auto    
(* (must, forward, under) *)
lemma "pc (P, c, Q) \<longleftrightarrow> (sp(NOT Q, c\<inverse>) \<subseteq> NOT P)" by auto 
(* (must, backward, over) *)
lemma "nt (P, c, Q) \<longleftrightarrow> (sp(NOT Q, c\<inverse>) \<supseteq> NOT P)" by auto 
(* (must, backward, under) *)

lemma "il (P, c, Q) \<longleftrightarrow> sil (Q, c\<inverse>, P)" by auto

lemma "pc (P, c, Q) \<longleftrightarrow> (sp(P, c) \<subseteq> Q)" by auto    (* (may, forward, over) *)
lemma "il (P, c, Q) \<longleftrightarrow> (sp(P, c) \<supseteq> Q)" by auto    (* (may, forward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (sp(Q, c\<inverse>) \<subseteq> P)" by auto (* (may, backward, over) *)
lemma "sil (P, c, Q) \<longleftrightarrow> (sp(Q, c\<inverse>) \<supseteq> P)" by auto (* (may, backward, under) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (Q \<subseteq> wlp(c\<inverse>, P))" by auto (* (must, forward, over) *)
lemma "yt (P, c, Q) \<longleftrightarrow> (Q \<supseteq> wlp(c\<inverse>, P))" by auto (* (must, forward, under) *)
lemma "pc (P, c, Q) \<longleftrightarrow> (P \<subseteq> wlp(c, Q))" by auto    (* (must, backward, over) *)
lemma "nt (P, c, Q) \<longleftrightarrow> (P \<supseteq> wlp(c, Q))" by auto    (* (must, backward, under) *)

lemma "c' \<subseteq> c \<Longrightarrow> pc (P, c, Q) \<longrightarrow> pc (P, c', Q)" by fastforce (* over *)
lemma "c \<subseteq> c' \<Longrightarrow> il (P, c, Q) \<longrightarrow> il (P, c', Q)" by fastforce (* under *)
lemma "c' \<subseteq> c \<Longrightarrow> nc (P, c, Q) \<longrightarrow> nc (P, c', Q)" by fastforce (* over *)
lemma "c \<subseteq> c' \<Longrightarrow> sil (P, c, Q) \<longrightarrow> sil (P, c', Q)" by fastforce (* under *)
lemma "c \<subseteq> c' \<Longrightarrow> yt (P, c, Q) \<longrightarrow> yt (P, c', Q)" by fastforce (* under *)
lemma "c \<subseteq> c' \<Longrightarrow> nt (P, c, Q) \<longrightarrow> nt (P, c', Q)" by fastforce (* under *)

lemma "pc (P, c, Q) \<longleftrightarrow> (wpp(c\<inverse>, P) \<subseteq> Q)" by auto (* (may, forward, over) *)
lemma "il (P, c, Q) \<longleftrightarrow> (wpp(c\<inverse>, P) \<supseteq> Q)" by auto (* (may, forward, under) *)
lemma "sil (P, c, Q) \<longleftrightarrow> (P \<subseteq> sp(Q, c\<inverse>))" by auto  (* (may, backward, over) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (P \<supseteq> sp(Q, c\<inverse>))" by auto  (* (may, backward, under) *)
lemma "yt (P, c, Q) \<longleftrightarrow> (wlp(c\<inverse>, P) \<subseteq> Q)" by auto  (* (must, forward, over) *)
lemma "nc (P, c, Q) \<longleftrightarrow> (wlp(c\<inverse>, P) \<supseteq> Q)" by auto  (* (must, forward, under) *)
lemma "pc (P, c, Q) \<longleftrightarrow> (P \<subseteq> slp(Q, c\<inverse>))" by auto (* (must, backward, over) *)
lemma "nt (P, c, Q) \<longleftrightarrow> (P \<supseteq> slp(Q, c\<inverse>))" by auto (* (must, backward, under) *)

(* So, there are just 3 interesting semantics for these triples.
  1. The original Hoare partial correctness interpretation.
  2. Incorrectness triples.
  3. Sufficient incorrectness triples.
*)

(* Formulations of partial correctness *)
lemma "pc (P, c, Q) \<longleftrightarrow> (wpp(c\<inverse>, P) \<subseteq> Q)" by auto
lemma "pc (P, c, Q) \<longleftrightarrow> (P \<subseteq> slp(Q, c\<inverse>))" by auto
lemma "pc (P, c, Q) \<longleftrightarrow> (P \<subseteq> wlp(c, Q))" by auto
lemma "pc (P, c, Q) \<longleftrightarrow> (sp(P, c) \<subseteq> Q)" by auto
(* And these have equivalent "power" *)
lemma "pc (NOT P, c, NOT Q) \<longleftrightarrow> (Q \<subseteq> slp(P, c))" by auto
lemma "pc (NOT P, c, NOT Q) \<longleftrightarrow> (Q \<subseteq> wlp(c\<inverse>, P))" by auto
lemma "pc (NOT P, c, NOT Q) \<longleftrightarrow> (wpp(c, Q) \<subseteq> P)" by auto
lemma "pc (NOT P, c, NOT Q) \<longleftrightarrow> (sp(Q, c\<inverse>) \<subseteq> P)" by auto


(* Formulations of incorrectness logic *)
lemma "il (P, c, Q) \<longleftrightarrow> (wpp(c\<inverse>, P) \<supseteq> Q)" by auto
lemma "il (P, c, Q) \<longleftrightarrow> (sp(P, c) \<supseteq> Q)" by auto
(* And these have equivalent "power" *)
lemma "il (NOT P, c, NOT Q) \<longleftrightarrow> (Q \<supseteq> wlp(c\<inverse>, P))" by auto
lemma "il (NOT P, c, NOT Q) \<longleftrightarrow> (Q \<supseteq> slp(P, c))" by auto

(* Formulations of sufficient incorrectness logic *)
lemma "sil (P, c, Q) \<longleftrightarrow> (P \<subseteq> sp(Q, c\<inverse>))" by auto
lemma "sil (P, c, Q) \<longleftrightarrow> (wpp(c, Q) \<supseteq> P)" by auto
(* And these have equivalent "power" *)
lemma "sil (NOT P, c, NOT Q) \<longleftrightarrow> (P \<supseteq> slp(Q, c\<inverse>))" by auto
lemma "sil (NOT P, c, NOT Q) \<longleftrightarrow> (P \<supseteq> wlp(c, Q))" by auto



text \<open> What happens when command does nothing \<close>
theorem "pc (P, skip, Q) \<longleftrightarrow> P \<subseteq> Q" by auto
theorem "il (P, skip, Q) \<longleftrightarrow> Q \<subseteq> P" by auto
theorem "nt (P, skip, Q) \<longleftrightarrow> Q \<subseteq> P" by auto
theorem "sil (P, skip, Q) \<longleftrightarrow> P \<subseteq> Q" by auto

text \<open> What happens when command diverges? \<close>
theorem "pc (P, diverge, Q) \<longleftrightarrow> True" by (simp add: diverge_def)
theorem "il (P, diverge, Q) \<longleftrightarrow> Q = FALSE" by (simp add: diverge_def FALSE_def)
theorem "nt (P, diverge, Q) \<longleftrightarrow> P = TRUE" by (auto simp add: diverge_def) 
theorem "sil (P, diverge, Q) \<longleftrightarrow> P = FALSE" by (simp add: diverge_def FALSE_def)

text \<open> What happens when precondition is unsatisfiable \<close>
theorem "pc (FALSE, c, Q) \<longleftrightarrow> True" by (simp add: FALSE_def)
theorem "il (FALSE, c, Q) \<longleftrightarrow> Q = FALSE" by (simp add: FALSE_def)
theorem "nt (FALSE, c, Q) \<longleftrightarrow> (may_reach (NOT Q, c) = TRUE)" oops
(* nt(FALSE, c, Q) says no matter what state c is executed from, it can always reach a state that violates Q. *)
theorem "sil (FALSE, c, Q) \<longleftrightarrow> True" by (simp add: FALSE_def)

text \<open> What happens when precondition is a tautology? \<close>
theorem "pc (TRUE, c, Q) \<longleftrightarrow> (\<forall>\<sigma> \<sigma>'. (\<sigma>, \<sigma>') \<in> c \<longrightarrow> \<sigma>' \<in> Q)" by simp
(* ht(TRUE, c, Q) says no matter what state c is executed from, every state it reaches satisfies Q. *)
theorem "il (TRUE, c, Q) \<longleftrightarrow> (\<forall>\<sigma>' \<in> Q. \<exists>\<sigma>. (\<sigma>, \<sigma>') \<in> c)" by auto
(* it(TRUE, c, Q) says that every state that satisfies Q can be reached by executing c. *)
theorem "nt (TRUE, c, Q) \<longleftrightarrow> True" by auto
theorem "sil (TRUE, c, Q) \<longleftrightarrow> (may_reach (Q, c) = TRUE)" oops

text \<open> What happens when postcondition is unsatisfiable \<close>
theorem "pc (P, c, FALSE) \<longleftrightarrow> P \<subseteq> diverges c" by (auto simp add: FALSE_def)
(* ht(P, c, FALSE) holds iff P is a sufficient condition for c diverging. *)
theorem "il (P, c, FALSE) \<longleftrightarrow> True" by (simp add: FALSE_def)
theorem "nt (P, c, FALSE) \<longleftrightarrow> diverges c \<subseteq> P" by (auto simp add: FALSE_def)
(* ht(P, c, FALSE) holds iff P is a necessary condition for c diverging. *)
theorem "sil (P, c, FALSE) \<longleftrightarrow> P = FALSE" by (auto simp add: FALSE_def)

text \<open> What happens when postcondition is a tautology? \<close>
theorem "pc (P, c, TRUE) \<longleftrightarrow> True" by auto
theorem "il (P, c, TRUE) \<longleftrightarrow> (\<forall>\<sigma>'. \<exists>\<sigma> \<in> P. (\<sigma>, \<sigma>') \<in> c)" by auto
(* it (P, c, TRUE) holds iff every state can be reached by running c on a state that satisfies P, *)
theorem "nt (P, c, TRUE) \<longleftrightarrow> P = TRUE" by auto
theorem "sil (P, c, TRUE) \<longleftrightarrow> diverges c \<subseteq> NOT P" by auto

text \<open> Law of consequence \<close>
theorem "\<lbrakk> pc (P, c, Q); P' \<subseteq> P; Q \<subseteq> Q' \<rbrakk> \<Longrightarrow> pc (P', c, Q')" by force
theorem "\<lbrakk> il (P, c, Q); P \<subseteq> P'; Q' \<subseteq> Q \<rbrakk> \<Longrightarrow> il (P', c, Q')" by force
theorem "\<lbrakk> nt (P, c, Q); P \<subseteq> P'; Q' \<subseteq> Q \<rbrakk> \<Longrightarrow> nt (P', c, Q)" by force
theorem "\<lbrakk> sil (P, c, Q); P' \<subseteq> P; Q \<subseteq> Q' \<rbrakk> \<Longrightarrow> sil (P', c, Q')" by force

text \<open> Sequencing of commands \<close>
theorem "\<lbrakk> pc (P, c1, Q); pc (Q, c2, R) \<rbrakk> \<Longrightarrow> pc (P, c1 O c2, R)" by fastforce
theorem "\<lbrakk> il (P, c1, Q); il (Q, c2, R) \<rbrakk> \<Longrightarrow> il (P, c1 O c2, R)" by fastforce
theorem "\<lbrakk> nt (P, c1, Q); nt (Q, c2, R) \<rbrakk> \<Longrightarrow> nt (P, c1 O c2, R)" by fastforce
theorem "\<lbrakk> sil (P, c1, Q); sil (Q, c2, R) \<rbrakk> \<Longrightarrow> sil (P, c1 O c2, R)" by fastforce

text \<open> Union of commands \<close>
theorem "\<lbrakk> pc (P1, c1, Q1); pc (P2, c2, Q2) \<rbrakk> \<Longrightarrow> pc (P1 \<inter> P2, c1 \<union> c2, Q1 \<union> Q2)" by fastforce
theorem "\<lbrakk> il (P1, c1, Q1); il (P2, c2, Q2) \<rbrakk> \<Longrightarrow> il (P1 \<union> P2, c1 \<union> c2, Q1 \<union> Q2)" by fastforce
theorem "\<lbrakk> nt (P1, c1, Q1); nt (P2, c2, Q2) \<rbrakk> \<Longrightarrow> nt (P1 \<inter> P2, c1 \<union> c2, Q1 \<inter> Q2)" by fastforce
theorem "\<lbrakk> sil (P1, c1, Q1); sil (P2, c2, Q2) \<rbrakk> \<Longrightarrow> sil (P1 \<union> P2, c1 \<union> c2, Q1 \<union> Q2)" by fastforce

text \<open> Disjunction / conjunction \<close>
theorem "\<lbrakk> pc (P1, c, Q1); pc (P2, c, Q2) \<rbrakk> \<Longrightarrow> pc (P1 \<union> P2, c, Q1 \<union> Q2)" by fastforce
theorem "\<lbrakk> pc (P1, c, Q1); pc (P2, c, Q2) \<rbrakk> \<Longrightarrow> pc (P1 \<inter> P2, c, Q1 \<inter> Q2)" by fastforce
theorem "\<lbrakk> il (P1, c, Q1); il (P2, c, Q2) \<rbrakk> \<Longrightarrow> il (P1 \<union> P2, c, Q1 \<inter> Q2)" by fastforce
theorem "\<lbrakk> nt (P1, c, Q1); nt (P2, c, Q2) \<rbrakk> \<Longrightarrow> nt (P1 \<inter> P2, c, Q1 \<inter> Q2)" by fastforce
theorem "\<lbrakk> sil (P1, c, Q1); sil (P2, c, Q2) \<rbrakk> \<Longrightarrow> sil (P1 \<union> P2, c, Q1 \<union> Q2)" by fastforce

text \<open> Iteration \<close>
theorem il_iter0: "il (P, c\<^sup>*, P)" by auto
theorem "nt (P, c\<^sup>*, P)" by auto
theorem "sil (P, c\<^sup>*, P)" by auto

theorem "pc (P, c, P) \<Longrightarrow> pc (P, c\<^sup>*, P)" 
  apply (subgoal_tac "\<And>k. pc (P, c^^k, P)")
   apply (metis rtrancl_power pc.simps)
  apply (rule nat.induct)
   apply simp
  apply (meson pc.simps relpow_Suc_E)
  done

text \<open> Comparing pc and it \<close>
theorem "\<lbrakk> P \<subseteq> determ c; P \<inter> diverges c = {} \<rbrakk> \<Longrightarrow> pc (P, c, Q) \<longleftrightarrow> il (Q, c\<inverse>, P)" by force
theorem "\<lbrakk> P \<inter> diverges c = {} \<rbrakk>                \<Longrightarrow> pc (P, c, Q) \<longrightarrow> il (Q, c\<inverse>, P)" by force
theorem "\<lbrakk> P \<subseteq> determ c  \<rbrakk>                  \<Longrightarrow> il (Q, c\<inverse>, P) \<longrightarrow> pc (P, c, Q)" by force

text \<open> Comparing ht and si \<close>
theorem "\<lbrakk> P \<subseteq> determ c; P \<inter> diverges c = {} \<rbrakk> \<Longrightarrow> pc(P, c, Q) \<longleftrightarrow> sil (P, c, Q)" by fastforce
theorem "\<lbrakk> P \<inter> diverges c = {} \<rbrakk>               \<Longrightarrow> pc(P, c, Q) \<longrightarrow> sil (P, c, Q)" by fastforce
theorem "\<lbrakk> P \<subseteq> determ c \<rbrakk>                  \<Longrightarrow> sil (P, c, Q) \<longrightarrow> pc(P, c, Q)" by fastforce

text \<open> Comparing il and sil \<close>
lemma "il (P, c, Q) \<longleftrightarrow> sil (Q, c\<inverse>, P)" by auto
(* and the proof rules can be rewritten using...*)
lemma "(c1 O c2)\<inverse> = c2\<inverse> O c1\<inverse>" by blast
lemma "(c1 \<union> c2)\<inverse> = c1\<inverse> \<union> c2\<inverse>" by blast
lemma "(c1 \<inter> c2)\<inverse> = c1\<inverse> \<inter> c2\<inverse>" by blast
lemma "(c\<^sup>*)\<inverse> = (c\<inverse>)\<^sup>*" using rtrancl_converse by blast





definition init :: state where [simp]:
  "init x = 0"

definition is_eq :: "var \<Rightarrow> int \<Rightarrow> assertion" (infix "===" 55) where [simp]:
  "x === n = {\<sigma>. \<sigma> x = n }"

definition is_gt :: "var \<Rightarrow> int \<Rightarrow> assertion" (infix ">>>" 55) where [simp]:
  "x >>> n = {\<sigma>. \<sigma> x > n }"

definition inc :: "var \<Rightarrow> command" ("++") where [simp]:
  "++ x = {(\<sigma>, \<sigma>') | \<sigma> \<sigma>'. \<sigma>' = \<sigma>(x := \<sigma> x + 1)}"

definition assign_const :: "var \<Rightarrow> int \<Rightarrow> command" where [simp]:
  "assign_const x n = {(\<sigma>, \<sigma>') | \<sigma> \<sigma>'. \<sigma>' = \<sigma>(x := n)}"

text \<open> Does the triple (x=n, ++x, x=n+1) hold? \<close>
theorem "pc(x===n, ++x, x===n+1)" by auto
theorem "sil(x===n, ++x, x===n+1)" by auto
theorem "nt(x===n, ++x, x===n+1)" by auto
theorem "il(x===n, ++x, x===n+1)"
  apply simp 
  apply (metis fun_upd_same fun_upd_triv fun_upd_upd)
  done

text \<open> Does the triple (x>n, ++x, x>n+1) hold? \<close>
theorem "pc(x>>>n, ++x, x>>>n+1)" by auto
theorem "sil(x>>>n, ++x, x>>>n+1)" by auto
theorem "nt(x>>>n, ++x, x>>>n+1)" by auto
theorem "il(x>>>n, ++x, x>>>n+1)"
  apply clarsimp
  apply (rule_tac x="\<sigma>'(x := \<sigma>' x - 1)" in exI)
  apply auto
  done

text \<open> Does the triple (x>2, assign x 5, x==5) hold? \<close>
theorem "pc(x>>>2, assign_const x 5, x===5)" by auto
theorem "sil(x>>>2, assign_const x 5, x===5)" by auto
theorem "il(x>>>2, assign_const x 5, x===5)" by force
theorem "nt(x>>>2, assign_const x 5, x===5) \<longrightarrow> False" by auto

text \<open> Does the triple (x>2, assign x n, x==n) hold? \<close>
theorem "pc(x>>>2, assign_const x n, x===n)" by auto
theorem "sil(x>>>2, assign_const x n, x===n)" by auto
theorem "nt(x>>>2, assign_const x n, x===n) \<longrightarrow> False" by auto
theorem "il(x>>>2, assign_const x n, x===n)"
  apply clarsimp
  apply (rule_tac x="\<sigma>'(x := 3)" in exI)
  apply auto
  done

text \<open> Does the triple (TRUE, assign x n, x==n) hold? \<close>
theorem "pc(TRUE, assign_const x n, x===n)" by auto
theorem "sil(TRUE, assign_const x n, x===n)" by auto
theorem "il(TRUE, assign_const x n, x===n)" by force
theorem "nt(TRUE, assign_const x n, x===n)" by auto

text \<open> Does the triple (x>2, assign x 5, x>3) hold? \<close>
theorem "pc(x>>>2, assign_const x 5, x>>>3)" by auto
theorem "sil(x>>>2, assign_const x 5, x>>>3)" by auto
theorem "nt(x>>>2, assign_const x 5, x>>>3) \<longrightarrow> False" by auto
theorem "il(x>>>2, assign_const x 5, x>>>3) \<longrightarrow> False" 
  apply clarsimp
  apply (rule_tac x="init(x := 4)" in exI)
  apply auto
  apply (drule fun_upd_eqD, simp)
  done

text \<open> Does the triple (TRUE, assign x n \<union> assign x m, x==n \<union> x==m) hold? \<close>
theorem "pc(TRUE, assign_const x n \<union> assign_const x m, (x===n) \<union> (x===m))" by auto
theorem "sil(TRUE, assign_const x n \<union> assign_const x m, (x===n) \<union> (x===m))" by auto
theorem "il(TRUE, assign_const x n \<union> assign_const x m, (x===n) \<union> (x===m))" by force
theorem "nt(TRUE, assign_const x n \<union> assign_const x m, (x===n) \<union> (x===m))" by auto

text \<open> Does the triple (x>n, ++x \<union> skip, x>n) hold? \<close>
theorem "pc(x>>>n, ++x \<union> skip, x>>>n)" by auto
theorem "sil(x>>>n, ++x \<union> skip, x>>>n)" by auto
theorem "nt(x>>>n, ++x \<union> skip, x>>>n)" by auto
theorem "il(x>>>n, ++x \<union> skip, x>>>n)" by auto

definition assign :: "var \<Rightarrow> (state \<Rightarrow> int) \<Rightarrow> command" where [simp]:
  "assign x e = {(\<sigma>, \<sigma>') | \<sigma> \<sigma>'. \<sigma>' = \<sigma>(x := e \<sigma>)}"

theorem "pc(Q, assign x e, {\<sigma>(x := e \<sigma>) | \<sigma>. \<sigma> \<in> Q})" by auto
theorem "sil(Q, assign x e, {\<sigma>(x := e \<sigma>) | \<sigma>. \<sigma> \<in> Q})" by auto
theorem "il(Q, assign x e, {\<sigma>(x := e \<sigma>) | \<sigma>. \<sigma> \<in> Q})" by auto
theorem "nc(Q, assign x e, {\<sigma>(x := e \<sigma>) | \<sigma>. \<sigma> \<in> Q})" oops



datatype expr =
  Num "int"
| Var "var"
| Add "expr" "expr"

fun subst_expr :: "var \<Rightarrow> expr \<Rightarrow> expr \<Rightarrow> expr"
where 
  "subst_expr x e (Num n) = Num n"
| "subst_expr x e (Var y) = (if y=x then e else Var y)"
| "subst_expr x e (Add e1 e2) = Add (subst_expr x e e1) (subst_expr x e e2)"

fun sem_expr :: "expr \<Rightarrow> state \<Rightarrow> int"
where
  "sem_expr (Num n) _ = n"
| "sem_expr (Var x) \<sigma> = \<sigma> x"
| "sem_expr (Add e1 e2) \<sigma> = sem_expr e1 \<sigma> + sem_expr e2 \<sigma>"

datatype assn =
  Conj "assn" "assn"
| TT
| Eq "expr" "expr"

fun subst :: "var \<Rightarrow> expr \<Rightarrow> assn \<Rightarrow> assn"
where 
  "subst x e (Conj Q1 Q2) = Conj (subst x e Q1) (subst x e Q2)"
| "subst x e TT = TT"
| "subst x e (Eq e1 e2) = Eq (subst_expr x e e1) (subst_expr x e e2)"

fun sem :: "assn \<Rightarrow> state set"
where
  "sem (Conj Q1 Q2) = sem Q1 \<inter> sem Q2"
| "sem TT = UNIV"
| "sem (Eq e1 e2) = { \<sigma>. sem_expr e1 \<sigma> = sem_expr e2 \<sigma> }"

lemma sem_subst_expr: "sem_expr (subst_expr x e1 e) \<sigma> = sem_expr e (\<sigma>(x := sem_expr e1 \<sigma>))" 
  by (induct e, auto)

theorem hoare_assign_pc: 
  "pc(sem(subst x e Q), assign x (sem_expr e), sem Q)"
  by (induct Q, auto simp add: sem_subst_expr)

theorem hoare_assign_sil: 
  "sil(sem(subst x e Q), assign x (sem_expr e), sem Q)" 
  by (induct Q, auto simp add: sem_subst_expr)

theorem hoare_assign_nc: 
  "nc(sem(subst x e Q), assign x (sem_expr e), sem Q)" 
  by (induct Q, auto simp add: sem_subst_expr)


type_synonym heap = "int \<Rightarrow> int option option" 
(* "Some (Some n)" means allocated *)
(* "Some None" means deallocated *)
(* "None" means never allocated *) 

type_synonym sl_state = "heap \<times> state"

type_synonym sl_assertion = "sl_state set"
type_synonym sl_command = "(sl_state \<times> sl_state) set"

definition sl_skip where [simp]:
  "sl_skip \<equiv> { (\<sigma>,\<sigma>') | \<sigma> \<sigma>'. \<sigma> = \<sigma>' }"

definition sl_alloc where [simp]:
  "sl_alloc x \<equiv> { ((h,s), (h(l := Some (Some v)), s(x := l))) | h s l v. h l \<in> {None, Some None} }"

definition sl_free where [simp]:
  "sl_free x \<equiv> { ((h,s),(h(l := Some None),s)) | h s l. s x = l \<and> h l \<notin> {None, Some None} }" 

fun sl_sil :: "(sl_assertion \<times> sl_command \<times> sl_assertion) \<Rightarrow> bool" where
  "sl_sil (P, c, Q) = (\<forall>\<sigma> \<in> P. \<exists>\<sigma>' \<in> Q. (\<sigma>, \<sigma>') \<in> c)"

fun sl_il :: "(sl_assertion \<times> sl_command \<times> sl_assertion) \<Rightarrow> bool" where
  "sl_il (P, c, Q) = (\<forall>\<sigma>'\<in> Q. \<exists>\<sigma> \<in> P. (\<sigma>, \<sigma>') \<in> c)"

definition emp where [simp]:
  "emp \<equiv> { (h,s) | h s. dom h = {} }"

definition pointsto where [simp]:
  "pointsto x v \<equiv> { (h,s) | h s. \<exists>l. s x = l \<and> dom h = {l} \<and> h l = Some (Some v) }"

definition dealloc where [simp]:
  "dealloc x \<equiv> { (h,s) | h s. \<exists>l. s x = l \<and> dom h = {l} \<and> h l = Some None }"

definition eq where [simp]:
  "eq x y \<equiv> { (h,s) | h s. s x = s y }"

lemma sil_alloc1: "sl_sil (emp, sl_alloc x, pointsto x v)"
  by (auto, metis dom_eq_singleton_conv fun_upd_same)

lemma sil_alloc2: "sl_sil (dealloc y, sl_alloc x, eq x y \<inter> pointsto x v)"
  by force

lemma sil_free: "sl_sil (pointsto x e, sl_free x, dealloc x)"
  by simp

lemma il_free: "sl_il (pointsto x e, sl_free x, dealloc x)"
  apply auto
  apply (rename_tac h' s)
  apply (rule_tac x="[s x \<mapsto> Some e]" in exI)
  apply fastforce
  done




end