Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quelle Quotient_Option.thy Sprache: 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

quality93%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.