# Isabelle Light
## Isabelle/Procedural style additions for [HOL Light](https://code.google.com/p/hol-light/)

### (c) Copyright Petros Papapanagiotou and Jacques Fleuriot,
Centre of Intelligent Systems and their Applications
University of Edinburgh, 2009-2017

This directory is distributed under the same license as HOL-Light (BSD-2-Clause).
- - - -

This README contains some brief information on the usage of this system.
Please refer to the paper [1] for a general description as well as the comments
in the code for details on each available function.

- - - -

### HOW TO LOAD:

loads "IsabelleLight/make.ml";;

- - - -

### LIST OF FILES:

make.ml        : HOL Light style makefile with some examples.
isalight.ml    : Main loader.
support.ml     : Support functions and various shortcuts.
new_tactics.ml : Various tactics to facilitate procedural-style users.
meta_rules.ml  : Main emulation of Isabelle's natural deduction rules and tactics.

- - - -

### BRIEF DESCRIPTION OF AVAILABLE FUNCTIONS AND TACTICS:
(refer to the comments in the files for more information)

GEN_ALL_TAC           : Eliminates all universal quantifiers.

REWRITE_ASM_TAC thl   : Rewrites assumptions. PURE_, ONCE_ and PURE_ONCE_
                        versions also available.
FULL_REWRITE_TAC thl  : Rewrites assumptions then goal.
FULL_SIMP_TAC thl     : SIMP_TAC then FULL_REWRITE_TAC.

X_MATCH_GEN_TAC tm    : X_GEN_TAC, X_CHOOSE_TAC, EXISTS_TAC with
X_MATCH_CHOOSE_TAC tm   type matching
MATCH_EXISTS_TAC tm

gen_case_tac          : Applies case_tac to leading universally quantified
                        variable in the goal.

induct_tac            : Induction with any inductive datatype.
						
- - - -

### LIST OF ISABELLE STYLE TACTICS AND RULES:
(refer to the comments in the files and the paper [1] for more information)

#### TACTICS:

simp
assumption
case_tac
subgoal_tac
cut_tac

rule
erule
drule
frule

rule_tac
erule_tac
drule_tac
frule_tac


#### RULES:

conjI
conjunct1
conjunct2
conjE
disjI1
disjI2
disjE
impI
impE
mp
iffI
iffE
allE
exI
notI
notE


#### EXTRAS:

meta_assumption mvs  : Use this for assumption matching with meta-variables.
exE                  : Use this tactic for existential elimination.
allI                 : Use this tactic for forall introduction.
meson                : Shortcut to automated procedure MESON.

erulen               : Use these to match numbered assumptions.
drulen
frulen

erulen_tac
drulen_tac
frulen_tac

- - - -

[1] Papapanagiotou, P. and Fleuriot, J.:
An Isabelle-Like Procedural Mode for HOL Light.
Logic for Programming, Artificial Intelligence, and Reasoning, #
pp 565-580, Springer (2010)