equal
deleted
inserted
replaced
14 qed "insert_map_inverse"; |
14 qed "insert_map_inverse"; |
15 |
15 |
16 Goal "(insert_map i x (delete_map i g)) = g(i:=x)"; |
16 Goal "(insert_map i x (delete_map i g)) = g(i:=x)"; |
17 by (rtac ext 1); |
17 by (rtac ext 1); |
18 by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
18 by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
19 by (cases_tac "d" 1); |
19 by (case_tac "d" 1); |
20 by (ALLGOALS Asm_simp_tac); |
20 by (ALLGOALS Asm_simp_tac); |
21 qed "insert_map_delete_map_eq"; |
21 qed "insert_map_delete_map_eq"; |
22 |
22 |
23 (*** Injectiveness proof ***) |
23 (*** Injectiveness proof ***) |
24 |
24 |