equal
deleted
inserted
replaced
358 thus ?thesis |
358 thus ?thesis |
359 proof (cases n) |
359 proof (cases n) |
360 case 0 note b = this |
360 case 0 note b = this |
361 show ?thesis |
361 show ?thesis |
362 proof (cases ys) |
362 proof (cases ys) |
363 case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3) |
363 case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3) |
364 next |
364 next |
365 case (Cons y ys) |
365 case (Cons y ys) |
366 show ?thesis |
366 show ?thesis |
367 proof (cases j) |
367 proof (cases j) |
368 case 0 with a b Cons.prems show ?thesis by simp |
368 case 0 with a b Cons.prems show ?thesis by simp |
369 next |
369 next |
370 case (Suc j') with a b Cons.prems Cons show ?thesis |
370 case (Suc j') with a b Cons.prems Cons show ?thesis |
371 apply - |
371 apply - |
372 apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto) |
372 apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto) |
373 done |
373 done |
374 qed |
374 qed |
375 qed |
375 qed |
376 next |
376 next |
377 case (Suc n') |
377 case (Suc n') |
378 show ?thesis |
378 show ?thesis |
379 proof (cases ys) |
379 proof (cases ys) |
380 case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3) |
380 case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3) |
381 next |
381 next |
382 case (Cons y ys) with Suc a Cons.prems show ?thesis |
382 case (Cons y ys) with Suc a Cons.prems show ?thesis |
383 apply - |
383 apply - |
384 apply simp |
384 apply simp |
385 apply (cases j) |
385 apply (cases j) |
386 apply simp |
386 apply simp |
387 apply (cases i) |
387 apply (cases i) |
388 apply simp |
388 apply simp |
389 apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"]) |
389 apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"]) |
390 apply simp |
390 apply simp |
391 apply simp |
391 apply simp |
392 apply simp |
392 apply simp |
393 apply simp |
393 apply simp |
394 apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"]) |
394 apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"]) |
395 apply simp |
395 apply simp |
396 apply simp |
396 apply simp |
397 apply simp |
397 apply simp |
398 done |
398 done |
399 qed |
399 qed |
400 qed |
400 qed |
401 qed |
401 qed |
402 qed |
402 qed |
403 |
403 |