src/HOL/Algebra/FiniteProduct.thy
changeset 23746 a455e69c31cc
parent 23350 50c5b0912a0c
child 27699 489e3f33af0e
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -18,13 +18,12 @@
     1.4    @{text "x \<in> carrier G"}.  We introduce an explicit argument for the domain
     1.5    @{text D}. *}
     1.6  
     1.7 -consts
     1.8 +inductive_set
     1.9    foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    1.10 -
    1.11 -inductive "foldSetD D f e"
    1.12 -  intros
    1.13 +  for D :: "'a set" and f :: "'b => 'a => 'a" and e :: 'a
    1.14 +  where
    1.15      emptyI [intro]: "e \<in> D ==> ({}, e) \<in> foldSetD D f e"
    1.16 -    insertI [intro]: "[| x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
    1.17 +  | insertI [intro]: "[| x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
    1.18                        (insert x A, f x y) \<in> foldSetD D f e"
    1.19  
    1.20  inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
    1.21 @@ -36,7 +35,7 @@
    1.22  lemma foldSetD_closed:
    1.23    "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
    1.24        |] ==> z \<in> D";
    1.25 -  by (erule foldSetD.elims) auto
    1.26 +  by (erule foldSetD.cases) auto
    1.27  
    1.28  lemma Diff1_foldSetD:
    1.29    "[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; f x y \<in> D |] ==>
    1.30 @@ -75,7 +74,7 @@
    1.31  
    1.32  lemma (in LCD) foldSetD_closed [dest]:
    1.33    "(A, z) \<in> foldSetD D f e ==> z \<in> D";
    1.34 -  by (erule foldSetD.elims) auto
    1.35 +  by (erule foldSetD.cases) auto
    1.36  
    1.37  lemma (in LCD) Diff1_foldSetD:
    1.38    "[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; A \<subseteq> B |] ==>
    1.39 @@ -117,7 +116,7 @@
    1.40    apply (erule rev_mp)
    1.41    apply (simp add: less_Suc_eq_le)
    1.42    apply (rule impI)
    1.43 -  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
    1.44 +  apply (rename_tac xa Aa ya xb Ab yb, case_tac "xa = xb")
    1.45     apply (subgoal_tac "Aa = Ab")
    1.46      prefer 2 apply (blast elim!: equalityE)
    1.47     apply blast