equal
deleted
inserted
replaced
70 proof - |
70 proof - |
71 fix xs |
71 fix xs |
72 fix n |
72 fix n |
73 assume "n < length xs" |
73 assume "n < length xs" |
74 then show "pick (map (Pair 1) xs) n = nth xs n" |
74 then show "pick (map (Pair 1) xs) n = nth xs n" |
75 proof (induct xs fixing: n) |
75 proof (induct xs arbitrary: n) |
76 case Nil then show ?case by simp |
76 case Nil then show ?case by simp |
77 next |
77 next |
78 case (Cons x xs) show ?case |
78 case (Cons x xs) show ?case |
79 proof (cases n) |
79 proof (cases n) |
80 case 0 then show ?thesis by simp |
80 case 0 then show ?thesis by simp |