| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Real_Asymp/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 679 B |
|
Quelle Inst_Existentials.thySprache: Isabelle |
|||||||||||||||
|
section ‹Tactic for instantiating existentials› theory Inst_Existentials imports Main begin text ‹ Coinduction proofs in Isabelle often lead to proof obligations with nested con existential quantifiers, e.g. 🍋‹∃x y. P x y ∧ (∃z. Q x y z)› . The following tactic allows instantiating these existentials with a given list › ML_file ‹inst_existentials.ML› method_setup inst_existentials = ‹ Scan.lift (Scan.repeat Parse.term) >> (fn ts => fn ctxt => SIMPLE_METHOD' (Inst_Existentials.tac ctxt (map (Syntax.read_term ctxt) ts))) › end
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-05-03) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26