--- a/src/HOL/Divides.thy Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/Divides.thy Thu May 17 19:49:16 2007 +0200
@@ -8,6 +8,7 @@
theory Divides
imports Datatype Power
+uses "~~/src/Provers/Arith/cancel_div_mod.ML"
begin
(*We use the same class for div and mod;
@@ -31,11 +32,11 @@
notation
mod (infixl "mod" 70)
-instance nat :: "Divides.div"
+instance nat :: Divides.div
+ div_def: "m div n == wfrec (pred_nat^+)
+ (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
mod_def: "m mod n == wfrec (pred_nat^+)
- (%f j. if j<n | n=0 then j else f (j-n)) m"
- div_def: "m div n == wfrec (pred_nat^+)
- (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
+ (%f j. if j<n | n=0 then j else f (j-n)) m" ..
definition
(*The definition of dvd is polymorphic!*)
--- a/src/HOL/HOL.thy Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/HOL.thy Thu May 17 19:49:16 2007 +0200
@@ -227,7 +227,7 @@
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' [@{const_syntax "HOL.one"}, @{const_syntax "HOL.zero"}] end;
+in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
*} -- {* show types that are presumably too general *}
@@ -913,7 +913,7 @@
struct
type claset = Classical.claset
val equality_name = @{const_name "op ="}
- val not_name = @{const_name "Not"}
+ val not_name = @{const_name Not}
val notE = @{thm HOL.notE}
val ccontr = @{thm HOL.ccontr}
val contr_tac = Classical.contr_tac
--- a/src/HOL/Hyperreal/StarClasses.thy Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy Thu May 17 19:49:16 2007 +0200
@@ -35,7 +35,7 @@
instance star :: (number) number
star_number_def: "number_of b \<equiv> star_of (number_of b)" ..
-instance star :: ("Divides.div") "Divides.div"
+instance star :: (Divides.div) Divides.div
star_div_def: "(op div) \<equiv> *f2* (op div)"
star_mod_def: "(op mod) \<equiv> *f2* (op mod)" ..
--- a/src/HOL/Integ/IntDiv.thy Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/Integ/IntDiv.thy Thu May 17 19:49:16 2007 +0200
@@ -251,8 +251,8 @@
structure CancelDivMod = CancelDivModFun(
struct
- val div_name = @{const_name "Divides.div"};
- val mod_name = @{const_name "Divides.mod"};
+ val div_name = @{const_name Divides.div};
+ val mod_name = @{const_name Divides.mod};
val mk_binop = HOLogic.mk_binop;
val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
val dest_sum = Int_Numeral_Simprocs.dest_sum;
--- a/src/HOL/Library/Word.thy Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/Library/Word.thy Thu May 17 19:49:16 2007 +0200
@@ -7,7 +7,6 @@
theory Word
imports Main
-uses "word_setup.ML"
begin
subsection {* Auxilary Lemmas *}
@@ -2501,7 +2500,42 @@
declare fast_bv_to_nat_Cons0 [simp]
declare fast_bv_to_nat_Cons1 [simp]
-setup setup_word
+setup {*
+(*comments containing lcp are the removal of fast_bv_of_nat*)
+let
+ fun is_const_bool (Const("True",_)) = true
+ | is_const_bool (Const("False",_)) = true
+ | is_const_bool _ = false
+ fun is_const_bit (Const("Word.bit.Zero",_)) = true
+ | is_const_bit (Const("Word.bit.One",_)) = true
+ | is_const_bit _ = false
+ fun num_is_usable (Const("Numeral.Pls",_)) = true
+ | num_is_usable (Const("Numeral.Min",_)) = false
+ | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
+ num_is_usable w andalso is_const_bool b
+ | num_is_usable _ = false
+ fun vec_is_usable (Const("List.list.Nil",_)) = true
+ | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
+ vec_is_usable bs andalso is_const_bit b
+ | vec_is_usable _ = false
+ (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"*)
+ val fast2_th = @{thm "Word.fast_bv_to_nat_def"};
+ (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const(@{const_name Numeral.number_of},_) $ t)) =
+ if num_is_usable t
+ then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.int",[]))),cterm_of sg t)] fast1_th)
+ else NONE
+ | f _ _ _ = NONE *)
+ fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
+ if vec_is_usable t then
+ SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
+ else NONE
+ | g _ _ _ = NONE
+ (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
+ val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
+in
+ (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2]);
+ thy))
+end*}
declare bv_to_nat1 [simp del]
declare bv_to_nat_helper [simp del]
--- a/src/HOL/Library/word_setup.ML Thu May 17 19:29:39 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: HOL/Library/word_setup.ML
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
-
-comments containing lcp are the removal of fast_bv_of_nat.
-*)
-
-local
- fun is_const_bool (Const("True",_)) = true
- | is_const_bool (Const("False",_)) = true
- | is_const_bool _ = false
- fun is_const_bit (Const("Word.bit.Zero",_)) = true
- | is_const_bit (Const("Word.bit.One",_)) = true
- | is_const_bit _ = false
- fun num_is_usable (Const("Numeral.Pls",_)) = true
- | num_is_usable (Const("Numeral.Min",_)) = false
- | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
- num_is_usable w andalso is_const_bool b
- | num_is_usable _ = false
- fun vec_is_usable (Const("List.list.Nil",_)) = true
- | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
- vec_is_usable bs andalso is_const_bit b
- | vec_is_usable _ = false
- fun add_word thy =
- let
- (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
- val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
- (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
- if num_is_usable t
- then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.int",[]))),cterm_of sg t)] fast1_th)
- else NONE
- | f _ _ _ = NONE **)
- fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
- if vec_is_usable t
- then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
- else NONE
- | g _ _ _ = NONE
- (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
- val simproc2 = Simplifier.simproc thy "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
- in
- Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
- thy
- end
-in
-val setup_word = add_word
-end
--- a/src/HOL/Ring_and_Field.thy Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Thu May 17 19:49:16 2007 +0200
@@ -932,16 +932,18 @@
"inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
proof cases
assume "a \<noteq> 0 & b \<noteq> 0"
- thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
+ thus ?thesis
+ by (simp add: nonzero_inverse_mult_distrib mult_commute)
next
assume "~ (a \<noteq> 0 & b \<noteq> 0)"
- thus ?thesis by force
+ thus ?thesis
+ by force
qed
lemma division_ring_inverse_add:
"[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
==> inverse a + inverse b = inverse a * (a+b) * inverse b"
-by (simp add: right_distrib left_distrib mult_assoc)
+ by (simp add: right_distrib left_distrib mult_assoc)
lemma division_ring_inverse_diff:
"[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]