author berghofe Wed Feb 07 17:32:52 2007 +0100 (2007-02-07) changeset 22265 3c5c6bdf61de parent 22264 6a65e9b2ae05 child 22266 9f3198585c89
Adapted to changes in Finite_Set theory.
 src/HOL/Algebra/FiniteProduct.thy file | annotate | diff | revisions src/HOL/Algebra/Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/Ring.thy file | annotate | diff | revisions src/HOL/Auth/Smartcard/Smartcard.thy file | annotate | diff | revisions
```     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
```