923

1 
(* Title: HOL/Set.thy


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1993 University of Cambridge


5 
*)


6 


7 
Set = Ord +


8 


9 
types


10 
'a set


11 


12 
arities


13 
set :: (term) term


14 


15 
instance


16 
set :: (term) {ord, minus}


17 


18 
consts


19 
"{}" :: "'a set" ("{}")


20 
insert :: "['a, 'a set] => 'a set"


21 
Collect :: "('a => bool) => 'a set" (*comprehension*)


22 
Compl :: "('a set) => 'a set" (*complement*)


23 
Int :: "['a set, 'a set] => 'a set" (infixl 70)


24 
Un :: "['a set, 'a set] => 'a set" (infixl 65)


25 
UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)


26 
UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)


27 
INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)


28 
Union, Inter :: "(('a set)set) => 'a set" (*of a set*)


29 
Pow :: "'a set => 'a set set" (*powerset*)


30 
range :: "('a => 'b) => 'b set" (*of function*)


31 
Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)


32 
inj, surj :: "('a => 'b) => bool" (*inj/surjective*)


33 
inj_onto :: "['a => 'b, 'a set] => bool"


34 
"``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90)


35 
":" :: "['a, 'a set] => bool" (infixl 50) (*membership*)


36 


37 


38 
syntax


39 


40 
"~:" :: "['a, 'a set] => bool" (infixl 50)


41 


42 
"@Finset" :: "args => 'a set" ("{(_)}")


43 


44 
"@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})")


45 
"@SetCompr" :: "['a, idts, bool] => 'a set" ("(1{_ /_./ _})")


46 


47 
(* Big Intersection / Union *)


48 


49 
"@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10)


50 
"@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10)


51 


52 
(* Bounded Quantifiers *)


53 


54 
"@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10)


55 
"@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10)


56 
"*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10)


57 
"*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10)


58 


59 
translations


60 
"x ~: y" == "~ (x : y)"


61 
"{x, xs}" == "insert x {xs}"


62 
"{x}" == "insert x {}"


63 
"{x. P}" == "Collect (%x. P)"


64 
"INT x:A. B" == "INTER A (%x. B)"


65 
"UN x:A. B" == "UNION A (%x. B)"


66 
"! x:A. P" == "Ball A (%x. P)"


67 
"? x:A. P" == "Bex A (%x. P)"


68 
"ALL x:A. P" => "Ball A (%x. P)"


69 
"EX x:A. P" => "Bex A (%x. P)"


70 


71 


72 
rules


73 


74 
(* Isomorphisms between Predicates and Sets *)


75 


76 
mem_Collect_eq "(a : {x.P(x)}) = P(a)"


77 
Collect_mem_eq "{x.x:A} = A"


78 


79 


80 
defs


81 
Ball_def "Ball A P == ! x. x:A > P(x)"


82 
Bex_def "Bex A P == ? x. x:A & P(x)"


83 
subset_def "A <= B == ! x:A. x:B"


84 
Compl_def "Compl(A) == {x. ~x:A}"


85 
Un_def "A Un B == {x.x:A  x:B}"


86 
Int_def "A Int B == {x.x:A & x:B}"


87 
set_diff_def "A  B == {x. x:A & ~x:B}"


88 
INTER_def "INTER A B == {y. ! x:A. y: B(x)}"


89 
UNION_def "UNION A B == {y. ? x:A. y: B(x)}"


90 
INTER1_def "INTER1(B) == INTER {x.True} B"


91 
UNION1_def "UNION1(B) == UNION {x.True} B"


92 
Inter_def "Inter(S) == (INT x:S. x)"


93 
Union_def "Union(S) == (UN x:S. x)"


94 
Pow_def "Pow(A) == {B. B <= A}"


95 
empty_def "{} == {x. False}"


96 
insert_def "insert a B == {x.x=a} Un B"


97 
range_def "range(f) == {y. ? x. y=f(x)}"


98 
image_def "f``A == {y. ? x:A. y=f(x)}"


99 
inj_def "inj(f) == ! x y. f(x)=f(y) > x=y"


100 
inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) > x=y"


101 
surj_def "surj(f) == ! y. ? x. y=f(x)"


102 


103 
end


104 


105 
ML


106 


107 
local


108 


109 
(* Translates between { e  x1..xn. P} and {u. ? x1..xn. u=e & P} *)


110 
(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)


111 


112 
val ex_tr = snd(mk_binder_tr("? ","Ex"));


113 


114 
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1


115 
 nvars(_) = 1;


116 


117 
fun setcompr_tr[e,idts,b] =


118 
let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e


119 
val P = Syntax.const("op &") $ eq $ b


120 
val exP = ex_tr [idts,P]


121 
in Syntax.const("Collect") $ Abs("",dummyT,exP) end;


122 


123 
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));


124 


125 
fun setcompr_tr'[Abs(_,_,P)] =


126 
let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)


127 
 ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =


128 
if n>0 andalso m=n andalso


129 
((0 upto (n1)) subset add_loose_bnos(e,0,[]))


130 
then () else raise Match


131 


132 
fun tr'(_ $ abs) =


133 
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]


134 
in Syntax.const("@SetCompr") $ e $ idts $ Q end


135 
in ok(P,0); tr'(P) end;


136 


137 
in


138 


139 
val parse_translation = [("@SetCompr", setcompr_tr)];


140 
val print_translation = [("Collect", setcompr_tr')];


141 
val print_ast_translation =


142 
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];


143 


144 
end;


145 
