Quelle  Base.thy

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"
  using Max_ge Suc_n_not_le_n assms by blast


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 sumList     :: "nat list ==> nat"
  where
    "sumList [] = 0"
  | "sumList (x#xs) = x + sumList xs"


subsection "Functions"

abbreviation (input) "preImage ≡ vimage"

abbreviation (input) "pre f a ≡ f-` {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 ∪ preImage f A"
  by auto

lemma equalOn_Un:  "equalOn (A ∪ B) f g = (equalOn A f g ∧ equalOn B f g)"
  by(auto simp add: equalOn_def) 

lemma equalOnD: "equalOn A f g ==> (∀ x ∈ A . f x = g x)"
  by(simp add: equalOn_def)

lemma equalOnI:"(∀ x ∈ A . f x = g x) ==> equalOn A f g"
  by(simp add: equalOn_def)

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

lemma inj_inv_singleton[simp]: "[ inj f; f z = y ] ==> {x. f x = y} = {z}"
  using inj_eq by fastforce

lemma finite_pre[simp]: "inj f ==> finite (pre f x)"
  by (simp add: finite_vimageI)

declare finite_vimageI [simp]

end