--- a/NEWS Thu May 17 19:49:21 2007 +0200
+++ b/NEWS Thu May 17 19:49:40 2007 +0200
@@ -530,6 +530,15 @@
*** HOL ***
+* Constant renames due to introduction of canonical name prefixing for
+ class package:
+
+ HOL.abs ~> HOL.minus_class.abs
+ HOL.divide ~> HOL.divide_class.divide
+ Nat.power ~> Nat.power_class.power
+ Nat.size ~> Nat.size_class.size
+ Numeral.number_of ~> Numeral.number_class.number_of
+
* case expressions and primrec: missing cases now mapped to "undefined"
instead of "arbitrary"
@@ -675,7 +684,7 @@
type "'a::size ==> bool"
* Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
-dvd" to "Divides.div", "Divides.mod" and "Divides.dvd". INCOMPATIBILITY.
+dvd" to "Divides.div_class.div", "Divides.div_class.mod" and "Divides.dvd". INCOMPATIBILITY.
* Added method "lexicographic_order" automatically synthesizes
termination relations as lexicographic combinations of size measures
@@ -708,7 +717,7 @@
rarely occuring name references (e.g. ``List.op mem.simps'') require
renaming (e.g. ``List.memberl.simps'').
-* Renamed constants "0" to "HOL.zero" and "1" to "HOL.one".
+* Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one".
INCOMPATIBILITY.
* Added theory Code_Generator providing class 'eq', allowing for code
@@ -737,12 +746,12 @@
"A = B" (with priority 50).
* Renamed constants in HOL.thy and Orderings.thy:
- op + ~> HOL.plus
- op - ~> HOL.minus
- uminus ~> HOL.uminus
- op * ~> HOL.times
- op < ~> Orderings.less
- op <= ~> Orderings.less_eq
+ op + ~> HOL.plus_class.plus
+ op - ~> HOL.minus_class.minus
+ uminus ~> HOL.minus_class.uminus
+ op * ~> HOL.times_class.times
+ op < ~> Orderings.ord_class.less
+ op <= ~> Orderings.ord_class.less_eq
Adaptions may be required in the following cases:
@@ -763,7 +772,8 @@
d) ML code directly refering to constant names
This in general only affects hand-written proof tactics, simprocs and so on.
-INCOMPATIBILITY: grep your sourcecode and replace names.
+INCOMPATIBILITY: grep your sourcecode and replace names. Consider use
+of const_name ML antiquotations.
* Relations less (<) and less_eq (<=) are also available on type bool.
Modified syntax to disallow nesting without explicit parentheses,
--- a/src/HOL/Algebra/abstract/Ring2.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Thu May 17 19:49:40 2007 +0200
@@ -217,7 +217,8 @@
ML {*
fun ring_ord (Const (a, _)) =
find_index (fn a' => a = a')
- ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"]
+ [@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus},
+ @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
| ring_ord _ = ~1;
fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
--- a/src/HOL/Hoare/hoare.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Hoare/hoare.ML Thu May 17 19:49:40 2007 +0200
@@ -65,7 +65,7 @@
fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm
in Collect_const t $ trm end;
-fun inclt ty = Const ("Orderings.less_eq", [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
(** Makes "Mset <= t" **)
fun Mset_incl t = let val MsetT = fastype_of t
--- a/src/HOL/Hoare/hoareAbort.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML Thu May 17 19:49:40 2007 +0200
@@ -66,7 +66,7 @@
fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm
in Collect_const t $ trm end;
-fun inclt ty = Const ("Orderings.less_eq", [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
(** Makes "Mset <= t" **)
fun Mset_incl t = let val MsetT = fastype_of t
--- a/src/HOL/Hyperreal/NSA.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Thu May 17 19:49:40 2007 +0200
@@ -671,13 +671,13 @@
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
fun reorient_proc sg _ (_ $ t $ u) =
case u of
- Const("HOL.zero", _) => NONE
- | Const("HOL.one", _) => NONE
- | Const("Numeral.number_of", _) $ _ => NONE
+ Const(@{const_name HOL.zero}, _) => NONE
+ | Const(@{const_name HOL.one}, _) => NONE
+ | Const(@{const_name Numeral.number_of}, _) $ _ => NONE
| _ => SOME (case t of
- Const("HOL.zero", _) => meta_zero_approx_reorient
- | Const("HOL.one", _) => meta_one_approx_reorient
- | Const("Numeral.number_of", _) $ _ =>
+ Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient
+ | Const(@{const_name HOL.one}, _) => meta_one_approx_reorient
+ | Const(@{const_name Numeral.number_of}, _) $ _ =>
meta_number_of_approx_reorient);
in
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu May 17 19:49:40 2007 +0200
@@ -166,7 +166,7 @@
import_theory prim_rec;
const_maps
- "<" > "Orderings.less" :: "[nat,nat]=>bool";
+ "<" > Orderings.ord_class.less :: "[nat,nat]=>bool";
end_import;
@@ -181,15 +181,15 @@
">" > HOL4Compat.nat_gt
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
- "<=" > "Orderings.less_eq" :: "[nat,nat]=>bool"
- "+" > "HOL.plus" :: "[nat,nat]=>nat"
- "*" > "HOL.times" :: "[nat,nat]=>nat"
- "-" > "HOL.minus" :: "[nat,nat]=>nat"
+ "<=" > Orderings.ord_class.less_eq :: "[nat,nat]=>bool"
+ "+" > HOL.plus_class.plus :: "[nat,nat]=>nat"
+ "*" > HOL.times_class.times :: "[nat,nat]=>nat"
+ "-" > HOL.minus_class.minus :: "[nat,nat]=>nat"
MIN > Orderings.min :: "[nat,nat]=>nat"
MAX > Orderings.max :: "[nat,nat]=>nat"
- DIV > "Divides.div" :: "[nat,nat]=>nat"
- MOD > "Divides.mod" :: "[nat,nat]=>nat"
- EXP > Nat.power :: "[nat,nat]=>nat";
+ DIV > Divides.div_class.div :: "[nat,nat]=>nat"
+ MOD > Divides.div_class.mod :: "[nat,nat]=>nat"
+ EXP > Nat.power_class.power :: "[nat,nat]=>nat";
end_import;
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Thu May 17 19:49:40 2007 +0200
@@ -23,7 +23,7 @@
inv > HOL.inverse :: "real => real"
real_add > HOL.plus :: "[real,real] => real"
real_mul > HOL.times :: "[real,real] => real"
- real_lt > "Orderings.less" :: "[real,real] => bool";
+ real_lt > Orderings.ord_class.less :: "[real,real] => bool";
ignore_thms
real_TY_DEF
@@ -51,7 +51,7 @@
const_maps
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
- real_lte > Orderings.less_eq :: "[real,real] => bool"
+ real_lte > Orderings.ord_class.less_eq :: "[real,real] => bool"
real_sub > HOL.minus :: "[real,real] => real"
"/" > HOL.divide :: "[real,real] => real"
pow > Nat.power :: "[real,nat] => real"
--- a/src/HOL/Import/HOL/arithmetic.imp Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Thu May 17 19:49:40 2007 +0200
@@ -14,19 +14,19 @@
"NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
"NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
"NUMERAL" > "HOL4Compat.NUMERAL"
- "MOD" > "Divides.mod" :: "nat => nat => nat"
"MIN" > "Orderings.min" :: "nat => nat => nat"
"MAX" > "Orderings.max" :: "nat => nat => nat"
"FUNPOW" > "HOL4Compat.FUNPOW"
- "EXP" > "Nat.power" :: "nat => nat => nat"
- "DIV" > "Divides.div" :: "nat => nat => nat"
+ "EXP" > "Nat.power_class.power" :: "nat => nat => nat"
+ "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
+ "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
- "<=" > "Orderings.less_eq" :: "nat => nat => bool"
- "-" > "HOL.minus" :: "nat => nat => nat"
- "+" > "HOL.plus" :: "nat => nat => nat"
- "*" > "HOL.times" :: "nat => nat => nat"
+ "<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
+ "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
+ "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
+ "*" > "HOL.times_class.times" :: "nat => nat => nat"
thm_maps
"num_case_def" > "HOL4Compat.num_case_def"
--- a/src/HOL/Import/HOL/list.imp Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/list.imp Thu May 17 19:49:40 2007 +0200
@@ -22,7 +22,7 @@
"MEM" > "List.op mem"
"MAP2" > "HOL4Compat.map2"
"MAP" > "List.map"
- "LENGTH" > "Nat.size"
+ "LENGTH" > "Nat.size_class.size"
"LAST" > "List.last"
"HD" > "List.hd"
"FRONT" > "List.butlast"
--- a/src/HOL/Import/HOL/prim_rec.imp Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/prim_rec.imp Thu May 17 19:49:40 2007 +0200
@@ -18,7 +18,7 @@
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
"PRE" > "HOL4Base.prim_rec.PRE"
- "<" > "Orderings.less" :: "nat => nat => bool"
+ "<" > "Orderings.ord_class.less" :: "nat => nat => bool"
thm_maps
"wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
--- a/src/HOL/Import/HOL/real.imp Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/real.imp Thu May 17 19:49:40 2007 +0200
@@ -10,14 +10,14 @@
const_maps
"sup" > "HOL4Real.real.sup"
"sum" > "HOL4Real.real.sum"
- "real_sub" > "HOL.minus" :: "real => real => real"
+ "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
- "real_lte" > "Orderings.less_eq" :: "real => real => bool"
+ "real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
- "pow" > "Nat.power" :: "real => nat => real"
- "abs" > "HOL.abs" :: "real => real"
- "/" > "HOL.divide" :: "real => real => real"
+ "pow" > "Nat.power_class.power" :: "real => nat => real"
+ "abs" > "HOL.minus_class.abs" :: "real => real"
+ "/" > "HOL.divides_class.divide" :: "real => real => real"
thm_maps
"sup_def" > "HOL4Real.real.sup_def"
--- a/src/HOL/Import/HOL/realax.imp Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/realax.imp Thu May 17 19:49:40 2007 +0200
@@ -27,13 +27,13 @@
"treal_add" > "HOL4Real.realax.treal_add"
"treal_1" > "HOL4Real.realax.treal_1"
"treal_0" > "HOL4Real.realax.treal_0"
- "real_neg" > "HOL.uminus" :: "real => real"
- "real_mul" > "HOL.times" :: "real => real => real"
- "real_lt" > "Orderings.less" :: "real => real => bool"
- "real_add" > "HOL.plus" :: "real => real => real"
- "real_1" > "1" :: "real"
- "real_0" > "0" :: "real"
- "inv" > "HOL.inverse" :: "real => real"
+ "real_neg" > "HOL.minus_class.uminus" :: "real => real"
+ "real_mul" > "HOL.times_class.times" :: "real => real => real"
+ "real_lt" > "Orderings.ord_class.less" :: "real => real => bool"
+ "real_add" > "HOL.plus_class.plus" :: "real => real => real"
+ "real_1" > "HOL.one_class.one" :: "real"
+ "real_0" > "HOL.zero_class.zero" :: "real"
+ "inv" > "HOL.divide_class.inverse" :: "real => real"
"hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
thm_maps
--- a/src/HOL/Import/HOLLight/hollight.imp Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Thu May 17 19:49:40 2007 +0200
@@ -238,10 +238,10 @@
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
"/\\" > "op &"
- "-" > "HOL.minus" :: "nat => nat => nat"
+ "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
"," > "Pair"
- "+" > "HOL.plus" :: "nat => nat => nat"
- "*" > "HOL.times" :: "nat => nat => nat"
+ "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
+ "*" > "HOL.times_class.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
"!" > "All"
--- a/src/HOL/Integ/IntArith.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/IntArith.thy Thu May 17 19:49:40 2007 +0200
@@ -7,7 +7,7 @@
theory IntArith
imports Numeral "../Wellfounded_Relations"
-uses ("int_arith1.ML")
+uses "~~/src/Provers/Arith/assoc_fold.ML" ("int_arith1.ML")
begin
text{*Duplicate: can't understand why it's necessary*}
@@ -103,7 +103,6 @@
max_def[of "number_of u" "1::int", standard, simp]
min_def[of "number_of u" "1::int", standard, simp]
-
use "int_arith1.ML"
setup int_arith_setup
@@ -394,7 +393,7 @@
done
-subsection {* Legavy ML bindings *}
+subsection {* Legacy ML bindings *}
ML {*
val of_int_number_of_eq = @{thm of_int_number_of_eq};
--- a/src/HOL/Integ/Numeral.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy Thu May 17 19:49:40 2007 +0200
@@ -8,7 +8,7 @@
theory Numeral
imports IntDef
-uses "../Tools/numeral_syntax.ML"
+uses ("../Tools/numeral_syntax.ML")
begin
subsection {* Binary representation *}
@@ -50,6 +50,7 @@
syntax
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
+use "../Tools/numeral_syntax.ML"
setup NumeralSyntax.setup
abbreviation
@@ -648,14 +649,14 @@
setup {*
let
-fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
+fun number_of_codegen thy defs gr dep module b (Const (@{const_name Numeral.number_of}, Type ("fun", [_, T])) $ t) =
if T = HOLogic.intT then
(SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
(Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
else if T = HOLogic.natT then
SOME (Codegen.invoke_codegen thy defs dep module b (gr,
Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
- (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
+ (Const (@{const_name Numeral.number_of}, HOLogic.intT --> HOLogic.intT) $ t)))
else NONE
| number_of_codegen _ _ _ _ _ _ _ = NONE;
--- a/src/HOL/Integ/cooper_dec.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Thu May 17 19:49:40 2007 +0200
@@ -10,12 +10,12 @@
signature COOPER_DEC =
sig
exception COOPER
- val is_arith_rel : term -> bool
val mk_number : IntInf.int -> term
- val dest_number : term -> IntInf.int
- val is_numeral : term -> bool
val zero : term
val one : term
+ val dest_number : term -> IntInf.int
+ val is_number : term -> bool
+ val is_arith_rel : term -> bool
val linear_cmul : IntInf.int -> term -> term
val linear_add : string list -> term -> term -> term
val linear_sub : string list -> term -> term -> term
@@ -74,20 +74,13 @@
(*Function is_arith_rel returns true if and only if the term is an operation of the
form [int,int]---> int*)
-(*Transform a natural (FIXME?) number to a term*)
-val mk_number = HOLogic.mk_number HOLogic.intT
-
-(*Transform an Term to an natural (FIXME?) number*)
+val mk_number = HOLogic.mk_number HOLogic.intT;
+val zero = mk_number 0;
+val one = mk_number 1;
fun dest_number t = let
val (T, n) = HOLogic.dest_number t
in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end;
-
-(*Some terms often used for pattern matching*)
-val zero = mk_number 0;
-val one = mk_number 1;
-
-(*Tests if a Term is representing a number*)
-val is_numeral = can dest_number;
+val is_number = can dest_number;
(*maps a unary natural function on a term containing an natural number*)
fun numeral1 f n = mk_number (f (dest_number n));
@@ -106,8 +99,8 @@
fun linear_cmul n tm = if n = 0 then zero else let fun times n k = n*k in
( case tm of
- (Const("HOL.plus",T) $ (Const ("HOL.times",T1 ) $c1 $ x1) $ rest) =>
- Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
+ (Const(@{const_name HOL.plus},T) $ (Const (@{const_name HOL.times},T1 ) $c1 $ x1) $ rest) =>
+ Const(@{const_name HOL.plus},T) $ ((Const(@{const_name HOL.times},T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
|_ => numeral1 (times n) tm)
end ;
@@ -129,23 +122,23 @@
fun linear_add vars tm1 tm2 =
let fun addwith x y = x + y in
(case (tm1,tm2) of
- ((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $ x1) $ rest1),(Const
- ("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $ x2) $ rest2)) =>
+ ((Const (@{const_name HOL.plus},T1) $ ( Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1),(Const
+ (@{const_name HOL.plus},T3)$( Const(@{const_name HOL.times},T4) $ c2 $ x2) $ rest2)) =>
if x1 = x2 then
let val c = (numeral2 (addwith) c1 c2)
in
if c = zero then (linear_add vars rest1 rest2)
- else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars rest1 rest2))
+ else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c $ x1) $ (linear_add vars rest1 rest2))
end
else
- if earlierv vars x1 x2 then (Const("HOL.plus",T1) $
- (Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
- else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
- |((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) =>
- (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars
+ if earlierv vars x1 x2 then (Const(@{const_name HOL.plus},T1) $
+ (Const(@{const_name HOL.times},T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
+ else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
+ |((Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1) ,_) =>
+ (Const(@{const_name HOL.plus},T1)$ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ (linear_add vars
rest1 tm2))
- |(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) =>
- (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1
+ |(_, (Const(@{const_name HOL.plus},T1) $(Const(@{const_name HOL.times},T2) $ c2 $ x2) $ rest2)) =>
+ (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1
rest2))
| (_,_) => numeral2 (addwith) tm1 tm2)
@@ -169,19 +162,19 @@
c*Free(x,T) + t where c is a constant ant t is a Term which is not containing
Free(x,T)*)
-fun lint vars tm = if is_numeral tm then tm else case tm of
- (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero))
- |(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
- (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero)
- |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t))
- |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
- |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
- |(Const ("HOL.times",_) $ s $ t) =>
+fun lint vars tm = if is_number tm then tm else case tm of
+ (Free (x,T)) => (HOLogic.mk_binop @{const_name HOL.plus} ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1),Free (x,T))), zero))
+ |(Bound i) => (Const(@{const_name HOL.plus},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
+ (Const(@{const_name HOL.times},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero)
+ |(Const(@{const_name HOL.uminus},_) $ t ) => (linear_neg (lint vars t))
+ |(Const(@{const_name HOL.plus},_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
+ |(Const(@{const_name HOL.minus},_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
+ |(Const (@{const_name HOL.times},_) $ s $ t) =>
let val s' = lint vars s
val t' = lint vars t
in
- if is_numeral s' then (linear_cmul (dest_number s') t')
- else if is_numeral t' then (linear_cmul (dest_number t') s')
+ if is_number s' then (linear_cmul (dest_number s') t')
+ else if is_number t' then (linear_cmul (dest_number t') s')
else raise COOPER
end
@@ -196,20 +189,20 @@
fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t);
fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
- if is_numeral c then
+ if is_number c then
let val c' = (mk_number(abs(dest_number c)))
in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t))
end
else (warning "Nonlinear term --- Non numeral leftside at dvd"
;raise COOPER)
- |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
- |linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
- |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
- |linform vars (Const("Orderings.less_eq",_)$ s $ t ) =
- (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s))
+ |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
+ |linform vars (Const(@{const_name Orderings.less},_)$ s $t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+ |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
+ |linform vars (Const(@{const_name Orderings.less_eq},_)$ s $ t ) =
+ (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s))
|linform vars (Const("op >=",_)$ s $ t ) =
- (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
- HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
+ (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT -->
+ HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $s $(mk_number 1)) $ t))
|linform vars fm = fm;
@@ -219,8 +212,8 @@
(* ------------------------------------------------------------------------- *)
fun posineq fm = case fm of
- (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
- (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) )))
+ (Const ("Not",_)$(Const(@{const_name Orderings.less},_)$ c $ t)) =>
+ (HOLogic.mk_binrel @{const_name Orderings.less} (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) )))
| ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q)
| ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
| _ => fm;
@@ -236,7 +229,7 @@
fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b));
fun formlcm x fm = case fm of
- (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if
+ (Const (p,_)$ _ $(Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_)$ c $ y ) $z ) ) => if
(is_arith_rel fm) andalso (x = y) then (abs(dest_number c)) else 1
| ( Const ("Not", _) $p) => formlcm x p
| ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q)
@@ -249,13 +242,13 @@
fun adjustcoeff x l fm =
case fm of
- (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
+ (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_number c)
- val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x)
+ val n = (if p = @{const_name Orderings.less} then abs(m) else m)
+ val xtm = HOLogic.mk_binop @{const_name HOL.times} ((mk_number (m div n)), x)
in
- (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) ))))
end
else fm
|( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p)
@@ -272,8 +265,8 @@
val fm' = adjustcoeff x l fm in
if l = 1 then fm'
else
- let val xp = (HOLogic.mk_binop "HOL.plus"
- ((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
+ let val xp = (HOLogic.mk_binop @{const_name HOL.plus}
+ ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1), x )), zero))
in
HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm)
end
@@ -284,12 +277,12 @@
(*
fun adjustcoeffeq x l fm =
case fm of
- (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
+ (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_number c)
- val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
- in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ val n = (if p = @{const_name Orderings.less} then abs(m) else m)
+ val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x))
+ in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) ))))
end
else fm
|( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p)
@@ -305,11 +298,11 @@
(* ------------------------------------------------------------------------- *)
fun minusinf x fm = case fm of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const
@@ -326,11 +319,11 @@
(* ------------------------------------------------------------------------- *)
fun plusinf x fm = case fm of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -346,7 +339,7 @@
(* The LCM of all the divisors that involve x. *)
(* ------------------------------------------------------------------------- *)
-fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z ) ) =
if x = y then abs(dest_number d) else 1
|divlcm x ( Const ("Not", _) $ p) = divlcm x p
|divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
@@ -360,15 +353,15 @@
fun bset x fm = case fm of
(Const ("Not", _) $ p) => if (is_arith_rel p) then
(case p of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )
=> if (is_arith_rel p) andalso (x= y) andalso (c2 = one) andalso (c1 = zero)
then [linear_neg a]
else bset x p
|_ =>[])
else bset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else []
- |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else []
+ |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
|(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
|(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
|_ => [];
@@ -380,15 +373,15 @@
fun aset x fm = case fm of
(Const ("Not", _) $ p) => if (is_arith_rel p) then
(case p of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )
=> if (x= y) andalso (c2 = one) andalso (c1 = zero)
then [linear_neg a]
else []
|_ =>[])
else aset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else []
- |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else []
+ |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
|(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
|(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
|_ => [];
@@ -399,7 +392,7 @@
(* ------------------------------------------------------------------------- *)
fun linrep vars x t fm = case fm of
- ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) =>
+ ((Const(p,_)$ d $ (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$ c $ y) $ z))) =>
if (x = y) andalso (is_arith_rel fm)
then
let val ct = linear_cmul (dest_number c) t
@@ -420,18 +413,18 @@
exception DVD_UNKNOWN
fun dvd_op (d, t) =
- if not(is_numeral d) then raise DVD_UNKNOWN
+ if not(is_number d) then raise DVD_UNKNOWN
else let
val dn = dest_number d
fun coeffs_of x = case x of
Const(p,_) $ tl $ tr =>
- if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
- else if p = "HOL.times"
- then if (is_numeral tr)
+ if p = @{const_name HOL.plus} then (coeffs_of tl) union (coeffs_of tr)
+ else if p = @{const_name HOL.times}
+ then if (is_number tr)
then [(dest_number tr) * (dest_number tl)]
else [dest_number tl]
else []
- |_ => if (is_numeral t) then [dest_number t] else []
+ |_ => if (is_number t) then [dest_number t] else []
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
@@ -440,7 +433,7 @@
val operations =
- [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) ,
+ [("op =",op=), (@{const_name Orderings.less},IntInf.<), ("op >",IntInf.>), (@{const_name Orderings.less_eq},IntInf.<=) ,
("op >=",IntInf.>=),
("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
@@ -648,8 +641,8 @@
|mk_uni_vars T (Free (v,_)) = Free (v,T)
|mk_uni_vars T tm = tm;
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2))
- |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2))
+fun mk_uni_int T (Const (@{const_name HOL.zero},T2)) = if T = T2 then (mk_number 0) else (Const (@{const_name HOL.zero},T2))
+ |mk_uni_int T (Const (@{const_name HOL.one},T2)) = if T = T2 then (mk_number 1) else (Const (@{const_name HOL.one},T2))
|mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )
|mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p)
|mk_uni_int T tm = tm;
--- a/src/HOL/Integ/cooper_proof.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/cooper_proof.ML Thu May 17 19:49:40 2007 +0200
@@ -155,17 +155,17 @@
(* ------------------------------------------------------------------------- *)
(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*)
-(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
+(*Respectively by their abstract representation Const(@{const_name HOL.one},..) and Const(@{const_name HOL.zero},..)*)
(*this is necessary because the theorems use this representation.*)
(* This function should be elminated in next versions...*)
(* ------------------------------------------------------------------------- *)
fun norm_zero_one fm = case fm of
- (Const ("HOL.times",_) $ c $ t) =>
+ (Const (@{const_name HOL.times},_) $ c $ t) =>
if c = one then (norm_zero_one t)
else if (dest_number c = ~1)
- then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
- else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
+ then (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
+ else (HOLogic.mk_binop @{const_name HOL.times} (norm_zero_one c,norm_zero_one t))
|(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
|(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
|_ => fm;
@@ -251,32 +251,32 @@
(*==================================================*)
fun decomp_adjustcoeffeq sg x l fm = case fm of
- (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
+ (Const("Not",_)$(Const(@{const_name Orderings.less},_) $ zero $(rt as (Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ c $ y ) $z )))) =>
let
val m = l div (dest_number c)
val n = if (x = y) then abs (m) else 1
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
+ val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x))
val rs = if (x = y)
- then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
- else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
+ then (HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) ))))
+ else HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] one rt )
val ck = cterm_of sg (mk_number n)
val cc = cterm_of sg c
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
+ (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number n))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
- |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
+ |(Const(p,_) $a $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $
c $ y ) $t )) =>
if (is_arith_rel fm) andalso (x = y)
then
let val m = l div (dest_number c)
- val k = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
- val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
+ val k = (if p = @{const_name Orderings.less} then abs(m) else m)
+ val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div k)*l) ), x))
+ val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul k t) ))))
val ck = cterm_of sg (mk_number k)
val cc = cterm_of sg c
@@ -286,23 +286,23 @@
in
case p of
- "Orderings.less" =>
+ @{const_name Orderings.less} =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
+ (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number k))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"op =" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"Divides.dvd" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
@@ -331,31 +331,31 @@
val cfalse = cterm_of sg HOLogic.false_const
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 = zero) then
if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
(instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -369,22 +369,22 @@
let
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf))
@@ -392,7 +392,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -427,33 +427,33 @@
val cfalse = cterm_of sg HOLogic.false_const
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if ((x=y) andalso (c1= zero) andalso (c2= one))
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one))
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if ((y=x) andalso (c1 = zero)) then
if (pm1 = one)
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -468,22 +468,22 @@
let
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf))
@@ -491,7 +491,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -563,50 +563,52 @@
val cat = cterm_of sg (norm_zero_one at)
in
case at of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero ,dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel at) andalso (x=y)
- then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
- in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ then let
+ val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
+ in
+ let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const(@{const_name HOL.minus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ norm_zero_one z) $ HOLogic.mk_number HOLogic.intT 1))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
end
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -654,49 +656,49 @@
val cat = cterm_of sg (norm_zero_one at)
in
case at of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel at) andalso (x=y)
then let val ast_z = norm_zero_one (linear_sub [] one z )
val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const(@{const_name HOL.plus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ one))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = (mk_number ~1) then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm))
in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -773,7 +775,7 @@
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
|(Const("Divides.dvd",_)$d$r) =>
- if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
+ if is_number d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
else (warning "Nonlinear Term --- Non numeral leftside at dvd";
raise COOPER)
|_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
@@ -786,7 +788,7 @@
fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
(* Get the Bset thm*)
let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
in (dpos,minf_eqth,nbstpthm,minf_moddth)
end;
@@ -796,7 +798,7 @@
(* ------------------------------------------------------------------------- *)
fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
in (dpos,pinf_eqth,nastpthm,pinf_moddth)
end;
--- a/src/HOL/Integ/int_arith1.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML Thu May 17 19:49:40 2007 +0200
@@ -103,7 +103,7 @@
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (the_context()) name pats proc;
- fun is_numeral (Const("Numeral.number_of", _) $ w) = true
+ fun is_numeral (Const(@{const_name Numeral.number_of}, _) $ w) = true
| is_numeral _ = false
fun simplify_meta_eq f_number_of_eq f_eq =
@@ -118,13 +118,13 @@
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
fun reorient_proc sg _ (_ $ t $ u) =
case u of
- Const("HOL.zero", _) => NONE
- | Const("HOL.one", _) => NONE
- | Const("Numeral.number_of", _) $ _ => NONE
+ Const(@{const_name HOL.zero}, _) => NONE
+ | Const(@{const_name HOL.one}, _) => NONE
+ | Const(@{const_name Numeral.number_of}, _) $ _ => NONE
| _ => SOME (case t of
- Const("HOL.zero", _) => meta_zero_reorient
- | Const("HOL.one", _) => meta_one_reorient
- | Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
+ Const(@{const_name HOL.zero}, _) => meta_zero_reorient
+ | Const(@{const_name HOL.one}, _) => meta_one_reorient
+ | Const(@{const_name Numeral.number_of}, _) $ _ => meta_number_of_reorient)
val reorient_simproc =
prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
@@ -158,10 +158,10 @@
fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
(case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
| numterm_ord
- (Const("Numeral.number_of", _) $ v, Const("Numeral.number_of", _) $ w) =
+ (Const(@{const_name Numeral.number_of}, _) $ v, Const(@{const_name Numeral.number_of}, _) $ w) =
num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
- | numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
- | numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
+ | numterm_ord (Const(@{const_name Numeral.number_of}, _) $ _, _) = LESS
+ | numterm_ord (_, Const(@{const_name Numeral.number_of}, _) $ _) = GREATER
| numterm_ord (t, u) =
(case int_ord (size_of_term t, size_of_term u) of
EQUAL =>
@@ -187,11 +187,11 @@
handle TERM _ => find_first_numeral (t::past) terms)
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
-val mk_plus = HOLogic.mk_binop "HOL.plus";
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
fun mk_minus t =
let val T = Term.fastype_of t
- in Const ("HOL.uminus", T --> T) $ t
+ in Const (@{const_name HOL.uminus}, T --> T) $ t
end;
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
@@ -203,22 +203,22 @@
fun long_mk_sum T [] = mk_number T 0
| long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
-val dest_plus = HOLogic.dest_bin "HOL.plus" Term.dummyT;
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;
(*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const ("HOL.plus", _) $ t $ u, ts) =
+fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (pos, u, ts))
- | dest_summing (pos, Const ("HOL.minus", _) $ t $ u, ts) =
+ | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
if pos then t::ts else mk_minus t :: ts;
fun dest_sum t = dest_summing (true, t, []);
-val mk_diff = HOLogic.mk_binop "HOL.minus";
-val dest_diff = HOLogic.dest_bin "HOL.minus" Term.dummyT;
+val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
+val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
-val mk_times = HOLogic.mk_binop "HOL.times";
+val mk_times = HOLogic.mk_binop @{const_name HOL.times};
fun mk_prod T =
let val one = mk_number T 1
@@ -231,7 +231,7 @@
fun long_mk_prod T [] = mk_number T 1
| long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
-val dest_times = HOLogic.dest_bin "HOL.times" Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -242,7 +242,7 @@
fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const ("HOL.uminus", _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort Term.term_ord (dest_prod t)
val (n, ts') = find_first_numeral [] ts
@@ -338,8 +338,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less"
- val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
val bal_add1 = less_add_iff1 RS trans
val bal_add2 = less_add_iff2 RS trans
);
@@ -347,8 +347,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
- val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
val bal_add1 = le_add_iff1 RS trans
val bal_add2 = le_add_iff2 RS trans
);
--- a/src/HOL/Integ/int_factor_simprocs.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Thu May 17 19:49:40 2007 +0200
@@ -63,8 +63,8 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.div"
- val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
+ val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
val cancel = int_mult_div_cancel1 RS trans
val neg_exchanges = false
)
@@ -73,8 +73,8 @@
structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
val cancel = @{thm mult_divide_cancel_left} RS trans
val neg_exchanges = false
)
@@ -102,8 +102,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less"
- val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
val cancel = @{thm mult_less_cancel_left} RS trans
val neg_exchanges = true
)
@@ -111,8 +111,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
- val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
val cancel = @{thm mult_le_cancel_left} RS trans
val neg_exchanges = true
)
@@ -270,8 +270,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.div"
- val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
+ val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj
);
@@ -295,8 +295,8 @@
structure FieldDivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_cancel_eq_if}
);
--- a/src/HOL/Integ/nat_simprocs.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Thu May 17 19:49:40 2007 +0200
@@ -6,10 +6,6 @@
Simprocs for nat numerals.
*)
-val Let_number_of = thm"Let_number_of";
-val Let_0 = thm"Let_0";
-val Let_1 = thm"Let_1";
-
structure Nat_Numeral_Simprocs =
struct
@@ -32,7 +28,7 @@
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
val zero = mk_number 0;
-val mk_plus = HOLogic.mk_binop "HOL.plus";
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
fun mk_sum [] = zero
@@ -43,7 +39,7 @@
fun long_mk_sum [] = HOLogic.zero
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
(** Other simproc items **)
@@ -56,7 +52,7 @@
diff_nat_number_of, le_number_of_eq_not_less,
mult_nat_number_of, nat_number_of_mult_left,
less_nat_number_of,
- Let_number_of, nat_number_of] @
+ @{thm Let_number_of}, nat_number_of] @
arith_simps @ rel_simps;
fun prep_simproc (name, pats, proc) =
@@ -66,14 +62,14 @@
(*** CancelNumerals simprocs ***)
val one = mk_number 1;
-val mk_times = HOLogic.mk_binop "HOL.times";
+val mk_times = HOLogic.mk_binop @{const_name HOL.times};
fun mk_prod [] = one
| mk_prod [t] = t
| mk_prod (t :: ts) = if t = one then mk_prod ts
else mk_times (t, mk_prod ts);
-val dest_times = HOLogic.dest_bin "HOL.times" HOLogic.natT;
+val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -109,7 +105,7 @@
handle TERM _ => (k, t::ts);
(*Code for testing whether numerals are already used in the goal*)
-fun is_numeral (Const("Numeral.number_of", _) $ w) = true
+fun is_numeral (Const(@{const_name Numeral.number_of}, _) $ w) = true
| is_numeral _ = false;
fun prod_has_numeral t = exists is_numeral (dest_prod t);
@@ -130,7 +126,7 @@
(*Simplify 1*n and n*1 to n*)
val add_0s = map rename_numerals [add_0, add_0_right];
-val mult_1s = map rename_numerals [thm"nat_mult_1", thm"nat_mult_1_right"];
+val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
@@ -185,8 +181,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less"
- val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
val bal_add1 = nat_less_add_iff1 RS trans
val bal_add2 = nat_less_add_iff2 RS trans
);
@@ -194,8 +190,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
- val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
val bal_add1 = nat_le_add_iff1 RS trans
val bal_add2 = nat_le_add_iff2 RS trans
);
@@ -203,8 +199,8 @@
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.minus"
- val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
+ val mk_bal = HOLogic.mk_binop @{const_name HOL.minus}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
val bal_add1 = nat_diff_add_eq1 RS trans
val bal_add2 = nat_diff_add_eq2 RS trans
);
@@ -287,8 +283,8 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.div"
- val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
+ val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
val cancel = nat_mult_div_cancel1 RS trans
val neg_exchanges = false
)
@@ -305,8 +301,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less"
- val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
val cancel = nat_mult_less_cancel1 RS trans
val neg_exchanges = true
)
@@ -314,8 +310,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
- val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
val cancel = nat_mult_le_cancel1 RS trans
val neg_exchanges = true
)
@@ -380,24 +376,24 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less"
- val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_less_cancel_disj
);
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
- val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_le_cancel_disj
);
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.div"
- val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
+ val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj
);
@@ -527,7 +523,7 @@
(* reduce contradictory <= to False *)
val add_rules =
- [thm "Let_number_of", Let_0, Let_1, nat_0, nat_1,
+ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, nat_0, nat_1,
add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
le_Suc_number_of,le_number_of_Suc,
--- a/src/HOL/Integ/presburger.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/presburger.ML Thu May 17 19:49:40 2007 +0200
@@ -131,46 +131,46 @@
("op =", bT --> bT --> bT),
("Not", bT --> bT),
- ("Orderings.less_eq", iT --> iT --> bT),
+ (@{const_name Orderings.less_eq}, iT --> iT --> bT),
("op =", iT --> iT --> bT),
- ("Orderings.less", iT --> iT --> bT),
- ("Divides.dvd", iT --> iT --> bT),
- ("Divides.div", iT --> iT --> iT),
- ("Divides.mod", iT --> iT --> iT),
- ("HOL.plus", iT --> iT --> iT),
- ("HOL.minus", iT --> iT --> iT),
- ("HOL.times", iT --> iT --> iT),
- ("HOL.abs", iT --> iT),
- ("HOL.uminus", iT --> iT),
- ("HOL.max", iT --> iT --> iT),
- ("HOL.min", iT --> iT --> iT),
+ (@{const_name Orderings.less}, iT --> iT --> bT),
+ (@{const_name Divides.dvd}, iT --> iT --> bT),
+ (@{const_name Divides.div}, iT --> iT --> iT),
+ (@{const_name Divides.mod}, iT --> iT --> iT),
+ (@{const_name HOL.plus}, iT --> iT --> iT),
+ (@{const_name HOL.minus}, iT --> iT --> iT),
+ (@{const_name HOL.times}, iT --> iT --> iT),
+ (@{const_name HOL.abs}, iT --> iT),
+ (@{const_name HOL.uminus}, iT --> iT),
+ (@{const_name Orderings.max}, iT --> iT --> iT),
+ (@{const_name Orderings.min}, iT --> iT --> iT),
- ("Orderings.less_eq", nT --> nT --> bT),
+ (@{const_name Orderings.less_eq}, nT --> nT --> bT),
("op =", nT --> nT --> bT),
- ("Orderings.less", nT --> nT --> bT),
- ("Divides.dvd", nT --> nT --> bT),
- ("Divides.div", nT --> nT --> nT),
- ("Divides.mod", nT --> nT --> nT),
- ("HOL.plus", nT --> nT --> nT),
- ("HOL.minus", nT --> nT --> nT),
- ("HOL.times", nT --> nT --> nT),
- ("Suc", nT --> nT),
- ("HOL.max", nT --> nT --> nT),
- ("HOL.min", nT --> nT --> nT),
+ (@{const_name Orderings.less}, nT --> nT --> bT),
+ (@{const_name Divides.dvd}, nT --> nT --> bT),
+ (@{const_name Divides.div}, nT --> nT --> nT),
+ (@{const_name Divides.mod}, nT --> nT --> nT),
+ (@{const_name HOL.plus}, nT --> nT --> nT),
+ (@{const_name HOL.minus}, nT --> nT --> nT),
+ (@{const_name HOL.times}, nT --> nT --> nT),
+ (@{const_name Suc}, nT --> nT),
+ (@{const_name Orderings.max}, nT --> nT --> nT),
+ (@{const_name Orderings.min}, nT --> nT --> nT),
- ("Numeral.bit.B0", bitT),
- ("Numeral.bit.B1", bitT),
- ("Numeral.Bit", iT --> bitT --> iT),
- ("Numeral.Pls", iT),
- ("Numeral.Min", iT),
- ("Numeral.number_of", iT --> iT),
- ("Numeral.number_of", iT --> nT),
- ("HOL.zero", nT),
- ("HOL.zero", iT),
- ("HOL.one", nT),
- ("HOL.one", iT),
- ("False", bT),
- ("True", bT)];
+ (@{const_name Numeral.bit.B0}, bitT),
+ (@{const_name Numeral.bit.B1}, bitT),
+ (@{const_name Numeral.Bit}, iT --> bitT --> iT),
+ (@{const_name Numeral.Pls}, iT),
+ (@{const_name Numeral.Min}, iT),
+ (@{const_name Numeral.number_of}, iT --> iT),
+ (@{const_name Numeral.number_of}, iT --> nT),
+ (@{const_name HOL.zero}, nT),
+ (@{const_name HOL.zero}, iT),
+ (@{const_name HOL.one}, nT),
+ (@{const_name HOL.one}, iT),
+ (@{const_name False}, bT),
+ (@{const_name True}, bT)];
(* Preparation of the formula to be sent to the Integer quantifier *)
(* elimination procedure *)
--- a/src/HOL/Integ/reflected_cooper.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/reflected_cooper.ML Thu May 17 19:49:40 2007 +0200
@@ -8,29 +8,26 @@
open Generated;
(* pseudo reification : term -> intterm *)
-fun i_of_term vs t =
- case t of
- Free(xn,xT) => (case AList.lookup (op =) vs t of
- NONE => error "Variable not found in the list!!"
- | SOME n => Var n)
- | Const("HOL.zero",iT) => Cst 0
- | Const("HOL.one",iT) => Cst 1
- | Bound i => Var (nat (IntInf.fromInt i))
- | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
- | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
- | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
- | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
- | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
- | _ => error "i_of_term: unknown term";
-
+fun i_of_term vs t = case t of
+ Free(xn,xT) => (case AList.lookup (op =) vs t of
+ NONE => error "Variable not found in the list!!"
+ | SOME n => Var n)
+ | Const(@{const_name HOL.zero},iT) => Cst 0
+ | Const(@{const_name HOL.one},iT) => Cst 1
+ | Bound i => Var (nat (IntInf.fromInt i))
+ | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
+ | Const (@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+ | Const (@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+ | Const (@{const_name HOL.times},_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
+ | Const (@{const_name Numeral.number_of},_)$t' => Cst (HOLogic.dest_numeral t')
+ | _ => error "i_of_term: unknown term";
(* pseudo reification : term -> QF *)
-fun qf_of_term vs t =
- case t of
+fun qf_of_term vs t = case t of
Const("True",_) => T
| Const("False",_) => F
- | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
- | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
| Const ("Divides.dvd",_)$t1$t2 =>
Divides(i_of_term vs t1,i_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
@@ -77,25 +74,25 @@
case t of
Cst i => CooperDec.mk_number i
| Var n => valOf (myassoc2 vs n)
- | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
- | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
+ | Neg t' => Const(@{const_name HOL.uminus},iT --> iT)$(term_of_i vs t')
+ | Add(t1,t2) => Const(@{const_name HOL.plus},[iT,iT] ---> iT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
+ | Sub(t1,t2) => Const(@{const_name HOL.minus},[iT,iT] ---> iT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
+ | Mult(t1,t2) => Const(@{const_name HOL.times},[iT,iT] ---> iT)$
(term_of_i vs t1)$(term_of_i vs t2);
fun term_of_qf vs t =
case t of
T => HOLogic.true_const
| F => HOLogic.false_const
- | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+ | Lt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Le(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+ | Le(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+ | Gt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
- | Ge(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+ | Ge(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
| Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
--- a/src/HOL/Library/Executable_Real.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Library/Executable_Real.thy Thu May 17 19:49:40 2007 +0200
@@ -474,10 +474,11 @@
val rT = HOLogic.realT;
in if q = 1
then HOLogic.mk_number rT p
- else Const ("HOL.divide", rT --> rT --> rT) $
+ else @{term "op / \<Colon> real \<Rightarrow> real \<Rightarrow> real"} $
HOLogic.mk_number rT p $ HOLogic.mk_number rT q
end;
*}
consts_code INum ("")
+
end
\ No newline at end of file
--- a/src/HOL/Library/comm_ring.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Library/comm_ring.ML Thu May 17 19:49:40 2007 +0200
@@ -17,8 +17,8 @@
exception CRing of string;
(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name "HOL.zero"}, T);
-fun cring_one T = Const (@{const_name "HOL.one"}, T);
+fun cring_zero T = Const (@{const_name HOL.zero}, T);
+fun cring_one T = Const (@{const_name HOL.one}, T);
(* reification functions *)
(* add two polynom expressions *)
@@ -53,15 +53,15 @@
| reif_pol T vs t = pol_Pc T $ t;
(* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name "HOL.plus"}, _) $ a $ b) =
+fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
polex_add T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name "HOL.minus"}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
polex_sub T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name "HOL.times"}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
polex_mul T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name "HOL.uminus"}, _) $ a) =
+ | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
polex_neg T $ reif_polex T vs a
- | reif_polex T vs (Const (@{const_name "Nat.power"}, _) $ a $ n) =
+ | reif_polex T vs (Const (@{const_name Nat.power}, _) $ a $ n) =
polex_pow T $ reif_polex T vs a $ n
| reif_polex T vs t = polex_pol T $ reif_pol T vs t;
--- a/src/HOL/Library/sct.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Library/sct.ML Thu May 17 19:49:40 2007 +0200
@@ -63,8 +63,8 @@
in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
-val less_nat_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-val lesseq_nat_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val less_nat_const = Const (@{const_name Orderings.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val lesseq_nat_const = Const (@{const_name Orderings.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
@@ -298,8 +298,7 @@
THEN all_less_tac ts
-val length_const = "Nat.size"
-fun mk_length l = Const (length_const, fastype_of l --> HOLogic.natT) $ l
+fun mk_length l = HOLogic.size_const (fastype_of l) $ l;
val length_simps = thms "SCT_Interpretation.length_simps"
--- a/src/HOL/OrderedGroup.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/OrderedGroup.thy Thu May 17 19:49:40 2007 +0200
@@ -1058,7 +1058,8 @@
(* term order for abelian groups *)
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
- ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
+ [@{const_name HOL.zero}, @{const_name HOL.plus},
+ @{const_name HOL.uminus}, @{const_name HOL.minus}]
| agrp_ord _ = ~1;
fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
@@ -1067,9 +1068,9 @@
val ac1 = mk_meta_eq @{thm add_assoc};
val ac2 = mk_meta_eq @{thm add_commute};
val ac3 = mk_meta_eq @{thm add_left_commute};
- fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
+ fun solve_add_ac thy _ (_ $ (Const (@{const_name HOL.plus},_) $ _ $ _) $ _) =
SOME ac1
- | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
+ | solve_add_ac thy _ (_ $ x $ (Const (@{const_name HOL.plus},_) $ y $ z)) =
if termless_agrp (y, x) then SOME ac3 else NONE
| solve_add_ac thy _ (_ $ x $ y) =
if termless_agrp (y, x) then SOME ac2 else NONE
--- a/src/HOL/Orderings.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Orderings.thy Thu May 17 19:49:40 2007 +0200
@@ -380,11 +380,11 @@
if of_sort t1
then SOME (t1, "=", t2)
else NONE
- | dec (Const (@{const_name less_eq}, _) $ t1 $ t2) =
+ | dec (Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<=", t2)
else NONE
- | dec (Const (@{const_name less}, _) $ t1 $ t2) =
+ | dec (Const (@{const_name Orderings.less}, _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<", t2)
else NONE
--- a/src/HOL/ROOT.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ROOT.ML Thu May 17 19:49:40 2007 +0200
@@ -26,14 +26,12 @@
use "~~/src/Pure/General/rat.ML";
use "~~/src/Provers/Arith/fast_lin_arith.ML";
use "~~/src/Provers/Arith/cancel_sums.ML";
-use "~~/src/Provers/Arith/assoc_fold.ML";
use "~~/src/Provers/quantifier1.ML";
use "~~/src/Provers/project_rule.ML";
use "~~/src/Provers/Arith/cancel_numerals.ML";
use "~~/src/Provers/Arith/combine_numerals.ML";
use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
use "~~/src/Provers/Arith/extract_common_term.ML";
-use "~~/src/Provers/Arith/cancel_div_mod.ML";
use "~~/src/Provers/quasi.ML";
use "~~/src/Provers/order.ML";
--- a/src/HOL/Real/ferrante_rackoff_proof.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML Thu May 17 19:49:40 2007 +0200
@@ -24,10 +24,10 @@
case fm of
Const("op &",_)$p$q => (uset x p) union (uset x q)
| Const("op |",_)$p$q => (uset x p) union (uset x q)
- | Const("Orderings.less",_)$s$t => if s=x then [t]
+ | Const(@{const_name Orderings.less},_)$s$t => if s=x then [t]
else if t = x then [s]
else []
- | Const("Orderings.less_eq",_)$s$t => if s=x then [t]
+ | Const(@{const_name Orderings.less_eq},_)$s$t => if s=x then [t]
else if t = x then [s]
else []
| Const("op =",_)$s$t => if s=x then [t]
@@ -96,7 +96,7 @@
([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))
| Const("op |",_)$p$q =>
([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
- | Const("Orderings.less",_)$s$t =>
+ | Const(@{const_name Orderings.less},_)$s$t =>
if s= x then
let val ct = cterm_of sg t
val tinU = nth uths (find_index (fn a => a=t) U)
@@ -127,7 +127,7 @@
val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
end
- | Const("Orderings.less_eq",_)$s$t =>
+ | Const(@{const_name Orderings.less_eq},_)$s$t =>
if s= x then
let val ct = cterm_of sg t
val tinU = nth uths (find_index (fn a => a=t) U)
@@ -287,8 +287,8 @@
(* Normalization of arithmetical expressions *)
-val rzero = Const("HOL.zero",rT);
-val rone = Const("HOL.one",rT);
+val rzero = HOLogic.mk_number rT 0;
+val rone = HOLogic.mk_number rT 1;
fun mk_real i = HOLogic.mk_number rT i;
val dest_real = snd o HOLogic.dest_number;
@@ -301,18 +301,18 @@
fun proveprod thy m n =
prove_bysimp thy (simpset_of thy)
- (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
+ (HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.times} (mk_real m,mk_real n),mk_real (m*n)));
fun proveadd thy m n =
prove_bysimp thy (simpset_of thy)
- (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
+ (HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.plus} (mk_real m,mk_real n),mk_real (m+n)));
fun provediv thy m n =
let val g = gcd (m,n)
val m' = m div g
val n'= n div g
in
(prove_bysimp thy (simpset_of thy)
- (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
- HOLogic.mk_binop "HOL.divide"
+ (HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.divide} (mk_real m,mk_real n),
+ HOLogic.mk_binop @{const_name HOL.divide}
(mk_real m',mk_real n'))),m')
end;
(* Multiplication of a normal term by a constant *)
@@ -321,7 +321,7 @@
fun decomp_ncmulh thy c t =
if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] @{thm mult_zero_left}) else
case t of
- Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b =>
+ Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c'$v)$b =>
([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)]
((proveprod thy c (dest_real c')) RS ncmul_congh)))
| _ => ([],fn _ => proveprod thy c (dest_real t));
@@ -353,8 +353,8 @@
fun decomp_naddh thy vs (t,s) =
case (t,s) of
- (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,
- Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
+ (Const(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr,
+ Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name HOL.times},_)$sc$sv)$sr) =>
if tv = sv then
let val ntc = dest_real tc
val nsc = dest_real sc
@@ -368,9 +368,9 @@
else if earlier vs tv sv
then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
- | (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,_) =>
+ | (Const(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr,_) =>
([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
- | (_,Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
+ | (_,Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name HOL.times},_)$sc$sv)$sr) =>
([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
| (_,_) => ([], fn _ => proveadd thy (dest_real t) (dest_real s));
@@ -429,27 +429,27 @@
fun decomp_normalizeh thy vs t =
case t of
Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
- | Const("HOL.uminus",_)$a =>
+ | Const(@{const_name HOL.uminus},_)$a =>
([a],
fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
in [tha,prove_nneg thy (a',dest_real n')]
MRS uminus_cong
end )
- | Const("HOL.plus",_)$a$b =>
+ | Const(@{const_name HOL.plus},_)$a$b =>
([a,b],
fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
val _$(_$_$(_$b'$m')) = prop_of thb
in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')]
MRS plus_cong
end )
- | Const("HOL.minus",_)$a$b =>
+ | Const(@{const_name HOL.minus},_)$a$b =>
([a,b],
fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
val _$(_$_$(_$b'$m')) = prop_of thb
in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')]
MRS diff_cong
end )
- | Const("HOL.times",_)$a$b =>
+ | Const(@{const_name HOL.times},_)$a$b =>
if can dest_real a
then ([b], fn [thb] =>
let val _$(_$_$(_$b'$m')) = prop_of thb
@@ -461,7 +461,7 @@
in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
end )
else raise FAILURE "decomp_normalizeh: non linear term"
- | Const("HOL.divide",_)$a$b =>
+ | Const(@{const_name HOL.divide},_)$a$b =>
if can dest_real b
then ([a], fn [tha] =>
let val _$(_$_$(_$a'$m')) = prop_of tha
@@ -473,7 +473,7 @@
fun dest_xth vs th =
let val _$(_$_$(_$t$n)) = prop_of th
in (case t of
- Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r =>
+ Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$r =>
if vs = [] then (0,t,dest_real n)
else if hd vs = y then (dest_real c, r,dest_real n)
else (0,t,dest_real n)
@@ -482,12 +482,12 @@
fun prove_strictsign thy n =
prove_bysimp thy (simpset_of thy)
- (HOLogic.mk_binrel "Orderings.less"
+ (HOLogic.mk_binrel @{const_name Orderings.less}
(if n > 0 then (rzero, mk_real n) else (mk_real n, rzero)));
fun prove_fracsign thy (m,n) =
- let val mn = HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n)
+ let val mn = HOLogic.mk_binop @{const_name HOL.divide} (mk_real m, mk_real n)
in prove_bysimp thy (simpset_of thy)
- (HOLogic.mk_binrel "Orderings.less"
+ (HOLogic.mk_binrel @{const_name Orderings.less}
(if m*n > 0 then (rzero, mn) else (mn, rzero)))
end;
@@ -495,11 +495,11 @@
| holbool_of false = HOLogic.false_const;
fun prove_fracsign_eq thy s (m,n) =
- let fun f s = the (AList.lookup (op =) [("Orderings.less", op <),("Orderings.less_eq", op <=),("op =", op =)] s)
+ let fun f s = the (AList.lookup (op =) [(@{const_name Orderings.less}, op <),(@{const_name Orderings.less_eq}, op <=),("op =", op =)] s)
in
prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
(HOLogic.mk_binrel s
- (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero),
+ (HOLogic.mk_binop @{const_name HOL.divide} (mk_real m, mk_real n),rzero),
holbool_of (f s (m*n,0))))
end;
@@ -534,11 +534,11 @@
fun prove_normalize thy vs at =
case at of
- Const("Orderings.less",_)$s$t =>
- let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+ Const(@{const_name Orderings.less},_)$s$t =>
+ let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
val (cx,r,n) = dest_xth vs smtth
in if cx = 0 then if can dest_real r
- then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
+ then [smtth, prove_fracsign_eq thy @{const_name Orderings.less} (dest_real r, n)]
MRS normalize_ltground_cong
else [smtth, prove_strictsign thy n]
MRS (if n > 0 then normalize_ltnoxpos_cong
@@ -554,11 +554,11 @@
else normalize_ltxpos_cong)
end
end
- | Const("Orderings.less_eq",_)$s$t =>
- let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+ | Const(@{const_name Orderings.less_eq},_)$s$t =>
+ let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
val (cx,r,n) = dest_xth vs smtth
in if cx = 0 then if can dest_real r
- then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
+ then [smtth, prove_fracsign_eq thy @{const_name Orderings.less_eq} (dest_real r, n)]
MRS normalize_leground_cong
else [smtth, prove_strictsign thy n]
MRS (if n > 0 then normalize_lenoxpos_cong
@@ -575,7 +575,7 @@
end
end
| Const("op =",_)$s$t =>
- let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+ let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
val (cx,r,n) = dest_xth vs smtth
in if cx = 0 then if can dest_real r
then [smtth, provenz thy n,
@@ -593,10 +593,10 @@
else normalize_eqxpos_cong)
end
end
- | Const("Not",_)$(Const("Orderings.less",T)$s$t) =>
- (prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
- | Const("Not",_)$(Const("Orderings.less_eq",T)$s$t) =>
- (prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
+ | Const("Not",_)$(Const(@{const_name Orderings.less},T)$s$t) =>
+ (prove_normalize thy vs (Const(@{const_name Orderings.less_eq},T)$t$s)) RS normalize_not_lt
+ | Const("Not",_)$(Const(@{const_name Orderings.less_eq},T)$s$t) =>
+ (prove_normalize thy vs (Const(@{const_name Orderings.less},T)$t$s)) RS normalize_not_le
| (nt as Const("Not",_))$(Const("op =",T)$s$t) =>
(prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
| _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Thu May 17 19:49:40 2007 +0200
@@ -10,12 +10,12 @@
signature COOPER_DEC =
sig
exception COOPER
- val is_arith_rel : term -> bool
val mk_number : IntInf.int -> term
- val dest_number : term -> IntInf.int
- val is_numeral : term -> bool
val zero : term
val one : term
+ val dest_number : term -> IntInf.int
+ val is_number : term -> bool
+ val is_arith_rel : term -> bool
val linear_cmul : IntInf.int -> term -> term
val linear_add : string list -> term -> term -> term
val linear_sub : string list -> term -> term -> term
@@ -74,20 +74,13 @@
(*Function is_arith_rel returns true if and only if the term is an operation of the
form [int,int]---> int*)
-(*Transform a natural (FIXME?) number to a term*)
-val mk_number = HOLogic.mk_number HOLogic.intT
-
-(*Transform an Term to an natural (FIXME?) number*)
+val mk_number = HOLogic.mk_number HOLogic.intT;
+val zero = mk_number 0;
+val one = mk_number 1;
fun dest_number t = let
val (T, n) = HOLogic.dest_number t
in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end;
-
-(*Some terms often used for pattern matching*)
-val zero = mk_number 0;
-val one = mk_number 1;
-
-(*Tests if a Term is representing a number*)
-val is_numeral = can dest_number;
+val is_number = can dest_number;
(*maps a unary natural function on a term containing an natural number*)
fun numeral1 f n = mk_number (f (dest_number n));
@@ -106,8 +99,8 @@
fun linear_cmul n tm = if n = 0 then zero else let fun times n k = n*k in
( case tm of
- (Const("HOL.plus",T) $ (Const ("HOL.times",T1 ) $c1 $ x1) $ rest) =>
- Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
+ (Const(@{const_name HOL.plus},T) $ (Const (@{const_name HOL.times},T1 ) $c1 $ x1) $ rest) =>
+ Const(@{const_name HOL.plus},T) $ ((Const(@{const_name HOL.times},T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
|_ => numeral1 (times n) tm)
end ;
@@ -129,23 +122,23 @@
fun linear_add vars tm1 tm2 =
let fun addwith x y = x + y in
(case (tm1,tm2) of
- ((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $ x1) $ rest1),(Const
- ("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $ x2) $ rest2)) =>
+ ((Const (@{const_name HOL.plus},T1) $ ( Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1),(Const
+ (@{const_name HOL.plus},T3)$( Const(@{const_name HOL.times},T4) $ c2 $ x2) $ rest2)) =>
if x1 = x2 then
let val c = (numeral2 (addwith) c1 c2)
in
if c = zero then (linear_add vars rest1 rest2)
- else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars rest1 rest2))
+ else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c $ x1) $ (linear_add vars rest1 rest2))
end
else
- if earlierv vars x1 x2 then (Const("HOL.plus",T1) $
- (Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
- else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
- |((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) =>
- (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars
+ if earlierv vars x1 x2 then (Const(@{const_name HOL.plus},T1) $
+ (Const(@{const_name HOL.times},T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
+ else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
+ |((Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1) ,_) =>
+ (Const(@{const_name HOL.plus},T1)$ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ (linear_add vars
rest1 tm2))
- |(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) =>
- (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1
+ |(_, (Const(@{const_name HOL.plus},T1) $(Const(@{const_name HOL.times},T2) $ c2 $ x2) $ rest2)) =>
+ (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1
rest2))
| (_,_) => numeral2 (addwith) tm1 tm2)
@@ -169,19 +162,19 @@
c*Free(x,T) + t where c is a constant ant t is a Term which is not containing
Free(x,T)*)
-fun lint vars tm = if is_numeral tm then tm else case tm of
- (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero))
- |(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
- (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero)
- |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t))
- |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
- |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
- |(Const ("HOL.times",_) $ s $ t) =>
+fun lint vars tm = if is_number tm then tm else case tm of
+ (Free (x,T)) => (HOLogic.mk_binop @{const_name HOL.plus} ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1),Free (x,T))), zero))
+ |(Bound i) => (Const(@{const_name HOL.plus},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
+ (Const(@{const_name HOL.times},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero)
+ |(Const(@{const_name HOL.uminus},_) $ t ) => (linear_neg (lint vars t))
+ |(Const(@{const_name HOL.plus},_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
+ |(Const(@{const_name HOL.minus},_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
+ |(Const (@{const_name HOL.times},_) $ s $ t) =>
let val s' = lint vars s
val t' = lint vars t
in
- if is_numeral s' then (linear_cmul (dest_number s') t')
- else if is_numeral t' then (linear_cmul (dest_number t') s')
+ if is_number s' then (linear_cmul (dest_number s') t')
+ else if is_number t' then (linear_cmul (dest_number t') s')
else raise COOPER
end
@@ -196,20 +189,20 @@
fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t);
fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
- if is_numeral c then
+ if is_number c then
let val c' = (mk_number(abs(dest_number c)))
in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t))
end
else (warning "Nonlinear term --- Non numeral leftside at dvd"
;raise COOPER)
- |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
- |linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
- |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
- |linform vars (Const("Orderings.less_eq",_)$ s $ t ) =
- (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s))
+ |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
+ |linform vars (Const(@{const_name Orderings.less},_)$ s $t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+ |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
+ |linform vars (Const(@{const_name Orderings.less_eq},_)$ s $ t ) =
+ (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s))
|linform vars (Const("op >=",_)$ s $ t ) =
- (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
- HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
+ (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT -->
+ HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $s $(mk_number 1)) $ t))
|linform vars fm = fm;
@@ -219,8 +212,8 @@
(* ------------------------------------------------------------------------- *)
fun posineq fm = case fm of
- (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
- (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) )))
+ (Const ("Not",_)$(Const(@{const_name Orderings.less},_)$ c $ t)) =>
+ (HOLogic.mk_binrel @{const_name Orderings.less} (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) )))
| ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q)
| ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
| _ => fm;
@@ -236,7 +229,7 @@
fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b));
fun formlcm x fm = case fm of
- (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if
+ (Const (p,_)$ _ $(Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_)$ c $ y ) $z ) ) => if
(is_arith_rel fm) andalso (x = y) then (abs(dest_number c)) else 1
| ( Const ("Not", _) $p) => formlcm x p
| ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q)
@@ -249,13 +242,13 @@
fun adjustcoeff x l fm =
case fm of
- (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
+ (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_number c)
- val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x)
+ val n = (if p = @{const_name Orderings.less} then abs(m) else m)
+ val xtm = HOLogic.mk_binop @{const_name HOL.times} ((mk_number (m div n)), x)
in
- (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) ))))
end
else fm
|( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p)
@@ -272,8 +265,8 @@
val fm' = adjustcoeff x l fm in
if l = 1 then fm'
else
- let val xp = (HOLogic.mk_binop "HOL.plus"
- ((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
+ let val xp = (HOLogic.mk_binop @{const_name HOL.plus}
+ ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1), x )), zero))
in
HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm)
end
@@ -284,12 +277,12 @@
(*
fun adjustcoeffeq x l fm =
case fm of
- (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
+ (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_number c)
- val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
- in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ val n = (if p = @{const_name Orderings.less} then abs(m) else m)
+ val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x))
+ in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) ))))
end
else fm
|( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p)
@@ -305,11 +298,11 @@
(* ------------------------------------------------------------------------- *)
fun minusinf x fm = case fm of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const
@@ -326,11 +319,11 @@
(* ------------------------------------------------------------------------- *)
fun plusinf x fm = case fm of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -346,7 +339,7 @@
(* The LCM of all the divisors that involve x. *)
(* ------------------------------------------------------------------------- *)
-fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z ) ) =
if x = y then abs(dest_number d) else 1
|divlcm x ( Const ("Not", _) $ p) = divlcm x p
|divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
@@ -360,15 +353,15 @@
fun bset x fm = case fm of
(Const ("Not", _) $ p) => if (is_arith_rel p) then
(case p of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )
=> if (is_arith_rel p) andalso (x= y) andalso (c2 = one) andalso (c1 = zero)
then [linear_neg a]
else bset x p
|_ =>[])
else bset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else []
- |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else []
+ |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
|(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
|(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
|_ => [];
@@ -380,15 +373,15 @@
fun aset x fm = case fm of
(Const ("Not", _) $ p) => if (is_arith_rel p) then
(case p of
- (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
+ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )
=> if (x= y) andalso (c2 = one) andalso (c1 = zero)
then [linear_neg a]
else []
|_ =>[])
else aset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else []
- |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else []
+ |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
|(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
|(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
|_ => [];
@@ -399,7 +392,7 @@
(* ------------------------------------------------------------------------- *)
fun linrep vars x t fm = case fm of
- ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) =>
+ ((Const(p,_)$ d $ (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$ c $ y) $ z))) =>
if (x = y) andalso (is_arith_rel fm)
then
let val ct = linear_cmul (dest_number c) t
@@ -420,18 +413,18 @@
exception DVD_UNKNOWN
fun dvd_op (d, t) =
- if not(is_numeral d) then raise DVD_UNKNOWN
+ if not(is_number d) then raise DVD_UNKNOWN
else let
val dn = dest_number d
fun coeffs_of x = case x of
Const(p,_) $ tl $ tr =>
- if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
- else if p = "HOL.times"
- then if (is_numeral tr)
+ if p = @{const_name HOL.plus} then (coeffs_of tl) union (coeffs_of tr)
+ else if p = @{const_name HOL.times}
+ then if (is_number tr)
then [(dest_number tr) * (dest_number tl)]
else [dest_number tl]
else []
- |_ => if (is_numeral t) then [dest_number t] else []
+ |_ => if (is_number t) then [dest_number t] else []
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
@@ -440,7 +433,7 @@
val operations =
- [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) ,
+ [("op =",op=), (@{const_name Orderings.less},IntInf.<), ("op >",IntInf.>), (@{const_name Orderings.less_eq},IntInf.<=) ,
("op >=",IntInf.>=),
("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
@@ -648,8 +641,8 @@
|mk_uni_vars T (Free (v,_)) = Free (v,T)
|mk_uni_vars T tm = tm;
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2))
- |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2))
+fun mk_uni_int T (Const (@{const_name HOL.zero},T2)) = if T = T2 then (mk_number 0) else (Const (@{const_name HOL.zero},T2))
+ |mk_uni_int T (Const (@{const_name HOL.one},T2)) = if T = T2 then (mk_number 1) else (Const (@{const_name HOL.one},T2))
|mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )
|mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p)
|mk_uni_int T tm = tm;
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Thu May 17 19:49:40 2007 +0200
@@ -155,17 +155,17 @@
(* ------------------------------------------------------------------------- *)
(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*)
-(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
+(*Respectively by their abstract representation Const(@{const_name HOL.one},..) and Const(@{const_name HOL.zero},..)*)
(*this is necessary because the theorems use this representation.*)
(* This function should be elminated in next versions...*)
(* ------------------------------------------------------------------------- *)
fun norm_zero_one fm = case fm of
- (Const ("HOL.times",_) $ c $ t) =>
+ (Const (@{const_name HOL.times},_) $ c $ t) =>
if c = one then (norm_zero_one t)
else if (dest_number c = ~1)
- then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
- else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
+ then (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
+ else (HOLogic.mk_binop @{const_name HOL.times} (norm_zero_one c,norm_zero_one t))
|(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
|(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
|_ => fm;
@@ -251,32 +251,32 @@
(*==================================================*)
fun decomp_adjustcoeffeq sg x l fm = case fm of
- (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
+ (Const("Not",_)$(Const(@{const_name Orderings.less},_) $ zero $(rt as (Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ c $ y ) $z )))) =>
let
val m = l div (dest_number c)
val n = if (x = y) then abs (m) else 1
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
+ val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x))
val rs = if (x = y)
- then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
- else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
+ then (HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) ))))
+ else HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] one rt )
val ck = cterm_of sg (mk_number n)
val cc = cterm_of sg c
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
+ (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number n))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
- |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
+ |(Const(p,_) $a $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $
c $ y ) $t )) =>
if (is_arith_rel fm) andalso (x = y)
then
let val m = l div (dest_number c)
- val k = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
- val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
+ val k = (if p = @{const_name Orderings.less} then abs(m) else m)
+ val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div k)*l) ), x))
+ val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul k t) ))))
val ck = cterm_of sg (mk_number k)
val cc = cterm_of sg c
@@ -286,23 +286,23 @@
in
case p of
- "Orderings.less" =>
+ @{const_name Orderings.less} =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
+ (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number k))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"op =" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"Divides.dvd" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
@@ -331,31 +331,31 @@
val cfalse = cterm_of sg HOLogic.false_const
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 = zero) then
if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
(instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -369,22 +369,22 @@
let
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf))
@@ -392,7 +392,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -427,33 +427,33 @@
val cfalse = cterm_of sg HOLogic.false_const
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if ((x=y) andalso (c1= zero) andalso (c2= one))
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one))
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if ((y=x) andalso (c1 = zero)) then
if (pm1 = one)
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -468,22 +468,22 @@
let
val fm = norm_zero_one fm1
in case fm1 of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf))
@@ -491,7 +491,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -563,50 +563,52 @@
val cat = cterm_of sg (norm_zero_one at)
in
case at of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero ,dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel at) andalso (x=y)
- then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
- in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ then let
+ val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
+ in
+ let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const(@{const_name HOL.minus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ norm_zero_one z) $ HOLogic.mk_number HOLogic.intT 1))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
end
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -654,49 +656,49 @@
val cat = cterm_of sg (norm_zero_one at)
in
case at of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
+ (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) =>
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+ |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
if (is_arith_rel at) andalso (x=y)
then let val ast_z = norm_zero_one (linear_sub [] one z )
val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const(@{const_name HOL.plus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ one))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = (mk_number ~1) then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm))
in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -773,7 +775,7 @@
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
|(Const("Divides.dvd",_)$d$r) =>
- if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
+ if is_number d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
else (warning "Nonlinear Term --- Non numeral leftside at dvd";
raise COOPER)
|_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
@@ -786,7 +788,7 @@
fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
(* Get the Bset thm*)
let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
in (dpos,minf_eqth,nbstpthm,minf_moddth)
end;
@@ -796,7 +798,7 @@
(* ------------------------------------------------------------------------- *)
fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
in (dpos,pinf_eqth,nastpthm,pinf_moddth)
end;
--- a/src/HOL/Tools/Presburger/presburger.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Thu May 17 19:49:40 2007 +0200
@@ -131,46 +131,46 @@
("op =", bT --> bT --> bT),
("Not", bT --> bT),
- ("Orderings.less_eq", iT --> iT --> bT),
+ (@{const_name Orderings.less_eq}, iT --> iT --> bT),
("op =", iT --> iT --> bT),
- ("Orderings.less", iT --> iT --> bT),
- ("Divides.dvd", iT --> iT --> bT),
- ("Divides.div", iT --> iT --> iT),
- ("Divides.mod", iT --> iT --> iT),
- ("HOL.plus", iT --> iT --> iT),
- ("HOL.minus", iT --> iT --> iT),
- ("HOL.times", iT --> iT --> iT),
- ("HOL.abs", iT --> iT),
- ("HOL.uminus", iT --> iT),
- ("HOL.max", iT --> iT --> iT),
- ("HOL.min", iT --> iT --> iT),
+ (@{const_name Orderings.less}, iT --> iT --> bT),
+ (@{const_name Divides.dvd}, iT --> iT --> bT),
+ (@{const_name Divides.div}, iT --> iT --> iT),
+ (@{const_name Divides.mod}, iT --> iT --> iT),
+ (@{const_name HOL.plus}, iT --> iT --> iT),
+ (@{const_name HOL.minus}, iT --> iT --> iT),
+ (@{const_name HOL.times}, iT --> iT --> iT),
+ (@{const_name HOL.abs}, iT --> iT),
+ (@{const_name HOL.uminus}, iT --> iT),
+ (@{const_name Orderings.max}, iT --> iT --> iT),
+ (@{const_name Orderings.min}, iT --> iT --> iT),
- ("Orderings.less_eq", nT --> nT --> bT),
+ (@{const_name Orderings.less_eq}, nT --> nT --> bT),
("op =", nT --> nT --> bT),
- ("Orderings.less", nT --> nT --> bT),
- ("Divides.dvd", nT --> nT --> bT),
- ("Divides.div", nT --> nT --> nT),
- ("Divides.mod", nT --> nT --> nT),
- ("HOL.plus", nT --> nT --> nT),
- ("HOL.minus", nT --> nT --> nT),
- ("HOL.times", nT --> nT --> nT),
- ("Suc", nT --> nT),
- ("HOL.max", nT --> nT --> nT),
- ("HOL.min", nT --> nT --> nT),
+ (@{const_name Orderings.less}, nT --> nT --> bT),
+ (@{const_name Divides.dvd}, nT --> nT --> bT),
+ (@{const_name Divides.div}, nT --> nT --> nT),
+ (@{const_name Divides.mod}, nT --> nT --> nT),
+ (@{const_name HOL.plus}, nT --> nT --> nT),
+ (@{const_name HOL.minus}, nT --> nT --> nT),
+ (@{const_name HOL.times}, nT --> nT --> nT),
+ (@{const_name Suc}, nT --> nT),
+ (@{const_name Orderings.max}, nT --> nT --> nT),
+ (@{const_name Orderings.min}, nT --> nT --> nT),
- ("Numeral.bit.B0", bitT),
- ("Numeral.bit.B1", bitT),
- ("Numeral.Bit", iT --> bitT --> iT),
- ("Numeral.Pls", iT),
- ("Numeral.Min", iT),
- ("Numeral.number_of", iT --> iT),
- ("Numeral.number_of", iT --> nT),
- ("HOL.zero", nT),
- ("HOL.zero", iT),
- ("HOL.one", nT),
- ("HOL.one", iT),
- ("False", bT),
- ("True", bT)];
+ (@{const_name Numeral.bit.B0}, bitT),
+ (@{const_name Numeral.bit.B1}, bitT),
+ (@{const_name Numeral.Bit}, iT --> bitT --> iT),
+ (@{const_name Numeral.Pls}, iT),
+ (@{const_name Numeral.Min}, iT),
+ (@{const_name Numeral.number_of}, iT --> iT),
+ (@{const_name Numeral.number_of}, iT --> nT),
+ (@{const_name HOL.zero}, nT),
+ (@{const_name HOL.zero}, iT),
+ (@{const_name HOL.one}, nT),
+ (@{const_name HOL.one}, iT),
+ (@{const_name False}, bT),
+ (@{const_name True}, bT)];
(* Preparation of the formula to be sent to the Integer quantifier *)
(* elimination procedure *)
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Thu May 17 19:49:40 2007 +0200
@@ -8,29 +8,26 @@
open Generated;
(* pseudo reification : term -> intterm *)
-fun i_of_term vs t =
- case t of
- Free(xn,xT) => (case AList.lookup (op =) vs t of
- NONE => error "Variable not found in the list!!"
- | SOME n => Var n)
- | Const("HOL.zero",iT) => Cst 0
- | Const("HOL.one",iT) => Cst 1
- | Bound i => Var (nat (IntInf.fromInt i))
- | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
- | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
- | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
- | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
- | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
- | _ => error "i_of_term: unknown term";
-
+fun i_of_term vs t = case t of
+ Free(xn,xT) => (case AList.lookup (op =) vs t of
+ NONE => error "Variable not found in the list!!"
+ | SOME n => Var n)
+ | Const(@{const_name HOL.zero},iT) => Cst 0
+ | Const(@{const_name HOL.one},iT) => Cst 1
+ | Bound i => Var (nat (IntInf.fromInt i))
+ | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
+ | Const (@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+ | Const (@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+ | Const (@{const_name HOL.times},_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
+ | Const (@{const_name Numeral.number_of},_)$t' => Cst (HOLogic.dest_numeral t')
+ | _ => error "i_of_term: unknown term";
(* pseudo reification : term -> QF *)
-fun qf_of_term vs t =
- case t of
+fun qf_of_term vs t = case t of
Const("True",_) => T
| Const("False",_) => F
- | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
- | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
| Const ("Divides.dvd",_)$t1$t2 =>
Divides(i_of_term vs t1,i_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
@@ -77,25 +74,25 @@
case t of
Cst i => CooperDec.mk_number i
| Var n => valOf (myassoc2 vs n)
- | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
- | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
+ | Neg t' => Const(@{const_name HOL.uminus},iT --> iT)$(term_of_i vs t')
+ | Add(t1,t2) => Const(@{const_name HOL.plus},[iT,iT] ---> iT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
+ | Sub(t1,t2) => Const(@{const_name HOL.minus},[iT,iT] ---> iT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
+ | Mult(t1,t2) => Const(@{const_name HOL.times},[iT,iT] ---> iT)$
(term_of_i vs t1)$(term_of_i vs t2);
fun term_of_qf vs t =
case t of
T => HOLogic.true_const
| F => HOLogic.false_const
- | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+ | Lt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Le(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+ | Le(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+ | Gt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
- | Ge(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+ | Ge(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
| Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Thu May 17 19:49:40 2007 +0200
@@ -62,7 +62,7 @@
| _ => [(t, tt)]
fun mk_base_fun_header fulltyp (t, typ) =
- Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
+ Abs ("x", fulltyp, HOLogic.size_const typ $ t)
fun mk_base_funs (tt: typ) =
mk_base_fun_bodys (Bound 0) tt |>
@@ -121,13 +121,13 @@
fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) =
let
val goals = mk_goal (vars, prems, lhs, rhs)
- val less_thm = goals "Orderings.less" |> prove thy
+ val less_thm = goals "Orderings.ord_class.less" |> prove thy
in
if Thm.no_prems less_thm then
Less (Goal.finish less_thm)
else
let
- val lesseq_thm = goals "Orderings.less_eq" |> prove thy
+ val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy
in
if Thm.no_prems lesseq_thm then
LessEq (Goal.finish lesseq_thm)
--- a/src/HOL/Tools/inductive_package.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu May 17 19:49:40 2007 +0200
@@ -158,7 +158,7 @@
case concl of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
| _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
- | _ $ (Const ("Orderings.less_eq", _) $ _ $ _) =>
+ | _ $ (Const ("Orderings.ord_class.less_eq", _) $ _ $ _) =>
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [le_funI, le_boolI'])) thm))]
| _ => [thm]
@@ -532,7 +532,7 @@
(make_bool_args HOLogic.mk_not I bs i)) preds));
val ind_concl = HOLogic.mk_Trueprop
- (HOLogic.mk_binrel "Orderings.less_eq" (rec_const, ind_pred));
+ (HOLogic.mk_binrel "Orderings.ord_class.less_eq" (rec_const, ind_pred));
val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
--- a/src/HOL/Tools/numeral_syntax.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Thu May 17 19:49:40 2007 +0200
@@ -20,16 +20,16 @@
fun mk_bin num =
let
val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
- fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
- fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
- | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
+ fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b;
+ fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls})
+ | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min})
| mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
in mk value end;
in
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
- Syntax.const "Numeral.number_of" $ mk_bin num
+ Syntax.const @{const_name Numeral.number_of} $ mk_bin num
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
end;
@@ -39,15 +39,15 @@
local
-fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
- | dest_bit (Const ("Numeral.bit.B1", _)) = 1
+fun dest_bit (Const (@{const_syntax Numeral.bit.B0}, _)) = 0
+ | dest_bit (Const (@{const_syntax Numeral.bit.B1}, _)) = 1
| dest_bit (Const ("bit.B0", _)) = 0
| dest_bit (Const ("bit.B1", _)) = 1
| dest_bit _ = raise Match;
-fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
- | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
- | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
+fun dest_bin (Const (@{const_syntax "Numeral.Pls"}, _)) = []
+ | dest_bin (Const (@{const_syntax "Numeral.Min"}, _)) = [~1]
+ | dest_bin (Const (@{const_syntax "Numeral.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
| dest_bin _ = raise Match;
fun leading _ [] = 0
@@ -89,6 +89,6 @@
val setup =
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
- Theory.add_trfunsT [("\\<^const>Numeral.number_of", numeral_tr')];
+ Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
end;
--- a/src/HOL/Tools/refute.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/refute.ML Thu May 17 19:49:40 2007 +0200
@@ -696,13 +696,13 @@
| Const ("Finite_Set.card", _) => t
| Const ("Finite_Set.Finites", _) => t
| Const ("Finite_Set.finite", _) => t
- | Const ("Orderings.less", Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
- | Const ("HOL.plus", Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const ("HOL.minus", Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const ("HOL.times", Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
| Const ("List.op @", _) => t
| Const ("Lfp.lfp", _) => t
@@ -883,16 +883,16 @@
| Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
| Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T)
- | Const ("Orderings.less", T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
collect_type_axioms (axs, T)
- | Const ("HOL.plus", T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms (axs, T)
- | Const ("HOL.minus", T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms (axs, T)
- | Const ("HOL.times", T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms (axs, T)
| Const ("List.op @", T) => collect_type_axioms (axs, T)
@@ -2608,7 +2608,7 @@
fun Nat_less_interpreter thy model args t =
case t of
- Const ("Orderings.less", Type ("fun", [Type ("nat", []),
+ Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
let
val (i_nat, _, _) = interpret thy model
@@ -2634,7 +2634,7 @@
fun Nat_plus_interpreter thy model args t =
case t of
- Const ("HOL.plus", Type ("fun", [Type ("nat", []),
+ Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val (i_nat, _, _) = interpret thy model
@@ -2668,7 +2668,7 @@
fun Nat_minus_interpreter thy model args t =
case t of
- Const ("HOL.minus", Type ("fun", [Type ("nat", []),
+ Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val (i_nat, _, _) = interpret thy model
@@ -2699,7 +2699,7 @@
fun Nat_times_interpreter thy model args t =
case t of
- Const ("HOL.times", Type ("fun", [Type ("nat", []),
+ Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val (i_nat, _, _) = interpret thy model
--- a/src/HOL/Tools/res_clause.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML Thu May 17 19:49:40 2007 +0200
@@ -103,15 +103,15 @@
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
Symtab.make [("op =", "equal"),
- ("Orderings.less_eq", "lessequals"),
- ("Orderings.less", "less"),
+ (@{const_name Orderings.less_eq}, "lessequals"),
+ (@{const_name Orderings.less}, "less"),
("op &", "and"),
("op |", "or"),
- ("HOL.plus", "plus"),
- ("HOL.minus", "minus"),
- ("HOL.times", "times"),
- ("Divides.div", "div"),
- ("HOL.divide", "divide"),
+ (@{const_name HOL.plus}, "plus"),
+ (@{const_name HOL.minus}, "minus"),
+ (@{const_name HOL.times}, "times"),
+ (@{const_name Divides.div}, "div"),
+ (@{const_name HOL.divide}, "divide"),
("op -->", "implies"),
("{}", "emptyset"),
("op :", "in"),
--- a/src/HOL/arith_data.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/arith_data.ML Thu May 17 19:49:40 2007 +0200
@@ -16,7 +16,7 @@
(* mk_sum, mk_norm_sum *)
-val mk_plus = HOLogic.mk_binop "HOL.plus";
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
fun mk_sum [] = HOLogic.zero
| mk_sum [t] = t
@@ -30,7 +30,7 @@
(* dest_sum *)
-val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
fun dest_sum tm =
if HOLogic.is_zero tm then []
@@ -107,8 +107,8 @@
structure LessCancelSums = CancelSumsFun
(struct
open Sum;
- val mk_bal = HOLogic.mk_binrel "Orderings.less";
- val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
end);
@@ -117,8 +117,8 @@
structure LeCancelSums = CancelSumsFun
(struct
open Sum;
- val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
- val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
end);
@@ -127,8 +127,8 @@
structure DiffCancelSums = CancelSumsFun
(struct
open Sum;
- val mk_bal = HOLogic.mk_binop "HOL.minus";
- val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
+ val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
end);
@@ -283,17 +283,17 @@
*)
fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
let
- fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
+ fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) = (
(case s of
- Const ("Numeral.number_of", _) $ n =>
+ Const ("Numeral.number_class.number_of", _) $ n =>
demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
- | Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) =>
+ | Const (@{const_name HOL.uminus}, _) $ (Const ("Numeral.number_class.number_of", _) $ n) =>
demult (t, Rat.mult m (Rat.rat_of_int (~(HOLogic.dest_numeral n))))
- | Const ("Suc", _) $ _ =>
+ | Const (@{const_name Suc}, _) $ _ =>
demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat s)))
- | Const ("HOL.times", _) $ s1 $ s2 =>
+ | Const (@{const_name HOL.times}, _) $ s1 $ s2 =>
demult (mC $ s1 $ (mC $ s2 $ t), m)
- | Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) =>
+ | Const (@{const_name HOL.divide}, _) $ numt $ (Const ("Numeral.number_class.number_of", _) $ dent) =>
let
val den = HOLogic.dest_numeral dent
in
@@ -306,7 +306,7 @@
atomult (mC, s, t, m)
) handle TERM _ => atomult (mC, s, t, m)
)
- | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
+ | demult (atom as Const(@{const_name HOL.divide}, _) $ t $ (Const ("Numeral.number_class.number_of", _) $ dent), m) =
(let
val den = HOLogic.dest_numeral dent
in
@@ -316,14 +316,14 @@
demult (t, Rat.mult m (Rat.inv (Rat.rat_of_int den)))
end
handle TERM _ => (SOME atom, m))
- | demult (Const ("HOL.zero", _), m) = (NONE, Rat.zero)
- | demult (Const ("HOL.one", _), m) = (NONE, m)
- | demult (t as Const ("Numeral.number_of", _) $ n, m) =
+ | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero)
+ | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m)
+ | demult (t as Const ("Numeral.number_class.number_of", _) $ n, m) =
((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
handle TERM _ => (SOME t, m))
- | demult (Const ("HOL.uminus", _) $ t, m) = demult (t, Rat.neg m)
+ | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m)
| demult (t as Const f $ x, m) =
- (if f mem inj_consts then SOME x else SOME t, m)
+ (if member (op =) inj_consts f then SOME x else SOME t, m)
| demult (atom, m) = (SOME atom, m)
and
atomult (mC, atom, t, m) = (
@@ -336,27 +336,27 @@
((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
let
(* Turn term into list of summand * multiplicity plus a constant *)
- fun poly (Const ("HOL.plus", _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) =
+ fun poly (Const (@{const_name HOL.plus}, _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) =
poly (s, m, poly (t, m, pi))
- | poly (all as Const ("HOL.minus", T) $ s $ t, m, pi) =
+ | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) =
if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
- | poly (all as Const ("HOL.uminus", T) $ t, m, pi) =
+ | poly (all as Const (@{const_name HOL.uminus}, T) $ t, m, pi) =
if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
- | poly (Const ("HOL.zero", _), _, pi) =
+ | poly (Const (@{const_name HOL.zero}, _), _, pi) =
pi
- | poly (Const ("HOL.one", _), m, (p, i)) =
+ | poly (Const (@{const_name HOL.one}, _), m, (p, i)) =
(p, Rat.add i m)
- | poly (Const ("Suc", _) $ t, m, (p, i)) =
+ | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
poly (t, m, (p, Rat.add i m))
- | poly (all as Const ("HOL.times", _) $ _ $ _, m, pi as (p, i)) =
+ | poly (all as Const (@{const_name HOL.times}, _) $ _ $ _, m, pi as (p, i)) =
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const ("HOL.divide", _) $ _ $ _, m, pi as (p, i)) =
+ | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) =
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const ("Numeral.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
+ | poly (all as Const ("Numeral.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
(let val k = HOLogic.dest_numeral t
val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end
@@ -369,8 +369,8 @@
val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
in
case rel of
- "Orderings.less" => SOME (p, i, "<", q, j)
- | "Orderings.less_eq" => SOME (p, i, "<=", q, j)
+ @{const_name Orderings.less} => SOME (p, i, "<", q, j)
+ | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
| "op =" => SOME (p, i, "=", q, j)
| _ => NONE
end handle Zero => NONE;
@@ -445,13 +445,13 @@
case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
(* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
case head_of lhs of
- Const (a, _) => a mem_string ["Orderings.max",
- "Orderings.min",
- "HOL.abs",
- "HOL.minus",
+ Const (a, _) => member (op =) [@{const_name Orderings.max},
+ @{const_name Orderings.min},
+ @{const_name HOL.abs},
+ @{const_name HOL.minus},
"IntDef.nat",
- "Divides.mod",
- "Divides.div"]
+ "Divides.div_class.mod",
+ "Divides.div_class.div"] a
| _ => (warning ("Lin. Arith.: wrong format for split rule " ^
Display.string_of_thm thm);
false))
@@ -515,12 +515,12 @@
(* ignore all but the first possible split *)
case strip_comb split_term of
(* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
- (Const ("Orderings.max", _), [t1, t2]) =>
+ (Const (@{const_name Orderings.max}, _), [t1, t2]) =>
let
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const ("Orderings.less_eq",
+ val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -530,12 +530,12 @@
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
(* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
- | (Const ("Orderings.min", _), [t1, t2]) =>
+ | (Const (@{const_name Orderings.min}, _), [t1, t2]) =>
let
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const ("Orderings.less_eq",
+ val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -545,16 +545,16 @@
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
(* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
- | (Const ("HOL.abs", _), [t1]) =>
+ | (Const (@{const_name HOL.abs}, _), [t1]) =>
let
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
- val terms2 = map (subst_term [(split_term, Const ("HOL.uminus",
+ val terms2 = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
split_type --> split_type) $ t1)]) rev_terms
- val zero = Const ("HOL.zero", split_type)
- val zero_leq_t1 = Const ("Orderings.less_eq",
+ val zero = Const (@{const_name HOL.zero}, split_type)
+ val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ t1
- val t1_lt_zero = Const ("Orderings.less",
+ val t1_lt_zero = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
@@ -563,22 +563,22 @@
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
(* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
- | (Const ("HOL.minus", _), [t1, t2]) =>
+ | (Const (@{const_name HOL.minus}, _), [t1, t2]) =>
let
(* "d" in the above theorem becomes a new bound variable after NNF *)
(* transformation, therefore some adjustment of indices is necessary *)
val rev_terms = rev terms
- val zero = Const ("HOL.zero", split_type)
+ val zero = Const (@{const_name HOL.zero}, split_type)
val d = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)])
(map (incr_boundvars 1) rev_terms)
val t1' = incr_boundvars 1 t1
val t2' = incr_boundvars 1 t2
- val t1_lt_t2 = Const ("Orderings.less",
+ val t1_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const ("HOL.plus",
+ (Const (@{const_name HOL.plus},
split_type --> split_type --> split_type) $ t2' $ d)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
@@ -590,8 +590,8 @@
| (Const ("IntDef.nat", _), [t1]) =>
let
val rev_terms = rev terms
- val zero_int = Const ("HOL.zero", HOLogic.intT)
- val zero_nat = Const ("HOL.zero", HOLogic.natT)
+ val zero_int = Const (@{const_name HOL.zero}, HOLogic.intT)
+ val zero_nat = Const (@{const_name HOL.zero}, HOLogic.natT)
val n = Bound 0
val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)])
(map (incr_boundvars 1) rev_terms)
@@ -599,7 +599,7 @@
val t1' = incr_boundvars 1 t1
val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
- val t1_lt_zero = Const ("Orderings.less",
+ val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
@@ -610,10 +610,10 @@
(* "?P ((?n::nat) mod (number_of ?k)) =
((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
(ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
- | (Const ("Divides.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const ("HOL.zero", split_type)
+ val zero = Const (@{const_name HOL.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -625,11 +625,11 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const ("Orderings.less",
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times",
+ (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -642,10 +642,10 @@
(* "?P ((?n::nat) div (number_of ?k)) =
((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
(ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
- | (Const ("Divides.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const ("HOL.zero", split_type)
+ val zero = Const (@{const_name HOL.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
@@ -657,11 +657,11 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const ("Orderings.less",
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times",
+ (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -677,11 +677,11 @@
(ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
(neg (number_of ?k) -->
(ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
- | (Const ("Divides.mod",
+ | (Const ("Divides.div_class.mod",
Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
- val zero = Const ("HOL.zero", split_type)
+ val zero = Const (@{const_name HOL.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -692,20 +692,20 @@
val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
(number_of $
- (Const ("HOL.uminus",
+ (Const (@{const_name HOL.uminus},
HOLogic.intT --> HOLogic.intT) $ k'))
- val zero_leq_j = Const ("Orderings.less_eq",
+ val zero_leq_j = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_lt_t2 = Const ("Orderings.less",
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times",
+ (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const ("Orderings.less",
+ val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const ("Orderings.less_eq",
+ val j_leq_zero = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -729,11 +729,11 @@
(ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
(neg (number_of ?k) -->
(ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
- | (Const ("Divides.div",
+ | (Const ("Divides.div_class.div",
Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
- val zero = Const ("HOL.zero", split_type)
+ val zero = Const (@{const_name HOL.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
@@ -744,21 +744,21 @@
val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
(number_of $
- (Const ("HOL.uminus",
+ (Const (@{const_name HOL.uminus},
HOLogic.intT --> HOLogic.intT) $ k'))
- val zero_leq_j = Const ("Orderings.less_eq",
+ val zero_leq_j = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_lt_t2 = Const ("Orderings.less",
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times",
+ (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const ("Orderings.less",
+ val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const ("Orderings.less_eq",
+ val j_leq_zero = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -1009,24 +1009,24 @@
val r = #prop(rep_thm thm);
in
case r of
- Tr $ ((c as Const("Orderings.less_eq",T)) $ s $ t) =>
+ Tr $ ((c as Const(@{const_name Orderings.less_eq},T)) $ s $ t) =>
let val r' = Tr $ (c $ t $ s)
in
case Library.find_first (prp r') prems of
NONE =>
- let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ s $ t))
+ let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ s $ t))
in case Library.find_first (prp r') prems of
NONE => []
| SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
end
| SOME thm' => [thm' RS (thm RS antisym)]
end
- | Tr $ (Const("Not",_) $ (Const("Orderings.less",T) $ s $ t)) =>
- let val r' = Tr $ (Const("Orderings.less_eq",T) $ s $ t)
+ | Tr $ (Const("Not",_) $ (Const(@{const_name Orderings.less},T) $ s $ t)) =>
+ let val r' = Tr $ (Const(@{const_name Orderings.less_eq},T) $ s $ t)
in
case Library.find_first (prp r') prems of
NONE =>
- let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ t $ s))
+ let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ t $ s))
in case Library.find_first (prp r') prems of
NONE => []
| SOME thm' =>
--- a/src/HOL/ex/Binary.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ex/Binary.thy Thu May 17 19:49:40 2007 +0200
@@ -25,8 +25,8 @@
| dest_bit (Const ("True", _)) = 1
| dest_bit t = raise TERM ("dest_bit", [t]);
- fun dest_binary (Const ("HOL.zero", Type ("nat", _))) = 0
- | dest_binary (Const ("HOL.one", Type ("nat", _))) = 1
+ fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0
+ | dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1
| dest_binary (Const ("Binary.bit", _) $ bs $ b) =
2 * dest_binary bs + IntInf.fromInt (dest_bit b)
| dest_binary t = raise TERM ("dest_binary", [t]);
--- a/src/HOL/ex/svc_funcs.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ex/svc_funcs.ML Thu May 17 19:49:40 2007 +0200
@@ -112,8 +112,8 @@
b1 orelse b2)
end
else (*might be numeric equality*) (t, is_intnat T)
- | Const("Orderings.less", Type ("fun", [T,_])) => (t, is_intnat T)
- | Const("Orderings.less_eq", Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name Orderings.less}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
| _ => (t, false)
end
in #1 o tag end;
@@ -151,38 +151,38 @@
(*translation of a literal*)
val lit = snd o HOLogic.dest_number;
(*translation of a literal expression [no variables]*)
- fun litExp (Const("HOL.plus", T) $ x $ y) =
+ fun litExp (Const(@{const_name HOL.plus}, T) $ x $ y) =
if is_numeric_op T then (litExp x) + (litExp y)
else fail t
- | litExp (Const("HOL.minus", T) $ x $ y) =
+ | litExp (Const(@{const_name HOL.minus}, T) $ x $ y) =
if is_numeric_op T then (litExp x) - (litExp y)
else fail t
- | litExp (Const("HOL.times", T) $ x $ y) =
+ | litExp (Const(@{const_name HOL.times}, T) $ x $ y) =
if is_numeric_op T then (litExp x) * (litExp y)
else fail t
- | litExp (Const("HOL.uminus", T) $ x) =
+ | litExp (Const(@{const_name HOL.uminus}, T) $ x) =
if is_numeric_op T then ~(litExp x)
else fail t
| litExp t = lit t
handle Match => fail t
(*translation of a real/rational expression*)
fun suc t = Interp("+", [Int 1, t])
- fun tm (Const("Suc", T) $ x) = suc (tm x)
- | tm (Const("HOL.plus", T) $ x $ y) =
+ fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x)
+ | tm (Const(@{const_name HOL.plus}, T) $ x $ y) =
if is_numeric_op T then Interp("+", [tm x, tm y])
else fail t
- | tm (Const("HOL.minus", T) $ x $ y) =
+ | tm (Const(@{const_name HOL.minus}, T) $ x $ y) =
if is_numeric_op T then
Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
else fail t
- | tm (Const("HOL.times", T) $ x $ y) =
+ | tm (Const(@{const_name HOL.times}, T) $ x $ y) =
if is_numeric_op T then Interp("*", [tm x, tm y])
else fail t
- | tm (Const("RealDef.rinv", T) $ x) =
+ | tm (Const(@{const_name HOL.inverse}, T) $ x) =
if domain_type T = HOLogic.realT then
Rat(1, litExp x)
else fail t
- | tm (Const("HOL.uminus", T) $ x) =
+ | tm (Const(@{const_name HOL.uminus}, T) $ x) =
if is_numeric_op T then Interp("*", [Int ~1, tm x])
else fail t
| tm t = Int (lit t)
@@ -216,13 +216,13 @@
else fail t
end
(*inequalities: possible types are nat, int, real*)
- | fm pos (t as Const("Orderings.less", Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ x $ y) =
if not pos orelse T = HOLogic.realT then
Buildin("<", [tm x, tm y])
else if is_intnat T then
Buildin("<=", [suc (tm x), tm y])
else fail t
- | fm pos (t as Const("Orderings.less_eq", Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ x $ y) =
if pos orelse T = HOLogic.realT then
Buildin("<=", [tm x, tm y])
else if is_intnat T then
--- a/src/HOL/ex/svc_oracle.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ex/svc_oracle.ML Thu May 17 19:49:40 2007 +0200
@@ -41,27 +41,27 @@
SOME v => v
| NONE => insert t)
(*abstraction of a numeric literal*)
- fun lit (t as Const("0", _)) = t
- | lit (t as Const("1", _)) = t
- | lit (t as Const("Numeral.number_of", _) $ w) = t
+ fun lit (t as Const(@{const_name HOL.zero}, _)) = t
+ | lit (t as Const(@{const_name HOL.one}, _)) = t
+ | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
| lit t = replace t
(*abstraction of a real/rational expression*)
- fun rat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("HOL.minus", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("HOL.divide", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("HOL.times", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("HOL.uminus", _)) $ x) = c $ (rat x)
+ fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
| rat t = lit t
(*abstraction of an integer expression: no div, mod*)
- fun int ((c as Const("HOL.plus", _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const("HOL.minus", _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const("HOL.times", _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const("HOL.uminus", _)) $ x) = c $ (int x)
+ fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
| int t = lit t
(*abstraction of a natural number expression: no minus*)
- fun nat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (nat x) $ (nat y)
- | nat ((c as Const("HOL.times", _)) $ x $ y) = c $ (nat x) $ (nat y)
- | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
+ fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+ | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+ | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
| nat t = lit t
(*abstraction of a relation: =, <, <=*)
fun rel (T, c $ x $ y) =
@@ -78,8 +78,8 @@
| fm ((c as Const("True", _))) = c
| fm ((c as Const("False", _))) = c
| fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const("Orderings.less", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const("Orderings.less_eq", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
--- a/src/Provers/Arith/abel_cancel.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Thu May 17 19:49:40 2007 +0200
@@ -28,29 +28,29 @@
(* FIXME dependent on abstract syntax *)
-fun zero t = Const ("HOL.zero", t);
-fun minus t = Const ("HOL.uminus", t --> t);
+fun zero t = Const (@{const_name HOL.zero}, t);
+fun minus t = Const (@{const_name HOL.uminus}, t --> t);
-fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =
+fun add_terms pos (Const (@{const_name HOL.plus}, _) $ x $ y, ts) =
add_terms pos (x, add_terms pos (y, ts))
- | add_terms pos (Const ("HOL.minus", _) $ x $ y, ts) =
+ | add_terms pos (Const (@{const_name HOL.minus}, _) $ x $ y, ts) =
add_terms pos (x, add_terms (not pos) (y, ts))
- | add_terms pos (Const ("HOL.uminus", _) $ x, ts) =
+ | add_terms pos (Const (@{const_name HOL.uminus}, _) $ x, ts) =
add_terms (not pos) (x, ts)
| add_terms pos (x, ts) = (pos,x) :: ts;
fun terms fml = add_terms true (fml, []);
-fun zero1 pt (u as (c as Const("HOL.plus",_)) $ x $ y) =
+fun zero1 pt (u as (c as Const(@{const_name HOL.plus},_)) $ x $ y) =
(case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
| SOME z => SOME(c $ x $ z))
| SOME z => SOME(c $ z $ y))
- | zero1 (pos,t) (u as (c as Const("HOL.minus",_)) $ x $ y) =
+ | zero1 (pos,t) (u as (c as Const(@{const_name HOL.minus},_)) $ x $ y) =
(case zero1 (pos,t) x of
NONE => (case zero1 (not pos,t) y of NONE => NONE
| SOME z => SOME(c $ x $ z))
| SOME z => SOME(c $ z $ y))
- | zero1 (pos,t) (u as (c as Const("HOL.uminus",_)) $ x) =
+ | zero1 (pos,t) (u as (c as Const(@{const_name HOL.uminus},_)) $ x) =
(case zero1 (not pos,t) x of NONE => NONE
| SOME z => SOME(c $ z))
| zero1 (pos,t) u =
@@ -71,7 +71,7 @@
fun cancel t =
let
val c $ lhs $ rhs = t
- val opp = case c of Const("HOL.plus",_) => true | _ => false;
+ val opp = case c of Const(@{const_name HOL.plus},_) => true | _ => false;
val (pos,l) = find_common opp (terms lhs) (terms rhs)
val posr = if opp then not pos else pos
val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
--- a/src/Provers/Arith/assoc_fold.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/Provers/Arith/assoc_fold.ML Thu May 17 19:49:40 2007 +0200
@@ -30,7 +30,7 @@
(*Separate the literals from the other terms being combined*)
fun sift_terms plus (t, (lits,others)) =
(case t of
- Const("Numeral.number_of", _) $ _ => (* FIXME logic dependent *)
+ Const (@{const_name Numeral.number_of}, _) $ _ => (* FIXME logic dependent *)
(t::lits, others) (*new literal*)
| (f as Const _) $ x $ y =>
if f = plus
--- a/src/Provers/Arith/cancel_div_mod.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Thu May 17 19:49:40 2007 +0200
@@ -6,8 +6,8 @@
A + n*(m div n) + B + (m mod n) + C == A + B + C + m
-FIXME: Is parameterized but assumes for simplicity that + and * are called
-"HOL.plus" and "HOL.minus"
+FIXME: Is parameterized but assumes for simplicity that + and * are named
+HOL.plus and HOL.minus
*)
signature CANCEL_DIV_MOD_DATA =
@@ -35,12 +35,12 @@
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
struct
-fun coll_div_mod (Const("HOL.plus",_) $ s $ t) dms =
+fun coll_div_mod (Const(@{const_name HOL.plus},_) $ s $ t) dms =
coll_div_mod t (coll_div_mod s dms)
- | coll_div_mod (Const("HOL.times",_) $ m $ (Const(d,_) $ s $ n))
+ | coll_div_mod (Const(@{const_name HOL.times},_) $ m $ (Const(d,_) $ s $ n))
(dms as (divs,mods)) =
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
- | coll_div_mod (Const("HOL.times",_) $ (Const(d,_) $ s $ n) $ m)
+ | coll_div_mod (Const(@{const_name HOL.times},_) $ (Const(d,_) $ s $ n) $ m)
(dms as (divs,mods)) =
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
| coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
@@ -56,8 +56,8 @@
==> thesis by transitivity
*)
-val mk_plus = Data.mk_binop "HOL.plus"
-val mk_times = Data.mk_binop "HOL.times"
+val mk_plus = Data.mk_binop @{const_name HOL.plus};
+val mk_times = Data.mk_binop @{const_name HOL.times};
fun rearrange t pq =
let val ts = Data.dest_sum t;
--- a/src/Pure/Tools/class_package.ML Thu May 17 19:49:21 2007 +0200
+++ b/src/Pure/Tools/class_package.ML Thu May 17 19:49:40 2007 +0200
@@ -97,22 +97,27 @@
let
val superclasses = map (Sign.certify_class thy) raw_superclasses;
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
+ val prefix = Logic.const_of_class name;
+ fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
+ (Sign.full_name thy c);
fun add_const ((c, ty), syn) =
Sign.add_consts_authentic [(c, ty, syn)]
- #> pair (Sign.full_name thy c, ty);
+ #> pair (mk_const_name c, ty);
fun mk_axioms cs thy =
raw_dep_axioms thy cs
|> (map o apsnd o map) (Sign.cert_prop thy)
|> rpair thy;
fun add_constraint class (c, ty) =
- Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
+ Sign.add_const_constraint_i (c, SOME
+ (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
in
thy
- (* |> Theory.add_path name *)
+ |> Theory.add_path prefix
|> fold_map add_const consts
- (* ||> Theory.restore_naming thy *)
+ ||> Theory.restore_naming thy
|-> (fn cs => mk_axioms cs
- #-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop
+ #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
+ (map fst cs @ other_consts) axioms_prop
#-> (fn class => `(fn thy => AxClass.get_definition thy class)
#-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
#> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))