src/HOL/List.thy
changeset 46439 2388be11cb50
parent 46424 b447318e5e1a
child 46440 d4994e2e7364
equal deleted inserted replaced
46438:93344b60cb30 46439:2388be11cb50
   932 by (cases xs) auto
   932 by (cases xs) auto
   933 
   933 
   934 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
   934 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
   935 by (cases xs) auto
   935 by (cases xs) auto
   936 
   936 
   937 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
   937 lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
   938 apply (induct xs arbitrary: ys, force)
   938 apply (induct xs arbitrary: ys, force)
   939 apply (case_tac ys, simp, force)
   939 apply (case_tac ys, simp, force)
   940 done
   940 done
   941 
   941 
   942 lemma inj_on_rev[iff]: "inj_on rev A"
   942 lemma inj_on_rev[iff]: "inj_on rev A"