src/HOL/Finite_Set.thy
 changeset 15327 0230a10582d3 parent 15318 e9669e0d6452 child 15376 302ef111b621
```     1.1 --- a/src/HOL/Finite_Set.thy	Wed Nov 24 10:37:38 2004 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Wed Nov 24 11:12:10 2004 +0100
1.3 @@ -36,16 +36,16 @@
1.4
1.5  lemma finite_induct [case_names empty insert, induct set: Finites]:
1.6    "finite F ==>
1.7 -    P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
1.8 +    P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
1.9    -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
1.10  proof -
1.11    assume "P {}" and
1.12 -    insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
1.13 +    insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
1.14    assume "finite F"
1.15    thus "P F"
1.16    proof induct
1.17      show "P {}" .
1.18 -    fix F x assume F: "finite F" and P: "P F"
1.19 +    fix x F assume F: "finite F" and P: "P F"
1.20      show "P (insert x F)"
1.21      proof cases
1.22        assume "x \<in> F"
1.23 @@ -60,16 +60,16 @@
1.24
1.25  lemma finite_subset_induct [consumes 2, case_names empty insert]:
1.26    "finite F ==> F \<subseteq> A ==>
1.27 -    P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
1.28 +    P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
1.29      P F"
1.30  proof -
1.31    assume "P {}" and insert:
1.32 -    "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
1.33 +    "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
1.34    assume "finite F"
1.35    thus "F \<subseteq> A ==> P F"
1.36    proof induct
1.37      show "P {}" .
1.38 -    fix F x assume "finite F" and "x \<notin> F"
1.39 +    fix x F assume "finite F" and "x \<notin> F"
1.40        and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
1.41      show "P (insert x F)"
1.42      proof (rule insert)
1.43 @@ -93,7 +93,7 @@
1.44      case empty
1.45      thus ?case by simp
1.46    next
1.47 -    case (insert F x A)
1.48 +    case (insert x F A)
1.49      have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
1.50      show "finite A"
1.51      proof cases
1.52 @@ -143,7 +143,7 @@
1.53        case empty
1.54        from P1 show ?case by simp
1.55      next
1.56 -      case (insert F x)
1.57 +      case (insert x F)
1.58        have "P (b - F - {x})"
1.59        proof (rule P2)
1.60          from _ b show "finite (b - F)" by (rule finite_subset) blast
1.61 @@ -751,7 +751,7 @@
1.62      case empty
1.63      thus ?case by simp
1.64    next
1.65 -    case (insert F x)
1.66 +    case (insert x F)
1.67      have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
1.68        by simp
1.69      also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
1.70 @@ -1014,7 +1014,7 @@
1.71        case empty
1.72        thus ?case by auto
1.73      next
1.74 -      case (insert F x)
1.75 +      case (insert x F)
1.76        thus ?case using le finiteB
1.77  	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
1.78      qed
1.79 @@ -1073,7 +1073,7 @@
1.80    proof (induct)
1.81      case empty thus ?case by simp
1.82    next
1.83 -    case (insert A x) thus ?case by (simp add: right_distrib)
1.84 +    case (insert x A) thus ?case by (simp add: right_distrib)
1.85    qed
1.86  next
1.87    case False thus ?thesis by (simp add: setsum_def)
1.88 @@ -1087,7 +1087,7 @@
1.89  proof (induct)
1.90    case empty thus ?case by simp
1.91  next
1.92 -  case (insert A x)
1.93 +  case (insert x A)
1.94    thus ?case by (auto intro: abs_triangle_ineq order_trans)
1.95  qed
1.96
1.97 @@ -1099,7 +1099,7 @@
1.98  proof (induct)
1.99    case empty thus ?case by simp
1.100  next
1.101 -  case (insert A x) thus ?case by (auto intro: order_trans)
1.102 +  case (insert x A) thus ?case by (auto intro: order_trans)
1.103  qed
1.104
1.105  subsubsection {* Cardinality of unions and Sigma sets *}
1.106 @@ -1388,7 +1388,7 @@
1.107  proof (induct)
1.108    case empty thus ?case by simp
1.109  next
1.110 -  case (insert S x)
1.111 +  case (insert x S)
1.112    show ?case
1.113    proof (cases)
1.114      assume "S = {}" thus ?thesis by simp
1.115 @@ -1411,7 +1411,7 @@
1.116  proof (induct)
1.117    case empty thus ?case by simp
1.118  next
1.119 -  case (insert S x)
1.120 +  case (insert x S)
1.121    show ?case
1.122    proof (cases)
1.123      assume "S = {}" thus ?thesis by simp
```