Theory Collecting

theory Collecting
imports Complete_Lattice Big_Step ACom
begin

subsection "Collecting Semantics of Commands"

subsubsection "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 {P}) ≤ (SKIP {P'}) = (P ≤ P')" |
"(x ::= e {P}) ≤ (x' ::= e' {P'}) = (x=x' ∧ e=e' ∧ P ≤ P')" |
"(C1;C2) ≤ (C1';C2') = (C1 ≤ C1' ∧ C2 ≤ C2')" |
"(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) ≤ (IF b' THEN {P1'} C1' ELSE {P2'} C2' {Q'}) =
  (b=b' ∧ P1 ≤ P1' ∧ C1 ≤ C1' ∧ P2 ≤ P2' ∧ C2 ≤ C2' ∧ Q ≤ Q')" |
"({I} WHILE b DO {P} C {Q}) ≤ ({I'} WHILE b' DO {P'} C' {Q'}) =
  (b=b' ∧ C ≤ C' ∧ I ≤ I' ∧ P ≤ P' ∧ Q ≤ Q')" |
"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 {p1} C1 ELSE {p2} C2 {S} ≤ C <->
  (∃p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} ∧
     p1 ≤ p1' ∧ p2 ≤ p2' ∧ C1 ≤ C1' ∧ C2 ≤ C2' ∧ S ≤ S')"
by (cases C) auto

lemma While_le: "{I} WHILE b DO {p} C {P} ≤ W <->
  (∃I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} ∧ C ≤ C' ∧ p ≤ p' ∧ I ≤ I' ∧ 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
  case goal1 show ?case by(simp add: less_acom_def)
next
  case goal2 thus ?case by (induct x) auto
next
  case goal3 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 goal4 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 {P1} C1 ELSE {P2} C2 {Q}) = C1" |
"sub⇣1({I} WHILE b DO {P} C {Q}) = C"

fun sub⇣2 :: "'a acom => 'a acom" where
"sub⇣2(C1;C2) = C2" |
"sub⇣2(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = C2"

fun anno⇣1 :: "'a acom => 'a" where
"anno⇣1(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = P1" |
"anno⇣1({I} WHILE b DO {P} C {Q}) = I"

fun anno⇣2 :: "'a acom => 'a" where
"anno⇣2(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = P2" |
"anno⇣2({I} WHILE b DO {P} C {Q}) = P"


fun Union_acom :: "com => 'a acom set => 'a set acom" where
"Union_acom com.SKIP M = (SKIP {post ` M})" |
"Union_acom (x ::= a) M = (x ::= a {post ` M})" |
"Union_acom (c1;c2) M =
  Union_acom c1 (sub⇣1 ` M); Union_acom c2 (sub⇣2 ` M)" |
"Union_acom (IF b THEN c1 ELSE c2) M =
  IF b THEN {anno⇣1 ` M} Union_acom c1 (sub⇣1 ` M) ELSE {anno⇣2 ` M} Union_acom c2 (sub⇣2 ` M)
  {post ` M}" |
"Union_acom (WHILE b DO c) M =
 {anno⇣1 ` M}
 WHILE b DO {anno⇣2 ` M} Union_acom c (sub⇣1 ` M)
 {post ` M}"

interpretation
  Complete_Lattice "{C. strip C = c}" "map_acom Inter o (Union_acom c)" for c
proof
  case goal1
  have "a:A ==> map_acom Inter (Union_acom (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 goal1 show ?case by auto
next
  case goal2
  thus ?case
  proof(simp, induction b arbitrary: c 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 goal3
  have "strip(Union_acom c A) = c"
  proof(induction c 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


subsubsection "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(x := aval e s) |s. s : S}}" |
"step S (C1; C2) = step S C1; step (post C1) C2" |
"step S (IF b THEN {P1} C1 ELSE {P2} C2 {P}) =
  IF b THEN {{s:S. bval b s}} step P1 C1 ELSE {{s:S. ¬ bval b s}} step P2 C2
  {post C1 ∪ post C2}" |
"step S ({I} WHILE b DO {P} C {P'}) =
  {S ∪ post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. ¬ bval b s}}"

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

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 set_mp)+
next
  case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
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 c (step S) = step S (lfp c (step S))"
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])


subsubsection "Relation to big-step semantics"

lemma post_Union_acom: "∀ c' ∈ M. strip c' = c ==> post (Union_acom c M) = post ` M"
proof(induction c arbitrary: M)
  case (Seq c1 c2)
  have "post ` M = post ` sub⇣2 ` M" using Seq.prems by (force simp: strip_eq_Seq)
  moreover have "∀ c' ∈ sub⇣2 ` M. strip c' = c2" using Seq.prems by (auto simp: strip_eq_Seq)
  ultimately show ?case using Seq.IH(2)[of "sub⇣2 ` M"] by simp
qed simp_all


lemma post_lfp: "post(lfp c f) = (\<Inter>{post C|C. strip C = c ∧ f C ≤ C})"
by(auto simp add: lfp_def post_Union_acom)

lemma big_step_post_step:
  "[| (c, s) => t;  strip C = c;  s ∈ S;  step S C ≤ C |] ==> t ∈ post C"
proof(induction arbitrary: C S rule: big_step_induct)
  case Skip thus ?case by(auto simp: strip_eq_SKIP)
next
  case Assign thus ?case by(fastforce simp: strip_eq_Assign)
next
  case Seq thus ?case by(fastforce simp: strip_eq_Seq)
next
  case IfTrue thus ?case apply(auto simp: strip_eq_If)
    by (metis (lifting) mem_Collect_eq set_mp)
next
  case IfFalse thus ?case apply(auto simp: strip_eq_If)
    by (metis (lifting) mem_Collect_eq set_mp)
next
  case (WhileTrue b s1 c' s2 s3)
  from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
    by(auto simp: strip_eq_While)
  from WhileTrue.prems(3) `C = _`
  have "step P C' ≤ C'"  "{s ∈ I. bval b s} ≤ P"  "S ≤ I"  "step (post C') C ≤ C"  by auto
  have "step {s ∈ I. bval b s} C' ≤ C'"
    by (rule order_trans[OF mono2_step[OF order_refl `{s ∈ I. bval b s} ≤ P`] `step P C' ≤ C'`])
  have "s1: {s:I. bval b s}" using `s1 ∈ S` `S ⊆ I` `bval b s1` by auto
  note s2_in_post_C' = WhileTrue.IH(1)[OF `strip C' = c'` this `step {s ∈ I. bval b s} C' ≤ C'`]
  from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' `step (post C') C ≤ C`]
  show ?case .
next
  case (WhileFalse b s1 c') thus ?case by (force simp: strip_eq_While)
qed

lemma big_step_lfp: "[| (c,s) => t;  s ∈ S |] ==> t ∈ post(lfp c (step S))"
by(auto simp add: post_lfp intro: big_step_post_step)

lemma big_step_CS: "(c,s) => t ==> t : post(CS c)"
by(simp add: CS_def big_step_lfp)

end