Theory JBasis

Up to index of Isabelle/HOL/MicroJava

(*  Title:      HOL/MicroJava/J/JBasis.thy
    ID:         $Id: JBasis.thy,v 1.3 2000/09/21 08:42:58 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 TU Muenchen

Some auxiliary definitions.
*)

JBasis = Main + 

constdefs

  unique  :: "('a × 'b) list => bool"
 "unique  == nodups \<circ> map fst"

end

theorem image_rev:

  x : f `` A ==> EX y. y : A & x = f y

theorem some_subset_the:

  {y. x = Some y} <= {the x}

unique

theorem fst_in_set_lemma:

  (x, y) : set l ==> x : fst `` set l

theorem unique_Nil:

  unique []

theorem unique_Cons:

  unique ((x, y) # l) = (unique l & (ALL y. (x, y) ~: set l))

theorem unique_append:

  [| unique l'; unique l; ALL (x, y):set l. ALL (x', y'):set l'. x' ~= x |]
  ==> unique (l @ l')

theorem unique_map_inj:

  [| unique l; inj f |] ==> unique (map (%(k, x). (f k, g k x)) l)

theorem unique_map_Pair:

  unique l ==> unique (map (split (%k. Pair (k, C))) l)

theorem image_cong:

  [| M = N; !!x. x : N ==> f x = g x |] ==> f `` M = g `` N

theorem unique_map_of_Some_conv:

  unique xys ==> (map_of xys x = Some y) = ((x, y) : set xys)

theorem Ball_set_table:

  Ball (set l) (split P) ==> ALL x y. map_of l x = Some y --> P x y

theorem map_of_map:

  map_of (map (%(a, b). (a, f b)) xs) x = option_map f (map_of xs x)