# HG changeset patch # User haftmann # Date 1159270456 -7200 # Node ID 823967ef47f17339388c5b41ba10b188ca0e166d # Parent b3cd1233167fa4a72d3f01f325c933e89534cb9e renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Algebra/abstract/order.ML --- 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); *) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/HOL.thy --- 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 \ type -axclass one \ 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 \ 'a \ 'a" (infixl "\<^loc>+" 65) + fixes plus :: "'a \ 'a \ 'a" (infixl "\<^loc>+" 65) class minus = fixes uminus :: "'a \ 'a" @@ -203,31 +208,25 @@ fixes abs :: "'a \ 'a" class times = - fixes times :: "'a \ 'a \ 'a" (infixl "\<^loc>*" 70) + fixes times :: "'a \ 'a \ 'a" (infixl "\<^loc>*" 70) class inverse = fixes inverse :: "'a \ 'a" - fixes divide :: "'a \ 'a => 'a" (infixl "\<^loc>'/" 70) - -global - -consts - "0" :: "'a::zero" ("0") - "1" :: "'a::one" ("1") + fixes divide :: "'a \ 'a \ 'a" (infixl "\<^loc>'/" 70) syntax "_index1" :: index ("\<^sub>1") translations (index) "\<^sub>1" => (index) "\<^bsub>\\<^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 {* diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Hyperreal/NSA.thy --- 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); diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Integ/IntDef.thy --- 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" ("(_ */ _)") diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Integ/cooper_dec.ML --- 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; diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Integ/cooper_proof.ML --- 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)) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Integ/int_arith1.ML --- 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])) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Integ/nat_simprocs.ML --- 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) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Integ/presburger.ML --- 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)]; diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Integ/reflected_cooper.ML --- 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) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Lambda/WeakNorm.thy --- 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"; diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Library/EfficientNat.thy --- 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 {* diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Library/ExecutableRat.thy --- 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 \ rat \ rat" ("{*op + :: erat \ erat \ erat*}") uminus :: "rat \ rat" ("{*uminus :: erat \ erat*}") HOL.times :: "rat \ rat \ rat" ("{*op * :: erat \ erat \ erat*}") diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Library/comm_ring.ML --- 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) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Nat.thy --- 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 \ 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" diff -r b3cd1233167f -r 823967ef47f1 src/HOL/OrderedGroup.ML --- 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); diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Prolog/Func.thy --- 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" (* "++", "--", diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Prolog/Type.ML --- 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 *) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Real/ferrante_rackoff_proof.ML --- 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: diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Tools/Presburger/cooper_dec.ML --- 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; diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Tools/Presburger/cooper_proof.ML --- 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)) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Tools/Presburger/presburger.ML --- 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)]; diff -r b3cd1233167f -r 823967ef47f1 src/HOL/Tools/Presburger/reflected_cooper.ML --- 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) diff -r b3cd1233167f -r 823967ef47f1 src/HOL/arith_data.ML --- 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 diff -r b3cd1233167f -r 823967ef47f1 src/HOL/ex/Abstract_NAT.thy --- 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 \ ('n \ 'n) \ 'a \ ('n \ 'a \ 'a) \ ('n * 'a) set" -inductive "REC zero succ e r" +inductive "REC zer succ e r" intros - Rec_zero: "NAT zero succ \ (zero, e) \ REC zero succ e r" - Rec_succ: "NAT zero succ \ (m, n) \ REC zero succ e r \ - (succ m, r m n) \ REC zero succ e r" + Rec_zero: "NAT zer succ \ (zer, e) \ REC zer succ e r" + Rec_succ: "NAT zer succ \ (m, n) \ REC zer succ e r \ + (succ m, r m n) \ REC zer succ e r" abbreviation (in NAT) "Rec == REC zero succ" diff -r b3cd1233167f -r 823967ef47f1 src/HOL/ex/Codegenerator.thy --- 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" diff -r b3cd1233167f -r 823967ef47f1 src/HOL/ex/mesontest2.ML --- 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 = - "(\\X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),zero)) & \ -\ (\\X Y. equal(Divide(X::'a,Y),zero) --> mless_equal(X::'a,Y)) & \ + "(\\X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),Zero)) & \ +\ (\\X Y. equal(Divide(X::'a,Y),Zero) --> mless_equal(X::'a,Y)) & \ \ (\\Y X. mless_equal(Divide(X::'a,Y),X)) & \ \ (\\X Y Z. mless_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) & \ -\ (\\X. mless_equal(zero::'a,X)) & \ +\ (\\X. mless_equal(Zero::'a,X)) & \ \ (\\X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \ \ (\\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 ^ " & \ -\ (\\X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) & \ -\ (\\X Y. quotient(X::'a,Y,zero) --> mless_equal(X::'a,Y)) & \ +\ (\\X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,Zero)) & \ +\ (\\X Y. quotient(X::'a,Y,Zero) --> mless_equal(X::'a,Y)) & \ \ (\\Y Z X. quotient(X::'a,Y,Z) --> mless_equal(Z::'a,X)) & \ \ (\\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)) & \ -\ (\\X. mless_equal(zero::'a,X)) & \ +\ (\\X. mless_equal(Zero::'a,X)) & \ \ (\\X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \ \ (\\X. mless_equal(X::'a,identity)) & \ \ (\\X Y. quotient(X::'a,Y,Divide(X::'a,Y))) & \ @@ -1025,10 +1025,10 @@ \ (\\X Y Z. equal(X::'a,Y) & mless_equal(X::'a,Z) --> mless_equal(Y::'a,Z)) & \ \ (\\X Y W. equal(X::'a,Y) --> equal(Divide(X::'a,W),Divide(Y::'a,W))) & \ \ (\\X W Y. equal(X::'a,Y) --> equal(Divide(W::'a,X),Divide(W::'a,Y))) & \ -\ (\\X. quotient(X::'a,identity,zero)) & \ -\ (\\X. quotient(zero::'a,X,zero)) & \ -\ (\\X. quotient(X::'a,X,zero)) & \ -\ (\\X. quotient(X::'a,zero,X)) & \ +\ (\\X. quotient(X::'a,identity,Zero)) & \ +\ (\\X. quotient(Zero::'a,X,Zero)) & \ +\ (\\X. quotient(X::'a,X,Zero)) & \ +\ (\\X. quotient(X::'a,Zero,X)) & \ \ (\\Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \ \ (\\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 ^ " & \ -\ (\\X. equal(Divide(X::'a,identity),zero)) & \ -\ (\\X. equal(Divide(zero::'a,X),zero)) & \ -\ (\\X. equal(Divide(X::'a,X),zero)) & \ -\ (equal(Divide(a::'a,zero),a)) & \ +\ (\\X. equal(Divide(X::'a,identity),Zero)) & \ +\ (\\X. equal(Divide(Zero::'a,X),Zero)) & \ +\ (\\X. equal(Divide(X::'a,X),Zero)) & \ +\ (equal(Divide(a::'a,Zero),a)) & \ \ (\\Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \ \ (\\X Z Y. mless_equal(Divide(X::'a,Y),Z) --> mless_equal(Divide(X::'a,Z),Y)) & \ \ (\\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 ^ " & \ -\ (\\Y X. equal(Divide(Divide(X::'a,Y),X),zero)) & \ -\ (\\X Y Z. equal(Divide(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z)),zero)) & \ -\ (\\X. equal(Divide(zero::'a,X),zero)) & \ -\ (\\X Y. equal(Divide(X::'a,Y),zero) & equal(Divide(Y::'a,X),zero) --> equal(X::'a,Y)) & \ -\ (\\X. equal(Divide(X::'a,identity),zero)) & \ +\ (\\Y X. equal(Divide(Divide(X::'a,Y),X),Zero)) & \ +\ (\\X Y Z. equal(Divide(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z)),Zero)) & \ +\ (\\X. equal(Divide(Zero::'a,X),Zero)) & \ +\ (\\X Y. equal(Divide(X::'a,Y),Zero) & equal(Divide(Y::'a,X),Zero) --> equal(X::'a,Y)) & \ +\ (\\X. equal(Divide(X::'a,identity),Zero)) & \ \ (\\A B C. equal(A::'a,B) --> equal(Divide(A::'a,C),Divide(B::'a,C))) & \ \ (\\D F' E. equal(D::'a,E) --> equal(Divide(F'::'a,D),Divide(F'::'a,E))) & \ -\ (\\Y X Z. equal(Divide(X::'a,Y),zero) & equal(Divide(Y::'a,Z),zero) --> equal(Divide(X::'a,Z),zero)) & \ -\ (\\X Z Y. equal(Divide(Divide(X::'a,Y),Z),zero) --> equal(Divide(Divide(X::'a,Z),Y),zero)) & \ -\ (\\Y Z X. equal(Divide(X::'a,Y),zero) --> equal(Divide(Divide(Z::'a,Y),Divide(Z::'a,X)),zero)) & \ +\ (\\Y X Z. equal(Divide(X::'a,Y),Zero) & equal(Divide(Y::'a,Z),Zero) --> equal(Divide(X::'a,Z),Zero)) & \ +\ (\\X Z Y. equal(Divide(Divide(X::'a,Y),Z),Zero) --> equal(Divide(Divide(X::'a,Z),Y),Zero)) & \ +\ (\\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))) & \ \ (\\X. mless_THAN(X::'a,j) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,i)) & \ -\ (\\X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \ -\ (\\X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) & \ +\ (\\X. mless_THAN(One::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \ +\ (\\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)))) & \ \ (\\X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,l)) & \ -\ (\\X. mless_THAN(one::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) & \ -\ (\\X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,l) & mless_THAN(a(X),a(predecessor(X))))) --> False", +\ (\\X. mless_THAN(One::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) & \ +\ (\\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))) & \ \ (\\X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(m)) --> mless_THAN(X::'a,i)) & \ -\ (\\X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \ -\ (\\X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) --> False", +\ (\\X. mless_THAN(One::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \ +\ (\\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 @@ \ (\\M O_ N. equal(M::'a,N) --> equal(multiply(O_::'a,M),multiply(O_::'a,N))) & \ \ (\\P Q. equal(P::'a,Q) --> equal(successor(P),successor(Q))) & \ \ (\\R S'. equal(R::'a,S') & positive_integer(R) --> positive_integer(S')) & \ -\ (\\X. equal(multiply(one::'a,X),X)) & \ +\ (\\X. equal(multiply(One::'a,X),X)) & \ \ (\\V X. positive_integer(X) --> equal(multiply(successor(V),X),add(X::'a,multiply(V::'a,X)))) & \ -\ (positive_integer(one)) & \ +\ (positive_integer(One)) & \ \ (\\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 - ("(\\Subset Element Superset. member(Element::'a,Subset) & subset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \ -\ (\\Superset Subset. subset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \ -\ (\\Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> subset(Subset::'a,Superset)) & \ -\ (\\Subset Superset. equal_sets(Subset::'a,Superset) --> subset(Subset::'a,Superset)) & \ -\ (\\Subset Superset. equal_sets(Superset::'a,Subset) --> subset(Subset::'a,Superset)) & \ -\ (\\Set2 Set1. subset(Set1::'a,Set2) & subset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) & \ + ("(\\Subset Element Superset. member(Element::'a,Subset) & ssubset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \ +\ (\\Superset Subset. ssubset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \ +\ (\\Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> ssubset(Subset::'a,Superset)) & \ +\ (\\Subset Superset. equal_sets(Subset::'a,Superset) --> ssubset(Subset::'a,Superset)) & \ +\ (\\Subset Superset. equal_sets(Superset::'a,Subset) --> ssubset(Subset::'a,Superset)) & \ +\ (\\Set2 Set1. ssubset(Set1::'a,Set2) & ssubset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) & \ \ (\\Set2 Difference Element Set1. difference(Set1::'a,Set2,Difference) & member(Element::'a,Difference) --> member(Element::'a,Set1)) & \ \ (\\Element A_set Set1 Set2. ~(member(Element::'a,Set1) & member(Element::'a,Set2) & difference(A_set::'a,Set1,Set2))) & \ \ (\\Set1 Difference Element Set2. member(Element::'a,Set1) & difference(Set1::'a,Set2,Difference) --> member(Element::'a,Difference) | member(Element::'a,Set2)) & \ \ (\\Set1 Set2 Difference. difference(Set1::'a,Set2,Difference) | member(k(Set1::'a,Set2,Difference),Set1) | member(k(Set1::'a,Set2,Difference),Difference)) & \ \ (\\Set1 Set2 Difference. member(k(Set1::'a,Set2,Difference),Set2) --> member(k(Set1::'a,Set2,Difference),Difference) | difference(Set1::'a,Set2,Difference)) & \ \ (\\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 @@ \ (\\Z X. member(Z::'a,sigma(X)) --> member(Z::'a,f16(Z::'a,X))) & \ \ (\\X Z Y. member(Y::'a,X) & member(Z::'a,Y) --> member(Z::'a,sigma(X))) & \ \ (\\U. little_set(U) --> little_set(sigma(U))) & \ -\ (\\X U Y. subset(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) & \ -\ (\\Y X. subset(X::'a,Y) | member(f17(X::'a,Y),X)) & \ -\ (\\X Y. member(f17(X::'a,Y),Y) --> subset(X::'a,Y)) & \ -\ (\\X Y. proper_subset(X::'a,Y) --> subset(X::'a,Y)) & \ +\ (\\X U Y. ssubset(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) & \ +\ (\\Y X. ssubset(X::'a,Y) | member(f17(X::'a,Y),X)) & \ +\ (\\X Y. member(f17(X::'a,Y),Y) --> ssubset(X::'a,Y)) & \ +\ (\\X Y. proper_subset(X::'a,Y) --> ssubset(X::'a,Y)) & \ \ (\\X Y. ~(proper_subset(X::'a,Y) & equal(X::'a,Y))) & \ -\ (\\X Y. subset(X::'a,Y) --> proper_subset(X::'a,Y) | equal(X::'a,Y)) & \ -\ (\\Z X. member(Z::'a,powerset(X)) --> subset(Z::'a,X)) & \ -\ (\\Z X. little_set(Z) & subset(Z::'a,X) --> member(Z::'a,powerset(X))) & \ +\ (\\X Y. ssubset(X::'a,Y) --> proper_subset(X::'a,Y) | equal(X::'a,Y)) & \ +\ (\\Z X. member(Z::'a,powerset(X)) --> ssubset(Z::'a,X)) & \ +\ (\\Z X. little_set(Z) & ssubset(Z::'a,X) --> member(Z::'a,powerset(X))) & \ \ (\\U. little_set(U) --> little_set(powerset(U))) & \ \ (\\Z X. relation(Z) & member(X::'a,Z) --> ordered_pair_predicate(X)) & \ \ (\\Z. relation(Z) | member(f18(Z),Z)) & \ @@ -2354,8 +2354,8 @@ \ (\\Xf X Y. equal(apply_to_two_arguments(Xf::'a,X,Y),apply(Xf::'a,ordered_pair(X::'a,Y)))) & \ \ (\\X Y Xf. maps(Xf::'a,X,Y) --> function(Xf)) & \ \ (\\Y Xf X. maps(Xf::'a,X,Y) --> equal(domain_of(Xf),X)) & \ -\ (\\X Xf Y. maps(Xf::'a,X,Y) --> subset(range_of(Xf),Y)) & \ -\ (\\X Xf Y. function(Xf) & equal(domain_of(Xf),X) & subset(range_of(Xf),Y) --> maps(Xf::'a,X,Y)) & \ +\ (\\X Xf Y. maps(Xf::'a,X,Y) --> ssubset(range_of(Xf),Y)) & \ +\ (\\X Xf Y. function(Xf) & equal(domain_of(Xf),X) & ssubset(range_of(Xf),Y) --> maps(Xf::'a,X,Y)) & \ \ (\\Xf Xs. closed(Xs::'a,Xf) --> little_set(Xs)) & \ \ (\\Xs Xf. closed(Xs::'a,Xf) --> little_set(Xf)) & \ \ (\\Xf Xs. closed(Xs::'a,Xf) --> maps(Xf::'a,cross_product(Xs::'a,Xs),Xs)) & \ @@ -2494,8 +2494,8 @@ \ (\\P15 R15 Q15. equal(P15::'a,Q15) & proper_subset(R15::'a,P15) --> proper_subset(R15::'a,Q15)) & \ \ (\\S15 T15. equal(S15::'a,T15) & relation(S15) --> relation(T15)) & \ \ (\\U15 V15. equal(U15::'a,V15) & single_valued_set(U15) --> single_valued_set(V15)) & \ -\ (\\W15 X15 Y15. equal(W15::'a,X15) & subset(W15::'a,Y15) --> subset(X15::'a,Y15)) & \ -\ (\\Z15 B16 A16. equal(Z15::'a,A16) & subset(B16::'a,Z15) --> subset(B16::'a,A16)) & \ +\ (\\W15 X15 Y15. equal(W15::'a,X15) & ssubset(W15::'a,Y15) --> ssubset(X15::'a,Y15)) & \ +\ (\\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); diff -r b3cd1233167f -r 823967ef47f1 src/HOL/hologic.ML --- 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; diff -r b3cd1233167f -r 823967ef47f1 src/HOLCF/Pcpo.thy --- 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 diff -r b3cd1233167f -r 823967ef47f1 src/Provers/Arith/abel_cancel.ML --- 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) =