| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL M/ (Beweissystem der NASA Version 6.0.9©) Datei vom 4.1.2008 mit Größe 2 kB |
|
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.14 Sekunden (vorverarbeitet am 2026-05-03) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26