src/HOL/ex/Reflected_Presburger.thy

 "islintn (n0, Cst i) = True"
 "islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i \<noteq> 0 \<and> n0 \<le> n \<and> islintn (n+1,r))"
 "islintn (n0, t) = False"
 
 definition
-  islint :: "intterm \<Rightarrow> bool"
+  islint :: "intterm \<Rightarrow> bool" where
   "islint t = islintn(0,t)"
 
 (* And the equivalence to the first definition *)
 lemma islinintterm_eq_islint: "islinintterm t = islint t"
   using islint_def

   "\<And> m. islintn(m,t) \<Longrightarrow> islintn(m,lin_mul(l,t))"
   by (induct l t rule: lin_mul.induct) simp_all
 
 (* lin_neg neagtes a linear term *)
 definition
-  lin_neg :: "intterm \<Rightarrow> intterm"
+  lin_neg :: "intterm \<Rightarrow> intterm" where
   "lin_neg i = lin_mul ((-1::int),i)"
 
 (* lin_neg has the semantics of Neg *)
 lemma lin_neg_corr:
   assumes lint: "islinintterm  t"

 using linform_isqfree linform_lin 
 by simp
 
 (* Definitions and lemmas about gcd and lcm *)
 definition
-  lcm :: "nat \<times> nat \<Rightarrow> nat"
+  lcm :: "nat \<times> nat \<Rightarrow> nat" where
   "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
 
 definition
-  ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
+  ilcm :: "int \<Rightarrow> int \<Rightarrow> int" where
   "ilcm = (\<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j))))"
 
 (* ilcm_dvd12 are needed later *)
 lemma lcm_dvd1: 
   assumes mpos: " m >0"

 "adjustcoeff (l,p) = p"
 
 
 (* unitycoeff expects a quantifier free formula an transforms it to an equivalent formula where the bound variable occurs only with coeffitient 1  or -1 *)
 definition
-  unitycoeff :: "QF \<Rightarrow> QF"
+  unitycoeff :: "QF \<Rightarrow> QF" where
   "unitycoeff p =
   (let l = formlcm p;
        p' = adjustcoeff (l,p)
    in (if l=1 then p' else 
       (And (Divides (Cst l) (Add (Mult (Cst 1) (Var 0)) (Cst 0))) p')))"

 by (cases f, auto) (cases g, auto)+
 
 
 (* An implementation of sets trough lists *)
 definition
-  list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "list_insert x xs = (if x mem xs then xs else x#xs)"
 
 lemma list_insert_set: "set (list_insert x xs) = set (x#xs)"
 by(induct xs) (auto simp add: list_insert_def)
 

 qed
 
 (* An implementation of cooper's method for both plus/minus/infinity *)
 
 (* unify the formula *)
-definition unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
+definition unify:: "QF \<Rightarrow> (QF \<times> intterm list)" where
   "unify p =
   (let q = unitycoeff p;
        B = list_set(bset q);
        A = list_set (aset q)
   in

   from explode_minf_corr2[OF unifq bst] unify_ex[OF linp] show ?thesis
     using qB_def by simp
 qed
 (* An implementation of cooper's method *)
 definition
-  cooper:: "QF \<Rightarrow> QF option"
+  cooper:: "QF \<Rightarrow> QF option" where
   "cooper p = lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
 
 (* cooper eliminates quantifiers *)
 lemma cooper_qfree: "(\<And> q q'. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow>  isqfree q')"
 proof-

   show "?P ats (QEx q) = ?P ats q'" by simp
 qed  
 
 (* A decision procedure for Presburger Arithmetics *)
 definition
-  pa:: "QF \<Rightarrow> QF option"
+  pa:: "QF \<Rightarrow> QF option" where
   "pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
 
 lemma psimpl_qfree: "isqfree p \<Longrightarrow> isqfree (psimpl p)"
 apply(induct p rule: isqfree.induct)
 apply(auto simp add: Let_def)