author berghofe Tue Apr 08 09:44:21 2003 +0200 (2003-04-08) changeset 13905 3e496c70f2f3 parent 13904 c13e6e218a69 child 13906 eefdd6b14508
```     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Tue Apr 08 09:40:30 2003 +0200
1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Apr 08 09:44:21 2003 +0200
1.3 @@ -274,7 +274,7 @@
1.4         val m = l div (dest_numeral c)
1.5         val n = abs (m)
1.6         val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
1.7 -       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
1.8 +       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
1.9         in (ACPI(n,fm),rs)
1.10         end
1.11    else  let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt ))
1.12 @@ -765,21 +765,21 @@
1.13       val cx = cterm_of sg x
1.14       val ca = cterm_of sg a
1.15     in case p of
1.16 -     "op <" => let val pre = prove_elementar sg "ss"
1.17 +     "op <" => let val pre = prove_elementar sg "lf"
1.18  	                  (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
1.19  	           val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
1.20 -		      in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
1.21 +		      in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
1.22                     end
1.23 -    |"op =" =>let val pre = prove_elementar sg "ss"
1.24 +    |"op =" =>let val pre = prove_elementar sg "lf"
1.25  	    (HOLogic.Not \$ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
1.26  	          in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
1.27 -	             in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
1.28 +	             in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
1.29                        end
1.30                    end
1.31 -    |"Divides.op dvd" =>let val pre = prove_elementar sg "ss"
1.32 +    |"Divides.op dvd" =>let val pre = prove_elementar sg "lf"
1.33  	   (HOLogic.Not \$ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
1.34  	                 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
1.35 -                         in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
1.36 +                         in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
1.37
1.38                            end
1.39    end
1.40 @@ -789,7 +789,7 @@
1.41       val cc = cterm_of sg c
1.42       val ct = cterm_of sg t
1.43       val cx = cterm_of sg x
1.44 -     val pre = prove_elementar sg "ss"
1.45 +     val pre = prove_elementar sg "lf"
1.46         (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
1.47         val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
1.48
```
```     2.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Apr 08 09:40:30 2003 +0200
2.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Apr 08 09:44:21 2003 +0200
2.3 @@ -274,7 +274,7 @@
2.4         val m = l div (dest_numeral c)
2.5         val n = abs (m)
2.6         val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
2.7 -       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
2.8 +       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
2.9         in (ACPI(n,fm),rs)
2.10         end
2.11    else  let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt ))
2.12 @@ -765,21 +765,21 @@
2.13       val cx = cterm_of sg x
2.14       val ca = cterm_of sg a
2.15     in case p of
2.16 -     "op <" => let val pre = prove_elementar sg "ss"
2.17 +     "op <" => let val pre = prove_elementar sg "lf"
2.18  	                  (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
2.19  	           val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
2.20 -		      in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
2.21 +		      in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
2.22                     end
2.23 -    |"op =" =>let val pre = prove_elementar sg "ss"
2.24 +    |"op =" =>let val pre = prove_elementar sg "lf"
2.25  	    (HOLogic.Not \$ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
2.26  	          in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
2.27 -	             in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
2.28 +	             in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
2.29                        end
2.30                    end
2.31 -    |"Divides.op dvd" =>let val pre = prove_elementar sg "ss"
2.32 +    |"Divides.op dvd" =>let val pre = prove_elementar sg "lf"
2.33  	   (HOLogic.Not \$ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
2.34  	                 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
2.35 -                         in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
2.36 +                         in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
2.37
2.38                            end
2.39    end
2.40 @@ -789,7 +789,7 @@
2.41       val cc = cterm_of sg c
2.42       val ct = cterm_of sg t
2.43       val cx = cterm_of sg x
2.44 -     val pre = prove_elementar sg "ss"
2.45 +     val pre = prove_elementar sg "lf"
2.46         (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
2.47         val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
2.48
```