--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Jun 18 15:59:51 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Jun 18 21:22:05 2010 +0200
@@ -555,7 +555,6 @@
apply auto
apply (drule fold_steps_correct)
apply (simp add: correctArray_def array_ran_def)
-apply (cases "n = 0", auto)
apply (rule implies_empty_inconsistent)
apply (simp add:correctArray_def)
apply (drule bspec)
--- a/src/HOL/List.thy Fri Jun 18 15:59:51 2010 +0200
+++ b/src/HOL/List.thy Fri Jun 18 21:22:05 2010 +0200
@@ -3190,8 +3190,16 @@
lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
by auto
-lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
-by (simp add: set_replicate_conv_if split: split_if_asm)
+lemma in_set_replicate[simp]: "(x : set (replicate n y)) = (x = y & n \<noteq> 0)"
+by (simp add: set_replicate_conv_if)
+
+lemma Ball_set_replicate[simp]:
+ "(ALL x : set(replicate n a). P x) = (P a | n=0)"
+by(simp add: set_replicate_conv_if)
+
+lemma Bex_set_replicate[simp]:
+ "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"
+by(simp add: set_replicate_conv_if)
lemma replicate_append_same:
"replicate i x @ [x] = x # replicate i x"
@@ -4706,7 +4714,11 @@
lemma list_all_length:
"list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
- unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
+unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
+
+lemma list_all_cong[fundef_cong]:
+ "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
+by (simp add: list_all_iff)
lemma list_ex_iff [code_post]:
"list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
@@ -4717,7 +4729,11 @@
lemma list_ex_length:
"list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
- unfolding list_ex_iff set_conv_nth by auto
+unfolding list_ex_iff set_conv_nth by auto
+
+lemma list_ex_cong[fundef_cong]:
+ "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
+by (simp add: list_ex_iff)
lemma filtermap_conv:
"filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Jun 18 15:59:51 2010 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Jun 18 21:22:05 2010 +0200
@@ -2372,9 +2372,6 @@
apply (simp add: check_type_simps)
apply (simp only: list_def)
apply (auto simp: err_def)
-apply (subgoal_tac "set (replicate mxl Err) \<subseteq> {Err}")
-apply blast
-apply (rule subset_replicate)
done
--- a/src/HOL/ex/Recdefs.thy Fri Jun 18 15:59:51 2010 +0200
+++ b/src/HOL/ex/Recdefs.thy Fri Jun 18 21:22:05 2010 +0200
@@ -120,11 +120,13 @@
*}
consts mapf :: "nat => nat list"
-recdef (permissive) mapf "measure (\<lambda>m. m)"
+recdef mapf "measure (\<lambda>m. m)"
"mapf 0 = []"
"mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
(hints cong: map_cong)
+(* This used to be an example where recdef_tc etc is needed,
+ but now termination is proved outright
recdef_tc mapf_tc: mapf
apply (rule allI)
apply (case_tac "n = 0")
@@ -138,5 +140,6 @@
done
lemmas mapf_induct = mapf.induct [OF mapf_tc]
+*)
end