src/HOL/Presburger.thy
changeset 35050 9f841f20dca6
parent 33318 ddd97d9dfbfb
child 35216 7641e8d831d2
equal deleted inserted replaced
35049:00f311c32444 35050:9f841f20dca6
    28   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<noteq> t) = True"
    28   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<noteq> t) = True"
    29   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x < t) = True"
    29   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x < t) = True"
    30   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
    30   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
    31   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
    31   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
    32   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
    32   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
    33   "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (d dvd x + s) = (d dvd x + s)"
    33   "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
    34   "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    34   "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    35   "\<exists>z.\<forall>x<z. F = F"
    35   "\<exists>z.\<forall>x<z. F = F"
    36   by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
    36   by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
    37 
    37 
    38 lemma pinf:
    38 lemma pinf:
    39   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 
    39   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 
    44   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<noteq> t) = True"
    44   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<noteq> t) = True"
    45   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x < t) = False"
    45   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x < t) = False"
    46   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
    46   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
    47   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
    47   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
    48   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
    48   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
    49   "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (d dvd x + s) = (d dvd x + s)"
    49   "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
    50   "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    50   "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    51   "\<exists>z.\<forall>x>z. F = F"
    51   "\<exists>z.\<forall>x>z. F = F"
    52   by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
    52   by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
    53 
    53 
    54 lemma inf_period:
    54 lemma inf_period:
    55   "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    55   "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    56     \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
    56     \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
    57   "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    57   "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    58     \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
    58     \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
    59   "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
    59   "(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
    60   "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    60   "(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    61   "\<forall>x k. F = F"
    61   "\<forall>x k. F = F"
    62 apply (auto elim!: dvdE simp add: algebra_simps)
    62 apply (auto elim!: dvdE simp add: algebra_simps)
    63 unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
    63 unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
    64 unfolding dvd_def mult_commute [of d] 
    64 unfolding dvd_def mult_commute [of d] 
    65 by auto
    65 by auto
   241 next
   241 next
   242   case (step i)
   242   case (step i)
   243   {fix x
   243   {fix x
   244     have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
   244     have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
   245     also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"]
   245     also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"]
   246       by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
   246       by (simp add: algebra_simps)
   247     ultimately have "P x \<longrightarrow> P(x - (i + 1) * d)" by blast}
   247     ultimately have "P x \<longrightarrow> P(x - (i + 1) * d)" by blast}
   248   thus ?case ..
   248   thus ?case ..
   249 qed
   249 qed
   250 
   250 
   251 lemma  minusinfinity:
   251 lemma  minusinfinity:
   358 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
   358 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
   359 apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
   359 apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
   360 apply(fastsimp)
   360 apply(fastsimp)
   361 done
   361 done
   362 
   362 
   363 theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Ring_and_Field.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
   363 theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Rings.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
   364   apply (rule eq_reflection [symmetric])
   364   apply (rule eq_reflection [symmetric])
   365   apply (rule iffI)
   365   apply (rule iffI)
   366   defer
   366   defer
   367   apply (erule exE)
   367   apply (erule exE)
   368   apply (rule_tac x = "l * x" in exI)
   368   apply (rule_tac x = "l * x" in exI)