equal
deleted
inserted
replaced
40 qed |
40 qed |
41 |
41 |
42 lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)" |
42 lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)" |
43 using Nat.gr0_conv_Suc |
43 using Nat.gr0_conv_Suc |
44 by clarsimp |
44 by clarsimp |
45 |
|
46 lemma filter_length: "length (List.filter P xs) < Suc (length xs)" |
|
47 apply (induct xs, auto) done |
|
48 |
45 |
49 |
46 |
50 (*********************************************************************************) |
47 (*********************************************************************************) |
51 (**** SHADOW SYNTAX AND SEMANTICS ****) |
48 (**** SHADOW SYNTAX AND SEMANTICS ****) |
52 (*********************************************************************************) |
49 (*********************************************************************************) |