Theory Base

section "Base"

theory Base
imports PermutationLemmas

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
  case False
  with a have "Max A  A  (s  A. s  Max A)" by simp
  thus ?thesis by auto

    ― ‹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"
  "summation f 0 = f 0"
| "summation f (Suc n) = f (Suc n) + summation f n"

subsection "Termination Measure"

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

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

subsection "Functions"

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

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

  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"
  by(auto simp add: preImage_def pre_def)

lemma preImageI: "f x : A ==> x : preImage f A"
  by(simp add: preImage_def)
lemma preImageE: "x : preImage f A ==> f x : A"
  by(simp add: preImage_def)

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)

    ― ‹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)"
  apply(simp add: pre_def) 
  apply (cases " y. f y = x", auto) done

lemma finite_preImage[simp]: " finite A; inj f   finite (preImage f A)"
  apply(induct A rule: finite_induct) 
  apply(simp add: preImage_def)
  apply(simp add: preImage_insert) done