Adapted to changes in Finite_Set theory.
authorberghofe
Wed Feb 07 17:32:52 2007 +0100 (2007-02-07)
changeset 222653c5c6bdf61de
parent 22264 6a65e9b2ae05
child 22266 9f3198585c89
Adapted to changes in Finite_Set theory.
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Ring.thy
src/HOL/Auth/Smartcard/Smartcard.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Wed Feb 07 17:30:53 2007 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Feb 07 17:32:52 2007 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  lemma finite_imp_foldSetD:
     1.5    "[| finite A; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D |] ==>
     1.6     EX x. (A, x) \<in> foldSetD D f e"
     1.7 -proof (induct set: Finites)
     1.8 +proof (induct set: finite)
     1.9    case empty then show ?case by auto
    1.10  next
    1.11    case (insert x F)
    1.12 @@ -92,7 +92,7 @@
    1.13  
    1.14  lemma (in LCD) finite_imp_foldSetD:
    1.15    "[| finite A; A \<subseteq> B; e \<in> D |] ==> EX x. (A, x) \<in> foldSetD D f e"
    1.16 -proof (induct set: Finites)
    1.17 +proof (induct set: finite)
    1.18    case empty then show ?case by auto
    1.19  next
    1.20    case (insert x F)
    1.21 @@ -191,7 +191,7 @@
    1.22  
    1.23  lemma (in LCD) foldD_closed [simp]:
    1.24    "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
    1.25 -proof (induct set: Finites)
    1.26 +proof (induct set: finite)
    1.27    case empty then show ?case by (simp add: foldD_empty)
    1.28  next
    1.29    case insert then show ?case by (simp add: foldD_insert)
    1.30 @@ -200,7 +200,7 @@
    1.31  lemma (in LCD) foldD_commute:
    1.32    "[| finite A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
    1.33     f x (foldD D f e A) = foldD D f (f x e) A"
    1.34 -  apply (induct set: Finites)
    1.35 +  apply (induct set: finite)
    1.36     apply simp
    1.37    apply (auto simp add: left_commute foldD_insert)
    1.38    done
    1.39 @@ -212,7 +212,7 @@
    1.40  lemma (in LCD) foldD_nest_Un_Int:
    1.41    "[| finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B |] ==>
    1.42     foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
    1.43 -  apply (induct set: Finites)
    1.44 +  apply (induct set: finite)
    1.45     apply simp
    1.46    apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
    1.47      Int_mono2 Un_subset_iff)
    1.48 @@ -272,7 +272,7 @@
    1.49    "[| finite A; finite B; A \<subseteq> D; B \<subseteq> D |] ==>
    1.50      foldD D f e A \<cdot> foldD D f e B =
    1.51      foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
    1.52 -  apply (induct set: Finites)
    1.53 +  apply (induct set: finite)
    1.54     apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
    1.55    apply (simp add: AC insert_absorb Int_insert_left
    1.56      LCD.foldD_insert [OF LCD.intro [of D]]
    1.57 @@ -335,7 +335,7 @@
    1.58  
    1.59  lemma (in comm_monoid) finprod_one [simp]:
    1.60    "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
    1.61 -proof (induct set: Finites)
    1.62 +proof (induct set: finite)
    1.63    case empty show ?case by simp
    1.64  next
    1.65    case (insert a A)
    1.66 @@ -370,7 +370,7 @@
    1.67       finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
    1.68       finprod G g A \<otimes> finprod G g B"
    1.69  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    1.70 -proof (induct set: Finites)
    1.71 +proof (induct set: finite)
    1.72    case empty then show ?case by (simp add: finprod_closed)
    1.73  next
    1.74    case (insert a A)
    1.75 @@ -392,7 +392,7 @@
    1.76  lemma (in comm_monoid) finprod_multf:
    1.77    "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
    1.78     finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
    1.79 -proof (induct set: Finites)
    1.80 +proof (induct set: finite)
    1.81    case empty show ?case by simp
    1.82  next
    1.83    case (insert a A) then
     2.1 --- a/src/HOL/Algebra/Lattice.thy	Wed Feb 07 17:30:53 2007 +0100
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Feb 07 17:32:52 2007 +0100
     2.3 @@ -318,7 +318,7 @@
     2.4  
     2.5  lemma (in lattice) finite_sup_least:
     2.6    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
     2.7 -proof (induct set: Finites)
     2.8 +proof (induct set: finite)
     2.9    case empty
    2.10    then show ?case by simp
    2.11  next
    2.12 @@ -349,7 +349,7 @@
    2.13  
    2.14  lemma (in lattice) finite_sup_closed:
    2.15    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
    2.16 -proof (induct set: Finites)
    2.17 +proof (induct set: finite)
    2.18    case empty then show ?case by simp
    2.19  next
    2.20    case insert then show ?case
    2.21 @@ -544,7 +544,7 @@
    2.22  
    2.23  lemma (in lattice) finite_inf_greatest:
    2.24    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
    2.25 -proof (induct set: Finites)
    2.26 +proof (induct set: finite)
    2.27    case empty then show ?case by simp
    2.28  next
    2.29    case (insert x A)
    2.30 @@ -575,7 +575,7 @@
    2.31  
    2.32  lemma (in lattice) finite_inf_closed:
    2.33    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
    2.34 -proof (induct set: Finites)
    2.35 +proof (induct set: finite)
    2.36    case empty then show ?case by simp
    2.37  next
    2.38    case insert then show ?case
     3.1 --- a/src/HOL/Algebra/Ring.thy	Wed Feb 07 17:30:53 2007 +0100
     3.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Feb 07 17:32:52 2007 +0100
     3.3 @@ -552,7 +552,7 @@
     3.4  lemma (in cring) finsum_ldistr:
     3.5    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
     3.6     finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
     3.7 -proof (induct set: Finites)
     3.8 +proof (induct set: finite)
     3.9    case empty then show ?case by simp
    3.10  next
    3.11    case (insert x F) then show ?case by (simp add: Pi_def l_distr)
    3.12 @@ -561,7 +561,7 @@
    3.13  lemma (in cring) finsum_rdistr:
    3.14    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    3.15     a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
    3.16 -proof (induct set: Finites)
    3.17 +proof (induct set: finite)
    3.18    case empty then show ?case by simp
    3.19  next
    3.20    case (insert x F) then show ?case by (simp add: Pi_def r_distr)
    3.21 @@ -745,7 +745,7 @@
    3.22  lemma (in ring_hom_cring) hom_finsum [simp]:
    3.23    "[| finite A; f \<in> A -> carrier R |] ==>
    3.24    h (finsum R f A) = finsum S (h o f) A"
    3.25 -proof (induct set: Finites)
    3.26 +proof (induct set: finite)
    3.27    case empty then show ?case by simp
    3.28  next
    3.29    case insert then show ?case by (simp add: Pi_def)
    3.30 @@ -754,7 +754,7 @@
    3.31  lemma (in ring_hom_cring) hom_finprod:
    3.32    "[| finite A; f \<in> A -> carrier R |] ==>
    3.33    h (finprod R f A) = finprod S (h o f) A"
    3.34 -proof (induct set: Finites)
    3.35 +proof (induct set: finite)
    3.36    case empty then show ?case by simp
    3.37  next
    3.38    case insert then show ?case by (simp add: Pi_def)
     4.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Feb 07 17:30:53 2007 +0100
     4.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Feb 07 17:32:52 2007 +0100
     4.3 @@ -286,30 +286,30 @@
     4.4  
     4.5  
     4.6  lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
     4.7 -apply (rule Finites.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
     4.8 +apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
     4.9  done
    4.10  
    4.11  lemma Nonce_supply2: 
    4.12    "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
    4.13 -apply (cut_tac evs = evs in Finites.emptyI [THEN Nonce_supply_ax])
    4.14 +apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
    4.15  apply (erule exE)
    4.16 -apply (cut_tac evs = evs' in Finites.emptyI [THEN Finites.insertI, THEN Nonce_supply_ax]) 
    4.17 +apply (cut_tac evs = evs' in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
    4.18  apply auto
    4.19  done
    4.20  
    4.21  
    4.22  lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
    4.23                      Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
    4.24 -apply (cut_tac evs = evs in Finites.emptyI [THEN Nonce_supply_ax])
    4.25 +apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
    4.26  apply (erule exE)
    4.27 -apply (cut_tac evs = evs' and a1 = N in Finites.emptyI [THEN Finites.insertI, THEN Nonce_supply_ax]) 
    4.28 +apply (cut_tac evs = evs' and a1 = N in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
    4.29  apply (erule exE)
    4.30 -apply (cut_tac evs = evs'' and a1 = Na and a2 = N in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Nonce_supply_ax]) 
    4.31 +apply (cut_tac evs = evs'' and a1 = Na and a2 = N in finite.emptyI [THEN finite.insertI, THEN finite.insertI, THEN Nonce_supply_ax]) 
    4.32  apply blast
    4.33  done
    4.34  
    4.35  lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
    4.36 -apply (rule Finites.emptyI [THEN Nonce_supply_ax, THEN exE])
    4.37 +apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE])
    4.38  apply (rule someI, blast)
    4.39  done
    4.40