Theory Multiset_Extension_Impl

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2011-2015)
Author:  Guillaume Allais (2011)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Multiset_Extension_Impl
imports 
  Multiset_Extension2 
  "../Orderings/List_Order_Impl"
  Multiset_Extension_Pair_Impl
begin

(**
We use the lifting when it is sufficient to prove the non-strict
domination to also prove the strict one. For example if [a > x] then
it is sufficient to prove that [A ≥ X] to get [A + {#a#} > X + {#x#}]
**)

lemma mul_ext_list_ext: "∃ s ns. list_order_extension_impl s ns mul_ext"
proof(intro exI)
  let ?s = "λ s ns. {(as,bs). (mset as, mset bs) ∈ s_mul_ext ns s}"
  let ?ns = "λ s ns. {(as,bs). (mset as, mset bs) ∈ ns_mul_ext ns s}" 
  let ?m = mset
  show "list_order_extension_impl ?s ?ns mul_ext"
  proof
    fix s ns
    show "?s {(a,b). s a b} {(a,b). ns a b} = {(as,bs). fst (mul_ext (λ a b. (s a b, ns a b)) as bs)}"
      unfolding mul_ext_def Let_def by auto
  next
    fix s ns
    show "?ns {(a,b). s a b} {(a,b). ns a b} = {(as,bs). snd (mul_ext (λ a b. (s a b, ns a b)) as bs)}"
      unfolding mul_ext_def Let_def by auto
  next
    fix s ns s' ns' as bs
    assume "set as × set bs ∩ ns ⊆ ns'"
           "set as × set bs ∩ s ⊆ s'"
           "(as,bs) ∈ ?s s ns"
    thus "(as,bs) ∈ ?s s' ns'"
      using s_mul_ext_local_mono[of "?m as" "?m bs" ns ns' s s']
      unfolding set_mset_mset by auto
  next
    fix s ns s' ns' as bs
    assume "set as × set bs ∩ ns ⊆ ns'"
           "set as × set bs ∩ s ⊆ s'"
           "(as,bs) ∈ ?ns s ns"
    thus "(as,bs) ∈ ?ns s' ns'"
      using ns_mul_ext_local_mono[of "?m as" "?m bs" ns ns' s s']
      unfolding set_mset_mset by auto
  qed
qed

context fixes sns :: "'a ⇒ 'a ⇒ bool × bool"
begin

fun mul_ext_impl :: "'a list ⇒ 'a list ⇒ bool × bool"
and mul_ex_dom :: "'a list ⇒ 'a list ⇒ 'a ⇒ 'a list ⇒ bool × bool"
where
  "mul_ext_impl [] []       = (False, True)"
| "mul_ext_impl [] ys       = (False, False)"
| "mul_ext_impl xs []       = (True, True)"
| "mul_ext_impl xs (y # ys) = mul_ex_dom xs [] y ys"

| "mul_ex_dom []       xs' y ys = (False, False)"
| "mul_ex_dom (x # xs) xs' y ys =
    (case sns x y of
      (True, _) ⇒ if snd (mul_ext_impl (xs @ xs') (filter (λy. ¬ fst (sns x y)) ys)) then (True, True)
                   else mul_ex_dom xs (x # xs') y ys
    | (False, True) ⇒ or2 (mul_ext_impl (xs @ xs') ys) (mul_ex_dom xs (x # xs') y ys)
    | _ ⇒ mul_ex_dom xs (x # xs') y ys)"

end

lemma mul_ext_impl_sound0:
  "mul_ext_impl sns xs ys = mult2_impl (λx y. sns y x) ys xs"
  "mul_ex_dom sns xs xs' y ys = mult2_ex_dom (λx y. sns y x) y ys xs xs'"
by (induct xs ys and xs xs' y ys taking: sns rule: mul_ext_impl_mul_ex_dom.induct)
  (auto split: prod.splits bool.splits)

definition cond1 where
  "cond1 f bs y xs ys ≡
  ((∃b. b ∈ set bs ∧ fst (f b y) ∧ snd (mul_ext f (remove1 b xs) [y←ys . ¬ fst (f b y)]))
  ∨ (∃b. b ∈ set bs ∧ snd (f b y) ∧ fst (mul_ext f (remove1 b xs) ys)))"

lemma cond1_propagate:
  assumes "cond1 f bs y xs ys"
  shows "cond1 f (b # bs) y xs ys"
using assms unfolding cond1_def by auto

definition cond2 where
  "cond2 f bs y xs ys ≡ (cond1 f bs y xs ys
  ∨ (∃b. b ∈ set bs ∧ snd (f b y) ∧ snd (mul_ext f (remove1 b xs) ys)))"

lemma cond2_propagate:
  assumes "cond2 f bs y xs ys"
  shows "cond2 f (b # bs) y xs ys"
using assms and cond1_propagate[of f bs y xs ys]
unfolding cond2_def by auto

lemma cond1_cond2:
  assumes "cond1 f bs y xs ys"
  shows "cond2 f bs y xs ys"
using assms unfolding cond2_def by simp

lemma mul_ext_impl_sound:
  shows "mul_ext_impl f xs ys = mul_ext f xs ys"
unfolding mul_ext_def s_mul_ext_def ns_mul_ext_def
by (auto simp: Let_def converse_def mul_ext_impl_sound0 mult2_impl_sound)

lemma [code]: "mul_ext = mul_ext_impl"
  by (intro ext, unfold mul_ext_impl_sound, auto)

lemma mul_ext_impl_cong[fundef_cong]:
  assumes "⋀x x'. x ∈ set xs ⟹ x' ∈ set ys ⟹ f x x' = g x x'"
  shows "mul_ext_impl f xs ys = mul_ext_impl g xs ys"
using assms
 stri_mul_ext_map[of xs ys g f id] nstri_mul_ext_map[of xs ys g f id]
 stri_mul_ext_map[of xs ys f g id] nstri_mul_ext_map[of xs ys f g id]
by (auto simp: mul_ext_impl_sound mul_ext_def Let_def)

end