equal
deleted
inserted
replaced
1240 lemma inj_on_rev[iff]: "inj_on rev A" |
1240 lemma inj_on_rev[iff]: "inj_on rev A" |
1241 by(simp add:inj_on_def) |
1241 by(simp add:inj_on_def) |
1242 |
1242 |
1243 lemma rev_induct [case_names Nil snoc]: |
1243 lemma rev_induct [case_names Nil snoc]: |
1244 "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs" |
1244 "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs" |
1245 apply(subst rev_rev_ident[symmetric]) |
1245 apply(simplesubst rev_rev_ident[symmetric]) |
1246 apply(rule_tac list = "rev xs" in list.induct, simp_all) |
1246 apply(rule_tac list = "rev xs" in list.induct, simp_all) |
1247 done |
1247 done |
1248 |
1248 |
1249 lemma rev_exhaust [case_names Nil snoc]: |
1249 lemma rev_exhaust [case_names Nil snoc]: |
1250 "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P" |
1250 "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P" |