equal
deleted
inserted
replaced
48 |
48 |
49 lemma compute_fst: "fst (x,y) = x" by simp |
49 lemma compute_fst: "fst (x,y) = x" by simp |
50 lemma compute_snd: "snd (x,y) = y" by simp |
50 lemma compute_snd: "snd (x,y) = y" by simp |
51 lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto |
51 lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto |
52 |
52 |
53 lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp |
53 lemma case_prod_simp: "case_prod f (x,y) = f x y" by simp |
54 |
54 |
55 lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp |
55 lemmas compute_pair = compute_fst compute_snd compute_pair_eq case_prod_simp |
56 |
56 |
57 (*** compute_option ***) |
57 (*** compute_option ***) |
58 |
58 |
59 lemma compute_the: "the (Some x) = x" by simp |
59 lemma compute_the: "the (Some x) = x" by simp |
60 lemma compute_None_Some_eq: "(None = Some x) = False" by auto |
60 lemma compute_None_Some_eq: "(None = Some x) = False" by auto |