# HG changeset patch
# User berghofe
# Date 1170865972 -3600
# Node ID 3c5c6bdf61de085298b13bcced462b3eb7e8f1e8
# Parent  6a65e9b2ae056f67e9e1286464a9dd6a0fa88e21
Adapted to changes in Finite_Set theory.

diff -r 6a65e9b2ae05 -r 3c5c6bdf61de src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Wed Feb 07 17:30:53 2007 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Feb 07 17:32:52 2007 +0100
@@ -51,7 +51,7 @@
 lemma finite_imp_foldSetD:
   "[| finite A; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D |] ==>
    EX x. (A, x) \<in> foldSetD D f e"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by auto
 next
   case (insert x F)
@@ -92,7 +92,7 @@
 
 lemma (in LCD) finite_imp_foldSetD:
   "[| finite A; A \<subseteq> B; e \<in> D |] ==> EX x. (A, x) \<in> foldSetD D f e"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by auto
 next
   case (insert x F)
@@ -191,7 +191,7 @@
 
 lemma (in LCD) foldD_closed [simp]:
   "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by (simp add: foldD_empty)
 next
   case insert then show ?case by (simp add: foldD_insert)
@@ -200,7 +200,7 @@
 lemma (in LCD) foldD_commute:
   "[| finite A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
    f x (foldD D f e A) = foldD D f (f x e) A"
-  apply (induct set: Finites)
+  apply (induct set: finite)
    apply simp
   apply (auto simp add: left_commute foldD_insert)
   done
@@ -212,7 +212,7 @@
 lemma (in LCD) foldD_nest_Un_Int:
   "[| finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B |] ==>
    foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
-  apply (induct set: Finites)
+  apply (induct set: finite)
    apply simp
   apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
     Int_mono2 Un_subset_iff)
@@ -272,7 +272,7 @@
   "[| finite A; finite B; A \<subseteq> D; B \<subseteq> D |] ==>
     foldD D f e A \<cdot> foldD D f e B =
     foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
-  apply (induct set: Finites)
+  apply (induct set: finite)
    apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
   apply (simp add: AC insert_absorb Int_insert_left
     LCD.foldD_insert [OF LCD.intro [of D]]
@@ -335,7 +335,7 @@
 
 lemma (in comm_monoid) finprod_one [simp]:
   "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty show ?case by simp
 next
   case (insert a A)
@@ -370,7 +370,7 @@
      finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
      finprod G g A \<otimes> finprod G g B"
 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by (simp add: finprod_closed)
 next
   case (insert a A)
@@ -392,7 +392,7 @@
 lemma (in comm_monoid) finprod_multf:
   "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
    finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty show ?case by simp
 next
   case (insert a A) then
diff -r 6a65e9b2ae05 -r 3c5c6bdf61de src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Feb 07 17:30:53 2007 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Wed Feb 07 17:32:52 2007 +0100
@@ -318,7 +318,7 @@
 
 lemma (in lattice) finite_sup_least:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty
   then show ?case by simp
 next
@@ -349,7 +349,7 @@
 
 lemma (in lattice) finite_sup_closed:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by simp
 next
   case insert then show ?case
@@ -544,7 +544,7 @@
 
 lemma (in lattice) finite_inf_greatest:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by simp
 next
   case (insert x A)
@@ -575,7 +575,7 @@
 
 lemma (in lattice) finite_inf_closed:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by simp
 next
   case insert then show ?case
diff -r 6a65e9b2ae05 -r 3c5c6bdf61de src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Feb 07 17:30:53 2007 +0100
+++ b/src/HOL/Algebra/Ring.thy	Wed Feb 07 17:32:52 2007 +0100
@@ -552,7 +552,7 @@
 lemma (in cring) finsum_ldistr:
   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by simp
 next
   case (insert x F) then show ?case by (simp add: Pi_def l_distr)
@@ -561,7 +561,7 @@
 lemma (in cring) finsum_rdistr:
   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by simp
 next
   case (insert x F) then show ?case by (simp add: Pi_def r_distr)
@@ -745,7 +745,7 @@
 lemma (in ring_hom_cring) hom_finsum [simp]:
   "[| finite A; f \<in> A -> carrier R |] ==>
   h (finsum R f A) = finsum S (h o f) A"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by simp
 next
   case insert then show ?case by (simp add: Pi_def)
@@ -754,7 +754,7 @@
 lemma (in ring_hom_cring) hom_finprod:
   "[| finite A; f \<in> A -> carrier R |] ==>
   h (finprod R f A) = finprod S (h o f) A"
-proof (induct set: Finites)
+proof (induct set: finite)
   case empty then show ?case by simp
 next
   case insert then show ?case by (simp add: Pi_def)
diff -r 6a65e9b2ae05 -r 3c5c6bdf61de src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Feb 07 17:30:53 2007 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Feb 07 17:32:52 2007 +0100
@@ -286,30 +286,30 @@
 
 
 lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
-apply (rule Finites.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
+apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
 done
 
 lemma Nonce_supply2: 
   "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
-apply (cut_tac evs = evs in Finites.emptyI [THEN Nonce_supply_ax])
+apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
 apply (erule exE)
-apply (cut_tac evs = evs' in Finites.emptyI [THEN Finites.insertI, THEN Nonce_supply_ax]) 
+apply (cut_tac evs = evs' in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
 apply auto
 done
 
 
 lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
                     Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
-apply (cut_tac evs = evs in Finites.emptyI [THEN Nonce_supply_ax])
+apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
 apply (erule exE)
-apply (cut_tac evs = evs' and a1 = N in Finites.emptyI [THEN Finites.insertI, THEN Nonce_supply_ax]) 
+apply (cut_tac evs = evs' and a1 = N in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
 apply (erule exE)
-apply (cut_tac evs = evs'' and a1 = Na and a2 = N in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Nonce_supply_ax]) 
+apply (cut_tac evs = evs'' and a1 = Na and a2 = N in finite.emptyI [THEN finite.insertI, THEN finite.insertI, THEN Nonce_supply_ax]) 
 apply blast
 done
 
 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
-apply (rule Finites.emptyI [THEN Nonce_supply_ax, THEN exE])
+apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE])
 apply (rule someI, blast)
 done