1.1 --- a/More_MPoly.thy	Mon May 30 16:55:59 2016 +0200
     1.2 +++ b/More_MPoly.thy	Wed Jun 01 10:30:14 2016 +0200
     1.3 @@ -395,9 +395,87 @@
     1.4  definition extract_var::"'a::comm_ring_1 mpoly \<Rightarrow> nat \<Rightarrow> 'a::comm_ring_1 mpoly mpoly" where
     1.5  "extract_var p v = (\<Sum>m. monom (remove_key v m) (monom (Poly_Mapping.single v (Poly_Mapping.lookup m v)) (coeff p m)))"
     1.6  
     1.7 +lemma extract_var_finite_set: 
     1.8 +assumes "{m'. coeff p m' \<noteq> 0} \<subseteq> S"
     1.9 +assumes "finite S"
    1.10 +shows "extract_var p v = (\<Sum>m\<in>S. monom (remove_key v m) (monom (Poly_Mapping.single v (Poly_Mapping.lookup m v)) (coeff p m)))"
    1.11 +proof-
    1.12 +  {
    1.13 +    fix m' assume "coeff p m' = 0" 
    1.14 +    then have "monom (remove_key v m') (monom (Poly_Mapping.single v (Poly_Mapping.lookup m' v)) (coeff p m')) = 0" 
    1.15 +      using monom.abs_eq monom_zero single_zero by metis
    1.16 +  }
    1.17 +  then have 0:"{a. monom (remove_key v a) (monom (Poly_Mapping.single v (Poly_Mapping.lookup a v)) (coeff p a)) \<noteq> 0} \<subseteq> S"
    1.18 +    using `{m'. coeff p m' \<noteq> 0} \<subseteq> S` by fastforce
    1.19 +  then show ?thesis 
    1.20 +    unfolding extract_var_def using Sum_any.expand_superset [OF `finite S` 0] by metis
    1.21 +qed
    1.22  
    1.23 -lemma "(\<And>m'. m\<noteq>m' \<Longrightarrow> f m' = 0) \<Longrightarrow> (\<Sum>m'. f m') = f m" sorry
    1.24 +lemma extract_var_non_zero_coeff: "extract_var p v = (\<Sum>m\<in>{m'. coeff p m' \<noteq> 0}. monom (remove_key v m) (monom (Poly_Mapping.single v (Poly_Mapping.lookup m v)) (coeff p m)))"
    1.25 +  using extract_var_finite_set  coeff_def finite_lookup order_refl by (metis (no_types, lifting) Collect_cong setsum.cong)
    1.26  
    1.27 +
    1.28 +lemma remove_key_single[simp]: "remove_key v (Poly_Mapping.single v n) = 0"
    1.29 +proof - 
    1.30 + have 0:"\<And>k. (Poly_Mapping.lookup (Poly_Mapping.single v n) k when k \<noteq> v) = 0" by (simp add: lookup_single_not_eq when_def)
    1.31 + show ?thesis unfolding remove_key_def 0 by (simp add: zero_poly_mapping_def)
    1.32 +qed
    1.33 +
    1.34 +
    1.35 +lemma extract_var_monom: 
    1.36 +shows "extract_var (monom m a) v = monom (remove_key v m) (monom (Poly_Mapping.single v (Poly_Mapping.lookup m v)) a)"
    1.37 +proof (cases "a = 0")
    1.38 +  assume "a \<noteq> 0"
    1.39 +  have 0:"{m'. coeff (monom m a) m' \<noteq> 0} = {m}" 
    1.40 +    unfolding coeff_monom using \<open>a \<noteq> 0\<close> by auto
    1.41 +  show ?thesis
    1.42 +    unfolding extract_var_non_zero_coeff unfolding 0 unfolding coeff_monom  
    1.43 +    using setsum.insert[OF finite.emptyI, unfolded setsum.empty add.right_neutral] when_def
    1.44 +    by auto
    1.45 +next 
    1.46 +  assume "a = 0"
    1.47 +  have 0:"{m'. coeff (monom m a) m' \<noteq> 0} = {}" 
    1.48 +    unfolding coeff_monom using \<open>a = 0\<close> by auto
    1.49 +  show ?thesis unfolding extract_var_non_zero_coeff 0 
    1.50 +    by (smt \<open>a = 0\<close> monom.abs_eq monom_zero setsum.empty single_zero)
    1.51 +qed
    1.52 +
    1.53 +
    1.54 +lemma extract_var_single: "extract_var (monom (Poly_Mapping.single v n) a) v = monom 0 (monom (Poly_Mapping.single v n) a)"
    1.55 +unfolding extract_var_monom by simp
    1.56 +
    1.57 +lemma extract_var_single': 
    1.58 +assumes "v \<noteq> v'"
    1.59 +shows "extract_var (monom (Poly_Mapping.single v n) a) v' = monom (Poly_Mapping.single v n) (monom 0 a)"
    1.60 +unfolding extract_var_monom using assms by (metis add.right_neutral lookup_single_not_eq remove_key_sum single_zero)
    1.61 +
    1.62 +lemma
    1.63 +fixes p::"'a::comm_ring_1 mpoly"
    1.64 +shows "reduce_nested_mpoly (extract_var p v) = p" 
    1.65 +proof (induction p rule:mpoly_induct)
    1.66 +  case (monom m a)
    1.67 +  then show ?case
    1.68 +  proof (induction m arbitrary:a rule:poly_mapping_induct)
    1.69 +    case (single v' n)
    1.70 +    show ?case 
    1.71 +    proof (cases "v' = v") 
    1.72 +      case True
    1.73 +      then show ?thesis 
    1.74 +        by (metis (no_types, lifting) insertion_single mult.right_neutral power_0 
    1.75 +        reduce_nested_mpoly_def single_zero extract_var_single)
    1.76 +    next
    1.77 +      case False
    1.78 +      then show ?thesis unfolding extract_var_single'[OF False] reduce_nested_mpoly_def insertion_single
    1.79 +        by (simp add: monom_pow mult_monom) 
    1.80 +    qed
    1.81 +  next
    1.82 +    case (sum m m' v n a)
    1.83 +    then show ?case using mult_monom[of m a m' 1] unfolding extract_var_monom
    1.84 +    
    1.85 +   
    1.86 +qed 
    1.87 +
    1.88 +thm insertion_single
    1.89  lemma "reduce_nested_mpoly (extract_var p v) = p" 
    1.90  proof (induction p rule:mpoly_induct)
    1.91    case (monom m a)
    1.92 @@ -408,9 +486,11 @@
    1.93        (monom (Poly_Mapping.single v (Poly_Mapping.lookup m' v)) (coeff (monom m a) m')) = 0" 
    1.94        using monom.abs_eq monom_zero single_zero by metis
    1.95    }
    1.96 -  then have "extract_var (monom m a) v = monom (remove_key v m) (monom (Poly_Mapping.single v (Poly_Mapping.lookup m v)) (coeff (monom m a) m))" unfolding extract_var_def  by (smt Sum_any.cong Sum_any.delta)
    1.97 -  then show ?case 
    1.98 -   sorry
    1.99 +  then have 0:"extract_var (monom m a) v = monom (remove_key v m) (monom (Poly_Mapping.single v (Poly_Mapping.lookup m v)) (coeff (monom m a) m))" 
   1.100 +    unfolding extract_var_def Sum_any.delta[of m "\<lambda>ma. monom (remove_key v ma) (monom (Poly_Mapping.single v (Poly_Mapping.lookup ma v)) (coeff (monom m a) ma))", symmetric] 
   1.101 +    by (metis (no_types, hide_lams) coeff_def lookup_single_not_eq monom.abs_eq monom.rep_eq monom_zero single_zero)
   1.102 +  show ?case unfolding 0 reduce_nested_mpoly_def 
   1.103 +   sledgehammer
   1.104  qed 
   1.105  
   1.106  end
   1.107 \ No newline at end of file