equal
deleted
inserted
replaced
71 shows "(Rep ---> option_map Abs) Some = Some" |
71 shows "(Rep ---> option_map Abs) Some = Some" |
72 apply(simp add: expand_fun_eq) |
72 apply(simp add: expand_fun_eq) |
73 apply(simp add: Quotient_abs_rep[OF q]) |
73 apply(simp add: Quotient_abs_rep[OF q]) |
74 done |
74 done |
75 |
75 |
76 lemma option_map_id[id_simps]: |
76 lemma option_map_id[id_simps]: |
77 shows "option_map id \<equiv> id" |
77 shows "option_map id = id" |
78 apply (rule eq_reflection) |
|
79 apply (auto simp add: expand_fun_eq) |
78 apply (auto simp add: expand_fun_eq) |
80 apply (case_tac x) |
79 apply (case_tac x) |
81 apply (auto) |
80 apply (auto) |
82 done |
81 done |
83 |
82 |
84 lemma option_rel_eq[id_simps]: |
83 lemma option_rel_eq[id_simps]: |
85 shows "option_rel (op =) \<equiv> (op =)" |
84 shows "option_rel (op =) = (op =)" |
86 apply(rule eq_reflection) |
|
87 apply(auto simp add: expand_fun_eq) |
85 apply(auto simp add: expand_fun_eq) |
88 apply(case_tac x) |
86 apply(case_tac x) |
89 apply(case_tac [!] xa) |
87 apply(case_tac [!] xa) |
90 apply(auto) |
88 apply(auto) |
91 done |
89 done |