| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/BTree/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 816 B |
|
Quelle Inst_Ex_Assn.thySprache: Isabelle |
|||||||||||||||
|
section ‹Tactic for instantiating existentials› theory Inst_Ex_Assn imports Separation_Logic_Imperative_HOL.Assertions begin thm ent_ex_postI text ‹ Coinduction proofs in Isabelle often lead to proof obligations with nested conju existential quantifiers, e.g. prop‹∃x y. P x y ∧ (∃z. Q x y z)› . The following tactic allows instantiating these existentials with a given list o This tactic was adjusted to work with the assertion specific prop‹∃A› ML_file ‹inst_ex_assn.ML› method_setup inst_ex_assn = ‹ Scan.lift (Scan.repeat Parse.term) >> (fn ts => fn ctxt => SIMPLE_METHOD' (Inst_Ex_Assn.tac ctxt (map (Syntax.read_term ctxt) ts))) › end
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09