# HG changeset patch
# User nipkow
# Date 1276885326 -7200
# Node ID 0a1cc267595892686124346d0bf3bede70812006
# Parent  059ee31766866d8f8579edb67af12b4ea3d1e7da
tuned set_replicate lemmas

diff -r 059ee3176686 -r 0a1cc2675958 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jun 18 14:14:42 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jun 18 20:22:06 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)
diff -r 059ee3176686 -r 0a1cc2675958 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 18 14:14:42 2010 +0200
+++ b/src/HOL/List.thy	Fri Jun 18 20:22:06 2010 +0200
@@ -3190,6 +3190,9 @@
 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
 by auto
 
+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)
@@ -3198,9 +3201,6 @@
   "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"
 by(simp add: set_replicate_conv_if)
 
-lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
-by (simp add: set_replicate_conv_if split: split_if_asm)
-
 lemma replicate_append_same:
   "replicate i x @ [x] = x # replicate i x"
   by (induct i) simp_all
diff -r 059ee3176686 -r 0a1cc2675958 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Jun 18 14:14:42 2010 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Jun 18 20:22:06 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
 
 
diff -r 059ee3176686 -r 0a1cc2675958 src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Fri Jun 18 14:14:42 2010 +0200
+++ b/src/HOL/ex/Recdefs.thy	Fri Jun 18 20:22:06 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