src/HOL/Library/Quotient_Option.thy
 author haftmann Mon, 15 Nov 2010 14:59:21 +0100 changeset 40542 9a173a22771c parent 40464 e1db06cf6254 child 40820 fd9c98ead9a9 permissions -rw-r--r--
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
```
(*  Title:      HOL/Library/Quotient_Option.thy
Author:     Cezary Kaliszyk and Christian Urban
*)

header {* Quotient infrastructure for the option type *}

theory Quotient_Option
imports Main Quotient_Syntax
begin

fun
option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
where
"option_rel R None None = True"
| "option_rel R (Some x) None = False"
| "option_rel R None (Some x) = False"
| "option_rel R (Some x) (Some y) = R x y"

declare [[map option = (Option.map, option_rel)]]

text {* should probably be in Option.thy *}
lemma split_option_all:
shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
apply(auto)
apply(case_tac x)
apply(simp_all)
done

lemma option_quotient[quot_thm]:
assumes q: "Quotient R Abs Rep"
shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
unfolding Quotient_def
apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
using q
unfolding Quotient_def
apply(blast)
done

lemma option_equivp[quot_equiv]:
assumes a: "equivp R"
shows "equivp (option_rel R)"
apply(rule equivpI)
unfolding reflp_def symp_def transp_def
apply(blast intro: equivp_reflp[OF a])
apply(blast intro: equivp_symp[OF a])
apply(blast intro: equivp_transp[OF a])
done

lemma option_None_rsp[quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "option_rel R None None"
by simp

lemma option_Some_rsp[quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "(R ===> option_rel R) Some Some"
by auto

lemma option_None_prs[quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "Option.map Abs None = None"
by simp

lemma option_Some_prs[quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "(Rep ---> Option.map Abs) Some = Some"