--- a/src/HOL/MicroJava/BV/Listn.thy Tue Jul 28 08:49:03 2009 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy Tue Jul 28 13:37:08 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/BV/Listn.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
@@ -8,7 +7,9 @@
header {* \isaheader{Fixed Length Lists} *}
-theory Listn imports Err begin
+theory Listn
+imports Err
+begin
constdefs
@@ -317,6 +318,10 @@
apply (simp add: nth_Cons split: nat.split)
done
+lemma equals0I_aux:
+ "(\<And>y. A y \<Longrightarrow> False) \<Longrightarrow> A = bot_class.bot"
+ by (rule equals0I) (auto simp add: mem_def)
+
lemma acc_le_listI [intro!]:
"\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
apply (unfold acc_def)
@@ -330,7 +335,7 @@
apply (rename_tac m n)
apply (case_tac "m=n")
apply simp
- apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
+ apply (fast intro!: equals0I_aux dest: not_sym)
apply clarify
apply (rename_tac n)
apply (induct_tac n)
--- a/src/HOL/Wellfounded.thy Tue Jul 28 08:49:03 2009 +0200
+++ b/src/HOL/Wellfounded.thy Tue Jul 28 13:37:08 2009 +0200
@@ -283,8 +283,10 @@
apply (blast elim!: allE)
done
-lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
- to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
+lemma wfP_SUP:
+ "\<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)"
+ 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])
+ (simp_all add: bot_fun_eq bot_bool_eq)
lemma wf_Union:
"[| ALL r:R. wf r;