fixed proof
authornipkow
Mon Oct 20 23:53:17 2008 +0200 (2008-10-20)
changeset 28643caa1137d25dc
parent 28642 658b598d8af4
child 28644 e2ae4a6cf166
fixed proof
src/HOL/Word/WordDefinition.thy
src/HOL/Word/WordShift.thy
     1.1 --- a/src/HOL/Word/WordDefinition.thy	Mon Oct 20 23:52:59 2008 +0200
     1.2 +++ b/src/HOL/Word/WordDefinition.thy	Mon Oct 20 23:53:17 2008 +0200
     1.3 @@ -830,10 +830,7 @@
     1.4  lemma ucast_up_app': 
     1.5    "uc = ucast ==> source_size uc + n = target_size uc ==> 
     1.6      to_bl (uc w) = replicate n False @ (to_bl w)"
     1.7 -  apply (auto simp add : source_size target_size to_bl_ucast)
     1.8 -  apply (rule_tac f = "%n. replicate n False" in arg_cong)
     1.9 -  apply simp
    1.10 -  done
    1.11 +  by (auto simp add : source_size target_size to_bl_ucast)
    1.12  
    1.13  lemma ucast_down_drop': 
    1.14    "uc = ucast ==> source_size uc = target_size uc + n ==> 
     2.1 --- a/src/HOL/Word/WordShift.thy	Mon Oct 20 23:52:59 2008 +0200
     2.2 +++ b/src/HOL/Word/WordShift.thy	Mon Oct 20 23:53:17 2008 +0200
     2.3 @@ -458,7 +458,6 @@
     2.4     apply (simp add: bl_word_and to_bl_0)
     2.5     apply (rule align_lem_and [THEN trans])
     2.6         apply (simp_all add: word_size)[5]
     2.7 -   apply (rule_tac f = "%n. replicate n False" in arg_cong)
     2.8     apply simp
     2.9    apply (subst word_plus_and_or [symmetric])
    2.10    apply (simp add : bl_word_or)
    2.11 @@ -710,8 +709,6 @@
    2.12    apply (rule bl_shiftl [THEN trans])
    2.13    apply (subst ucast_up_app)
    2.14    apply (auto simp add: wsst_TYs)
    2.15 -  apply (drule sym)
    2.16 -  apply (simp add: min_def)
    2.17    done
    2.18  
    2.19  lemmas revcast_up = refl [THEN revcast_up']