src/HOL/NumberTheory/BijectionRel.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9508 4d01dbf6ded7
child 11049 7eef34adb852
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     1
(*  Title:	BijectionRel.thy
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     2
    ID:         $Id$
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     3
    Author:	Thomas M. Rasmussen
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     4
    Copyright	2000  University of Cambridge
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     5
*)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     6
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     7
BijectionRel = Main +
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     8
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     9
consts
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    10
  bijR :: "(['a, 'b] => bool) => ('a set * 'b set) set"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    11
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    12
inductive "bijR P"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    13
intrs
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    14
  empty  "({},{}) : bijR P"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    15
  insert "[| P a b; a ~: A; b ~: B; (A,B) : bijR P |] \ 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    16
\        ==> (insert a A, insert b B) : bijR P" 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    17
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    18
(* Add extra condition to insert: ALL b:B. ~(P a b) (and similar for A) *) 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    19
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    20
consts
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    21
  bijP :: "(['a, 'a] => bool) => 'a set => bool"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    22
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    23
defs
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    24
  bijP_def "bijP P F == (ALL a b. a:F & P a b --> b:F)" 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    25
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    26
consts
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    27
  uniqP :: "(['a, 'a] => bool) => bool"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    28
  symP :: "(['a, 'a] => bool) => bool"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    29
  
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    30
defs
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    31
  uniqP_def "uniqP P == (ALL a b c d. P a b & P c d --> (a=c) = (b=d))" 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    32
  symP_def  "symP P  == (ALL a b. (P a b) = (P b a))" 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    33
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    34
consts
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    35
  bijER :: "(['a, 'a] => bool) => 'a set set"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    36
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    37
inductive "bijER P"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    38
intrs
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    39
  empty   "{} : bijER P"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    40
  insert1 "[| P a a; a ~: A; A : bijER P |] \ 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    41
\         ==> (insert a A) : bijER P" 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    42
  insert2 "[| P a b; a ~= b; a ~: A; b ~: A; A : bijER P |] \ 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    43
\         ==> (insert a (insert b A)) : bijER P" 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    44
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    45
end
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    46