1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
# 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)
|
