Coq has tactic language Ltac with match facilities and so on. Does Isabelle/HOL have some programming language for tactics with the services for parsing, pattern matching and so on? I skimmed through Isabelle's Isar reference manual and the old Pawlson tutorial but I have found cues for that.
Does Isabelle/HOL have its tactic language?
317 Views Asked by TomR At
1
There are 1 best solutions below
Related Questions in COQ
- CoqIDE loadpath error for ssreflect
- How to assign a natural number to variable in Coq?
- Handling let in hypothesis
- Sum of exponents with same base
- How to run Athena | Coq | Isabelle codes remotely?
- Is equality decidable on any coinductive type?
- Coq "convoy pattern"
- In coq, how to do "induction n eqn: Hn" in a way that doesn't mess up the inductive hypothesis?
- Pattern matching multiple constructors in a single clause in Coq
- How to use Coq GenericMinMax to prove facts about the reals
- what does the colon greater than sign mean in coq
- Subtyping in Coq
- How to write coq definitions with "subtypes"
- Stronger completeness axiom for real numbers in Coq
- When is the first input to `list_rec` not a constant function?
Related Questions in ISABELLE
- Using type classes to overload notation for constructors (now a namespace issue)
- Existing constants (e.g. constructors) in type class instantiations
- Automated tools for applying formal methods to verify security policy in existing software
- How to use a main bib file with the Isabelle document preparation system?
- Isabelle: Unsupported recursive occurrence of a datatype via type constructor "Set.set"
- How to run Athena | Coq | Isabelle codes remotely?
- Usage of "also have...finally have" in Isabelle
- Why won't the 'linordered_field_class.frac_le' rule work? (Isabelle)
- Limit of c^n (with ¦c¦<1) is 0 (Isabelle)
- 'real_of_int' and 'real' in Isabelle?
- Is there a lemma like "∃x. a^x = b" proved in Isabelle?
- Proof by induction with three base cases (Isabelle)
- Constraining type variables in locales
- Lists and simplification rules: More difficult when using @ rather than #?
- How type casting is possible in isabelle
Related Questions in LTAC
- How to initialize empty hint database
- Interaction between type classes and auto tactic
- Coq forward reasoning: apply with multiple hypotheses
- Coq tactic for applying a concrete hypothesis to an existential goal
- Coq: Ltac for transitivity of implication (a.k.a. hypothetical syllogism)
- Tactics with variable arity
- Ltac: do something different in each goal
- Ltac: Matching goal with type that depends on name of previous goal
- Using backtracking to find value for existential in Coq
- Ltac: Matching with ltac on hypothesis which contains user defined notations
- Automatically specializing hypotheses in Coq
- Raising the failure level of a coq tactic
- Matching expression context under `forall` with Ltac
- rewrite single occurence in ltac
- Coq coercions and goal matching
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
I am not serious Isabelle/HOL user, so take it with grain of salt. There is a tactic language called Eisbach. You can see more in the paper A Proof Method Language for Isabelle. ts.data61.csiro.au/publications/nicta_full_text/8465.pdf