author berghofe Wed, 11 Jul 2007 11:00:46 +0200 changeset 23736 bf8d4a46452d parent 23735 afc12f93f64f child 23737 9194aecbf20e
Renamed inductive2 to inductive.
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Finite_Set.thy	Wed Jul 11 11:00:09 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jul 11 11:00:46 2007 +0200
@@ -12,7 +12,7 @@

subsection {* Definition and basic properties *}

-inductive2 finite :: "'a set => bool"
+inductive finite :: "'a set => bool"
where
emptyI [simp, intro!]: "finite {}"
| insertI [simp, intro!]: "finite A ==> finite (insert a A)"
@@ -427,7 +427,7 @@
se the definitions of sums and products over finite sets.
*}

-inductive2
+inductive
foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool"
for f ::  "'a => 'a => 'a"
and g :: "'b => 'a"
@@ -438,7 +438,7 @@
"\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk>
\<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)"

-inductive_cases2 empty_foldSetE [elim!]: "foldSet f g z {} x"
+inductive_cases empty_foldSetE [elim!]: "foldSet f g z {} x"

constdefs
fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
@@ -1794,7 +1794,7 @@

text{* Does not require start value. *}

-inductive2
+inductive
fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
for f :: "'a => 'a => 'a"
where
@@ -1809,9 +1809,9 @@
"fold1Set f A x \<Longrightarrow> A \<noteq> {}"
by(erule fold1Set.cases, simp_all)

-inductive_cases2 empty_fold1SetE [elim!]: "fold1Set f {} x"
-
-inductive_cases2 insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
+inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
+
+inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"

lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"```