Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Quotient_Option.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Quotient_Option.thy
    Author:     Cezary Kaliszyk and Christian Urban
*)

section \<open>Quotient infrastructure for the option type\<close>

theory Quotient_Option
imports Quotient_Syntax
begin

subsection \<open>Rules for the Quotient package\<close>

lemma rel_option_map1:
  "rel_option R (map_option f x) y \ rel_option (\x. R (f x)) x y"
  by (simp add: rel_option_iff split: option.split)

lemma rel_option_map2:
  "rel_option R x (map_option f y) \ rel_option (\x y. R x (f y)) x y"
  by (simp add: rel_option_iff split: option.split)

declare
  map_option.id [id_simps]
  option.rel_eq [id_simps]

lemma reflp_rel_option:
  "reflp R \ reflp (rel_option R)"
  unfolding reflp_def split_option_all by simp

lemma option_symp:
  "symp R \ symp (rel_option R)"
  unfolding symp_def split_option_all
  by (simp only: option.rel_inject option.rel_distinct) fast

lemma option_transp:
  "transp R \ transp (rel_option R)"
  unfolding transp_def split_option_all
  by (simp only: option.rel_inject option.rel_distinct) fast

lemma option_equivp [quot_equiv]:
  "equivp R \ equivp (rel_option R)"
  by (blast intro: equivpI reflp_rel_option option_symp option_transp elim: equivpE)

lemma option_quotient [quot_thm]:
  assumes "Quotient3 R Abs Rep"
  shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
  apply (rule Quotient3I)
  apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] option.rel_eq rel_option_map1 rel_option_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
  using Quotient3_rel [OF assms]
  apply (simp add: rel_option_iff split: option.split)
  done

declare [[mapQ3 option = (rel_option, option_quotient)]]

lemma option_None_rsp [quot_respect]:
  assumes q: "Quotient3 R Abs Rep"
  shows "rel_option R None None"
  by (rule option.ctr_transfer(1))

lemma option_Some_rsp [quot_respect]:
  assumes q: "Quotient3 R Abs Rep"
  shows "(R ===> rel_option R) Some Some"
  by (rule option.ctr_transfer(2))

lemma option_None_prs [quot_preserve]:
  assumes q: "Quotient3 R Abs Rep"
  shows "map_option Abs None = None"
  by (rule Option.option.map(1))

lemma option_Some_prs [quot_preserve]:
  assumes q: "Quotient3 R Abs Rep"
  shows "(Rep ---> map_option Abs) Some = Some"
  apply(simp add: fun_eq_iff)
  apply(simp add: Quotient3_abs_rep[OF q])
  done

end

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.