diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Wed Nov 28 15:38:12 2012 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Nov 28 15:59:18 2012 +0100 @@ -1004,7 +1004,7 @@ plusinf:: "fm \ fm" (* Virtual substitution of +\*) minusinf:: "fm \ fm" (* Virtual substitution of -\*) \ :: "fm \ int" (* Compute lcm {d| N\<^isup>? Dvd c*x+t \ p}*) - d\ :: "fm \ int \ bool" (* checks if a given l divides all the ds above*) + d_\ :: "fm \ int \ bool" (* checks if a given l divides all the ds above*) recdef minusinf "measure size" "minusinf (And p q) = And (minusinf p) (minusinf q)" @@ -1038,18 +1038,18 @@ "\ (NDvd i (CN 0 c e)) = i" "\ p = 1" -recdef d\ "measure size" - "d\ (And p q) = (\ d. d\ p d \ d\ q d)" - "d\ (Or p q) = (\ d. d\ p d \ d\ q d)" - "d\ (Dvd i (CN 0 c e)) = (\ d. i dvd d)" - "d\ (NDvd i (CN 0 c e)) = (\ d. i dvd d)" - "d\ p = (\ d. True)" +recdef d_\ "measure size" + "d_\ (And p q) = (\ d. d_\ p d \ d_\ q d)" + "d_\ (Or p q) = (\ d. d_\ p d \ d_\ q d)" + "d_\ (Dvd i (CN 0 c e)) = (\ d. i dvd d)" + "d_\ (NDvd i (CN 0 c e)) = (\ d. i dvd d)" + "d_\ p = (\ d. True)" lemma delta_mono: assumes lin: "iszlfm p" and d: "d dvd d'" - and ad: "d\ p d" - shows "d\ p d'" + and ad: "d_\ p d" + shows "d_\ p d'" using lin ad d proof(induct p rule: iszlfm.induct) case (9 i c e) thus ?case using d @@ -1060,61 +1060,61 @@ qed simp_all lemma \ : assumes lin:"iszlfm p" - shows "d\ p (\ p) \ \ p >0" + shows "d_\ p (\ p) \ \ p >0" using lin proof (induct p rule: iszlfm.induct) case (1 p q) let ?d = "\ (And p q)" from 1 lcm_pos_int have dp: "?d >0" by simp have d1: "\ p dvd \ (And p q)" using 1 by simp - hence th: "d\ p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps) + hence th: "d_\ p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps) have "\ q dvd \ (And p q)" using 1 by simp - hence th': "d\ q ?d" using delta_mono 1 by(simp only: iszlfm.simps) + hence th': "d_\ q ?d" using delta_mono 1 by(simp only: iszlfm.simps) from th th' dp show ?case by simp next case (2 p q) let ?d = "\ (And p q)" from 2 lcm_pos_int have dp: "?d >0" by simp have "\ p dvd \ (And p q)" using 2 by simp - hence th: "d\ p ?d" using delta_mono 2 by(simp only: iszlfm.simps) + hence th: "d_\ p ?d" using delta_mono 2 by(simp only: iszlfm.simps) have "\ q dvd \ (And p q)" using 2 by simp - hence th': "d\ q ?d" using delta_mono 2 by(simp only: iszlfm.simps) + hence th': "d_\ q ?d" using delta_mono 2 by(simp only: iszlfm.simps) from th th' dp show ?case by simp qed simp_all consts - a\ :: "fm \ int \ fm" (* adjusts the coeffitients of a formula *) - d\ :: "fm \ int \ bool" (* tests if all coeffs c of c divide a given l*) + a_\ :: "fm \ int \ fm" (* adjusts the coeffitients of a formula *) + d_\ :: "fm \ int \ bool" (* tests if all coeffs c of c divide a given l*) \ :: "fm \ int" (* computes the lcm of all coefficients of x*) \ :: "fm \ num list" \ :: "fm \ num list" -recdef a\ "measure size" - "a\ (And p q) = (\ k. And (a\ p k) (a\ q k))" - "a\ (Or p q) = (\ k. Or (a\ p k) (a\ q k))" - "a\ (Eq (CN 0 c e)) = (\ k. Eq (CN 0 1 (Mul (k div c) e)))" - "a\ (NEq (CN 0 c e)) = (\ k. NEq (CN 0 1 (Mul (k div c) e)))" - "a\ (Lt (CN 0 c e)) = (\ k. Lt (CN 0 1 (Mul (k div c) e)))" - "a\ (Le (CN 0 c e)) = (\ k. Le (CN 0 1 (Mul (k div c) e)))" - "a\ (Gt (CN 0 c e)) = (\ k. Gt (CN 0 1 (Mul (k div c) e)))" - "a\ (Ge (CN 0 c e)) = (\ k. Ge (CN 0 1 (Mul (k div c) e)))" - "a\ (Dvd i (CN 0 c e)) =(\ k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" - "a\ (NDvd i (CN 0 c e))=(\ k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" - "a\ p = (\ k. p)" +recdef a_\ "measure size" + "a_\ (And p q) = (\ k. And (a_\ p k) (a_\ q k))" + "a_\ (Or p q) = (\ k. Or (a_\ p k) (a_\ q k))" + "a_\ (Eq (CN 0 c e)) = (\ k. Eq (CN 0 1 (Mul (k div c) e)))" + "a_\ (NEq (CN 0 c e)) = (\ k. NEq (CN 0 1 (Mul (k div c) e)))" + "a_\ (Lt (CN 0 c e)) = (\ k. Lt (CN 0 1 (Mul (k div c) e)))" + "a_\ (Le (CN 0 c e)) = (\ k. Le (CN 0 1 (Mul (k div c) e)))" + "a_\ (Gt (CN 0 c e)) = (\ k. Gt (CN 0 1 (Mul (k div c) e)))" + "a_\ (Ge (CN 0 c e)) = (\ k. Ge (CN 0 1 (Mul (k div c) e)))" + "a_\ (Dvd i (CN 0 c e)) =(\ k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" + "a_\ (NDvd i (CN 0 c e))=(\ k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" + "a_\ p = (\ k. p)" -recdef d\ "measure size" - "d\ (And p q) = (\ k. (d\ p k) \ (d\ q k))" - "d\ (Or p q) = (\ k. (d\ p k) \ (d\ q k))" - "d\ (Eq (CN 0 c e)) = (\ k. c dvd k)" - "d\ (NEq (CN 0 c e)) = (\ k. c dvd k)" - "d\ (Lt (CN 0 c e)) = (\ k. c dvd k)" - "d\ (Le (CN 0 c e)) = (\ k. c dvd k)" - "d\ (Gt (CN 0 c e)) = (\ k. c dvd k)" - "d\ (Ge (CN 0 c e)) = (\ k. c dvd k)" - "d\ (Dvd i (CN 0 c e)) =(\ k. c dvd k)" - "d\ (NDvd i (CN 0 c e))=(\ k. c dvd k)" - "d\ p = (\ k. True)" +recdef d_\ "measure size" + "d_\ (And p q) = (\ k. (d_\ p k) \ (d_\ q k))" + "d_\ (Or p q) = (\ k. (d_\ p k) \ (d_\ q k))" + "d_\ (Eq (CN 0 c e)) = (\ k. c dvd k)" + "d_\ (NEq (CN 0 c e)) = (\ k. c dvd k)" + "d_\ (Lt (CN 0 c e)) = (\ k. c dvd k)" + "d_\ (Le (CN 0 c e)) = (\ k. c dvd k)" + "d_\ (Gt (CN 0 c e)) = (\ k. c dvd k)" + "d_\ (Ge (CN 0 c e)) = (\ k. c dvd k)" + "d_\ (Dvd i (CN 0 c e)) =(\ k. c dvd k)" + "d_\ (NDvd i (CN 0 c e))=(\ k. c dvd k)" + "d_\ p = (\ k. True)" recdef \ "measure size" "\ (And p q) = lcm (\ p) (\ q)" @@ -1169,7 +1169,7 @@ lemma minusinf_inf: assumes linp: "iszlfm p" - and u: "d\ p 1" + and u: "d_\ p 1" shows "\ (z::int). \ x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p" (is "?P p" is "\ (z::int). \ x < z. ?I x (?M p) = ?I x p") using linp u @@ -1242,7 +1242,7 @@ qed auto lemma minusinf_repeats: - assumes d: "d\ p d" and linp: "iszlfm p" + assumes d: "d_\ p d" and linp: "iszlfm p" shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)" using linp d proof(induct p rule: iszlfm.induct) @@ -1301,7 +1301,7 @@ qed qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"]) -lemma mirror\\: +lemma mirror_\_\: assumes lp: "iszlfm p" shows "(Inum (i#bs)) ` set (\ p) = (Inum (i#bs)) ` set (\ (mirror p))" using lp @@ -1337,8 +1337,8 @@ finally show ?case by simp qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc) -lemma mirror_l: "iszlfm p \ d\ p 1 - \ iszlfm (mirror p) \ d\ (mirror p) 1" +lemma mirror_l: "iszlfm p \ d_\ p 1 + \ iszlfm (mirror p) \ d_\ (mirror p) 1" by (induct p rule: mirror.induct) auto lemma mirror_\: "iszlfm p \ \ (mirror p) = \ p" @@ -1348,11 +1348,11 @@ shows "\ b\ set (\ p). numbound0 b" using lp by (induct p rule: \.induct) auto -lemma d\_mono: +lemma d_\_mono: assumes linp: "iszlfm p" - and dr: "d\ p l" + and dr: "d_\ p l" and d: "l dvd l'" - shows "d\ p l'" + shows "d_\ p l'" using dr linp dvd_trans[of _ "l" "l'", simplified d] by (induct p rule: iszlfm.induct) simp_all @@ -1363,26 +1363,26 @@ lemma \: assumes linp: "iszlfm p" - shows "\ p > 0 \ d\ p (\ p)" + shows "\ p > 0 \ d_\ p (\ p)" using linp proof(induct p rule: iszlfm.induct) case (1 p q) from 1 have dl1: "\ p dvd lcm (\ p) (\ q)" by simp from 1 have dl2: "\ q dvd lcm (\ p) (\ q)" by simp - from 1 d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] - d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] + from 1 d_\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] + d_\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] dl1 dl2 show ?case by (auto simp add: lcm_pos_int) next case (2 p q) from 2 have dl1: "\ p dvd lcm (\ p) (\ q)" by simp from 2 have dl2: "\ q dvd lcm (\ p) (\ q)" by simp - from 2 d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] - d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] + from 2 d_\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] + d_\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] dl1 dl2 show ?case by (auto simp add: lcm_pos_int) qed (auto simp add: lcm_pos_int) -lemma a\: assumes linp: "iszlfm p" and d: "d\ p l" and lp: "l > 0" - shows "iszlfm (a\ p l) \ d\ (a\ p l) 1 \ (Ifm bbs (l*x #bs) (a\ p l) = Ifm bbs (x#bs) p)" +lemma a_\: assumes linp: "iszlfm p" and d: "d_\ p l" and lp: "l > 0" + shows "iszlfm (a_\ p l) \ d_\ (a_\ p l) 1 \ (Ifm bbs (l*x #bs) (a_\ p l) = Ifm bbs (x#bs) p)" using linp d proof (induct p rule: iszlfm.induct) case (5 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+ @@ -1530,20 +1530,20 @@ finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def) qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"]) -lemma a\_ex: assumes linp: "iszlfm p" and d: "d\ p l" and lp: "l>0" - shows "(\ x. l dvd x \ Ifm bbs (x #bs) (a\ p l)) = (\ (x::int). Ifm bbs (x#bs) p)" +lemma a_\_ex: assumes linp: "iszlfm p" and d: "d_\ p l" and lp: "l>0" + shows "(\ x. l dvd x \ Ifm bbs (x #bs) (a_\ p l)) = (\ (x::int). Ifm bbs (x#bs) p)" (is "(\ x. l dvd x \ ?P x) = (\ x. ?P' x)") proof- have "(\ x. l dvd x \ ?P x) = (\ (x::int). ?P (l*x))" using unity_coeff_ex[where l="l" and P="?P", simplified] by simp - also have "\ = (\ (x::int). ?P' x)" using a\[OF linp d lp] by simp + also have "\ = (\ (x::int). ?P' x)" using a_\[OF linp d lp] by simp finally show ?thesis . qed lemma \: assumes lp: "iszlfm p" - and u: "d\ p 1" - and d: "d\ p d" + and u: "d_\ p 1" + and d: "d_\ p d" and dp: "d > 0" and nob: "\(\(j::int) \ {1 .. d}. \ b\ (Inum (a#bs)) ` set(\ p). x = b + j)" and p: "Ifm bbs (x#bs) p" (is "?P x") @@ -1637,8 +1637,8 @@ lemma \': assumes lp: "iszlfm p" - and u: "d\ p 1" - and d: "d\ p d" + and u: "d_\ p 1" + and d: "d_\ p d" and dp: "d > 0" shows "\ x. \(\(j::int) \ {1 .. d}. \ b\ set(\ p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \ Ifm bbs (x#bs) p \ Ifm bbs ((x - d)#bs) p" (is "\ x. ?b \ ?P x \ ?P (x - d)") proof(clarify) @@ -1672,8 +1672,8 @@ theorem cp_thm: assumes lp: "iszlfm p" - and u: "d\ p 1" - and d: "d\ p d" + and u: "d_\ p 1" + and d: "d_\ p d" and dp: "d > 0" shows "(\ (x::int). Ifm bbs (x #bs) p) = (\ j\ {1.. d}. Ifm bbs (j #bs) (minusinf p) \ (\ b \ set (\ p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))" (is "(\ (x::int). ?P (x)) = (\ j\ ?D. ?M j \ (\ b\ ?B. ?P (?I b + j)))") @@ -1706,27 +1706,27 @@ lemma cp_thm': assumes lp: "iszlfm p" - and up: "d\ p 1" and dd: "d\ p d" and dp: "d > 0" + and up: "d_\ p 1" and dd: "d_\ p d" and dp: "d > 0" shows "(\ x. Ifm bbs (x#bs) p) = ((\ j\ {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \ (\ j\ {1.. d}. \ b\ (Inum (i#bs)) ` set (\ p). Ifm bbs ((b+j)#bs) p))" using cp_thm[OF lp up dd dp,where i="i"] by auto definition unit :: "fm \ fm \ num list \ int" where - "unit p \ (let p' = zlfm p ; l = \ p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\ p' l); d = \ q; + "unit p \ (let p' = zlfm p ; l = \ p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\ p' l); d = \ q; B = remdups (map simpnum (\ q)) ; a = remdups (map simpnum (\ q)) in if length B \ length a then (q,B,d) else (mirror q, a,d))" lemma unit: assumes qf: "qfree p" - shows "\ q B d. unit p = (q,B,d) \ ((\ x. Ifm bbs (x#bs) p) = (\ x. Ifm bbs (x#bs) q)) \ (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\ q) \ d\ q 1 \ d\ q d \ d >0 \ iszlfm q \ (\ b\ set B. numbound0 b)" + shows "\ q B d. unit p = (q,B,d) \ ((\ x. Ifm bbs (x#bs) p) = (\ x. Ifm bbs (x#bs) q)) \ (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\ q) \ d_\ q 1 \ d_\ q d \ d >0 \ iszlfm q \ (\ b\ set B. numbound0 b)" proof- fix q B d assume qBd: "unit p = (q,B,d)" let ?thes = "((\ x. Ifm bbs (x#bs) p) = (\ x. Ifm bbs (x#bs) q)) \ Inum (i#bs) ` set B = Inum (i#bs) ` set (\ q) \ - d\ q 1 \ d\ q d \ 0 < d \ iszlfm q \ (\ b\ set B. numbound0 b)" + d_\ q 1 \ d_\ q d \ 0 < d \ iszlfm q \ (\ b\ set B. numbound0 b)" let ?I = "\ x p. Ifm bbs (x#bs) p" let ?p' = "zlfm p" let ?l = "\ ?p'" - let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\ ?p' ?l)" + let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\ ?p' ?l)" let ?d = "\ ?q" let ?B = "set (\ ?q)" let ?B'= "remdups (map simpnum (\ ?q))" @@ -1736,11 +1736,11 @@ have pp': "\ i. ?I i ?p' = ?I i p" by auto from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]] have lp': "iszlfm ?p'" . - from lp' \[where p="?p'"] have lp: "?l >0" and dl: "d\ ?p' ?l" by auto - from a\_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp' + from lp' \[where p="?p'"] have lp: "?l >0" and dl: "d_\ ?p' ?l" by auto + from a_\_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp' have pq_ex:"(\ (x::int). ?I x p) = (\ x. ?I x ?q)" by simp - from lp' lp a\[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d\ ?q 1" by auto - from \[OF lq] have dp:"?d >0" and dd: "d\ ?q ?d" by blast+ + from lp' lp a_\[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\ ?q 1" by auto + from \[OF lq] have dp:"?d >0" and dd: "d_\ ?q ?d" by blast+ let ?N = "\ t. Inum (i#bs) t" have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto also have "\ = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto @@ -1762,13 +1762,13 @@ {assume "\ (length ?B' \ length ?A')" hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d" using qBd by (auto simp add: Let_def unit_def) - with AA' mirror\\[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\ q)" + with AA' mirror_\_\[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\ q)" and bn: "\b\ set B. numbound0 b" by simp+ from mirror_ex[OF lq] pq_ex q have pqm_eq:"(\ (x::int). ?I x p) = (\ (x::int). ?I x q)" by simp from lq uq q mirror_l[where p="?q"] - have lq': "iszlfm q" and uq: "d\ q 1" by auto - from \[OF lq'] mirror_\[OF lq] q d have dq:"d\ q d " by auto + have lq': "iszlfm q" and uq: "d_\ q 1" by auto + from \[OF lq'] mirror_\[OF lq] q d have dq:"d_\ q d " by auto from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp } ultimately show ?thes by blast @@ -1803,7 +1803,7 @@ have qbf:"unit p = (?q,?B,?d)" by simp from unit[OF qf qbf] have pq_ex: "(\(x::int). ?I x p) = (\ (x::int). ?I x ?q)" and B:"?N ` set ?B = ?N ` set (\ ?q)" and - uq:"d\ ?q 1" and dd: "d\ ?q ?d" and dp: "?d > 0" and + uq:"d_\ ?q 1" and dd: "d_\ ?q ?d" and dp: "?d > 0" and lq: "iszlfm ?q" and Bn: "\ b\ set ?B. numbound0 b" by auto from zlin_qfree[OF lq] have qfq: "qfree ?q" .