Basis.thy

Basis = Sum + WF_Rel + Option + List + IntDef + 

constdefs

  first		:: "'a * 'b * 'c  => 'a"
 "first == fst"
  secnd		:: "'a * 'b * 'c  => 'b"
 "secnd == fst  o  snd"
  third		:: "'a * 'b * 'c  => 'c"
 "third == snd  o  snd"

consts

  atmost1	:: "'a set => bool"
  s2o		:: "'a set => 'a option"
  o2s		:: "'a option => 'a set"

defs

  atmost1_def	"atmost1 == %A. !x:A. !y:A. x = y"
  s2o_def	"s2o     == %A. if ?!x. x:A then Some (@x. x:A) else None"
  o2s_def	"o2s     == %y. case y of None => {} | Some x => {x}"

constdefs

  unique  :: "('a * 'b) list => bool"
 "unique t == !(x,y):set t. !(x',y'):set t. x = x' --> y = y'"

end

Theorems proved in Basis.ML:

(? x. P x) = (? a b. P (a, b))

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