proof mod
authornipkow
Wed Aug 04 19:09:58 2004 +0200 (2004-08-04)
changeset 15109bba563cdd997
parent 15108 492e5f3a8571
child 15110 78b5636eabc7
proof mod
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/NumberTheory/Finite2.thy
     1.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Aug 04 19:09:41 2004 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Aug 04 19:09:58 2004 +0200
     1.3 @@ -301,7 +301,7 @@
     1.4  proof -
     1.5    from pc have "0 < length (drop pc is)" by simp
     1.6    then  obtain i r where Cons: "drop pc is = i#r" 
     1.7 -    by (auto simp add: neq_Nil_conv simp del: length_drop)
     1.8 +    by (auto simp add: neq_Nil_conv simp del: length_drop drop_eq_Nil)
     1.9    hence "i#r = drop pc is" ..
    1.10    with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
    1.11    from pc have "is!pc = drop pc is ! 0" by simp
     2.1 --- a/src/HOL/NumberTheory/Finite2.thy	Wed Aug 04 19:09:41 2004 +0200
     2.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Wed Aug 04 19:09:58 2004 +0200
     2.3 @@ -266,13 +266,7 @@
     2.4  
     2.5  lemma sum_prop [rule_format]: "finite B ==>
     2.6                    inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
     2.7 -apply (rule finite_induct, assumption, force)
     2.8 -apply (rule impI, auto)
     2.9 -apply (simp add: inj_on_def)
    2.10 -apply (subgoal_tac "f x \<notin> f ` F")
    2.11 -apply (subgoal_tac "finite (f ` F)");
    2.12 -apply (auto simp add: setsum_insert)
    2.13 -by (simp add: inj_on_def) 
    2.14 +by (rule finite_induct, auto)
    2.15  
    2.16  lemma sum_prop_id: "finite B ==> inj_on f B ==> 
    2.17      setsum f B = setsum id (f ` B)";