SSL Inst_Ex_Assn.thy

Sprache: 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 conjunctions and
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 of witnesses.

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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.1 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.