| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Deriving/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 936 B |
|
Quelle Generator_Aux.thySprache: Isabelle |
|||||||||||||||
|
section ‹Shared Utilities for all Generator› text ‹In this theory we mainly provide some Isabelle/ML infrastructure that is used by several generators. It consists of a uniform interface to access all the theorems, terms, etc.\ from the BNF package, and some auxiliary functions which provide recursors on datatypes, common tactics, e theory Generator_Aux imports Main begin ML_file ‹bnf_access.ML› ML_file ‹generator_aux.ML› lemma in_set_simps: "x ∈ set (y # z # ys) = (x = y ∨ x ∈ set (z # ys))" "x ∈ set ([y]) = (x = y)" "x ∈ set [] = False" "Ball (set []) P = True" "Ball (set [x]) P = P x" "Ball (set (x # y # zs)) P = (P x ∧ Ball (set (y # zs)) P)" by auto lemma conj_weak_cong: "a = b ==> c = d ==> (a ∧ c) = (b ∧ d)" by auto lemma refl_True: "(x = x) = True" by simp end
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09