Theory Restrict_Bounds_Impl

(*<*)
theory Restrict_Bounds_Impl
imports Restrict_Bounds
begin
(*>*)

section ‹Refining the Non-Deterministic @{term simplification.rb} Function›

fun gen_size where
  "gen_size (Bool b) = 1"
| "gen_size (Eq x t) = 1"
| "gen_size (Pred p ts) = 1"
| "gen_size (Neg (Neg Q)) = Suc (gen_size Q)"
| "gen_size (Neg (Conj Q1 Q2)) = Suc (Suc (gen_size (Neg Q1) + gen_size (Neg Q2)))"
| "gen_size (Neg (Disj Q1 Q2)) = Suc (Suc (gen_size (Neg Q1) + gen_size (Neg Q2)))"
| "gen_size (Neg Q) = Suc (gen_size Q)"
| "gen_size (Conj Q1 Q2) = Suc (gen_size Q1 + gen_size Q2)"
| "gen_size (Disj Q1 Q2) = Suc (gen_size Q1 + gen_size Q2)"
| "gen_size (Exists x Q) = Suc (gen_size Q)"


function (sequential) gen_impl where
  "gen_impl x (Bool False) = [{}]"
| "gen_impl x (Bool True) = []"
| "gen_impl x (Eq y (Const c)) = (if x = y then [{Eq y (Const c)}] else [])"
| "gen_impl x (Eq y (Var z)) = []"
| "gen_impl x (Pred p ts) = (if x ∈ fv_terms_set ts then [{Pred p ts}] else [])"
| "gen_impl x (Neg (Neg Q)) = gen_impl x Q"
| "gen_impl x (Neg (Conj Q1 Q2)) = gen_impl x (Disj (Neg Q1) (Neg Q2))"
| "gen_impl x (Neg (Disj Q1 Q2)) = gen_impl x (Conj (Neg Q1) (Neg Q2))"
| "gen_impl x (Neg _) = []"
| "gen_impl x (Disj Q1 Q2) =  [G1 ∪ G2. G1 ← gen_impl x Q1, G2 ← gen_impl x Q2]"
| "gen_impl x (Conj Q1 (y ≈ z)) = (if x = y then List.union (gen_impl x Q1) (map (image (λQ. cp (Q[z ❙→ x]))) (gen_impl z Q1))
     else if x = z then List.union (gen_impl x Q1) (map (image (λQ. cp (Q[y ❙→ x]))) (gen_impl y Q1))
     else gen_impl x Q1)"|
 "gen_impl x (Conj Q1 Q2) = List.union (gen_impl x Q1) (gen_impl x Q2)"
| "gen_impl x (Exists y Q) = (if x = y then [] else map (image (exists y)) (gen_impl x Q))"
  by pat_completeness auto
termination by (relation "measure (λ(x, Q). gen_size Q)") simp_all

lemma gen_impl_gen: "G ∈ set (gen_impl x Q) ⟹ gen x Q G"
  by (induct x Q arbitrary: G rule: gen_impl.induct)
    (auto 5 2 simp: fv_terms_set_def intro: gen.intros simp: image_iff split: if_splits)

lemma gen_gen_impl: "gen x Q G ⟹ G ∈ set (gen_impl x Q)"
proof (induct x Q G rule: gen.induct)
  case (7 x Q1 G Q2)
  then show ?case
  proof (cases Q2)
    case (Eq x t)
    with 7 show ?thesis
      by (cases t) auto
  qed auto
qed (auto elim!: ap.cases simp: image_iff)

lemma set_gen_impl: "set (gen_impl x Q) = {G. gen x Q G}"
  by (auto simp: gen_impl_gen gen_gen_impl)

definition "flat xss = fold List.union xss []"

(*much faster than fun*)
primrec cov_impl where
  "cov_impl x (Bool b) = [{}]"
| "cov_impl x (Eq y t) = (case t of
      Const c ⇒ [if x = y then {Eq y (Const c)} else {}]
    | Var z ⇒ [if x = y ∧ x ≠ z then {x ≈ z} 
                else if x = z ∧ x ≠ y then {x ≈ y}
                else {}])"
| "cov_impl x (Pred p ts) = [if x ∈ fv_terms_set ts then {Pred p ts} else {}]"
| "cov_impl x (Neg Q) = cov_impl x Q"
| "cov_impl x (Disj Q1 Q2) = (case (cp (Q1 ❙⊥ x), cp (Q2 ❙⊥ x)) of
     (Bool True, Bool True) ⇒ List.union (cov_impl x Q1) (cov_impl x Q2)
   | (Bool True, _) ⇒ cov_impl x Q1
   | (_, Bool True) ⇒ cov_impl x Q2
   | (_, _) ⇒ [G1 ∪ G2. G1 ← cov_impl x Q1, G2 ← cov_impl x Q2])"
| "cov_impl x (Conj Q1 Q2) = (case (cp (Q1 ❙⊥ x), cp (Q2 ❙⊥ x)) of
     (Bool False, Bool False) ⇒ List.union (cov_impl x Q1) (cov_impl x Q2)
   | (Bool False, _) ⇒ cov_impl x Q1
   | (_, Bool False) ⇒ cov_impl x Q2
   | (_, _) ⇒ [G1 ∪ G2. G1 ← cov_impl x Q1, G2 ← cov_impl x Q2])"
| "cov_impl x (Exists y Q) = (if x = y then [{}] else flat (map (λG.
     (if x ≈ y ∈ G then [exists y ` (G - {x ≈ y}) ∪ (λQ. cp (Q[y ❙→ x])) ` G'. G' ← gen_impl y Q]
      else [exists y ` G])) (cov_impl x Q)))"

lemma union_empty_iff: "List.union xs ys = [] ⟷ xs = [] ∧ ys = []"
  by (induct xs arbitrary: ys) (force simp: List.union_def List.insert_def)+

lemma fold_union_empty_iff: "fold List.union xss ys = [] ⟷ (∀xs ∈ set xss. xs = []) ∧ ys = []"
  by (induct xss arbitrary: ys) (auto simp: union_empty_iff)

lemma flat_empty_iff: "flat xss = [] ⟷ (∀xs ∈ set xss. xs = [])"
  by (auto simp: flat_def fold_union_empty_iff)

lemma set_fold_union: "set (fold List.union xss ys) = (⋃ (set ` set xss)) ∪ set ys"
  by (induct xss arbitrary: ys) auto

lemma set_flat: "set (flat xss) = ⋃ (set ` set xss)"
  unfolding flat_def by (auto simp: set_fold_union)

lemma rrb_cov_impl: "rrb Q ⟹ cov_impl x Q ≠ []"
proof (induct Q arbitrary: x)
  case (Exists y Q)
  then show ?case
    by (cases "∃G ∈ set (cov_impl x Q). x ≈ y ∈ G")
      (auto simp: flat_empty_iff image_iff dest: gen_gen_impl intro!: UnI1 bexI[rotated])
qed (auto split: term.splits fmla.splits bool.splits simp: union_empty_iff)

lemma cov_Eq_self: "cov x (y ≈ y) {}"
  by (metis Un_absorb cov.Eq_self cov.nonfree fv.simps(3) fv_term_set.simps(1) singletonD)

lemma cov_impl_cov: "G ∈ set (cov_impl x Q) ⟹ cov x Q G"
proof (induct Q arbitrary: x G)
  case (Eq y t)
  then show ?case
    by (auto simp: cov_Eq_self intro: cov.intros ap.intros split: term.splits)
qed (auto simp: set_flat set_gen_impl intro: cov.intros ap.intros
  split: term.splits fmla.splits bool.splits if_splits)

definition "fixbound_impl 𝒬 x = filter (λQ. x ∈ fv Q ∧ gen_impl x Q = []) (sorted_list_of_set 𝒬)"

lemma set_fixbound_impl: "finite 𝒬 ⟹ set (fixbound_impl 𝒬 x) = fixbound 𝒬 x"
  by (auto simp: fixbound_def nongens_def fixbound_impl_def set_gen_impl
    dest: arg_cong[of _ _ set] simp flip: List.set_empty)

lemma fixbound_empty_iff: "finite 𝒬 ⟹ fixbound 𝒬 x ≠ {} ⟷ fixbound_impl 𝒬 x ≠ []"
  by (auto simp: set_fixbound_impl dest: arg_cong[of _ _ set] simp flip: List.set_empty)

lemma fixbound_impl_hd_in: "finite 𝒬 ⟹ fixbound_impl 𝒬 x = y # ys ⟹ y ∈ 𝒬"
  by (auto simp: fixbound_impl_def dest!: arg_cong[of _ _ set])

fun (in simplification) rb_impl :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ ('a, 'b) fmla nres" where
  "rb_impl (Neg Q) = do { Q' ← rb_impl Q; RETURN (simp (Neg Q'))}"
| "rb_impl (Disj Q1 Q2) = do { Q1' ← rb_impl Q1; Q2' ← rb_impl Q2; RETURN (simp (Disj Q1' Q2'))}"
| "rb_impl (Conj Q1 Q2) = do { Q1' ← rb_impl Q1; Q2' ← rb_impl Q2; RETURN (simp (Conj Q1' Q2'))}"
| "rb_impl (Exists x Q) = do {
    Q' ← rb_impl Q;
    𝒬 ← WHILE
      (λ𝒬. fixbound_impl 𝒬 x ≠ []) (λ𝒬. do {
        Qfix ← RETURN (hd (fixbound_impl 𝒬 x));
        G ← RETURN (hd (cov_impl x Qfix));
        RETURN (𝒬 - {Qfix} ∪
          {simp (Conj Qfix (DISJ (qps G)))} ∪
          (⋃y ∈ eqs x G. {cp (Qfix[x ❙→ y])}) ∪
          {cp (Qfix ❙⊥ x)})})
      (flat_Disj Q');
    RETURN (simp (DISJ (exists x ` 𝒬)))}"
| "rb_impl Q = do { RETURN (simp Q) }"

lemma (in simplification) rb_impl_refines_rb: "rb_impl Q ≤ rb Q"
  apply (induct Q)
  apply (unfold rb.simps rb_impl.simps)
  apply refine_mono
  apply refine_mono
  apply refine_mono
  apply refine_mono
  apply refine_mono
  apply refine_mono
  apply refine_mono
  subgoal for x Q' Q
    apply (rule order_trans[OF WHILE_le_WHILEI[where I="rb_INV x Q"]])
    apply (rule order_trans[OF WHILEI_le_WHILEIT])
    apply (rule WHILEIT_refine[OF _ _ _ refine_IdI, THEN refine_IdD])
       apply (simp_all add: fixbound_empty_iff) [3]
    apply refine_mono
      apply (auto simp flip: set_fixbound_impl simp: neq_Nil_conv fixbound_impl_hd_in
        intro!: cov_impl_cov rrb_cov_impl hd_in_set rb_INV_rrb)
    done
  done

fun (in simplification) rb_impl_det :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ ('a, 'b) fmla dres" where
  "rb_impl_det (Neg Q) = do { Q' ← rb_impl_det Q; dRETURN (simp (Neg Q'))}"
| "rb_impl_det (Disj Q1 Q2) = do { Q1' ← rb_impl_det Q1; Q2' ← rb_impl_det Q2; dRETURN (simp (Disj Q1' Q2'))}"
| "rb_impl_det (Conj Q1 Q2) = do { Q1' ← rb_impl_det Q1; Q2' ← rb_impl_det Q2; dRETURN (simp (Conj Q1' Q2'))}"
| "rb_impl_det (Exists x Q) = do {
    Q' ← rb_impl_det Q;
    𝒬 ← dWHILE
      (λ𝒬. fixbound_impl 𝒬 x ≠ []) (λ𝒬. do {
        Qfix ← dRETURN (hd (fixbound_impl 𝒬 x));
        G ← dRETURN (hd (cov_impl x Qfix));
        dRETURN (𝒬 - {Qfix} ∪
          {simp (Conj Qfix (DISJ (qps G)))} ∪
          (⋃y ∈ eqs x G. {cp (Qfix[x ❙→ y])}) ∪
          {cp (Qfix ❙⊥ x)})})
      (flat_Disj Q');
    dRETURN (simp (DISJ (exists x ` 𝒬)))}"
| "rb_impl_det Q = do { dRETURN (simp Q) }"

lemma (in simplification) rb_impl_det_refines_rb_impl: "nres_of (rb_impl_det Q) ≤ rb_impl Q"
  by (induct Q; unfold rb_impl.simps rb_impl_det.simps) refine_transfer+

lemmas (in simplification) RB_correct =
  rb_impl_det_refines_rb_impl[THEN order_trans, OF
  rb_impl_refines_rb[THEN order_trans, OF
  rb_correct]]

(*<*)
end
(*>*)