(* Author: Tobias Nipkow *)

subsection "Collecting Semantics of Commands"

theory Collecting
imports Complete_Lattice Big_Step ACom
begin

subsubsection "The generic Step function"

notation
  sup (infixl ‹⊔› 65) and
  inf (infixl ‹⊓› 70) and
  bot (‹⊥›) and
  top (‹⊤›)

context
  fixes f :: "vname → aexp → 'a → 'a::sup"
  fixes g :: "bexp → 'a → 'a"
begin
fun Step :: "'a → 'a acom → 'a acom" where
"Step S (SKIP {Q}) = (SKIP {S})" |
"Step S (x ::= e {Q}) =
  x ::= e {f x e S}" |
"Step S (C1;; C2) = Step S C1;; Step (post C1) C2" |
"Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
  IF b THEN {g b S} Step P1 C1 ELSE {g (Not b) S} Step P2 C2
  {post C1 ⊔ post C2}" |
"Step S ({I} WHILE b DO {P} C {Q}) =
  {S ⊔ post C} WHILE b DO {g b I} Step P C {g (Not b) I}"
end

lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
by(induct C arbitrary: S) auto


subsubsection "Annotated commands as a complete lattice"

instantiation acom :: (order) order
begin

definition less_eq_acom :: "('a::order)acom → 'a acom → bool" where
"C1 ≤ C2 ⟷ strip C1 = strip C2 ∧ (∀p<size(annos C1). anno C1 p ≤ anno C2 p)"

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 thus ?case by(auto simp: less_eq_acom_def)
next
  case 3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
next
  case 4 thus ?case
    by(fastforce simp: le_antisym less_eq_acom_def size_annos
         eq_acom_iff_strip_anno)
qed

end

lemma less_eq_acom_annos:
  "C1 ≤ C2 ⟷ strip C1 = strip C2 ∧ list_all2 (≤) (annos C1) (annos C2)"
by(auto simp add: less_eq_acom_def anno_def list_all2_conv_all_nth size_annos_same2)

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

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

lemma Seq_le[simp]: "C1;;C2 ≤ C ⟷ (∃C1' C2'. C = C1';;C2' ∧ C1 ≤ C1' ∧ C2 ≤ C2')"
apply (cases C)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done

lemma If_le[simp]: "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')"
apply (cases C)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done

lemma While_le[simp]: "{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')"
apply (cases W)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done

lemma mono_post: "C ≤ C' ==> post C ≤ post C'"
using annos_ne[of C']
by(auto simp: post_def less_eq_acom_def last_conv_nth[OF annos_ne] anno_def
     dest: size_annos_same)

definition Inf_acom :: "com → 'a::complete_lattice acom set → 'a acom" where
"Inf_acom c M = annotate (λp. INF C∈M. anno C p) c"

global_interpretation
  Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
proof (standard, goal_cases)
  case 1 thus ?case
    by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_lower)
next
  case 2 thus ?case
    by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_greatest)
next
  case 3 thus ?case by(auto simp: Inf_acom_def)
qed


subsubsection "Collecting semantics"

definition "step = Step (λx e S. {s(x := aval e s) |s. s ∈ S}) (λb S. {s:S. bval b s})"

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

lemma mono2_Step: fixes C1 C2 :: "'a::semilattice_sup acom"
  assumes "!!x e S1 S2. S1 ≤ S2 ==> f x e S1 ≤ f x e S2"
          "!!b S1 S2. S1 ≤ S2 ==> g b S1 ≤ g b S2"
  shows "C1 ≤ C2 ==> S1 ≤ S2 ==> Step f g S1 C1 ≤ Step f g S2 C2"
proof(induction S1 C1 arbitrary: C2 S2 rule: Step.induct)
  case 1 thus ?case by(auto)
next
  case 2 thus ?case by (auto simp: assms(1))
next
  case 3 thus ?case by(auto simp: mono_post)
next
  case 4 thus ?case
    by(auto simp: subset_iff assms(2))
      (metis mono_post le_supI1 le_supI2)+
next
  case 5 thus ?case
    by(auto simp: subset_iff assms(2))
      (metis mono_post le_supI1 le_supI2)+
qed

lemma mono2_step: "C1 ≤ C2 ==> S1 ⊆ S2 ==> step S1 C1 ≤ step S2 C2"
unfolding step_def by(rule mono2_Step) 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 simp: step_def)

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 asize_nz: "asize(c::com) ≠ 0"
by (metis length_0_conv length_annos_annotate annos_ne)

lemma post_Inf_acom:
  "∀C∈M. strip C = c ==> post (Inf_acom c M) = ∩(post ` M)"
apply(subgoal_tac "∀C∈M. size(annos C) = asize c")
 apply(simp add: post_anno_asize Inf_acom_def asize_nz neq0_conv[symmetric])
apply(simp add: size_annos)
done

lemma post_lfp: "post(lfp c f) = (∩{post C|C. strip C = c ∧ f C ≤ C})"
by(auto simp add: lfp_def post_Inf_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 step_def post_def)
next
  case Assign thus ?case
    by(fastforce simp: strip_eq_Assign step_def post_def)
next
  case Seq thus ?case
    by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
next
  case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
    by (metis (lifting,full_types) mem_Collect_eq subsetD)
next
  case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
    by (metis (lifting,full_types) mem_Collect_eq subsetD)
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 simp: step_def post_def)
  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 step_def post_def)
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