| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Call_Arity/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 925 B |
|
Quelle ConstOn.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
theory ConstOn imports Main begin definition const_on :: "('a → 'b) → 'a set → 'b → bool" where "const_on f S x = (∀ y ∈ S . f y = x)" lemma const_onI[intro]: "(∧y. y ∈ S ==> f y = x) ==> const_on f S x" by (simp add: const_on_def) lemma const_onD[dest]: "const_on f S x ==> y ∈ S ==> f y = x" by (simp add: const_on_def) (* lemma const_onE[elim]: "const_on f S r ==> x : S ==> r = r' ==> f x = r'" *) lemma const_on_insert[simp]: "const_on f (insert x S) y ⟷ const_on f S y ∧ f x = y by auto lemma const_on_union[simp]: "const_on f (S ∪ S') y ⟷ const_on f S y ∧ const_on f S by auto lemma const_on_subset[elim]: "const_on f S y ==> S' ⊆ S ==> const_on f S' y" by auto end
¤ Dauer der Verarbeitung: 0.2 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01