explicit is better than implicit
authorhaftmann
Tue Jul 28 13:37:08 2009 +0200 (2009-07-28)
changeset 322638bc0fd4a23a0
parent 32245 0c1cb95a434d
child 32264 0be31453f698
explicit is better than implicit
src/HOL/MicroJava/BV/Listn.thy
src/HOL/Wellfounded.thy
     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)
     2.1 --- a/src/HOL/Wellfounded.thy	Tue Jul 28 08:49:03 2009 +0200
     2.2 +++ b/src/HOL/Wellfounded.thy	Tue Jul 28 13:37:08 2009 +0200
     2.3 @@ -283,8 +283,10 @@
     2.4  apply (blast elim!: allE)  
     2.5  done
     2.6  
     2.7 -lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
     2.8 -  to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
     2.9 +lemma wfP_SUP:
    2.10 +  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
    2.11 +  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2 pred_equals_eq])
    2.12 +    (simp_all add: bot_fun_eq bot_bool_eq)
    2.13  
    2.14  lemma wf_Union: 
    2.15   "[| ALL r:R. wf r;