--- a/NEWS Mon Sep 11 12:27:36 2006 +0200
+++ b/NEWS Mon Sep 11 14:28:47 2006 +0200
@@ -466,8 +466,8 @@
*** HOL ***
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
-abandoned in favour of plain 'int'. Significant changes for setting up numeral
-syntax for types:
+abandoned in favour of plain 'int'. INCOMPATIBILITY -- Significant changes
+for setting up numeral syntax for types:
- new constants Numeral.pred and Numeral.succ instead
of former Numeral.bin_pred and Numeral.bin_succ.
@@ -477,8 +477,6 @@
See HOL/Integ/IntArith.thy for an example setup.
-INCOMPATIBILITY.
-
* New top level command 'normal_form' computes the normal form of a term
that may contain free variables. For example 'normal_form "rev[a,b,c]"'
prints '[b,c,a]'. This command is suitable for heavy-duty computations
--- a/src/HOL/Integ/NatBin.thy Mon Sep 11 12:27:36 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy Mon Sep 11 14:28:47 2006 +0200
@@ -112,14 +112,14 @@
lemma Suc_nat_number_of_add:
"Suc (number_of v + n) =
- (if neg (number_of v :: int) then 1+n else number_of (succ v) + n)"
+ (if neg (number_of v :: int) then 1+n else number_of (Numeral.succ v) + n)"
by (simp del: nat_number_of
add: nat_number_of_def neg_nat
Suc_nat_eq_nat_zadd1 number_of_succ)
lemma Suc_nat_number_of [simp]:
"Suc (number_of v) =
- (if neg (number_of v :: int) then 1 else number_of (succ v))"
+ (if neg (number_of v :: int) then 1 else number_of (Numeral.succ v))"
apply (cut_tac n = 0 in Suc_nat_number_of_add)
apply (simp cong del: if_weak_cong)
done
@@ -447,7 +447,7 @@
lemma eq_number_of_Suc [simp]:
"(number_of v = Suc n) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then False else nat pv = n)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
@@ -458,13 +458,13 @@
lemma Suc_eq_number_of [simp]:
"(Suc n = number_of v) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then False else nat pv = n)"
by (rule trans [OF eq_sym_conv eq_number_of_Suc])
lemma less_number_of_Suc [simp]:
"(number_of v < Suc n) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then True else nat pv < n)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
@@ -475,7 +475,7 @@
lemma less_Suc_number_of [simp]:
"(Suc n < number_of v) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then False else n < nat pv)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
@@ -486,13 +486,13 @@
lemma le_number_of_Suc [simp]:
"(number_of v <= Suc n) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then True else nat pv <= n)"
by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
lemma le_Suc_number_of [simp]:
"(Suc n <= number_of v) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then False else n <= nat pv)"
by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
--- a/src/HOL/Integ/NatSimprocs.thy Mon Sep 11 12:27:36 2006 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy Mon Sep 11 14:28:47 2006 +0200
@@ -23,8 +23,8 @@
the right simplification, but with some redundant inequality
tests.*}
lemma neg_number_of_pred_iff_0:
- "neg (number_of (pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (pred v)) = (number_of v < Suc 0) ")
+ "neg (number_of (Numeral.pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (Numeral.pred v)) = (number_of v < Suc 0) ")
apply (simp only: less_Suc_eq_le le_0_eq)
apply (subst less_number_of_Suc, simp)
done
@@ -33,7 +33,7 @@
simproc*}
lemma Suc_diff_number_of:
"neg (number_of (uminus v)::int) ==>
- Suc m - (number_of v) = m - (number_of (pred v))"
+ Suc m - (number_of v) = m - (number_of (Numeral.pred v))"
apply (subst Suc_diff_eq_diff_pred)
apply simp
apply (simp del: nat_numeral_1_eq_1)
@@ -49,13 +49,13 @@
lemma nat_case_number_of [simp]:
"nat_case a f (number_of v) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then a else f (nat pv))"
by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
lemma nat_case_add_eq_if [simp]:
"nat_case a f ((number_of v) + n) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then nat_case a f n else f (nat pv + n))"
apply (subst add_eq_if)
apply (simp split add: nat.split
@@ -66,7 +66,7 @@
lemma nat_rec_number_of [simp]:
"nat_rec a f (number_of v) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
apply (case_tac " (number_of v) ::nat")
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
@@ -75,7 +75,7 @@
lemma nat_rec_add_eq_if [simp]:
"nat_rec a f (number_of v + n) =
- (let pv = number_of (pred v) in
+ (let pv = number_of (Numeral.pred v) in
if neg pv then nat_rec a f n
else f (nat pv + n) (nat_rec a f (nat pv + n)))"
apply (subst add_eq_if)
--- a/src/HOL/Integ/Numeral.thy Mon Sep 11 12:27:36 2006 +0200
+++ b/src/HOL/Integ/Numeral.thy Mon Sep 11 14:28:47 2006 +0200
@@ -533,6 +533,6 @@
done
-hide (open) const Pls Min B0 B1
+hide (open) const Pls Min B0 B1 succ pred
end
--- a/src/HOL/Integ/cooper_dec.ML Mon Sep 11 12:27:36 2006 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Mon Sep 11 14:28:47 2006 +0200
@@ -46,7 +46,7 @@
val integer_qelim : Term.term -> Term.term
end;
-structure CooperDec : COOPER_DEC =
+structure CooperDec : COOPER_DEC =
struct
(* ========================================================================= *)
@@ -66,12 +66,10 @@
(*Function is_arith_rel returns true if and only if the term is an atomar presburger
formula *)
-fun is_arith_rel tm = case tm of
- Const(p,Type ("fun",[Type ("Numeral.bin", []),Type ("fun",[Type ("Numeral.bin",
- []),Type ("bool",[])] )])) $ _ $_ => true
- |Const(p,Type ("fun",[Type ("IntDef.int", []),Type ("fun",[Type ("IntDef.int",
- []),Type ("bool",[])] )])) $ _ $_ => true
- |_ => false;
+fun is_arith_rel tm = case tm
+ of Const(p, Type ("fun", [Type ("IntDef.int", []), Type ("fun", [Type ("IntDef.int", []),
+ Type ("bool", [])])])) $ _ $_ => true
+ | _ => false;
(*Function is_arith_rel returns true if and only if the term is an operation of the
form [int,int]---> int*)
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Mon Sep 11 12:27:36 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Mon Sep 11 14:28:47 2006 +0200
@@ -46,7 +46,7 @@
val integer_qelim : Term.term -> Term.term
end;
-structure CooperDec : COOPER_DEC =
+structure CooperDec : COOPER_DEC =
struct
(* ========================================================================= *)
@@ -66,12 +66,10 @@
(*Function is_arith_rel returns true if and only if the term is an atomar presburger
formula *)
-fun is_arith_rel tm = case tm of
- Const(p,Type ("fun",[Type ("Numeral.bin", []),Type ("fun",[Type ("Numeral.bin",
- []),Type ("bool",[])] )])) $ _ $_ => true
- |Const(p,Type ("fun",[Type ("IntDef.int", []),Type ("fun",[Type ("IntDef.int",
- []),Type ("bool",[])] )])) $ _ $_ => true
- |_ => false;
+fun is_arith_rel tm = case tm
+ of Const(p, Type ("fun", [Type ("IntDef.int", []), Type ("fun", [Type ("IntDef.int", []),
+ Type ("bool", [])])])) $ _ $_ => true
+ | _ => false;
(*Function is_arith_rel returns true if and only if the term is an operation of the
form [int,int]---> int*)
--- a/src/HOL/ex/Abstract_NAT.thy Mon Sep 11 12:27:36 2006 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy Mon Sep 11 14:28:47 2006 +0200
@@ -11,8 +11,6 @@
text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *}
-hide (open) const succ
-
locale NAT =
fixes zero :: 'n
and succ :: "'n \<Rightarrow> 'n"