15 (* actually belongs to Finite.thy *) |
15 (* actually belongs to Finite.thy *) |
16 instance unit :: finite (finite_unit) |
16 instance unit :: finite (finite_unit) |
17 instance "*" :: (finite,finite) finite (finite_Prod) |
17 instance "*" :: (finite,finite) finite (finite_Prod) |
18 |
18 |
19 |
19 |
20 consts |
20 constdefs |
21 less_than :: "(nat*nat)set" |
21 less_than :: "(nat*nat)set" |
22 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
22 "less_than == trancl pred_nat" |
23 measure :: "('a => nat) => ('a * 'a)set" |
23 |
24 lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" |
24 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
|
25 "inv_image r f == {(x,y). (f(x), f(y)) : r}" |
|
26 |
|
27 measure :: "('a => nat) => ('a * 'a)set" |
|
28 "measure == inv_image less_than" |
|
29 |
|
30 lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" |
25 (infixr "<*lex*>" 80) |
31 (infixr "<*lex*>" 80) |
26 finite_psubset :: "('a set * 'a set) set" |
32 "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}" |
27 |
33 |
|
34 (* finite proper subset*) |
|
35 finite_psubset :: "('a set * 'a set) set" |
|
36 "finite_psubset == {(A,B). A < B & finite B}" |
28 |
37 |
29 defs |
38 (* For rec_defs where the first n parameters stay unchanged in the recursive |
30 less_than_def "less_than == trancl pred_nat" |
39 call. See While for an application. |
|
40 *) |
|
41 same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" |
|
42 "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" |
31 |
43 |
32 inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}" |
|
33 |
|
34 measure_def "measure == inv_image less_than" |
|
35 |
|
36 lex_prod_def "ra <*lex*> rb == {((a,b),(a',b')) | a a' b b'. |
|
37 ((a,a') : ra | a=a' & (b,b') : rb)}" |
|
38 |
|
39 (* finite proper subset*) |
|
40 finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}" |
|
41 end |
44 end |