| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/GPU_Kernel_PL/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 743 B |
|
Quelle Misc.thySprache: Isabelle |
|||||||||||||||
|
section ‹General purpose definitions and lemmas› theory Misc imports Main begin text ‹A handy abbreviation when working with maps› abbreviation make_map :: "'a set ==> 'b ==> ('a ⇀ 'b)" (‹[ _ |=> _ ]›) where "[ks |=> v] ≡ λk. if k ∈ ks then Some v else None" text ‹Projecting the components of a triple› definition "fst3 ≡ fst" definition "snd3 ≡ fst ∘ snd" definition "thd3 ≡ snd ∘ snd" lemma fst3_simp [simp]: "fst3 (a,b,c) = a" by (simp add: fst3_def) lemma snd3_simp [simp]: "snd3 (a,b,c) = b" by (simp add: snd3_def) lemma thd3_simp [simp]: "thd3 (a,b,c) = c" by (simp add: thd3_def) end
¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09