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.

(*  Title:	BijectionRel.thy
    ID:         $Id$
    Author:	Thomas M. Rasmussen
    Copyright	2000  University of Cambridge
*)

BijectionRel = Main +

consts
  bijR :: "(['a, 'b] => bool) => ('a set * 'b set) set"

inductive "bijR P"
intrs
  empty  "({},{}) : bijR P"
  insert "[| P a b; a ~: A; b ~: B; (A,B) : bijR P |] \ 
\        ==> (insert a A, insert b B) : bijR P" 

(* Add extra condition to insert: ALL b:B. ~(P a b) (and similar for A) *) 

consts
  bijP :: "(['a, 'a] => bool) => 'a set => bool"

defs
  bijP_def "bijP P F == (ALL a b. a:F & P a b --> b:F)" 

consts
  uniqP :: "(['a, 'a] => bool) => bool"
  symP :: "(['a, 'a] => bool) => bool"
  
defs
  uniqP_def "uniqP P == (ALL a b c d. P a b & P c d --> (a=c) = (b=d))" 
  symP_def  "symP P  == (ALL a b. (P a b) = (P b a))" 

consts
  bijER :: "(['a, 'a] => bool) => 'a set set"

inductive "bijER P"
intrs
  empty   "{} : bijER P"
  insert1 "[| P a a; a ~: A; A : bijER P |] \ 
\         ==> (insert a A) : bijER P" 
  insert2 "[| P a b; a ~= b; a ~: A; b ~: A; A : bijER P |] \ 
\         ==> (insert a (insert b A)) : bijER P" 

end