17 |
17 |
18 consts |
18 consts |
19 less_than :: "(nat*nat)set" |
19 less_than :: "(nat*nat)set" |
20 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
20 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
21 measure :: "('a => nat) => ('a * 'a)set" |
21 measure :: "('a => nat) => ('a * 'a)set" |
22 "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) |
22 lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" |
|
23 (infixr "<*lex*>" 80) |
23 finite_psubset :: "('a set * 'a set) set" |
24 finite_psubset :: "('a set * 'a set) set" |
24 |
25 |
25 |
26 |
26 defs |
27 defs |
27 less_than_def "less_than == trancl pred_nat" |
28 less_than_def "less_than == trancl pred_nat" |
28 |
29 |
29 inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}" |
30 inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}" |
30 |
31 |
31 measure_def "measure == inv_image less_than" |
32 measure_def "measure == inv_image less_than" |
32 |
33 |
33 lex_prod_def "ra**rb == {p. ? a a' b b'. |
34 lex_prod_def "ra <*lex*> rb == {((a,b),(a',b')) | a a' b b'. |
34 p = ((a,b),(a',b')) & |
35 ((a,a') : ra | a=a' & (b,b') : rb)}" |
35 ((a,a') : ra | a=a' & (b,b') : rb)}" |
|
36 |
36 |
37 (* finite proper subset*) |
37 (* finite proper subset*) |
38 finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}" |
38 finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}" |
39 end |
39 end |