src/HOL/ex/Reflected_Presburger.thy
changeset 29700 22faf21db3df
parent 29667 53103fc8ffa3
     1.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Fri Jan 30 13:41:45 2009 +0000
     1.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Sat Jan 31 09:04:16 2009 +0100
     1.3 @@ -995,7 +995,7 @@
     1.4      hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
     1.5    moreover
     1.6    {assume "?c=0" and "j\<noteq>0" hence ?case 
     1.7 -      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
     1.8 +      using zsplit0_I[OF spl, where x="i" and bs="bs"]
     1.9      apply (auto simp add: Let_def split_def algebra_simps) 
    1.10      apply (cases "?r",auto)
    1.11      apply (case_tac nat, auto)
    1.12 @@ -1003,14 +1003,12 @@
    1.13    moreover
    1.14    {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    1.15        by (simp add: nb Let_def split_def)
    1.16 -    hence ?case using Ia cp jnz by (simp add: Let_def split_def 
    1.17 -	zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
    1.18 +    hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
    1.19    moreover
    1.20    {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    1.21        by (simp add: nb Let_def split_def)
    1.22      hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
    1.23 -      by (simp add: Let_def split_def 
    1.24 -      zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
    1.25 +      by (simp add: Let_def split_def) }
    1.26    ultimately show ?case by blast
    1.27  next
    1.28    case (12 j a) 
    1.29 @@ -1026,7 +1024,7 @@
    1.30      hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
    1.31    moreover
    1.32    {assume "?c=0" and "j\<noteq>0" hence ?case 
    1.33 -      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
    1.34 +      using zsplit0_I[OF spl, where x="i" and bs="bs"]
    1.35      apply (auto simp add: Let_def split_def algebra_simps) 
    1.36      apply (cases "?r",auto)
    1.37      apply (case_tac nat, auto)
    1.38 @@ -1034,14 +1032,12 @@
    1.39    moreover
    1.40    {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    1.41        by (simp add: nb Let_def split_def)
    1.42 -    hence ?case using Ia cp jnz by (simp add: Let_def split_def 
    1.43 -	zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
    1.44 +    hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
    1.45    moreover
    1.46    {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    1.47        by (simp add: nb Let_def split_def)
    1.48      hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
    1.49 -      by (simp add: Let_def split_def 
    1.50 -      zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
    1.51 +      by (simp add: Let_def split_def)}
    1.52    ultimately show ?case by blast
    1.53  qed auto
    1.54  
    1.55 @@ -1210,7 +1206,7 @@
    1.56    "mirror p = p"
    1.57      (* Lemmas for the correctness of \<sigma>\<rho> *)
    1.58  lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
    1.59 -by auto
    1.60 +by simp
    1.61  
    1.62  lemma minusinf_inf:
    1.63    assumes linp: "iszlfm p"
    1.64 @@ -1220,12 +1216,12 @@
    1.65  using linp u
    1.66  proof (induct p rule: minusinf.induct)
    1.67    case (1 p q) thus ?case 
    1.68 -    by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
    1.69 +    by auto (rule_tac x="min z za" in exI,simp)
    1.70  next
    1.71    case (2 p q) thus ?case 
    1.72 -    by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
    1.73 +    by auto (rule_tac x="min z za" in exI,simp)
    1.74  next
    1.75 -  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
    1.76 +  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
    1.77    fix a
    1.78    from 3 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
    1.79    proof(clarsimp)
    1.80 @@ -1235,7 +1231,7 @@
    1.81    qed
    1.82    thus ?case by auto
    1.83  next
    1.84 -  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
    1.85 +  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
    1.86    fix a
    1.87    from 4 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
    1.88    proof(clarsimp)
    1.89 @@ -1245,7 +1241,7 @@
    1.90    qed
    1.91    thus ?case by auto
    1.92  next
    1.93 -  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
    1.94 +  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
    1.95    fix a
    1.96    from 5 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
    1.97    proof(clarsimp)
    1.98 @@ -1255,7 +1251,7 @@
    1.99    qed
   1.100    thus ?case by auto
   1.101  next
   1.102 -  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
   1.103 +  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
   1.104    fix a
   1.105    from 6 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
   1.106    proof(clarsimp)
   1.107 @@ -1265,7 +1261,7 @@
   1.108    qed
   1.109    thus ?case by auto
   1.110  next
   1.111 -  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
   1.112 +  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
   1.113    fix a
   1.114    from 7 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
   1.115    proof(clarsimp)
   1.116 @@ -1275,7 +1271,7 @@
   1.117    qed
   1.118    thus ?case by auto
   1.119  next
   1.120 -  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
   1.121 +  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
   1.122    fix a
   1.123    from 8 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
   1.124    proof(clarsimp)
   1.125 @@ -1595,15 +1591,15 @@
   1.126    shows "?P (x - d)"
   1.127  using lp u d dp nob p
   1.128  proof(induct p rule: iszlfm.induct)
   1.129 -  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   1.130 +  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp+
   1.131      with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
   1.132      show ?case by simp
   1.133  next
   1.134 -  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   1.135 +  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp+
   1.136      with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
   1.137      show ?case by simp
   1.138  next
   1.139 -  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   1.140 +  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp+
   1.141      let ?e = "Inum (x # bs) e"
   1.142      {assume "(x-d) +?e > 0" hence ?case using c1 
   1.143        numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
   1.144 @@ -1622,7 +1618,7 @@
   1.145      ultimately show ?case by blast
   1.146  next
   1.147    case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" 
   1.148 -    using dvd1_eq1[where x="c"] by simp+
   1.149 +    by simp+
   1.150      let ?e = "Inum (x # bs) e"
   1.151      {assume "(x-d) +?e \<ge> 0" hence ?case using  c1 
   1.152        numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
   1.153 @@ -1640,7 +1636,7 @@
   1.154        with nob have ?case by simp }
   1.155      ultimately show ?case by blast
   1.156  next
   1.157 -  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   1.158 +  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
   1.159      let ?e = "Inum (x # bs) e"
   1.160      let ?v="(Sub (C -1) e)"
   1.161      have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
   1.162 @@ -1648,7 +1644,7 @@
   1.163        by simp (erule ballE[where x="1"],
   1.164  	simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
   1.165  next
   1.166 -  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   1.167 +  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
   1.168      let ?e = "Inum (x # bs) e"
   1.169      let ?v="Neg e"
   1.170      have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
   1.171 @@ -1662,7 +1658,7 @@
   1.172         with prems(11) have ?case using dp by simp}
   1.173    ultimately show ?case by blast
   1.174  next 
   1.175 -  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   1.176 +  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
   1.177      let ?e = "Inum (x # bs) e"
   1.178      from prems have id: "j dvd d" by simp
   1.179      from c1 have "?p x = (j dvd (x+ ?e))" by simp
   1.180 @@ -1671,7 +1667,7 @@
   1.181      finally show ?case 
   1.182        using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
   1.183  next
   1.184 -  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   1.185 +  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
   1.186      let ?e = "Inum (x # bs) e"
   1.187      from prems have id: "j dvd d" by simp
   1.188      from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp