# Theory Extra

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

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"

(*

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 (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 (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
(*>*)
```