Theory Marvin_lemmas

Up to index of Isabelle/HOL/Marvin99-1

Marvin_lemmas = Map + Fun + HOL + List + Nat + Prod + Datatype + Set + Option +

end

theorem single_subs_cases:

  X <= {b} ==> X = {b} | X = {}

theorem single_int_collect:

  A b ==> {b} Int Collect A = {b}

theorem not_single_int_collect:

  ¬ A b ==> {b} Int Collect A = {}

theorem apply_None:

  s ~: dom f ==> f s = None

theorem single_set_empty:

  [| A ~= {x}; A <= {x} |] ==> A = {}

theorem single_Un:

  [| A Un B = {x}; A <= {x}; B <= {x} |] ==> A = {x} | B = {x}

theorem some_the_equiv:

  a : dom f ==> (f a = Some b) = (the (f a) = b)

theorem some_in_dom:

  [| a : dom f; the (f a) = b |] ==> f a = Some b

theorem if_eq_Some_simp:

  (EX y. (if P then Some f else None) = Some y) = P

theorem if_Some_point:

  ((if P then Some x else None) = Some y) = (P & x = y)

theorem expand_partial_fun_eq:

  [| dom f = dom g; ALL x:dom f. f x = g x |] ==> f = g