equal
deleted
inserted
replaced
|
1 (* Title: BijectionRel.thy |
|
2 ID: $Id$ |
|
3 Author: Thomas M. Rasmussen |
|
4 Copyright 2000 University of Cambridge |
|
5 *) |
|
6 |
|
7 BijectionRel = Main + |
|
8 |
|
9 consts |
|
10 bijR :: "(['a, 'b] => bool) => ('a set * 'b set) set" |
|
11 |
|
12 inductive "bijR P" |
|
13 intrs |
|
14 empty "({},{}) : bijR P" |
|
15 insert "[| P a b; a ~: A; b ~: B; (A,B) : bijR P |] \ |
|
16 \ ==> (insert a A, insert b B) : bijR P" |
|
17 |
|
18 (* Add extra condition to insert: ALL b:B. ~(P a b) (and similar for A) *) |
|
19 |
|
20 consts |
|
21 bijP :: "(['a, 'a] => bool) => 'a set => bool" |
|
22 |
|
23 defs |
|
24 bijP_def "bijP P F == (ALL a b. a:F & P a b --> b:F)" |
|
25 |
|
26 consts |
|
27 uniqP :: "(['a, 'a] => bool) => bool" |
|
28 symP :: "(['a, 'a] => bool) => bool" |
|
29 |
|
30 defs |
|
31 uniqP_def "uniqP P == (ALL a b c d. P a b & P c d --> (a=c) = (b=d))" |
|
32 symP_def "symP P == (ALL a b. (P a b) = (P b a))" |
|
33 |
|
34 consts |
|
35 bijER :: "(['a, 'a] => bool) => 'a set set" |
|
36 |
|
37 inductive "bijER P" |
|
38 intrs |
|
39 empty "{} : bijER P" |
|
40 insert1 "[| P a a; a ~: A; A : bijER P |] \ |
|
41 \ ==> (insert a A) : bijER P" |
|
42 insert2 "[| P a b; a ~= b; a ~: A; b ~: A; A : bijER P |] \ |
|
43 \ ==> (insert a (insert b A)) : bijER P" |
|
44 |
|
45 end |
|
46 |