equal
deleted
inserted
replaced
2405 |
2405 |
2406 lemma td_ext_nth [OF refl refl refl, unfolded word_size]: |
2406 lemma td_ext_nth [OF refl refl refl, unfolded word_size]: |
2407 "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> |
2407 "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> |
2408 td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)" |
2408 td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)" |
2409 apply (unfold word_size td_ext_def') |
2409 apply (unfold word_size td_ext_def') |
2410 apply (safe del: subset_antisym) |
2410 apply safe |
2411 apply (rule_tac [3] ext) |
2411 apply (rule_tac [3] ext) |
2412 apply (rule_tac [4] ext) |
2412 apply (rule_tac [4] ext) |
2413 apply (unfold word_size of_nth_def test_bit_bl) |
2413 apply (unfold word_size of_nth_def test_bit_bl) |
2414 apply safe |
2414 apply safe |
2415 defer |
2415 defer |