src/HOL/ex/Reflected_Presburger.thy

--- a/src/HOL/ex/Reflected_Presburger.thy	Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Jul 14 11:04:42 2008 +0200
@@ -1077,8 +1077,8 @@
   "plusinf p = p"
 
 recdef \<delta> "measure size"
-  "\<delta> (And p q) = ilcm (\<delta> p) (\<delta> q)" 
-  "\<delta> (Or p q) = ilcm (\<delta> p) (\<delta> q)" 
+  "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)" 
+  "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)" 
   "\<delta> (Dvd i (CN 0 c e)) = i"
   "\<delta> (NDvd i (CN 0 c e)) = i"
   "\<delta> p = 1"
@@ -1110,20 +1110,20 @@
 proof (induct p rule: iszlfm.induct)
   case (1 p q) 
   let ?d = "\<delta> (And p q)"
-  from prems ilcm_pos have dp: "?d >0" by simp
+  from prems zlcm_pos have dp: "?d >0" by simp
   have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
-  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_ilcm_self1)
+  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_zlcm_self1)
   have "\<delta> q dvd \<delta> (And p q)" using prems by simp
-  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
+  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
   from th th' dp show ?case by simp
 next
   case (2 p q)  
   let ?d = "\<delta> (And p q)"
-  from prems ilcm_pos have dp: "?d >0" by simp
+  from prems zlcm_pos have dp: "?d >0" by simp
   have "\<delta> p dvd \<delta> (And p q)" using prems by simp
-  hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_ilcm_self1)
+  hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_zlcm_self1)
   have "\<delta> q dvd \<delta> (And p q)" using prems by simp
-  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
+  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
   from th th' dp show ?case by simp
 qed simp_all
 
@@ -1162,8 +1162,8 @@
   "d\<beta> p = (\<lambda> k. True)"
 
 recdef \<zeta> "measure size"
-  "\<zeta> (And p q) = ilcm (\<zeta> p) (\<zeta> q)" 
-  "\<zeta> (Or p q) = ilcm (\<zeta> p) (\<zeta> q)" 
+  "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)" 
+  "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)" 
   "\<zeta> (Eq  (CN 0 c e)) = c"
   "\<zeta> (NEq (CN 0 c e)) = c"
   "\<zeta> (Lt  (CN 0 c e)) = c"
@@ -1412,19 +1412,19 @@
 using linp
 proof(induct p rule: iszlfm.induct)
   case (1 p q)
-  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)"  by simp
-  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
-    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
+  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)"  by simp
+  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
+    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
+    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
 next
   case (2 p q)
-  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
-    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
-qed (auto simp add: ilcm_pos)
+  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
+    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
+    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
+qed (auto simp add: zlcm_pos)
 
 lemma a\<beta>: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l > 0"
   shows "iszlfm (a\<beta> p l) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a\<beta> p l) = Ifm bbs (x#bs) p)"