| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Myhill-Nerode/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 1 kB |
|
Quelle Folds.thySprache: Isabelle |
|||||||||||||||
|
(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *) theory Folds imports "Regular-Sets.Regular_Exp" begin section ‹``Summation'' for regular expressions› text ‹ To obtain equational system out of finite set of equivalence classes, a fold ope on finite sets ‹folds› is defined. The use of ‹SOME› makes ‹folds› more robust than the ‹fold› in the Isabelle library. The expression ‹folds f› makes sense when ‹f› is not ‹associative› and ‹commutitive›, while ‹fold f› does not. definition folds :: "('a ==> 'b ==> 'b) ==> 'b ==> 'a set ==> 'b" where "folds f z S ≡ SOME x. fold_graph f z S x" text ‹Plus-combination for a set of regular expressions› abbreviation Setalt :: "'a rexp set ==> 'a rexp" (‹⊎_› [1000] 999) where "⊎A ≡ folds Plus Zero A" text ‹ For finite sets, @{term Setalt} is preserved under @{term lang}. › lemma folds_plus_simp [simp]: fixes rs::"('a rexp) set" assumes a: "finite rs" shows "lang (⊎rs) = ∪ (lang ` rs)" unfolding folds_def apply(rule set_eqI) apply(rule someI2_ex) apply(rule_tac finite_imp_fold_graph[OF a]) apply(erule fold_graph.induct) apply(auto) done end
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09