src/HOL/MicroJava/BV/Listn.thy
changeset 32263 8bc0fd4a23a0
parent 29235 2d62b637fa80
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 28 08:49:03 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 28 13:37:08 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/MicroJava/BV/Listn.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7      Copyright   2000 TUM
     1.8  
     1.9 @@ -8,7 +7,9 @@
    1.10  
    1.11  header {* \isaheader{Fixed Length Lists} *}
    1.12  
    1.13 -theory Listn imports Err begin
    1.14 +theory Listn
    1.15 +imports Err
    1.16 +begin
    1.17  
    1.18  constdefs
    1.19  
    1.20 @@ -317,6 +318,10 @@
    1.21  apply (simp add: nth_Cons split: nat.split)
    1.22  done
    1.23  
    1.24 +lemma equals0I_aux:
    1.25 +  "(\<And>y. A y \<Longrightarrow> False) \<Longrightarrow> A = bot_class.bot"
    1.26 +  by (rule equals0I) (auto simp add: mem_def)
    1.27 +
    1.28  lemma acc_le_listI [intro!]:
    1.29    "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
    1.30  apply (unfold acc_def)
    1.31 @@ -330,7 +335,7 @@
    1.32   apply (rename_tac m n)
    1.33   apply (case_tac "m=n")
    1.34    apply simp
    1.35 - apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
    1.36 + apply (fast intro!: equals0I_aux dest: not_sym)
    1.37  apply clarify
    1.38  apply (rename_tac n)
    1.39  apply (induct_tac n)