Language for the Hets command line interface

SCRIPT ::= COMMAND*

COMMAND ::=

-- commands for development graph mode

use PATH -- open a file with a HetCASL library

-- this will compute a development graph

-- and a list of open proof obligations

-- also all referenced libraries need to be loaded

-- (and this needs to be communicated to PGIP)

| dg DG-COMMAND GOAL* -- apply a proof step of the dg calculus

-- if no goal is specified, all goals are tried

| show -- display list of open dg goals

-- commands for theory mode

| show -- display list of theory goals

| show-theory -- show current theory and proof goals

| translate COMORPHISM -- translate theory goals along comorphism

| prover PROVER -- select a prover

| proof-script FORMULA PROOF-SCRIPT end-script

-- process proof script for one goal

| prove FORMULA*

| prove FORMULA* axioms FORMULA+

-- insert initial proof script

-- insert only the specified formulas as goals (top goal if none is specified)

-- insert only the specified axioms

| prove-all FORMULA*

| prove-all FORMULA* axioms FORMULA+

-- same for all goals

PROOF-SCRIPT -- can be anything (prover specific)

-- the end is recognized with "end-script"

DG-COMMAND ::= auto -- automatic tactic

| glob-subsume -- global subsumption

| glob-decomp -- global decomposition

| loc-infer -- local inference

| loc-decomp -- local decomposition

| comp -- composition

| comp-new -- composition with speculation of new egdes

| hide-thm -- Hide-Theorem-Shift

| thm-hide -- Theorem-Hide-Shift

| basic -- prove at a particular node,

-- i.e. start local proving in a theory

GOAL ::= NODE -- select local goals at a node

| NODE -> NODE -- select all edges between two given nodes

| NODE - DIGIT* -> NODE -- select specific edge between two nodes

NODE ::= ID -- specify nodes with their names

COMORPHISM ::= ID ; ... ; ID -- composite of basic comorphisms

PROVER ::= ID -- name of prover

FORMULA ::= ID -- label of formula