merged
authorpaulson
Wed Jun 24 16:28:30 2009 +0100 (2009-06-24)
changeset 3190867224d7d4448
parent 31791 c9a1caf218c8
parent 31907 9d4a03e008c0
child 31909 d3b020134006
merged
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Jun 24 15:51:07 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Jun 24 16:28:30 2009 +0100
     1.3 @@ -528,7 +528,7 @@
     1.4  subsection {* A fold functional for finite sets *}
     1.5  
     1.6  text {* The intended behaviour is
     1.7 -@{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
     1.8 +@{text "fold f z {x1, ..., xn} = f x1 (\<dots> (f xn z)\<dots>)"}
     1.9  if @{text f} is ``left-commutative'':
    1.10  *}
    1.11  
    1.12 @@ -1883,14 +1883,14 @@
    1.13    (if a:A then setprod f A / f a else setprod f A)"
    1.14  by (erule finite_induct) (auto simp add: insert_Diff_if)
    1.15  
    1.16 -lemma setprod_inversef: "finite A ==>
    1.17 -  ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
    1.18 -  setprod (inverse \<circ> f) A = inverse (setprod f A)"
    1.19 +lemma setprod_inversef: 
    1.20 +  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
    1.21 +  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
    1.22  by (erule finite_induct) auto
    1.23  
    1.24  lemma setprod_dividef:
    1.25 -   "[|finite A;
    1.26 -      \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
    1.27 +  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
    1.28 +  shows  "finite A
    1.29      ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
    1.30  apply (subgoal_tac
    1.31           "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
    1.32 @@ -2725,16 +2725,16 @@
    1.33  begin
    1.34  
    1.35  definition
    1.36 -  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
    1.37 +  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>fin_" [900] 900)
    1.38  where
    1.39    "Inf_fin = fold1 inf"
    1.40  
    1.41  definition
    1.42 -  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
    1.43 +  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>fin_" [900] 900)
    1.44  where
    1.45    "Sup_fin = fold1 sup"
    1.46  
    1.47 -lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
    1.48 +lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>finA \<le> \<Squnion>finA"
    1.49  apply(unfold Sup_fin_def Inf_fin_def)
    1.50  apply(subgoal_tac "EX a. a:A")
    1.51  prefer 2 apply blast
    1.52 @@ -2745,13 +2745,13 @@
    1.53  done
    1.54  
    1.55  lemma sup_Inf_absorb [simp]:
    1.56 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
    1.57 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>finA) = a"
    1.58  apply(subst sup_commute)
    1.59  apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
    1.60  done
    1.61  
    1.62  lemma inf_Sup_absorb [simp]:
    1.63 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
    1.64 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>finA) = a"
    1.65  by (simp add: Sup_fin_def inf_absorb1
    1.66    lower_semilattice.fold1_belowI [OF dual_lattice])
    1.67  
    1.68 @@ -2763,7 +2763,7 @@
    1.69  lemma sup_Inf1_distrib:
    1.70    assumes "finite A"
    1.71      and "A \<noteq> {}"
    1.72 -  shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
    1.73 +  shows "sup x (\<Sqinter>finA) = \<Sqinter>fin{sup x a|a. a \<in> A}"
    1.74  proof -
    1.75    interpret ab_semigroup_idem_mult inf
    1.76      by (rule ab_semigroup_idem_mult_inf)
    1.77 @@ -2775,7 +2775,7 @@
    1.78  
    1.79  lemma sup_Inf2_distrib:
    1.80    assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
    1.81 -  shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
    1.82 +  shows "sup (\<Sqinter>finA) (\<Sqinter>finB) = \<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B}"
    1.83  using A proof (induct rule: finite_ne_induct)
    1.84    case singleton thus ?case
    1.85      by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
    1.86 @@ -2792,13 +2792,13 @@
    1.87      thus ?thesis by(simp add: insert(1) B(1))
    1.88    qed
    1.89    have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
    1.90 -  have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
    1.91 +  have "sup (\<Sqinter>fin(insert x A)) (\<Sqinter>finB) = sup (inf x (\<Sqinter>finA)) (\<Sqinter>finB)"
    1.92      using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
    1.93 -  also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
    1.94 -  also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
    1.95 +  also have "\<dots> = inf (sup x (\<Sqinter>finB)) (sup (\<Sqinter>finA) (\<Sqinter>finB))" by(rule sup_inf_distrib2)
    1.96 +  also have "\<dots> = inf (\<Sqinter>fin{sup x b|b. b \<in> B}) (\<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B})"
    1.97      using insert by(simp add:sup_Inf1_distrib[OF B])
    1.98 -  also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
    1.99 -    (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
   1.100 +  also have "\<dots> = \<Sqinter>fin({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
   1.101 +    (is "_ = \<Sqinter>fin?M")
   1.102      using B insert
   1.103      by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
   1.104    also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
   1.105 @@ -2808,7 +2808,7 @@
   1.106  
   1.107  lemma inf_Sup1_distrib:
   1.108    assumes "finite A" and "A \<noteq> {}"
   1.109 -  shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
   1.110 +  shows "inf x (\<Squnion>finA) = \<Squnion>fin{inf x a|a. a \<in> A}"
   1.111  proof -
   1.112    interpret ab_semigroup_idem_mult sup
   1.113      by (rule ab_semigroup_idem_mult_sup)
   1.114 @@ -2819,7 +2819,7 @@
   1.115  
   1.116  lemma inf_Sup2_distrib:
   1.117    assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   1.118 -  shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
   1.119 +  shows "inf (\<Squnion>finA) (\<Squnion>finB) = \<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B}"
   1.120  using A proof (induct rule: finite_ne_induct)
   1.121    case singleton thus ?case
   1.122      by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
   1.123 @@ -2836,13 +2836,13 @@
   1.124    have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   1.125    interpret ab_semigroup_idem_mult sup
   1.126      by (rule ab_semigroup_idem_mult_sup)
   1.127 -  have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
   1.128 +  have "inf (\<Squnion>fin(insert x A)) (\<Squnion>finB) = inf (sup x (\<Squnion>finA)) (\<Squnion>finB)"
   1.129      using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
   1.130 -  also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
   1.131 -  also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
   1.132 +  also have "\<dots> = sup (inf x (\<Squnion>finB)) (inf (\<Squnion>finA) (\<Squnion>finB))" by(rule inf_sup_distrib2)
   1.133 +  also have "\<dots> = sup (\<Squnion>fin{inf x b|b. b \<in> B}) (\<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B})"
   1.134      using insert by(simp add:inf_Sup1_distrib[OF B])
   1.135 -  also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
   1.136 -    (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
   1.137 +  also have "\<dots> = \<Squnion>fin({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
   1.138 +    (is "_ = \<Squnion>fin?M")
   1.139      using B insert
   1.140      by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
   1.141    also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
   1.142 @@ -2861,7 +2861,7 @@
   1.143  
   1.144  lemma Inf_fin_Inf:
   1.145    assumes "finite A" and "A \<noteq> {}"
   1.146 -  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
   1.147 +  shows "\<Sqinter>finA = Inf A"
   1.148  proof -
   1.149      interpret ab_semigroup_idem_mult inf
   1.150      by (rule ab_semigroup_idem_mult_inf)
   1.151 @@ -2872,7 +2872,7 @@
   1.152  
   1.153  lemma Sup_fin_Sup:
   1.154    assumes "finite A" and "A \<noteq> {}"
   1.155 -  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
   1.156 +  shows "\<Squnion>finA = Sup A"
   1.157  proof -
   1.158    interpret ab_semigroup_idem_mult sup
   1.159      by (rule ab_semigroup_idem_mult_sup)