# HG changeset patch # User haftmann # Date 1157977727 -7200 # Node ID 11da1ce8dbd8b92ab34d5384fd5777eef43c4d47 # Parent 18845f9dbd096fa54e2faec3a2a9c54f7722d1a8 hid succ, pred in Numeral.thy diff -r 18845f9dbd09 -r 11da1ce8dbd8 NEWS --- 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 diff -r 18845f9dbd09 -r 11da1ce8dbd8 src/HOL/Integ/NatBin.thy --- 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]) diff -r 18845f9dbd09 -r 11da1ce8dbd8 src/HOL/Integ/NatSimprocs.thy --- 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) diff -r 18845f9dbd09 -r 11da1ce8dbd8 src/HOL/Integ/Numeral.thy --- 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 diff -r 18845f9dbd09 -r 11da1ce8dbd8 src/HOL/Integ/cooper_dec.ML --- 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*) diff -r 18845f9dbd09 -r 11da1ce8dbd8 src/HOL/Tools/Presburger/cooper_dec.ML --- 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*) diff -r 18845f9dbd09 -r 11da1ce8dbd8 src/HOL/ex/Abstract_NAT.thy --- 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 \ 'n"