src/HOL/NumberTheory/BijectionRel.thy
changeset 23755 1c4672d130b1
parent 22274 ce1459004c8d
     1.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -15,13 +15,12 @@
     1.4    \bigskip
     1.5  *}
     1.6  
     1.7 -consts
     1.8 +inductive_set
     1.9    bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
    1.10 -
    1.11 -inductive "bijR P"
    1.12 -  intros
    1.13 +  for P :: "'a => 'b => bool"
    1.14 +where
    1.15    empty [simp]: "({}, {}) \<in> bijR P"
    1.16 -  insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
    1.17 +| insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
    1.18      ==> (insert a A, insert b B) \<in> bijR P"
    1.19  
    1.20  text {*
    1.21 @@ -41,14 +40,13 @@
    1.22    symP :: "('a => 'a => bool) => bool" where
    1.23    "symP P = (\<forall>a b. P a b = P b a)"
    1.24  
    1.25 -consts
    1.26 +inductive_set
    1.27    bijER :: "('a => 'a => bool) => 'a set set"
    1.28 -
    1.29 -inductive "bijER P"
    1.30 -  intros
    1.31 +  for P :: "'a => 'a => bool"
    1.32 +where
    1.33    empty [simp]: "{} \<in> bijER P"
    1.34 -  insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
    1.35 -  insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
    1.36 +| insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
    1.37 +| insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
    1.38      ==> insert a (insert b A) \<in> bijER P"
    1.39  
    1.40