# Theory Base

```section "Base"

theory Base
imports PermutationLemmas
begin

subsection "Integrate with Isabelle libraries?"

― ‹Misc›

― ‹FIXME added by tjr, forms basis of a lot of proofs of existence of inf sets›
― ‹something like this should be in FiniteSet, asserting nats are not finite›
lemma natset_finite_max: assumes a: "finite A"
shows "Suc (Max A) ∉ A"
proof (cases "A = {}")
case True
thus ?thesis by auto
next
case False
with a have "Max A ∈ A ∧ (∀s ∈ A. s ≤ Max A)" by simp
thus ?thesis by auto
qed

― ‹not used›
lemma not_finite_univ: "~ finite (UNIV::nat set)"
apply rule
apply(drule_tac natset_finite_max)
by force

― ‹FIXME should be in main lib›
lemma LeastI_ex: "(∃ x. P (x::'a::wellorder)) ⟹ P (LEAST x. P x)"
by(blast intro: LeastI)

subsection "Summation"

primrec summation :: "(nat ⇒ nat) ⇒ nat ⇒ nat"
where
"summation f 0 = f 0"
| "summation f (Suc n) = f (Suc n) + summation f n"

subsection "Termination Measure"

primrec exp :: "[nat,nat] ⇒ nat"
where
"exp x 0       = 1"
| "exp x (Suc m) = x * exp x m"

primrec sumList     :: "nat list ⇒ nat"
where
"sumList []     = 0"
| "sumList (x#xs) = x + sumList xs"

subsection "Functions"

definition
preImage :: "('a ⇒ 'b) ⇒ 'b set ⇒ 'a set" where
"preImage f A = { x . f x ∈ A}"

definition
pre :: "('a ⇒ 'b) => 'b ⇒ 'a set" where
"pre f a = { x . f x = a}"

definition
equalOn :: "['a set,'a => 'b,'a => 'b] => bool" where
"equalOn A f g = (!x:A. f x = g x)"

lemma preImage_insert: "preImage f (insert a A) = pre f a Un preImage f A"

lemma preImageI: "f x : A ==> x : preImage f A"

lemma preImageE: "x : preImage f A ==> f x : A"

lemma equalOn_Un:  "equalOn (A ∪ B) f g = (equalOn A f g ∧ equalOn B f g)"

lemma equalOnD: "equalOn A f g ⟹ (∀ x ∈ A . f x = g x)"

lemma equalOnI:"(∀ x ∈ A . f x = g x) ⟹ equalOn A f g"

lemma equalOn_UnD: "equalOn (A Un B) f g ==> equalOn A f g & equalOn B f g"
by(auto simp: equalOn_def)

― ‹FIXME move following elsewhere?›
lemma inj_inv_singleton[simp]: "⟦ inj f; f z = y ⟧ ⟹ {x. f x = y} = {z}"
apply rule
apply(auto simp: inj_on_def) done

lemma finite_pre[simp]: "inj f ⟹ finite (pre f x)"