renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
--- a/src/HOL/Algebra/abstract/order.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Algebra/abstract/order.ML Tue Sep 26 13:34:16 2006 +0200
@@ -8,7 +8,7 @@
(*** Term order for commutative rings ***)
fun ring_ord (Const (a, _)) =
- find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"]
+ find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"]
| ring_ord _ = ~1;
fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
@@ -22,7 +22,7 @@
val plus = Const ("HOL.plus", [intT, intT]--->intT);
val mult = Const ("HOL.times", [intT, intT]--->intT);
val uminus = Const ("HOL.uminus", intT-->intT);
-val one = Const ("1", intT);
+val one = Const ("HOL.one", intT);
val f = Const("f", intT-->intT);
*)
--- a/src/HOL/HOL.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/HOL.thy Tue Sep 26 13:34:16 2006 +0200
@@ -191,11 +191,16 @@
subsubsection {* Generic algebraic operations *}
-axclass zero \<subseteq> type
-axclass one \<subseteq> type
+class zero =
+ fixes zero :: "'a" ("\<^loc>0")
+
+class one =
+ fixes one :: "'a" ("\<^loc>1")
+
+hide (open) const zero one
class plus =
- fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65)
+ fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65)
class minus =
fixes uminus :: "'a \<Rightarrow> 'a"
@@ -203,31 +208,25 @@
fixes abs :: "'a \<Rightarrow> 'a"
class times =
- fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70)
+ fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70)
class inverse =
fixes inverse :: "'a \<Rightarrow> 'a"
- fixes divide :: "'a \<Rightarrow> 'a => 'a" (infixl "\<^loc>'/" 70)
-
-global
-
-consts
- "0" :: "'a::zero" ("0")
- "1" :: "'a::one" ("1")
+ fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70)
syntax
"_index1" :: index ("\<^sub>1")
translations
(index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-local
-
typed_print_translation {*
- let
- fun tr' c = (c, fn show_sorts => fn T => fn ts =>
- if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
- else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
- in [tr' "0", tr' "1"] end;
+let
+ fun tr' c = (c, fn show_sorts => fn T => fn ts =>
+ if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
+ else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
+in
+ map (tr' o prefix Syntax.constN) ["HOL.one", "HOL.zero"]
+end;
*} -- {* show types that are presumably too general *}
syntax
@@ -1357,7 +1356,6 @@
hide const induct_forall induct_implies induct_equal induct_conj
-
text {* Method setup. *}
ML {*
--- a/src/HOL/Hyperreal/NSA.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Tue Sep 26 13:34:16 2006 +0200
@@ -675,12 +675,12 @@
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("0", _) => NONE
- | Const("1", _) => NONE
+ Const("HOL.zero", _) => NONE
+ | Const("HOL.one", _) => NONE
| Const("Numeral.number_of", _) $ _ => NONE
| _ => SOME (case t of
- Const("0", _) => meta_zero_approx_reorient
- | Const("1", _) => meta_one_approx_reorient
+ Const("HOL.zero", _) => meta_zero_approx_reorient
+ | Const("HOL.one", _) => meta_one_approx_reorient
| Const("Numeral.number_of", _) $ _ =>
meta_number_of_approx_reorient);
--- a/src/HOL/Integ/IntDef.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Tue Sep 26 13:34:16 2006 +0200
@@ -897,8 +897,8 @@
unfolding zabs_def by auto
consts_code
- "0" :: "int" ("0")
- "1" :: "int" ("1")
+ "HOL.zero" :: "int" ("0")
+ "HOL.one" :: "int" ("1")
"HOL.uminus" :: "int => int" ("~")
"HOL.plus" :: "int => int => int" ("(_ +/ _)")
"HOL.times" :: "int => int => int" ("(_ */ _)")
--- a/src/HOL/Integ/cooper_dec.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Tue Sep 26 13:34:16 2006 +0200
@@ -76,14 +76,14 @@
(*Transform a natural number to a term*)
-fun mk_numeral 0 = Const("0",HOLogic.intT)
- |mk_numeral 1 = Const("1",HOLogic.intT)
+fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
+ |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
|mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n);
(*Transform an Term to an natural number*)
-fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
- |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
+fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
+ |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
|dest_numeral (Const ("Numeral.number_of",_) $ n) =
HOLogic.dest_binum n;
(*Some terms often used for pattern matching*)
@@ -659,8 +659,8 @@
|mk_uni_vars T (Free (v,_)) = Free (v,T)
|mk_uni_vars T tm = tm;
-fun mk_uni_int T (Const ("0",T2)) = if T = T2 then (mk_numeral 0) else (Const ("0",T2))
- |mk_uni_int T (Const ("1",T2)) = if T = T2 then (mk_numeral 1) else (Const ("1",T2))
+fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2))
+ |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("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 Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Integ/cooper_proof.ML Tue Sep 26 13:34:16 2006 +0200
@@ -155,7 +155,7 @@
(* ------------------------------------------------------------------------- *)
(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*)
-(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
+(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
(*this is necessary because the theorems use this representation.*)
(* This function should be elminated in next versions...*)
(* ------------------------------------------------------------------------- *)
@@ -251,7 +251,7 @@
(*==================================================*)
fun decomp_adjustcoeffeq sg x l fm = case fm of
- (Const("Not",_)$(Const("Orderings.less",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
+ (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
let
val m = l div (dest_numeral c)
val n = if (x = y) then abs (m) else 1
@@ -264,7 +264,7 @@
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral n)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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
@@ -288,21 +288,21 @@
case p of
"Orderings.less" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral k)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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("0",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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.op dvd" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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)
@@ -567,7 +567,7 @@
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("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
@@ -576,8 +576,8 @@
if (is_arith_rel at) andalso (x=y)
then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 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("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
+ 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))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
end
end
@@ -590,7 +590,7 @@
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)))
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("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
@@ -658,7 +658,7 @@
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("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
@@ -667,8 +667,8 @@
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("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
+ 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))
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))
@@ -680,7 +680,7 @@
val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "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("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
--- a/src/HOL/Integ/int_arith1.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Integ/int_arith1.ML Tue Sep 26 13:34:16 2006 +0200
@@ -118,12 +118,12 @@
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("0", _) => NONE
- | Const("1", _) => NONE
+ Const("HOL.zero", _) => NONE
+ | Const("HOL.one", _) => NONE
| Const("Numeral.number_of", _) $ _ => NONE
| _ => SOME (case t of
- Const("0", _) => meta_zero_reorient
- | Const("1", _) => meta_one_reorient
+ Const("HOL.zero", _) => meta_zero_reorient
+ | Const("HOL.one", _) => meta_one_reorient
| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
val reorient_simproc =
@@ -184,8 +184,8 @@
fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_binum n;
(*Decodes a binary INTEGER*)
-fun dest_numeral (Const("0", _)) = 0
- | dest_numeral (Const("1", _)) = 1
+fun dest_numeral (Const("HOL.zero", _)) = 0
+ | dest_numeral (Const("HOL.one", _)) = 1
| dest_numeral (Const("Numeral.number_of", _) $ w) =
(HOLogic.dest_binum w
handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
--- a/src/HOL/Integ/nat_simprocs.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Tue Sep 26 13:34:16 2006 +0200
@@ -26,7 +26,7 @@
fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_binum n;
(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
-fun dest_numeral (Const ("0", _)) = 0
+fun dest_numeral (Const ("HOL.zero", _)) = 0
| dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
| dest_numeral (Const("Numeral.number_of", _) $ w) =
(IntInf.max (0, HOLogic.dest_binum w)
--- a/src/HOL/Integ/presburger.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Integ/presburger.ML Tue Sep 26 13:34:16 2006 +0200
@@ -166,10 +166,10 @@
("Numeral.Min", iT),
("Numeral.number_of", iT --> iT),
("Numeral.number_of", iT --> nT),
- ("0", nT),
- ("0", iT),
- ("1", nT),
- ("1", iT),
+ ("HOL.zero", nT),
+ ("HOL.zero", iT),
+ ("HOL.one", nT),
+ ("HOL.one", iT),
("False", bT),
("True", bT)];
--- a/src/HOL/Integ/reflected_cooper.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Integ/reflected_cooper.ML Tue Sep 26 13:34:16 2006 +0200
@@ -13,8 +13,8 @@
Free(xn,xT) => (case AList.lookup (op =) vs t of
NONE => error "Variable not found in the list!!"
| SOME n => Var n)
- | Const("0",iT) => Cst 0
- | Const("1",iT) => Cst 1
+ | 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)
--- a/src/HOL/Lambda/WeakNorm.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Tue Sep 26 13:34:16 2006 +0200
@@ -517,10 +517,10 @@
*}
ML {*
-fun nat_of_int 0 = Norm.id_0
+fun nat_of_int 0 = Norm.zero
| nat_of_int n = Norm.Suc (nat_of_int (n-1));
-fun int_of_nat Norm.id_0 = 0
+fun int_of_nat Norm.zero = 0
| int_of_nat (Norm.Suc n) = 1 + int_of_nat n;
fun dBtype_of_typ (Type ("fun", [T, U])) =
@@ -558,7 +558,7 @@
let val dBT = dBtype_of_typ T
in Norm.rtypingT_Abs (e, dBT, dB_of_term t,
dBtype_of_typ (fastype_of1 (T :: Ts, t)),
- typing_of_term (T :: Ts) (Norm.shift e Norm.id_0 dBT) t)
+ typing_of_term (T :: Ts) (Norm.shift e Norm.zero dBT) t)
end
| typing_of_term _ _ _ = error "typing_of_term: bad term";
--- a/src/HOL/Library/EfficientNat.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy Tue Sep 26 13:34:16 2006 +0200
@@ -127,8 +127,8 @@
types_code
nat ("int")
attach (term_of) {*
-fun term_of_nat 0 = Const ("0", HOLogic.natT)
- | term_of_nat 1 = Const ("1", HOLogic.natT)
+fun term_of_nat 0 = Const ("HOL.zero", HOLogic.natT)
+ | term_of_nat 1 = Const ("HOL.one", HOLogic.natT)
| term_of_nat i = HOLogic.number_of_const HOLogic.natT $
HOLogic.mk_binum (IntInf.fromInt i);
*}
@@ -141,7 +141,7 @@
(Haskell target_atom "Integer")
consts_code
- 0 :: nat ("0")
+ "HOL.zero" :: nat ("0")
Suc ("(_ + 1)")
text {*
--- a/src/HOL/Library/ExecutableRat.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy Tue Sep 26 13:34:16 2006 +0200
@@ -131,8 +131,8 @@
consts_code
div_zero ("raise/ (Fail/ \"non-defined rational number\")")
Fract ("{*of_quotient*}")
- 0 :: rat ("{*0::erat*}")
- 1 :: rat ("{*1::erat*}")
+ HOL.zero :: rat ("{*0::erat*}")
+ HOL.one :: rat ("{*1::erat*}")
HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
uminus :: "rat \<Rightarrow> rat" ("{*uminus :: erat \<Rightarrow> erat*}")
HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
--- a/src/HOL/Library/comm_ring.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Library/comm_ring.ML Tue Sep 26 13:34:16 2006 +0200
@@ -17,8 +17,8 @@
exception CRing of string;
(* Zero and One of the commutative ring *)
-fun cring_zero T = Const("0",T);
-fun cring_one T = Const("1",T);
+fun cring_zero T = Const("HOL.zero",T);
+fun cring_one T = Const("HOL.one",T);
(* reification functions *)
(* add two polynom expressions *)
@@ -30,8 +30,8 @@
(* Reification of the constructors *)
(* Nat*)
val succ = Const("Suc",nT --> nT);
-val zero = Const("0",nT);
-val one = Const("1",nT);
+val zero = Const("HOL.zero",nT);
+val one = Const("HOL.one",nT);
(* Lists *)
fun reif_list T [] = Const("List.list.Nil",listT T)
--- a/src/HOL/Nat.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Nat.thy Tue Sep 26 13:34:16 2006 +0200
@@ -112,7 +112,7 @@
rep_datatype nat
distinct Suc_not_Zero Zero_not_Suc
inject Suc_Suc_eq
- induction nat_induct
+ induction nat_induct [case_names 0 Suc]
lemma n_not_Suc_n: "n \<noteq> Suc n"
by (induct n) simp_all
@@ -1067,6 +1067,8 @@
code_instname
nat :: eq "IntDef.eq_nat"
+ nat :: zero "IntDef.zero_nat"
+ nat :: one "IntDef.one_nat"
nat :: ord "IntDef.ord_nat"
nat :: plus "IntDef.plus_nat"
nat :: minus "IntDef.minus_nat"
--- a/src/HOL/OrderedGroup.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/OrderedGroup.ML Tue Sep 26 13:34:16 2006 +0200
@@ -8,7 +8,7 @@
(*** Term order for abelian groups ***)
-fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"]
+fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
| agrp_ord _ = ~1;
fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
--- a/src/HOL/Prolog/Func.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Prolog/Func.thy Tue Sep 26 13:34:16 2006 +0200
@@ -23,7 +23,7 @@
"and" :: "tm => tm => tm" (infixr 999)
"eq" :: "tm => tm => tm" (infixr 999)
- "0" :: tm ("Z")
+ Z :: tm ("Z")
S :: "tm => tm"
(*
"++", "--",
--- a/src/HOL/Prolog/Type.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Prolog/Type.ML Tue Sep 26 13:34:16 2006 +0200
@@ -11,13 +11,13 @@
pgoal "typeof (fix (%x. x)) ?T";
-pgoal "typeof (fix (%fact. abs(%n. (app fact (n - 0))))) ?T";
+pgoal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T";
-pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \
- \(n * (app fact (n - (S 0))))))) ?T";
+pgoal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
+ \(n * (app fact (n - (S Z))))))) ?T";
-pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *)
-Goal "typeof (abs(%v. 0)) ?T";
+pgoal "typeof (abs(%v. Z)) ?T"; (*correct only solution (?A1 -> nat) *)
+Goal "typeof (abs(%v. Z)) ?T";
by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
back(); (* 2nd result (?A1 -> ?A1) wrong *)
--- a/src/HOL/Real/ferrante_rackoff_proof.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML Tue Sep 26 13:34:16 2006 +0200
@@ -287,16 +287,16 @@
(* Normalization of arithmetical expressions *)
-val rzero = Const("0",rT);
-val rone = Const("1",rT);
+val rzero = Const("HOL.zero",rT);
+val rone = Const("HOL.one",rT);
fun mk_real i =
case i of
0 => rzero
| 1 => rone
| _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i);
-fun dest_real (Const("0",_)) = 0
- | dest_real (Const("1",_)) = 1
+fun dest_real (Const("HOL.zero",_)) = 0
+ | dest_real (Const("HOL.one",_)) = 1
| dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
(* Normal form for terms is:
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Tue Sep 26 13:34:16 2006 +0200
@@ -76,14 +76,14 @@
(*Transform a natural number to a term*)
-fun mk_numeral 0 = Const("0",HOLogic.intT)
- |mk_numeral 1 = Const("1",HOLogic.intT)
+fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
+ |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
|mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n);
(*Transform an Term to an natural number*)
-fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
- |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
+fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
+ |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
|dest_numeral (Const ("Numeral.number_of",_) $ n) =
HOLogic.dest_binum n;
(*Some terms often used for pattern matching*)
@@ -659,8 +659,8 @@
|mk_uni_vars T (Free (v,_)) = Free (v,T)
|mk_uni_vars T tm = tm;
-fun mk_uni_int T (Const ("0",T2)) = if T = T2 then (mk_numeral 0) else (Const ("0",T2))
- |mk_uni_int T (Const ("1",T2)) = if T = T2 then (mk_numeral 1) else (Const ("1",T2))
+fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2))
+ |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("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 Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Tue Sep 26 13:34:16 2006 +0200
@@ -155,7 +155,7 @@
(* ------------------------------------------------------------------------- *)
(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*)
-(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
+(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
(*this is necessary because the theorems use this representation.*)
(* This function should be elminated in next versions...*)
(* ------------------------------------------------------------------------- *)
@@ -251,7 +251,7 @@
(*==================================================*)
fun decomp_adjustcoeffeq sg x l fm = case fm of
- (Const("Not",_)$(Const("Orderings.less",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
+ (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
let
val m = l div (dest_numeral c)
val n = if (x = y) then abs (m) else 1
@@ -264,7 +264,7 @@
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral n)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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
@@ -288,21 +288,21 @@
case p of
"Orderings.less" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral k)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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("0",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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.op dvd" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral 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)
@@ -567,7 +567,7 @@
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("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
@@ -576,8 +576,8 @@
if (is_arith_rel at) andalso (x=y)
then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 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("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
+ 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))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
end
end
@@ -590,7 +590,7 @@
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)))
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("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
@@ -658,7 +658,7 @@
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("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
@@ -667,8 +667,8 @@
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("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
+ 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))
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))
@@ -680,7 +680,7 @@
val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "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("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),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))
--- a/src/HOL/Tools/Presburger/presburger.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Tue Sep 26 13:34:16 2006 +0200
@@ -166,10 +166,10 @@
("Numeral.Min", iT),
("Numeral.number_of", iT --> iT),
("Numeral.number_of", iT --> nT),
- ("0", nT),
- ("0", iT),
- ("1", nT),
- ("1", iT),
+ ("HOL.zero", nT),
+ ("HOL.zero", iT),
+ ("HOL.one", nT),
+ ("HOL.one", iT),
("False", bT),
("True", bT)];
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Tue Sep 26 13:34:16 2006 +0200
@@ -13,8 +13,8 @@
Free(xn,xT) => (case AList.lookup (op =) vs t of
NONE => error "Variable not found in the list!!"
| SOME n => Var n)
- | Const("0",iT) => Cst 0
- | Const("1",iT) => Cst 1
+ | 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)
--- a/src/HOL/arith_data.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/arith_data.ML Tue Sep 26 13:34:16 2006 +0200
@@ -324,8 +324,8 @@
demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
end
handle TERM _ => (SOME atom, m))
- | demult (Const ("0", _), m) = (NONE, Rat.rat_of_int 0)
- | demult (Const ("1", _), m) = (NONE, m)
+ | demult (Const ("HOL.zero", _), m) = (NONE, Rat.rat_of_int 0)
+ | demult (Const ("HOL.one", _), m) = (NONE, m)
| demult (t as Const ("Numeral.number_of", _) $ n, m) =
((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
handle TERM _ => (SOME t,m))
@@ -350,9 +350,9 @@
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) =
if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
- | poly (Const ("0", _), _, pi) =
+ | poly (Const ("HOL.zero", _), _, pi) =
pi
- | poly (Const ("1", _), m, (p, i)) =
+ | poly (Const ("HOL.one", _), m, (p, i)) =
(p, Rat.add (i, m))
| poly (Const ("Suc", _) $ t, m, (p, i)) =
poly (t, m, (p, Rat.add (i, m)))
@@ -558,7 +558,7 @@
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, Const ("HOL.uminus",
split_type --> split_type) $ t1)]) rev_terms
- val zero = Const ("0", split_type)
+ val zero = Const ("HOL.zero", split_type)
val zero_leq_t1 = Const ("Orderings.less_eq",
split_type --> split_type --> HOLogic.boolT) $ zero $ t1
val t1_lt_zero = Const ("Orderings.less",
@@ -575,7 +575,7 @@
(* "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 ("0", split_type)
+ val zero = Const ("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)])
@@ -597,8 +597,8 @@
| (Const ("IntDef.nat", _), [t1]) =>
let
val rev_terms = rev terms
- val zero_int = Const ("0", HOLogic.intT)
- val zero_nat = Const ("0", HOLogic.natT)
+ val zero_int = Const ("HOL.zero", HOLogic.intT)
+ val zero_nat = Const ("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)
@@ -620,7 +620,7 @@
| (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const ("0", split_type)
+ val zero = Const ("HOL.zero", split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -652,7 +652,7 @@
| (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const ("0", split_type)
+ val zero = Const ("HOL.zero", split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
@@ -688,7 +688,7 @@
Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
- val zero = Const ("0", split_type)
+ val zero = Const ("HOL.zero", split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -740,7 +740,7 @@
Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
- val zero = Const ("0", split_type)
+ val zero = Const ("HOL.zero", split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
--- a/src/HOL/ex/Abstract_NAT.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy Tue Sep 26 13:34:16 2006 +0200
@@ -31,11 +31,11 @@
consts
REC :: "'n \<Rightarrow> ('n \<Rightarrow> 'n) \<Rightarrow> 'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('n * 'a) set"
-inductive "REC zero succ e r"
+inductive "REC zer succ e r"
intros
- Rec_zero: "NAT zero succ \<Longrightarrow> (zero, e) \<in> REC zero succ e r"
- Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
- (succ m, r m n) \<in> REC zero succ e r"
+ Rec_zero: "NAT zer succ \<Longrightarrow> (zer, e) \<in> REC zer succ e r"
+ Rec_succ: "NAT zer succ \<Longrightarrow> (m, n) \<in> REC zer succ e r \<Longrightarrow>
+ (succ m, r m n) \<in> REC zer succ e r"
abbreviation (in NAT)
"Rec == REC zero succ"
--- a/src/HOL/ex/Codegenerator.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy Tue Sep 26 13:34:16 2006 +0200
@@ -17,8 +17,6 @@
subsection {* natural numbers *}
definition
- one :: nat
- "one = 1"
n :: nat
"n = 42"
@@ -105,8 +103,10 @@
definition
"shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
-code_gen xor
-code_gen one
+code_gen
+ xor
+code_gen
+ "0::nat" "1::nat"
code_gen
Pair fst snd Let split swap
code_gen "0::int" "1::int"
--- a/src/HOL/ex/mesontest2.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/ex/mesontest2.ML Tue Sep 26 13:34:16 2006 +0200
@@ -985,11 +985,11 @@
meson_tac 1);
val HEN002_0_ax =
- "(\\<forall>X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),zero)) & \
-\ (\\<forall>X Y. equal(Divide(X::'a,Y),zero) --> mless_equal(X::'a,Y)) & \
+ "(\\<forall>X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),Zero)) & \
+\ (\\<forall>X Y. equal(Divide(X::'a,Y),Zero) --> mless_equal(X::'a,Y)) & \
\ (\\<forall>Y X. mless_equal(Divide(X::'a,Y),X)) & \
\ (\\<forall>X Y Z. mless_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) & \
-\ (\\<forall>X. mless_equal(zero::'a,X)) & \
+\ (\\<forall>X. mless_equal(Zero::'a,X)) & \
\ (\\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \
\ (\\<forall>X. mless_equal(X::'a,identity))";
@@ -1002,18 +1002,18 @@
(*250258 inferences so far. Searching to depth 16. 406.2 secs*)
val HEN003_3 = prove_hard
(EQU001_0_ax ^ "&" ^ HEN002_0_ax ^ "&" ^ HEN002_0_eq ^ " & \
-\ (~equal(Divide(a::'a,a),zero)) --> False",
+\ (~equal(Divide(a::'a,a),Zero)) --> False",
meson_tac 1);
(*202177 inferences so far. Searching to depth 14. 451 secs*)
val HEN007_2 = prove_hard
(EQU001_0_ax ^ " & \
-\ (\\<forall>X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) & \
-\ (\\<forall>X Y. quotient(X::'a,Y,zero) --> mless_equal(X::'a,Y)) & \
+\ (\\<forall>X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,Zero)) & \
+\ (\\<forall>X Y. quotient(X::'a,Y,Zero) --> mless_equal(X::'a,Y)) & \
\ (\\<forall>Y Z X. quotient(X::'a,Y,Z) --> mless_equal(Z::'a,X)) & \
\ (\\<forall>Y X V3 V2 V1 Z V4 V5. quotient(X::'a,Y,V1) & quotient(Y::'a,Z,V2) & quotient(X::'a,Z,V3) & quotient(V3::'a,V2,V4) & quotient(V1::'a,Z,V5) --> mless_equal(V4::'a,V5)) & \
-\ (\\<forall>X. mless_equal(zero::'a,X)) & \
+\ (\\<forall>X. mless_equal(Zero::'a,X)) & \
\ (\\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \
\ (\\<forall>X. mless_equal(X::'a,identity)) & \
\ (\\<forall>X Y. quotient(X::'a,Y,Divide(X::'a,Y))) & \
@@ -1025,10 +1025,10 @@
\ (\\<forall>X Y Z. equal(X::'a,Y) & mless_equal(X::'a,Z) --> mless_equal(Y::'a,Z)) & \
\ (\\<forall>X Y W. equal(X::'a,Y) --> equal(Divide(X::'a,W),Divide(Y::'a,W))) & \
\ (\\<forall>X W Y. equal(X::'a,Y) --> equal(Divide(W::'a,X),Divide(W::'a,Y))) & \
-\ (\\<forall>X. quotient(X::'a,identity,zero)) & \
-\ (\\<forall>X. quotient(zero::'a,X,zero)) & \
-\ (\\<forall>X. quotient(X::'a,X,zero)) & \
-\ (\\<forall>X. quotient(X::'a,zero,X)) & \
+\ (\\<forall>X. quotient(X::'a,identity,Zero)) & \
+\ (\\<forall>X. quotient(Zero::'a,X,Zero)) & \
+\ (\\<forall>X. quotient(X::'a,X,Zero)) & \
+\ (\\<forall>X. quotient(X::'a,Zero,X)) & \
\ (\\<forall>Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \
\ (\\<forall>W1 X Z W2 Y. quotient(X::'a,Y,W1) & mless_equal(W1::'a,Z) & quotient(X::'a,Z,W2) --> mless_equal(W2::'a,Y)) & \
\ (mless_equal(x::'a,y)) & \
@@ -1040,10 +1040,10 @@
(*60026 inferences so far. Searching to depth 12. 42.2 secs*)
val HEN008_4 = prove_hard
(EQU001_0_ax ^ "&" ^ HEN002_0_ax ^ "&" ^ HEN002_0_eq ^ " & \
-\ (\\<forall>X. equal(Divide(X::'a,identity),zero)) & \
-\ (\\<forall>X. equal(Divide(zero::'a,X),zero)) & \
-\ (\\<forall>X. equal(Divide(X::'a,X),zero)) & \
-\ (equal(Divide(a::'a,zero),a)) & \
+\ (\\<forall>X. equal(Divide(X::'a,identity),Zero)) & \
+\ (\\<forall>X. equal(Divide(Zero::'a,X),Zero)) & \
+\ (\\<forall>X. equal(Divide(X::'a,X),Zero)) & \
+\ (equal(Divide(a::'a,Zero),a)) & \
\ (\\<forall>Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \
\ (\\<forall>X Z Y. mless_equal(Divide(X::'a,Y),Z) --> mless_equal(Divide(X::'a,Z),Y)) & \
\ (\\<forall>Y Z X. mless_equal(X::'a,Y) --> mless_equal(Divide(Z::'a,Y),Divide(Z::'a,X))) & \
@@ -1055,16 +1055,16 @@
(*3160 inferences so far. Searching to depth 11. 3.5 secs*)
val HEN009_5 = prove
(EQU001_0_ax ^ " & \
-\ (\\<forall>Y X. equal(Divide(Divide(X::'a,Y),X),zero)) & \
-\ (\\<forall>X Y Z. equal(Divide(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z)),zero)) & \
-\ (\\<forall>X. equal(Divide(zero::'a,X),zero)) & \
-\ (\\<forall>X Y. equal(Divide(X::'a,Y),zero) & equal(Divide(Y::'a,X),zero) --> equal(X::'a,Y)) & \
-\ (\\<forall>X. equal(Divide(X::'a,identity),zero)) & \
+\ (\\<forall>Y X. equal(Divide(Divide(X::'a,Y),X),Zero)) & \
+\ (\\<forall>X Y Z. equal(Divide(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z)),Zero)) & \
+\ (\\<forall>X. equal(Divide(Zero::'a,X),Zero)) & \
+\ (\\<forall>X Y. equal(Divide(X::'a,Y),Zero) & equal(Divide(Y::'a,X),Zero) --> equal(X::'a,Y)) & \
+\ (\\<forall>X. equal(Divide(X::'a,identity),Zero)) & \
\ (\\<forall>A B C. equal(A::'a,B) --> equal(Divide(A::'a,C),Divide(B::'a,C))) & \
\ (\\<forall>D F' E. equal(D::'a,E) --> equal(Divide(F'::'a,D),Divide(F'::'a,E))) & \
-\ (\\<forall>Y X Z. equal(Divide(X::'a,Y),zero) & equal(Divide(Y::'a,Z),zero) --> equal(Divide(X::'a,Z),zero)) & \
-\ (\\<forall>X Z Y. equal(Divide(Divide(X::'a,Y),Z),zero) --> equal(Divide(Divide(X::'a,Z),Y),zero)) & \
-\ (\\<forall>Y Z X. equal(Divide(X::'a,Y),zero) --> equal(Divide(Divide(Z::'a,Y),Divide(Z::'a,X)),zero)) & \
+\ (\\<forall>Y X Z. equal(Divide(X::'a,Y),Zero) & equal(Divide(Y::'a,Z),Zero) --> equal(Divide(X::'a,Z),Zero)) & \
+\ (\\<forall>X Z Y. equal(Divide(Divide(X::'a,Y),Z),Zero) --> equal(Divide(Divide(X::'a,Z),Y),Zero)) & \
+\ (\\<forall>Y Z X. equal(Divide(X::'a,Y),Zero) --> equal(Divide(Divide(Z::'a,Y),Divide(Z::'a,X)),Zero)) & \
\ (~equal(Divide(identity::'a,a),Divide(identity::'a,Divide(identity::'a,Divide(identity::'a,a))))) & \
\ (equal(Divide(identity::'a,a),b)) & \
\ (equal(Divide(identity::'a,b),c)) & \
@@ -1735,8 +1735,8 @@
\ (mless_THAN(i::'a,n)) & \
\ (mless_THAN(a(j),a(k))) & \
\ (\\<forall>X. mless_THAN(X::'a,j) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,i)) & \
-\ (\\<forall>X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \
-\ (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) & \
+\ (\\<forall>X. mless_THAN(One::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \
+\ (\\<forall>X. ~(mless_THAN(One::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) & \
\ (mless_THAN(j::'a,i)) --> False",
meson_tac 1);
@@ -1747,11 +1747,11 @@
\ (~mless_THAN(k::'a,l)) & \
\ (~mless_THAN(k::'a,i)) & \
\ (mless_THAN(l::'a,n)) & \
-\ (mless_THAN(one::'a,l)) & \
+\ (mless_THAN(One::'a,l)) & \
\ (mless_THAN(a(k),a(predecessor(l)))) & \
\ (\\<forall>X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,l)) & \
-\ (\\<forall>X. mless_THAN(one::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) & \
-\ (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,l) & mless_THAN(a(X),a(predecessor(X))))) --> False",
+\ (\\<forall>X. mless_THAN(One::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) & \
+\ (\\<forall>X. ~(mless_THAN(One::'a,X) & mless_THAN(X::'a,l) & mless_THAN(a(X),a(predecessor(X))))) --> False",
meson_tac 1);
(*2343 inferences so far. Searching to depth 8. 3.5 secs*)
@@ -1760,11 +1760,11 @@
\ (~mless_THAN(n::'a,m)) & \
\ (mless_THAN(i::'a,m)) & \
\ (mless_THAN(i::'a,n)) & \
-\ (~mless_THAN(i::'a,one)) & \
+\ (~mless_THAN(i::'a,One)) & \
\ (mless_THAN(a(i),a(m))) & \
\ (\\<forall>X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(m)) --> mless_THAN(X::'a,i)) & \
-\ (\\<forall>X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \
-\ (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) --> False",
+\ (\\<forall>X. mless_THAN(One::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \
+\ (\\<forall>X. ~(mless_THAN(One::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) --> False",
meson_tac 1);
(*86 inferences so far. Searching to depth 14. 0.1 secs*)
@@ -2166,9 +2166,9 @@
\ (\\<forall>M O_ N. equal(M::'a,N) --> equal(multiply(O_::'a,M),multiply(O_::'a,N))) & \
\ (\\<forall>P Q. equal(P::'a,Q) --> equal(successor(P),successor(Q))) & \
\ (\\<forall>R S'. equal(R::'a,S') & positive_integer(R) --> positive_integer(S')) & \
-\ (\\<forall>X. equal(multiply(one::'a,X),X)) & \
+\ (\\<forall>X. equal(multiply(One::'a,X),X)) & \
\ (\\<forall>V X. positive_integer(X) --> equal(multiply(successor(V),X),add(X::'a,multiply(V::'a,X)))) & \
-\ (positive_integer(one)) & \
+\ (positive_integer(One)) & \
\ (\\<forall>X. positive_integer(X) --> positive_integer(successor(X))) & \
\ (equal(negate(add(d::'a,e)),negate(e))) & \
\ (positive_integer(k)) & \
@@ -2212,22 +2212,22 @@
(*6450 inferences so far. Searching to depth 14. 4.2 secs*)
val SET009_1 = prove
- ("(\\<forall>Subset Element Superset. member(Element::'a,Subset) & subset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \
-\ (\\<forall>Superset Subset. subset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \
-\ (\\<forall>Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> subset(Subset::'a,Superset)) & \
-\ (\\<forall>Subset Superset. equal_sets(Subset::'a,Superset) --> subset(Subset::'a,Superset)) & \
-\ (\\<forall>Subset Superset. equal_sets(Superset::'a,Subset) --> subset(Subset::'a,Superset)) & \
-\ (\\<forall>Set2 Set1. subset(Set1::'a,Set2) & subset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) & \
+ ("(\\<forall>Subset Element Superset. member(Element::'a,Subset) & ssubset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \
+\ (\\<forall>Superset Subset. ssubset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \
+\ (\\<forall>Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> ssubset(Subset::'a,Superset)) & \
+\ (\\<forall>Subset Superset. equal_sets(Subset::'a,Superset) --> ssubset(Subset::'a,Superset)) & \
+\ (\\<forall>Subset Superset. equal_sets(Superset::'a,Subset) --> ssubset(Subset::'a,Superset)) & \
+\ (\\<forall>Set2 Set1. ssubset(Set1::'a,Set2) & ssubset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) & \
\ (\\<forall>Set2 Difference Element Set1. difference(Set1::'a,Set2,Difference) & member(Element::'a,Difference) --> member(Element::'a,Set1)) & \
\ (\\<forall>Element A_set Set1 Set2. ~(member(Element::'a,Set1) & member(Element::'a,Set2) & difference(A_set::'a,Set1,Set2))) & \
\ (\\<forall>Set1 Difference Element Set2. member(Element::'a,Set1) & difference(Set1::'a,Set2,Difference) --> member(Element::'a,Difference) | member(Element::'a,Set2)) & \
\ (\\<forall>Set1 Set2 Difference. difference(Set1::'a,Set2,Difference) | member(k(Set1::'a,Set2,Difference),Set1) | member(k(Set1::'a,Set2,Difference),Difference)) & \
\ (\\<forall>Set1 Set2 Difference. member(k(Set1::'a,Set2,Difference),Set2) --> member(k(Set1::'a,Set2,Difference),Difference) | difference(Set1::'a,Set2,Difference)) & \
\ (\\<forall>Set1 Set2 Difference. member(k(Set1::'a,Set2,Difference),Difference) & member(k(Set1::'a,Set2,Difference),Set1) --> member(k(Set1::'a,Set2,Difference),Set2) | difference(Set1::'a,Set2,Difference)) & \
-\ (subset(d::'a,a)) & \
+\ (ssubset(d::'a,a)) & \
\ (difference(b::'a,a,bDa)) & \
\ (difference(b::'a,d,bDd)) & \
-\ (~subset(bDa::'a,bDd)) --> False",
+\ (~ssubset(bDa::'a,bDd)) --> False",
meson_tac 1);
(*34726 inferences so far. Searching to depth 6. 2420 secs: 40 mins! BIG*)
@@ -2299,14 +2299,14 @@
\ (\\<forall>Z X. member(Z::'a,sigma(X)) --> member(Z::'a,f16(Z::'a,X))) & \
\ (\\<forall>X Z Y. member(Y::'a,X) & member(Z::'a,Y) --> member(Z::'a,sigma(X))) & \
\ (\\<forall>U. little_set(U) --> little_set(sigma(U))) & \
-\ (\\<forall>X U Y. subset(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) & \
-\ (\\<forall>Y X. subset(X::'a,Y) | member(f17(X::'a,Y),X)) & \
-\ (\\<forall>X Y. member(f17(X::'a,Y),Y) --> subset(X::'a,Y)) & \
-\ (\\<forall>X Y. proper_subset(X::'a,Y) --> subset(X::'a,Y)) & \
+\ (\\<forall>X U Y. ssubset(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) & \
+\ (\\<forall>Y X. ssubset(X::'a,Y) | member(f17(X::'a,Y),X)) & \
+\ (\\<forall>X Y. member(f17(X::'a,Y),Y) --> ssubset(X::'a,Y)) & \
+\ (\\<forall>X Y. proper_subset(X::'a,Y) --> ssubset(X::'a,Y)) & \
\ (\\<forall>X Y. ~(proper_subset(X::'a,Y) & equal(X::'a,Y))) & \
-\ (\\<forall>X Y. subset(X::'a,Y) --> proper_subset(X::'a,Y) | equal(X::'a,Y)) & \
-\ (\\<forall>Z X. member(Z::'a,powerset(X)) --> subset(Z::'a,X)) & \
-\ (\\<forall>Z X. little_set(Z) & subset(Z::'a,X) --> member(Z::'a,powerset(X))) & \
+\ (\\<forall>X Y. ssubset(X::'a,Y) --> proper_subset(X::'a,Y) | equal(X::'a,Y)) & \
+\ (\\<forall>Z X. member(Z::'a,powerset(X)) --> ssubset(Z::'a,X)) & \
+\ (\\<forall>Z X. little_set(Z) & ssubset(Z::'a,X) --> member(Z::'a,powerset(X))) & \
\ (\\<forall>U. little_set(U) --> little_set(powerset(U))) & \
\ (\\<forall>Z X. relation(Z) & member(X::'a,Z) --> ordered_pair_predicate(X)) & \
\ (\\<forall>Z. relation(Z) | member(f18(Z),Z)) & \
@@ -2354,8 +2354,8 @@
\ (\\<forall>Xf X Y. equal(apply_to_two_arguments(Xf::'a,X,Y),apply(Xf::'a,ordered_pair(X::'a,Y)))) & \
\ (\\<forall>X Y Xf. maps(Xf::'a,X,Y) --> function(Xf)) & \
\ (\\<forall>Y Xf X. maps(Xf::'a,X,Y) --> equal(domain_of(Xf),X)) & \
-\ (\\<forall>X Xf Y. maps(Xf::'a,X,Y) --> subset(range_of(Xf),Y)) & \
-\ (\\<forall>X Xf Y. function(Xf) & equal(domain_of(Xf),X) & subset(range_of(Xf),Y) --> maps(Xf::'a,X,Y)) & \
+\ (\\<forall>X Xf Y. maps(Xf::'a,X,Y) --> ssubset(range_of(Xf),Y)) & \
+\ (\\<forall>X Xf Y. function(Xf) & equal(domain_of(Xf),X) & ssubset(range_of(Xf),Y) --> maps(Xf::'a,X,Y)) & \
\ (\\<forall>Xf Xs. closed(Xs::'a,Xf) --> little_set(Xs)) & \
\ (\\<forall>Xs Xf. closed(Xs::'a,Xf) --> little_set(Xf)) & \
\ (\\<forall>Xf Xs. closed(Xs::'a,Xf) --> maps(Xf::'a,cross_product(Xs::'a,Xs),Xs)) & \
@@ -2494,8 +2494,8 @@
\ (\\<forall>P15 R15 Q15. equal(P15::'a,Q15) & proper_subset(R15::'a,P15) --> proper_subset(R15::'a,Q15)) & \
\ (\\<forall>S15 T15. equal(S15::'a,T15) & relation(S15) --> relation(T15)) & \
\ (\\<forall>U15 V15. equal(U15::'a,V15) & single_valued_set(U15) --> single_valued_set(V15)) & \
-\ (\\<forall>W15 X15 Y15. equal(W15::'a,X15) & subset(W15::'a,Y15) --> subset(X15::'a,Y15)) & \
-\ (\\<forall>Z15 B16 A16. equal(Z15::'a,A16) & subset(B16::'a,Z15) --> subset(B16::'a,A16)) & \
+\ (\\<forall>W15 X15 Y15. equal(W15::'a,X15) & ssubset(W15::'a,Y15) --> ssubset(X15::'a,Y15)) & \
+\ (\\<forall>Z15 B16 A16. equal(Z15::'a,A16) & ssubset(B16::'a,Z15) --> ssubset(B16::'a,A16)) & \
\ (~little_set(ordered_pair(a::'a,b))) --> False",
meson_tac 1);
--- a/src/HOL/hologic.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/hologic.ML Tue Sep 26 13:34:16 2006 +0200
@@ -261,9 +261,9 @@
val natT = Type ("nat", []);
-val zero = Const ("0", natT);
+val zero = Const ("HOL.zero", natT);
-fun is_zero (Const ("0", _)) = true
+fun is_zero (Const ("HOL.zero", _)) = true
| is_zero _ = false;
fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
@@ -274,7 +274,7 @@
fun mk_nat 0 = zero
| mk_nat n = mk_Suc (mk_nat (n - 1));
-fun dest_nat (Const ("0", _)) = 0
+fun dest_nat (Const ("HOL.zero", _)) = 0
| dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
| dest_nat t = raise TERM ("dest_nat", [t]);
@@ -319,21 +319,17 @@
fun mk_binum n =
let
fun mk_bit n = if n = 0 then B0_const else B1_const;
-
fun bin_of n =
if n = 0 then pls_const
else if n = ~1 then min_const
else
let
- (*val (q,r) = IntInf.divMod (n, 2): doesn't work in SML 110.0.7,
- but in newer versions! FIXME: put this back after new SML released!*)
- val q = IntInf.div (n, 2);
- val r = IntInf.mod (n, 2);
+ val (q,r) = IntInf.divMod (n, 2);
in bit_const $ bin_of q $ mk_bit r end;
in bin_of n end;
-fun mk_int 0 = Const ("0", intT)
- | mk_int 1 = Const ("1", intT)
+fun mk_int 0 = Const ("HOL.zero", intT)
+ | mk_int 1 = Const ("HOL.one", intT)
| mk_int i = number_of_const intT $ mk_binum i;
--- a/src/HOLCF/Pcpo.thy Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOLCF/Pcpo.thy Tue Sep 26 13:34:16 2006 +0200
@@ -200,8 +200,8 @@
fun reorient_proc sg _ (_ $ t $ u) =
case u of
Const("Pcpo.UU",_) => NONE
- | Const("0", _) => NONE
- | Const("1", _) => NONE
+ | Const("HOL.zero", _) => NONE
+ | Const("HOL.one", _) => NONE
| Const("Numeral.number_of", _) $ _ => NONE
| _ => SOME meta_UU_reorient;
in
--- a/src/Provers/Arith/abel_cancel.ML Tue Sep 26 13:34:15 2006 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Tue Sep 26 13:34:16 2006 +0200
@@ -28,7 +28,7 @@
(* FIXME dependent on abstract syntax *)
-fun zero t = Const ("0", t);
+fun zero t = Const ("HOL.zero", t);
fun minus t = Const ("HOL.uminus", t --> t);
fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =