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
```