author haftmann Thu May 17 19:49:16 2007 +0200 (2007-05-17) changeset 22993 838c66e760b5 parent 22992 fc54d5fc4a7a child 22994 02440636214f
tuned
 src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/HOL.thy file | annotate | diff | revisions src/HOL/Hyperreal/StarClasses.thy file | annotate | diff | revisions src/HOL/Integ/IntDiv.thy file | annotate | diff | revisions src/HOL/Library/Word.thy file | annotate | diff | revisions src/HOL/Library/word_setup.ML file | annotate | diff | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | revisions
```     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.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