Theory Extra

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Extra
imports
  "HOL-Library.Option_ord"
  "HOL-Library.Product_Lexorder"
begin

(* Extra lemmas that are not noteworthy. *)

lemma relation_mono:
  "⟦ A ⊆ C; B ⊆ D ⟧ ⟹ A × B ⊆ C × D"
  by bestsimp

lemma quotientI2:
  "⟦ x ∈ A; X = r `` {x} ⟧ ⟹ X ∈ A // r"
  by (simp add: quotientI)

(*

Concretely enumerate all the agent action functions. Can't be too
abstract here as we want extensionality.

Introduced in the clock view.

*)

definition
  listToFun :: "('a × 'b list) list ⇒ ('a ⇒ 'b) list"
where
  "listToFun xs ≡ foldr (λ(a, acts) M. [ m(a := act) . m ← M, act ← acts ])
                     xs
                     [(λ_. undefined)]"

lemma listToFun_futz:
  "⟦ M ∈ set (listToFun xs); x ∈ fst ` set xs ⟧
     ⟹ M x ∈ { y |y ys. (x, ys) ∈ set xs ∧ y ∈ set ys}"
  unfolding listToFun_def
  apply (induct xs arbitrary: M)
   apply (simp_all add: split_def)
  apply (case_tac a)
  apply clarsimp
  apply auto
  done

lemma distinct_map_fst:
  "⟦ x ∉ fst ` set xs; distinct (map fst xs) ⟧ ⟹ (x, y) ∉ set xs"
  by (induct xs) auto

lemma listToFun_futz_rev:
  "⟦ ⋀x. M x ∈ (if x ∈ fst ` set xs then { y |y ys. (x, ys) ∈ set xs ∧ y ∈ set ys} else {undefined}); distinct (map fst xs) ⟧
      ⟹ M ∈ set (listToFun xs)"
proof(induct xs arbitrary: M)
  case Nil thus ?case
    unfolding listToFun_def by simp
next
  case (Cons x xs)
  let ?M' = "M(fst x := undefined)"
  have M': "?M' ∈ set (listToFun xs)"
    apply (rule Cons.hyps)
     prefer 2
     using Cons(3)
     apply simp
    apply (case_tac "xa = fst x")
     using Cons(3)
     apply simp
    apply (case_tac "xa ∈ fst ` set xs")
     apply (cut_tac x=xa in Cons(2))
     apply (cases x)
     apply auto[1]
    apply (cut_tac x=xa in Cons(2))
    apply simp
    done
  then show ?case
    unfolding listToFun_def
    apply (cases x)
    apply simp
    apply (rule bexI[where x="?M'"])
     apply simp_all
    apply (rule_tac x="M a" in image_eqI)
     apply simp
    apply (cut_tac x=a in Cons(2))
    using Cons(3)
    apply clarsimp
    apply (erule disjE)
     apply simp
    apply (auto dest: distinct_map_fst)
    done
qed

definition
  listToFuns :: "('a ⇒ 'b list) ⇒ 'a list ⇒ ('a ⇒ 'b) list"
where
  "listToFuns f ≡ listToFun ∘ map (λx. (x, f x))"

lemma map_id_clunky:
  "set xs = UNIV ⟹ x ∈ fst ` set (map (λx. (x, f x)) xs)"
  apply (simp only: set_map[symmetric] map_map)
  apply simp
  done

(*

The main result is that we can freely move between representations.

*)

lemma listToFuns_ext:
  assumes xs: "set xs = UNIV"
  assumes d: "distinct xs"
  shows "g ∈ set (listToFuns f xs) ⟷ (∀x. g x ∈ set (f x))"
  unfolding listToFuns_def
  apply simp
  apply rule
   apply clarsimp
   apply (cut_tac x=x in listToFun_futz[where M=g, OF _ map_id_clunky[OF xs]])
    apply simp
   apply clarsimp
  apply (rule listToFun_futz_rev)
   using map_id_clunky[OF xs]
   apply auto[1]
   apply (rule_tac x="f xa" in exI)
    apply simp
   apply simp
  using d
  apply (simp add: distinct_map)
  apply (auto intro: inj_onI)
  done

lemma listToFun_splice:
  assumes xs: "set xs = UNIV"
  assumes d: "distinct xs"
  assumes g: "g ∈ set (listToFuns f xs)"
  assumes h: "h ∈ set (listToFuns f xs)"
  shows "g(x := h x) ∈ set (listToFuns f xs)"
  using g h by (auto iff: listToFuns_ext[OF xs d])
(*<*)

end
(*>*)