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