Theory Collecting

section "Collecting Semantics of Commands"

theory Collecting
imports Complete_Lattice_ix ACom
begin

subsection "Annotated commands as a complete lattice"

(* Orderings could also be lifted generically (thus subsuming the
instantiation for preord and order), but then less_eq_acom would need to
become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would
need to unfold this defn first. *)

instantiation acom :: (order) order
begin

fun less_eq_acom :: "('a::order)acom ⇒ 'a acom ⇒ bool" where
"(SKIP {S}) ≤ (SKIP {S'}) = (S ≤ S')" |
"(x ::= e {S}) ≤ (x' ::= e' {S'}) = (x=x' ∧ e=e' ∧ S ≤ S')" |
"(c1;;c2) ≤ (c1';;c2') = (c1 ≤ c1' ∧ c2 ≤ c2')" |
"(IF b THEN c1 ELSE c2 {S}) ≤ (IF b' THEN c1' ELSE c2' {S'}) =
  (b=b' ∧ c1 ≤ c1' ∧ c2 ≤ c2' ∧ S ≤ S')" |
"({Inv} WHILE b DO c {P}) ≤ ({Inv'} WHILE b' DO c' {P'}) =
  (b=b' ∧ c ≤ c' ∧ Inv ≤ Inv' ∧ P ≤ P')" |
"less_eq_acom _ _ = False"

lemma SKIP_le: "SKIP {S} ≤ c ⟷ (∃S'. c = SKIP {S'} ∧ S ≤ S')"
by (cases c) auto

lemma Assign_le: "x ::= e {S} ≤ c ⟷ (∃S'. c = x ::= e {S'} ∧ S ≤ S')"
by (cases c) auto

lemma Seq_le: "c1;;c2 ≤ c ⟷ (∃c1' c2'. c = c1';;c2' ∧ c1 ≤ c1' ∧ c2 ≤ c2')"
by (cases c) auto

lemma If_le: "IF b THEN c1 ELSE c2 {S} ≤ c ⟷
  (∃c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} ∧ c1 ≤ c1' ∧ c2 ≤ c2' ∧ S ≤ S')"
by (cases c) auto

lemma While_le: "{Inv} WHILE b DO c {P} ≤ w ⟷
  (∃Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} ∧ c ≤ c' ∧ Inv ≤ Inv' ∧ P ≤ P')"
by (cases w) auto

definition less_acom :: "'a acom ⇒ 'a acom ⇒ bool" where
"less_acom x y = (x ≤ y ∧ ¬ y ≤ x)"

instance
proof (standard,goal_cases)
  case 1 show ?case by(simp add: less_acom_def)
next
  case (2 x) thus ?case by (induct x) auto
next
  case (3 x y z) thus ?case
  apply(induct x y arbitrary: z rule: less_eq_acom.induct)
  apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le)
  done
next
  case (4 x y) thus ?case
  apply(induct x y rule: less_eq_acom.induct)
  apply (auto intro: le_antisym)
  done
qed

end

fun sub⇩1 :: "'a acom ⇒ 'a acom" where
"sub⇩1(c1;;c2) = c1" |
"sub⇩1(IF b THEN c1 ELSE c2 {S}) = c1" |
"sub⇩1({I} WHILE b DO c {P}) = c"

fun sub⇩2 :: "'a acom ⇒ 'a acom" where
"sub⇩2(c1;;c2) = c2" |
"sub⇩2(IF b THEN c1 ELSE c2 {S}) = c2"

fun invar :: "'a acom ⇒ 'a" where
"invar({I} WHILE b DO c {P}) = I"

fun lift :: "('a set ⇒ 'b) ⇒ com ⇒ 'a acom set ⇒ 'b acom"
where
"lift F com.SKIP M = (SKIP {F (post ` M)})" |
"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
"lift F (c1;;c2) M =
  lift F c1 (sub⇩1 ` M);; lift F c2 (sub⇩2 ` M)" |
"lift F (IF b THEN c1 ELSE c2) M =
  IF b THEN lift F c1 (sub⇩1 ` M) ELSE lift F c2 (sub⇩2 ` M)
  {F (post ` M)}" |
"lift F (WHILE b DO c) M =
 {F (invar ` M)}
 WHILE b DO lift F c (sub⇩1 ` M)
 {F (post ` M)}"

global_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
proof (standard,goal_cases)
  case (1 A _ a)
  have "a:A ⟹ lift Inter (strip a) A ≤ a"
  proof(induction a arbitrary: A)
    case Seq from Seq.prems show ?case by(force intro!: Seq.IH)
  next
    case If from If.prems show ?case by(force intro!: If.IH)
  next
    case While from While.prems show ?case by(force intro!: While.IH)
  qed force+
  with 1 show ?case by auto
next
  case (2 b i A)
  thus ?case
  proof(induction b arbitrary: i A)
    case SKIP thus ?case by (force simp:SKIP_le)
  next
    case Assign thus ?case by (force simp:Assign_le)
  next
    case Seq from Seq.prems show ?case
      by (force intro!: Seq.IH simp:Seq_le)
  next
    case If from If.prems show ?case by (force simp: If_le intro!: If.IH)
  next
    case While from While.prems show ?case
      by(fastforce simp: While_le intro: While.IH)
  qed
next
  case (3 A i)
  have "strip(lift Inter i A) = i"
  proof(induction i arbitrary: A)
    case Seq from Seq.prems show ?case
      by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
  next
    case If from If.prems show ?case
      by (fastforce intro!: If.IH simp: strip_eq_If)
  next
    case While from While.prems show ?case
      by(fastforce intro: While.IH simp: strip_eq_While)
  qed auto
  thus ?case by auto
qed

lemma le_post: "c ≤ d ⟹ post c ≤ post d"
by(induction c d rule: less_eq_acom.induct) auto

subsection "Collecting semantics"

fun step :: "state set ⇒ state set acom ⇒ state set acom" where
"step S (SKIP {P}) = (SKIP {S})" |
"step S (x ::= e {P}) =
  (x ::= e {{s'. ∃s∈S. s' = s(x := aval e s)}})" |
"step S (c1;; c2) = step S c1;; step (post c1) c2" |
"step S (IF b THEN c1 ELSE c2 {P}) =
   IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. ¬ bval b s} c2
   {post c1 ∪ post c2}" |
"step S ({Inv} WHILE b DO c {P}) =
  {S ∪ post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. ¬ bval b s}}"

definition CS :: "com ⇒ state set acom" where
"CS c = lfp (step UNIV) c"

lemma mono2_step: "c1 ≤ c2 ⟹ S1 ⊆ S2 ⟹ step S1 c1 ≤ step S2 c2"
proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
  case 2 thus ?case by fastforce
next
  case 3 thus ?case by(simp add: le_post)
next
  case 4 thus ?case by(simp add: subset_iff)(metis le_post subsetD)+
next
  case 5 thus ?case by(simp add: subset_iff) (metis le_post subsetD)
qed auto

lemma mono_step: "mono (step S)"
by(blast intro: monoI mono2_step)

lemma strip_step: "strip(step S c) = strip c"
by (induction c arbitrary: S) auto

lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)"
apply(rule lfp_unfold[OF _  mono_step])
apply(simp add: strip_step)
done

lemma CS_unfold: "CS c = step UNIV (CS c)"
by (metis CS_def lfp_cs_unfold)

lemma strip_CS[simp]: "strip(CS c) = c"
by(simp add: CS_def index_lfp[simplified])

end