# HG changeset patch # User haftmann # Date 1179424156 -7200 # Node ID 838c66e760b550dbb39eec2830fb4bb0bae7aca1 # Parent fc54d5fc4a7a77065849147f22434daa42dde943 tuned diff -r fc54d5fc4a7a -r 838c66e760b5 src/HOL/Divides.thy --- 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 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 diff -r fc54d5fc4a7a -r 838c66e760b5 src/HOL/Hyperreal/StarClasses.thy --- 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 \ star_of (number_of b)" .. -instance star :: ("Divides.div") "Divides.div" +instance star :: (Divides.div) Divides.div star_div_def: "(op div) \ *f2* (op div)" star_mod_def: "(op mod) \ *f2* (op mod)" .. diff -r fc54d5fc4a7a -r 838c66e760b5 src/HOL/Integ/IntDiv.thy --- 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; diff -r fc54d5fc4a7a -r 838c66e760b5 src/HOL/Library/Word.thy --- 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] diff -r fc54d5fc4a7a -r 838c66e760b5 src/HOL/Library/word_setup.ML --- 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 diff -r fc54d5fc4a7a -r 838c66e760b5 src/HOL/Ring_and_Field.thy --- 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 \ 0 & b \ 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 \ 0 & b \ 0)" - thus ?thesis by force + thus ?thesis + by force qed lemma division_ring_inverse_add: "[|(a::'a::division_ring) \ 0; b \ 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) \ 0; b \ 0|]