tuned
authorhaftmann
Thu May 17 19:49:16 2007 +0200 (2007-05-17)
changeset 22993838c66e760b5
parent 22992 fc54d5fc4a7a
child 22994 02440636214f
tuned
src/HOL/Divides.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Library/Word.thy
src/HOL/Library/word_setup.ML
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Divides.thy	Thu May 17 19:29:39 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu May 17 19:49:16 2007 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  theory Divides
     1.6  imports Datatype Power
     1.7 +uses "~~/src/Provers/Arith/cancel_div_mod.ML"
     1.8  begin
     1.9  
    1.10  (*We use the same class for div and mod;
    1.11 @@ -31,11 +32,11 @@
    1.12  notation
    1.13    mod (infixl "mod" 70)
    1.14  
    1.15 -instance nat :: "Divides.div"
    1.16 +instance nat :: Divides.div
    1.17 +  div_def: "m div n == wfrec (pred_nat^+)
    1.18 +                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    1.19    mod_def: "m mod n == wfrec (pred_nat^+)
    1.20 -                          (%f j. if j<n | n=0 then j else f (j-n)) m"
    1.21 -  div_def: "m div n == wfrec (pred_nat^+)
    1.22 -                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
    1.23 +                          (%f j. if j<n | n=0 then j else f (j-n)) m" ..
    1.24  
    1.25  definition
    1.26    (*The definition of dvd is polymorphic!*)
     2.1 --- a/src/HOL/HOL.thy	Thu May 17 19:29:39 2007 +0200
     2.2 +++ b/src/HOL/HOL.thy	Thu May 17 19:49:16 2007 +0200
     2.3 @@ -227,7 +227,7 @@
     2.4    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
     2.5      if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     2.6      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
     2.7 -in map tr' [@{const_syntax "HOL.one"}, @{const_syntax "HOL.zero"}] end;
     2.8 +in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
     2.9  *} -- {* show types that are presumably too general *}
    2.10  
    2.11  
    2.12 @@ -913,7 +913,7 @@
    2.13  struct
    2.14    type claset = Classical.claset
    2.15    val equality_name = @{const_name "op ="}
    2.16 -  val not_name = @{const_name "Not"}
    2.17 +  val not_name = @{const_name Not}
    2.18    val notE = @{thm HOL.notE}
    2.19    val ccontr = @{thm HOL.ccontr}
    2.20    val contr_tac = Classical.contr_tac
     3.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Thu May 17 19:29:39 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Thu May 17 19:49:16 2007 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4  instance star :: (number) number
     3.5    star_number_def:  "number_of b \<equiv> star_of (number_of b)" ..
     3.6  
     3.7 -instance star :: ("Divides.div") "Divides.div"
     3.8 +instance star :: (Divides.div) Divides.div
     3.9    star_div_def:     "(op div) \<equiv> *f2* (op div)"
    3.10    star_mod_def:     "(op mod) \<equiv> *f2* (op mod)" ..
    3.11  
     4.1 --- a/src/HOL/Integ/IntDiv.thy	Thu May 17 19:29:39 2007 +0200
     4.2 +++ b/src/HOL/Integ/IntDiv.thy	Thu May 17 19:49:16 2007 +0200
     4.3 @@ -251,8 +251,8 @@
     4.4  
     4.5  structure CancelDivMod = CancelDivModFun(
     4.6  struct
     4.7 -  val div_name = @{const_name "Divides.div"};
     4.8 -  val mod_name = @{const_name "Divides.mod"};
     4.9 +  val div_name = @{const_name Divides.div};
    4.10 +  val mod_name = @{const_name Divides.mod};
    4.11    val mk_binop = HOLogic.mk_binop;
    4.12    val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
    4.13    val dest_sum = Int_Numeral_Simprocs.dest_sum;
     5.1 --- a/src/HOL/Library/Word.thy	Thu May 17 19:29:39 2007 +0200
     5.2 +++ b/src/HOL/Library/Word.thy	Thu May 17 19:49:16 2007 +0200
     5.3 @@ -7,7 +7,6 @@
     5.4  
     5.5  theory Word
     5.6  imports Main
     5.7 -uses "word_setup.ML"
     5.8  begin
     5.9  
    5.10  subsection {* Auxilary Lemmas *}
    5.11 @@ -2501,7 +2500,42 @@
    5.12  declare fast_bv_to_nat_Cons0 [simp]
    5.13  declare fast_bv_to_nat_Cons1 [simp]
    5.14  
    5.15 -setup setup_word
    5.16 +setup {*
    5.17 +(*comments containing lcp are the removal of fast_bv_of_nat*)
    5.18 +let
    5.19 +  fun is_const_bool (Const("True",_)) = true
    5.20 +    | is_const_bool (Const("False",_)) = true
    5.21 +    | is_const_bool _ = false
    5.22 +  fun is_const_bit (Const("Word.bit.Zero",_)) = true
    5.23 +    | is_const_bit (Const("Word.bit.One",_)) = true
    5.24 +    | is_const_bit _ = false
    5.25 +  fun num_is_usable (Const("Numeral.Pls",_)) = true
    5.26 +    | num_is_usable (Const("Numeral.Min",_)) = false
    5.27 +    | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
    5.28 +        num_is_usable w andalso is_const_bool b
    5.29 +    | num_is_usable _ = false
    5.30 +  fun vec_is_usable (Const("List.list.Nil",_)) = true
    5.31 +    | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
    5.32 +        vec_is_usable bs andalso is_const_bit b
    5.33 +    | vec_is_usable _ = false
    5.34 +  (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"*)
    5.35 +  val fast2_th = @{thm "Word.fast_bv_to_nat_def"};
    5.36 +  (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const(@{const_name Numeral.number_of},_) $ t)) =
    5.37 +    if num_is_usable t
    5.38 +      then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.int",[]))),cterm_of sg t)] fast1_th)
    5.39 +      else NONE
    5.40 +    | f _ _ _ = NONE *)
    5.41 +  fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
    5.42 +        if vec_is_usable t then
    5.43 +          SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
    5.44 +        else NONE
    5.45 +    | g _ _ _ = NONE
    5.46 +  (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
    5.47 +  val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
    5.48 +in
    5.49 +  (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2]);
    5.50 +    thy))
    5.51 +end*}
    5.52  
    5.53  declare bv_to_nat1 [simp del]
    5.54  declare bv_to_nat_helper [simp del]
     6.1 --- a/src/HOL/Library/word_setup.ML	Thu May 17 19:29:39 2007 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,46 +0,0 @@
     6.4 -(*  Title:      HOL/Library/word_setup.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Sebastian Skalberg (TU Muenchen)
     6.7 -
     6.8 -comments containing lcp are the removal of fast_bv_of_nat.
     6.9 -*)
    6.10 -
    6.11 -local
    6.12 -    fun is_const_bool (Const("True",_)) = true
    6.13 -      | is_const_bool (Const("False",_)) = true
    6.14 -      | is_const_bool _ = false
    6.15 -    fun is_const_bit (Const("Word.bit.Zero",_)) = true
    6.16 -      | is_const_bit (Const("Word.bit.One",_)) = true
    6.17 -      | is_const_bit _ = false
    6.18 -    fun num_is_usable (Const("Numeral.Pls",_)) = true
    6.19 -      | num_is_usable (Const("Numeral.Min",_)) = false
    6.20 -      | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
    6.21 -	num_is_usable w andalso is_const_bool b
    6.22 -      | num_is_usable _ = false
    6.23 -    fun vec_is_usable (Const("List.list.Nil",_)) = true
    6.24 -      | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
    6.25 -	vec_is_usable bs andalso is_const_bit b
    6.26 -      | vec_is_usable _ = false
    6.27 -    fun add_word thy =
    6.28 -	let
    6.29 - (*lcp**	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
    6.30 -	    val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
    6.31 - (*lcp**	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
    6.32 -		if num_is_usable t
    6.33 -		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.int",[]))),cterm_of sg t)] fast1_th)
    6.34 -		else NONE
    6.35 -	      | f _ _ _ = NONE **)
    6.36 -	    fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
    6.37 -		if vec_is_usable t
    6.38 -		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
    6.39 -		else NONE
    6.40 -	      | g _ _ _ = NONE
    6.41 -  (*lcp**	    val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
    6.42 -	    val simproc2 = Simplifier.simproc thy "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
    6.43 -	in
    6.44 -	  Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
    6.45 -          thy
    6.46 -	end
    6.47 -in
    6.48 -val setup_word = add_word
    6.49 -end
     7.1 --- a/src/HOL/Ring_and_Field.thy	Thu May 17 19:29:39 2007 +0200
     7.2 +++ b/src/HOL/Ring_and_Field.thy	Thu May 17 19:49:16 2007 +0200
     7.3 @@ -932,16 +932,18 @@
     7.4       "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
     7.5    proof cases
     7.6      assume "a \<noteq> 0 & b \<noteq> 0" 
     7.7 -    thus ?thesis  by (simp add: nonzero_inverse_mult_distrib mult_commute)
     7.8 +    thus ?thesis
     7.9 +      by (simp add: nonzero_inverse_mult_distrib mult_commute)
    7.10    next
    7.11      assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
    7.12 -    thus ?thesis  by force
    7.13 +    thus ?thesis
    7.14 +      by force
    7.15    qed
    7.16  
    7.17  lemma division_ring_inverse_add:
    7.18    "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
    7.19     ==> inverse a + inverse b = inverse a * (a+b) * inverse b"
    7.20 -by (simp add: right_distrib left_distrib mult_assoc)
    7.21 +  by (simp add: right_distrib left_distrib mult_assoc)
    7.22  
    7.23  lemma division_ring_inverse_diff:
    7.24    "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]