[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 23f7895 05/13: Remove Hol-Light support
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general 23f7895 05/13: Remove Hol-Light support |
|
Date: |
Thu, 25 Nov 2021 10:57:58 -0500 (EST) |
branch: elpa/proof-general
commit 23f789544ae93c08dafc53aeb9e340c9d1baebd6
Author: Stefan Monnier <monnier@iro.umontreal.ca>
Commit: Stefan Monnier <monnier@iro.umontreal.ca>
Remove Hol-Light support
---
Makefile | 2 +-
README.md | 4 +-
doc/ProofGeneral.texi | 49 +--
etc/hol-light/example4.ml | 13 -
generic/proof-site.el | 4 -
hol-light/LICENSE-HOL-LIGHT | 29 --
hol-light/README | 45 ---
hol-light/TODO | 17 -
hol-light/TacticRecording/INSTRUCTIONS | 36 --
hol-light/TacticRecording/LIMITATIONS | 18 -
hol-light/TacticRecording/biolayout.ml | 30 --
hol-light/TacticRecording/dltree.ml | 268 -------------
hol-light/TacticRecording/dltree.mli | 22 --
hol-light/TacticRecording/ex.dot | 24 --
hol-light/TacticRecording/ex2.dot | 13 -
hol-light/TacticRecording/ex3.dot | 24 --
hol-light/TacticRecording/ex3.png | Bin 39644 -> 0 bytes
hol-light/TacticRecording/ex3b.dot | 37 --
hol-light/TacticRecording/examples1.ml | 64 ---
hol-light/TacticRecording/examples1_output.txt | 72 ----
hol-light/TacticRecording/examples2.ml | 45 ---
hol-light/TacticRecording/examples3.ml | 236 -----------
hol-light/TacticRecording/examples3_LEMMA1.dot | 24 --
hol-light/TacticRecording/examples3_output.txt | 36 --
hol-light/TacticRecording/examples4.ml | 13 -
hol-light/TacticRecording/examples5.ml | 182 ---------
hol-light/TacticRecording/gvexport.ml | 47 ---
hol-light/TacticRecording/hiproofs.ml | 417 --------------------
hol-light/TacticRecording/lib.ml | 91 -----
hol-light/TacticRecording/main.ml | 31 --
hol-light/TacticRecording/mldata.ml | 33 --
hol-light/TacticRecording/mlexport.ml | 186 ---------
hol-light/TacticRecording/printutils.ml | 61 ---
hol-light/TacticRecording/promote.ml | 327 ----------------
hol-light/TacticRecording/prooftree.ml | 177 ---------
hol-light/TacticRecording/tacticrec.ml | 383 ------------------
hol-light/TacticRecording/wrappers.ml | 359 -----------------
hol-light/TacticRecording/xtactics.ml | 451 ---------------------
hol-light/TacticRecording/xthm.ml | 40 --
hol-light/example.ml | 19 -
hol-light/hol-light-autotest.el | 42 --
hol-light/hol-light-unicode-tokens.el | 252 ------------
hol-light/hol-light.el | 519 -------------------------
hol-light/pg_prompt.ml | 59 ---
hol-light/pg_tactics.ml | 349 -----------------
hol-light/temp-prooftree-configure.patch | 25 --
46 files changed, 4 insertions(+), 5171 deletions(-)
diff --git a/Makefile b/Makefile
index 912d246..f23ff28 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ PREFIX=$(DESTDIR)/usr
DEST_PREFIX=$(DESTDIR)/usr
# subdirectories for provers: to be compiled and installed
-PROVERS=acl2 coq easycrypt hol-light isar pghaskell pgocaml pgshell phox
+PROVERS=acl2 coq easycrypt isar pghaskell pgocaml pgshell phox
# generic lisp code: to be compiled and installed
OTHER_ELISP=generic lib
diff --git a/README.md b/README.md
index a4a4422..d10078a 100644
--- a/README.md
+++ b/README.md
@@ -140,9 +140,9 @@ instances are no longer maintained nor available in the
MELPA package:
* Legacy support of
[Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/)
-* Experimental support of: ACL2, Hol-Light, Lambda-Clam, Shell
+* Experimental support of: ACL2, Lambda-Clam, Shell
* Obsolete instances: Demoisa, Lambda-Clam, Plastic
-* Removed instances: Twelf, CCC, HOL98,
+* Removed instances: Twelf, CCC, Hol-Light, HOL98,
[LEGO](http://www.dcs.ed.ac.uk/home/lego)
A few example proofs are included in each prover subdirectory.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 48468b1..4a31443 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -160,7 +160,6 @@ assistants Coq, EasyCrypt, and PhoX.
* Hints and Tips::
* Coq Proof General::
* Isabelle Proof General::
-* HOL Light Proof General::
* EasyCrypt Proof General::
* Shell Proof General::
@c * PhoX Proof General::
@@ -208,7 +207,7 @@ other documentation, system downloads, etc.
@cindex news
The old code for the support of the following systems have been
-removed: Twelf, CCC, Lego, HOL98.
+removed: Twelf, CCC, Lego, Hol-Light, HOL98.
@node News for Version 4.4
@unnumberedsec News for Version 4.4
@@ -517,7 +516,6 @@ script file for your proof assistant, for example:
@item Coq @tab @file{.v} @tab @code{coq-mode}
@item Isabelle @tab @file{.thy} @tab @code{isar-mode}
@item Phox @tab @file{.phx} @tab @code{phox-mode}
-@item HOL Light @tab @file{.ml} @tab @code{hol-light-mode}
@item ACL2 @tab @file{.acl2} @tab @code{acl2-mode}
@item Plastic @tab @file{.lf} @tab @code{plastic-mode}
@item Lambda-CLAM @tab @file{.lcm} @tab @code{lclam-mode}
@@ -672,9 +670,6 @@ Isabelle for more details.
@c @b{PhoX Proof General} for PhoX 0.8X@*
@c @xref{PhoX Proof General}, for more details.
@item
-@b{HOL Light Proof General} for HOL Light@*
-@xref{HOL Light Proof General}, for more details.
-@item
@b{EasyCrypt Proof General} for EasyCrypt@*
@xref{EasyCrypt Proof General}, for mode details.
@item
@@ -5608,48 +5603,6 @@ URL of web page for Isabelle.
@c =================================================================
@c
-@c CHAPTER: HOL Light Proof General
-@c
-@node HOL Light Proof General
-@chapter HOL Light Proof General
-@cindex HOL Light Proof General
-
-HOL Light Proof General is a "technology demonstration" of Proof General
-for HOL Light. This means that only a basic instantiation has been
-provided, and that it is not yet supported as a maintained instantiation
-of Proof General.
-
-HOL Light Proof General has basic script management support, with a
-little bit of decoration of scripts and output. It does not rely on a
-modified version of HOL Light, so the pattern matching may be fragile in
-certain cases.
-
-@c Support for multiple files deduces dependencies
-@c automatically, so there is no interaction with the HOL make system yet.
-
-See the @file{example.ml} file for a demonstration proof script
-which works with Proof General.
-
-Note that HOL Light Proof Script proof scripts often use batch-oriented
-single step tactic proofs, but Proof General does not (yet) offer an
-easy way to edit these kind of proofs. They will replay simply as a
-single step proof and you will need to convert from the interactive to
-batch form as usual if you wish to obtain batch proofs. Also note that
-Proof General does not contain an SML parser, so there can be problems
-if you write complex ML in proof scripts.
-@c Old section was helpful on this: @xref{ML files}, for the same issue with
Isabelle.
-
-HOL Light is the most recently tested version of HOL with Proof General,
-but the Proof General distribution also contains experimental support
-for HOL 4 (aka HOL 98). To improve this older version, or to support a
-new HOL variant, a few of the settings probably need to be tweaked to
-cope with small differences in output between the systems. Please let
-us know if you try this out and want help. We welcome any interested
-collaborators from the HOL communities to help improve Proof General as
-an interface for HOL provers.
-
-@c =================================================================
-@c
@c CHAPTER: EasyCrypt Proof General
@c
@node EasyCrypt Proof General
diff --git a/etc/hol-light/example4.ml b/etc/hol-light/example4.ml
deleted file mode 100644
index 3178f65..0000000
--- a/etc/hol-light/example4.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-pg_mode_on ();;
-get_pg_mode ();;
-
-g `(?x:num. p(x) /\ q(x) /\ r(x)) ==> (?x. r(x) /\ p(x)) /\ (?x. p(x) /\ (q(x)
<=> r(x)))`;;
-e (STRIP_TAC);;
-e (STRIP_TAC);;
-e (X_META_EXISTS_TAC `n1:num` THEN CONJ_TAC);;
-e (FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n1:num`]));;
-e (ASM_REWRITE_TAC[]);;
-e (X_META_EXISTS_TAC `n2:num` THEN CONJ_TAC);;
-e (FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n2:num`]));;
-e (ASM_REWRITE_TAC[]);;
-let th = top_thm ();;
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 59e3c84..d2c282f 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -49,10 +49,6 @@
(easycrypt "EasyCrypt" "ec" "\\.eca?\\'")
(phox "PhoX" "phx" nil (".phi" ".pho"))
- ;; Obscure instances or conflict with other Emacs modes.
-
- ;; (hol-light "HOL Light" "ml") ; [for testing]
-
;; Cut-and-paste management only
(pgshell "PG-Shell" "pgsh")
diff --git a/hol-light/LICENSE-HOL-LIGHT b/hol-light/LICENSE-HOL-LIGHT
deleted file mode 100644
index f192eff..0000000
--- a/hol-light/LICENSE-HOL-LIGHT
+++ /dev/null
@@ -1,29 +0,0 @@
- HOL Light copyright notice, licence and disclaimer
-
- (c) University of Cambridge 1998
- (c) Copyright, John Harrison 1998-2008
-
-HOL Light version 2.20, hereinafter referred to as "the software", is a
-computer theorem proving system written by John Harrison. Much of the
-software was developed at the University of Cambridge Computer Laboratory,
-New Museums Site, Pembroke Street, Cambridge, CB2 3QG, England. The
-software is copyright, University of Cambridge 1998 and John Harrison
-1998-2007.
-
-Permission to use, copy, modify, and distribute the software and its
-documentation for any purpose and without fee is hereby granted. In the
-case of further distribution of the software the present text, including
-copyright notice, licence and disclaimer of warranty, must be included in
-full and unmodified form in any release. Distribution of derivative
-software obtained by modifying the software, or incorporating it into
-other software, is permitted, provided the inclusion of the software is
-acknowledged and that any changes made to the software are clearly
-documented.
-
-John Harrison and the University of Cambridge disclaim all warranties
-with regard to the software, including all implied warranties of
-merchantability and fitness. In no event shall John Harrison or the
-University of Cambridge be liable for any special, indirect,
-incidental or consequential damages or any damages whatsoever,
-including, but not limited to, those arising from computer failure or
-malfunction, work stoppage, loss of profit or loss of contracts.
diff --git a/hol-light/README b/hol-light/README
deleted file mode 100644
index 238586c..0000000
--- a/hol-light/README
+++ /dev/null
@@ -1,45 +0,0 @@
-HOL Light in Proof General.
-
-Written by David Aspinall and Mark Adams.
-
-Status: not officially supported yet
-Maintainer: volunteer required
-HOL-Light version: SVN trunk (a moving target 8-) - tested on 118)
-HOL homepage: https://www.cl.cam.ac.uk/~jrh13/hol-light/
-
-========================================
-
-
-This is a "technology demonstration" of Proof General for HOL-Light.
-
-We have written this in the hope that somebody from the HOL-Light
-community will adopt it, maintain and improve it, and thus turn it
-into a proper instantiation of Proof General.
-
-
-------------
-
-Notes:
-
-There are some problems at the moment. HOL proof scripts often use
-batch-oriented single step tactic proofs, but Proof General does not
-offer an easy way to edit these kind of proofs. The "Boomburg-HOL"
-Emacs interface by Koichi Takahashi and Masima Hagiya addressed this a
-long time ago, and to some extent so perhaps does the Emacs interface
-supplied with HOL. Perhaps one of these could be
-embedded/reimplemented inside Proof General. Implemented in a generic
-way, managing batch vs interactive proofs might also be useful for
-other provers.
-
-Another problem is that HOL scripts sometimes use OCaml modules, which
-will cause confusion because Proof General does not really parse OCaml,
-it just looks for semicolons. This could be improved by taking a
-better parser (perhaps from the OCaml mode for Emacs).
-
-These improvements would be worthwhile contributions to Proof General
-and also provide the HOL community with a nice front end.
-Please have a go!
-
-
-$Id$
-
diff --git a/hol-light/TODO b/hol-light/TODO
deleted file mode 100644
index 61efb54..0000000
--- a/hol-light/TODO
+++ /dev/null
@@ -1,17 +0,0 @@
-* Prooftree support: fix problem with successive proofs
- (try example.ml with tree turned on, gives exn in Prooftree)
- [da to investigate]
-
-* Prooftree: fix evar support so it works
- Need patch for proof tree program and (maybe) modification of
- output
- [ma to do]
-
-* PG: add patch for background startup (needs testing)
- [da to do]
-
-* Integrate Tactic recording/proof refactoring (e.g. menu commands,
- also load point: if it is to work from Proof General, make it
- work from here, otherwise distribute it separately)
- [ma to do]
-
diff --git a/hol-light/TacticRecording/INSTRUCTIONS
b/hol-light/TacticRecording/INSTRUCTIONS
deleted file mode 100644
index 86380b9..0000000
--- a/hol-light/TacticRecording/INSTRUCTIONS
+++ /dev/null
@@ -1,36 +0,0 @@
-To use this:
-1. first compile HOL Light and any extra files up to the particular proof you
want to record;
- #use "hol.ml";;
- #use ....
-
-2. Then process the 'main.ml' file
- #use "TacticRecording/main.ml";;
-
-3. Then perform the tactic proof you want to record, using g/e's or prove:
- g `...`;;
- e (...);;
- e (...);;
- OR
- prove (`...`, ... THEN ... THENL [...]);;
-
-4. Use the ML export commands to output the proof in the form you want:
-
- print_executed_proof ();;
- - Tries to reproduce the inputted proof verbatim, with steps
- corresponding one-to-one to original.
-
- print_flat_proof ();;
- - Prints the proof as a flatten series single-tactic steps, with no
- tacticals.
-
- print_thenl_proof ();;
- - Prints the proof as a single-step tactic, connected by THEN for
- single goals and THENL for multiple goals. This structure directly
- reflects the tree structure of the proof as it was executed.
-
- print_optimal_proof ();;
- - Like 'print_thenl_proof', but prints a more concise proof, not
- necessarily reflecting the original tree structure. Currently this
- only performs one improvement: seeing where THENL can be replaced
- with THEN.
-
diff --git a/hol-light/TacticRecording/LIMITATIONS
b/hol-light/TacticRecording/LIMITATIONS
deleted file mode 100644
index 56537d4..0000000
--- a/hol-light/TacticRecording/LIMITATIONS
+++ /dev/null
@@ -1,18 +0,0 @@
-ML objects that get recorded need to be promoted
-- and the promoted subgoal package commands don't work for unpromoted ML
objects
-- implementor needs to write promotion functions for each type shape
-- implementor needs to apply these promotion functions to lots of tactics/thms
-- user needs to promote their own stuff, e.g. their own rules/thms
-
-Tactic proofs with embedded arbitrary ML are problematic
-- sometimes this can still get recorded, and if so then exported ML will work
-- but exported ML is unlikely to faithfully reproduce original ML text
-
-Limitations in HOL Light's pretty printer for HOL terms
-- it outputs ambiguous expressions without type annotations
-- this is used by my ML exporter
-
-However, in practice the appraoch works well
-- the same old pool of 100 tactics, 100 rules, 1000 theorems get used
-- and any promotion that needs doing is easy anyway
-- hand tweaks are occasionally required for aribitrary ML and type annotations
diff --git a/hol-light/TacticRecording/biolayout.ml
b/hol-light/TacticRecording/biolayout.ml
deleted file mode 100644
index 0de3119..0000000
--- a/hol-light/TacticRecording/biolayout.ml
+++ /dev/null
@@ -1,30 +0,0 @@
-(* ==========================================================================
*)
-(* BIOLAYOUT EXPORT (HOL LIGHT)
*)
-(* - Support for BioLayout graph display of recorded tactics
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2012
*)
-(* ==========================================================================
*)
-
-
-(* biolayout_nodename *)
-
-let biolayout_nodename n =
- "Node" ^ string_of_int n;;
-
-
-(* biolayout_export *)
-
-let biolayout_export path name =
- let nns = gtree_graph () in
- let suffix = ".layout" in
- let fullname = Filename.concat path (name ^ suffix) in
- let ch = open_out fullname in
- let export_line ch (n1,n2) =
- (output_string ch (biolayout_nodename n1);
- output_string ch "\t";
- output_string ch (biolayout_nodename n2);
- output_string ch "\n") in
- (print_string ("Exporting to file \"" ^ fullname ^ "\"\n");
- do_list (export_line ch) nns;
- close_out ch);;
diff --git a/hol-light/TacticRecording/dltree.ml
b/hol-light/TacticRecording/dltree.ml
deleted file mode 100644
index e97ecd0..0000000
--- a/hol-light/TacticRecording/dltree.ml
+++ /dev/null
@@ -1,268 +0,0 @@
-(* ==========================================================================
*)
-(* DYNAMIC LOOKUP TREES (HOL Zero)
*)
-(* - Library support for data storage in dynamic indexed binary trees
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Proof Technologies Ltd, 2008-2011
*)
-(* ==========================================================================
*)
-
-
-module Dltree : Dltree_sig = struct
-
-
-(* This module provides library support for operations on dynamic lookup
*)
-(* trees - self-balancing binary trees that store information on nodes
*)
-(* ordered according to an index under '(<)'-comparison.
*)
-
-(* This is implemented as Andersson trees (also called AA trees), that stay
*)
-(* balanced within a factor of 2 - i.e. the maximum distance from root to
*)
-(* leaf is no more than twice the minimum distance. This has a fairly simple
*)
-(* implementation and yet is one of the most efficient forms of self-
*)
-(* balancing trees.
*)
-
-
-(* dltree datatype *)
-
-(* The 'dltree' datatype is a binary lookup tree datatype, where an index and
*)
-(* item are held at each node, and leaves hold no information. Comparison
*)
-(* between indexes is done using the polymorphic '(<)' total order relation.
*)
-
-(* An integer is also held at each node and is used to keep the tree balanced
*)
-(* as items are inserted/removed. This integer represents the distance from
*)
-(* the node to the left-most leaf descendant of the node. Thus every left-
*)
-(* branch node holds a value 1 less than its parent, and a node with a leaf
*)
-(* as its left branch holds value 1. Every right-branch holds an integer
*)
-(* either equal to its parent's or 1 less, and must be strictly less than its
*)
-(* grandparent's. Thus the integer at a node also represents an upper bound
*)
-(* of half the distance from the node to its rightmost leaf descendant, and
*)
-(* thus an upper bound of half the distance from the node to any descendant.
*)
-
-(* The tree is kept balanced by adjusting nodes' integers and left and right
*)
-(* branches as the tree is updated. This is done by the 'skew' and 'split'
*)
-(* operations. The number of nodes that need to be considered in this
*)
-(* process is at most O(log n). Note that reference types are used for a
*)
-(* node's branches, to save on unnecessary garbage collection that would
*)
-(* otherwise result in rebuilding all ancestor nodes of all adjusted nodes
*)
-(* each time a tree is updated.
*)
-
-type ('a,'b) dltree0 =
- Node of (int * ('a * 'b) * ('a,'b) dltree * ('a,'b) dltree)
- | Leaf
-
-and ('a,'b) dltree = ('a,'b) dltree0 ref;;
-
-
-(* dltree_empty : unit -> ('a,'b) dltree
*)
-(*
*)
-(* Returns a fresh empty dltree.
*)
-
-let dltree_empty () = ref Leaf;;
-
-
-(* dltree_reempty : ('a,'b) dltree -> unit
*)
-(*
*)
-(* Empties a given dltree.
*)
-
-let dltree_reempty tr = (tr := Leaf);;
-
-
-(* dltree_elems : ('a,'b) dltree -> ('a * 'b) list
*)
-(*
*)
-(* This converts the information held in a given lookup tree into an index-
*)
-(* ordered association list.
*)
-
-let rec dltree_elems0 tr0 xys0 =
- match !tr0 with
- Node (_,xy0,tr1,tr2) -> dltree_elems0 tr1 (xy0::(dltree_elems0 tr2 xys0))
- | Leaf -> xys0;;
-
-let dltree_elems tr = dltree_elems0 tr [];;
-
-
-(* Node destructors *)
-
-let dest_node tr0 =
- match !tr0 with
- Node info -> info
- | Leaf -> failwith "dest_node: ?";;
-
-let level tr0 =
- match !tr0 with
- Node (l,_,_,_) -> l
- | Leaf -> 0;;
-
-let left_branch tr0 =
- match !tr0 with
- Node (_,_,tr1,_) -> tr1
- | Leaf -> failwith "left_branch: No left branch";;
-
-let right_branch tr0 =
- match !tr0 with
- Node (_,_,_,tr2) -> tr2
- | Leaf -> failwith "right_branch: No right branch";;
-
-let rec leftmost_elem x tr0 =
- match !tr0 with
- Node (_,x0,tr1,_) -> leftmost_elem x0 tr1
- | Leaf -> x;;
-
-let rec rightmost_elem x tr0 =
- match !tr0 with
- Node (_,x0,_,tr2) -> rightmost_elem x0 tr2
- | Leaf -> x;;
-
-
-(* Tests *)
-
-let is_leaf tr0 =
- match !tr0 with
- Leaf -> true
- | _ -> false;;
-
-let is_node tr0 =
- match !tr0 with
- Node _ -> true
- | _ -> false;;
-
-
-(* skew *)
-
-let skew tr0 =
- if (is_leaf tr0) or (is_leaf (left_branch tr0))
- then ()
- else if (level (left_branch tr0) = level tr0)
- then let (l0,xy0,tr1,tr2) = dest_node tr0 in
- let (l1,xy1,tr11,tr12) = dest_node tr1 in
- (tr0 := Node (l1, xy1, tr11, ref (Node (l0,xy0,tr12,tr2))))
- else ();;
-
-
-(* split *)
-
-let split tr0 =
- if (is_leaf tr0) or (is_leaf (right_branch tr0))
- then ()
- else if (level (right_branch (right_branch tr0)) = level tr0)
- then let (l0,xy0,tr1,tr2) = dest_node tr0 in
- let (l2,xy2,tr21,tr22) = dest_node tr2 in
- (tr0 := Node (l2 + 1, xy2, ref (Node (l0,xy0,tr1,tr21)), tr22))
- else ();;
-
-
-(* dltree_insert : 'a * 'b -> ('a,'b) dltree -> unit
*)
-(*
*)
-(* This inserts the supplied single indexed item into a given lookup tree.
*)
-(* Fails if the tree already contains an entry for the supplied index.
*)
-
-let rec dltree_insert ((x,_) as xy) tr0 =
- match !tr0 with
- Node (_,(x0,_),tr1,tr2)
- -> ((if (x < x0)
- then (* Put into left branch *)
- dltree_insert xy tr1
- else if (x0 < x)
- then (* Put into right branch *)
- dltree_insert xy tr2
- else (* Element already in tree *)
- failwith "dltree_insert: Already in tree");
- (* Rebalance from the node *)
- skew tr0;
- split tr0)
- | Leaf
- -> (* Put element here *)
- (tr0 := Node (1, xy, ref Leaf, ref Leaf));;
-
-
-(* dltree_remove : 'a -> ('a,'b) dltree -> unit
*)
-(*
*)
-(* This removes the entry at the supplied index in a given lookup tree.
*)
-(* Fails if the tree does not contain an entry for the supplied index.
*)
-
-let decrease_level tr0 =
- let (l0,xy0,tr1,tr2) = dest_node tr0 in
- let n = 1 + min (level tr1) (level tr2) in
- if (n < l0) && (is_node tr2)
- then (tr0 := Node (n,xy0,tr1,tr2);
- if (is_node tr2)
- then let (l2,xy2,tr21,tr22) = dest_node tr2 in
- if (n < level tr2)
- then (tr2 := Node (n,xy2,tr21,tr22))
- else ()
- else ())
- else ();;
-
-let rec dltree_remove x tr0 =
- match !tr0 with
- Node (l0,((x0,_) as xy0),tr1,tr2)
- -> ((if (x < x0)
- then (* Element should be in left branch *)
- dltree_remove x tr1
- else if (x0 < x)
- then (* Element should be in right branch *)
- dltree_remove x tr2
- else (* Node holds element to be removed *)
- if (is_leaf tr1) && (is_leaf tr2)
- then (tr0 := Leaf)
- else if (is_leaf tr1)
- then let (x2,_) as xy2 = leftmost_elem xy0 tr2 in
- (dltree_remove x2 tr2;
- tr0 := Node (l0,xy2,tr1,tr2))
- else let (x1,_) as xy1 = rightmost_elem xy0 tr1 in
- (dltree_remove x1 tr1;
- tr0 := Node (l0,xy1,tr1,tr2)));
- (if (is_node tr0)
- then (decrease_level tr0;
- skew tr0;
- skew tr2;
- (if (is_node tr2) then skew (right_branch tr2)
- else ());
- split tr0;
- split tr2)
- else ()))
- | Leaf
- -> (* Element not in tree *)
- failwith "dltree_remove: Not in tree";;
-
-
-(* dltree_elem : 'a -> ('a,'b) dltree -> 'a * 'b
*)
-(*
*)
-(* This returns the index and item held at the supplied index in a given
*)
-(* lookup tree. Fails if the tree has no entry for the supplied index.
*)
-
-let rec dltree_elem x0 tr =
- match !tr with
- Node (_, ((x,_) as xy), tr1, tr2)
- -> if (x0 < x)
- then dltree_elem x0 tr1
- else if (x < x0)
- then dltree_elem x0 tr2
- else xy
- | Leaf -> failwith "dltree_elem: Not in tree";;
-
-
-(* dltree_lookup : 'a -> ('a,'b) dltree -> 'b
*)
-(*
*)
-(* This returns the item held at the supplied index in a given lookup tree.
*)
-
-let rec dltree_lookup x0 tr =
- let (_,y) = try dltree_elem x0 tr
- with Failure _ -> failwith "dltree_lookup: Not in tree" in
- y;;
-
-
-(* dltree_mem : 'a -> ('a,'b) dltree -> bool
*)
-(*
*)
-(* This returns "true" iff the supplied index occurs in a given lookup tree.
*)
-
-let rec dltree_mem x0 tr =
- match !tr with
- Node (_,(x,_),tr1,tr2)
- -> if (x0 < x)
- then dltree_mem x0 tr1
- else if (x < x0)
- then dltree_mem x0 tr2
- else true
- | Leaf -> false;;
-
-
-end;;
diff --git a/hol-light/TacticRecording/dltree.mli
b/hol-light/TacticRecording/dltree.mli
deleted file mode 100644
index 2f57049..0000000
--- a/hol-light/TacticRecording/dltree.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(* ==========================================================================
*)
-(* DYNAMIC LOOKUP TREES (HOL Zero)
*)
-(* - Library support for data storage in dynamic indexed binary trees
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Proof Technologies Ltd, 2008-2011
*)
-(* ==========================================================================
*)
-
-
-module type Dltree_sig = sig
-
- type ('a,'b) dltree
- val dltree_empty : unit -> ('a,'b) dltree
- val dltree_reempty : ('a,'b) dltree -> unit
- val dltree_mem : 'a -> ('a,'b) dltree -> bool
- val dltree_lookup : 'a -> ('a,'b) dltree -> 'b
- val dltree_elem : 'a -> ('a,'b) dltree -> 'a * 'b
- val dltree_elems : ('a,'b) dltree -> ('a * 'b) list
- val dltree_insert : ('a * 'b) -> ('a,'b) dltree -> unit
- val dltree_remove : 'a -> ('a,'b) dltree -> unit
-
-end;;
diff --git a/hol-light/TacticRecording/ex.dot b/hol-light/TacticRecording/ex.dot
deleted file mode 100644
index e96142f..0000000
--- a/hol-light/TacticRecording/ex.dot
+++ /dev/null
@@ -1,24 +0,0 @@
-digraph G {
- subgraph cluster1 {
- label = "induction";
- 517 -> 518;
- 517 -> 519;
- }
- subgraph cluster2 {
- label = "base case";
- 528;
- }
- subgraph cluster3 {
- label = "step case";
- 537 -> 538;
- 538 -> 540;
- 540 -> 542;
- 542 -> 544;
- 544 -> 546;
- 546 -> 548;
- }
- 512 -> 513;
- 513 -> 517;
- 518 -> 528;
- 519 -> 537;
-}
\ No newline at end of file
diff --git a/hol-light/TacticRecording/ex2.dot
b/hol-light/TacticRecording/ex2.dot
deleted file mode 100644
index fbe961b..0000000
--- a/hol-light/TacticRecording/ex2.dot
+++ /dev/null
@@ -1,13 +0,0 @@
-digraph G {
- subgraph cluster0 {
- label = "process #1"
- a0->a1->a2->a3
- }
- subgraph cluster1 {
- label = "process #2"
- b0->b1->b2->b3
- }
- b3->23
- b2->a3
- a3->23
-}
\ No newline at end of file
diff --git a/hol-light/TacticRecording/ex3.dot
b/hol-light/TacticRecording/ex3.dot
deleted file mode 100644
index 1704533..0000000
--- a/hol-light/TacticRecording/ex3.dot
+++ /dev/null
@@ -1,24 +0,0 @@
-digraph G {
- subgraph cluster1 {
- label = "induction";
- 351 -> 352;
- 351 -> 353;
- 352 -> 358;
- subgraph cluster2 {
- label = "base case";
- 358;
- }
- 353 -> 367;
- subgraph cluster3 {
- label = "step case";
- 367 -> 368;
- 368 -> 370;
- 370 -> 372;
- 372 -> 374;
- 374 -> 376;
- 376 -> 378;
- }
- }
- 344 -> 345;
- 345 -> 351;
-}
diff --git a/hol-light/TacticRecording/ex3.png
b/hol-light/TacticRecording/ex3.png
deleted file mode 100644
index f2edfbd..0000000
Binary files a/hol-light/TacticRecording/ex3.png and /dev/null differ
diff --git a/hol-light/TacticRecording/ex3b.dot
b/hol-light/TacticRecording/ex3b.dot
deleted file mode 100644
index 5b951b9..0000000
--- a/hol-light/TacticRecording/ex3b.dot
+++ /dev/null
@@ -1,37 +0,0 @@
-digraph G {
- 344 [label = "CONV_TAC"];
- 345 [label = "GEN_TAC"];
- 351 [label = "INDUCT_TAC"];
- 352 [label = "REWRITE_TAC"];
- 358 [label = "REAL_ARITH_TAC"];
- 353 [label = "REWRITE_TAC"];
- 367 [label = "REWRITE_TAC"];
- 368 [label = "SIMP_TAC"];
- 370 [label = "REWRITE_TAC"];
- 372 [label = "REWRITE_TAC"];
- 374 [label = "ASM_REWRITE_TAC"];
- 376 [label = "REWRITE_TAC"];
- 378 [label = "REAL_ARITH_TAC"];
- 344 -> 345;
- 345 -> 351;
- subgraph cluster1 {
- label = "induction";
- 351 -> 352;
- 351 -> 353;
- 352 -> 358;
- subgraph cluster2 {
- label = "base case";
- 358;
- }
- 353 -> 367;
- subgraph cluster3 {
- label = "step case";
- 367 -> 368;
- 368 -> 370;
- 370 -> 372;
- 372 -> 374;
- 374 -> 376;
- 376 -> 378;
- }
- }
-}
\ No newline at end of file
diff --git a/hol-light/TacticRecording/examples1.ml
b/hol-light/TacticRecording/examples1.ml
deleted file mode 100644
index 4e67ca1..0000000
--- a/hol-light/TacticRecording/examples1.ml
+++ /dev/null
@@ -1,64 +0,0 @@
-#use"TacticRecording/main.ml";;
-#use "TacticRecording/biolayout.ml";;
-
-pg_mode_off ();;
-
-g `x = x /\ y = y /\ z = z`;;
-e (CONJ_TAC);;
-e (REFL_TAC);;
-e (CONJ_TAC);;
-e (REFL_TAC);;
-e (REFL_TAC);;
-let th = top_thm ();;
-
-g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
-e (REPEAT CONJ_TAC THEN GEN_TAC);;
-e (REFL_TAC);;
-e (REFL_TAC);;
-e (REFL_TAC);;
-let th = top_thm ();;
-
-g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
-e (CONJ_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (CONJ_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-let th = top_thm ();;
-
-g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
-e (REPEAT CONJ_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-let th = top_thm ();;
-
-g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
-e (REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);;
-let th = top_thm ();;
-
-print_executed_proof true;;
-print_flat_proof true;;
-print_thenl_proof ();;
-print_packaged_proof ();;
-print_gv_proof ();;
-
-g `(y:A) = z ==> (x:A) = x /\ y = y /\ z = z`;;
-e (STRIP_TAC);;
-e (UNDISCH_TAC `(y:A) = z`);;
-e (DISCH_TAC);;
-e (CONJ_TAC);;
-e (REFL_TAC);;
-e (CONJ_TAC);;
-e (REFL_TAC);;
-e (REFL_TAC);;
-
-
-
-
diff --git a/hol-light/TacticRecording/examples1_output.txt
b/hol-light/TacticRecording/examples1_output.txt
deleted file mode 100644
index 85f58ad..0000000
--- a/hol-light/TacticRecording/examples1_output.txt
+++ /dev/null
@@ -1,72 +0,0 @@
-# g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
-Warning: inventing type variables
-val it : xgoalstack = 1 subgoal (1 total)
-
-`(!x. x = x) /\ (!y. y = y) /\ (!z. z = z)`
-
-# e (REPEAT CONJ_TAC);;
-val it : xgoalstack = 3 subgoals (3 total)
-
-`!z. z = z`
-
-`!y. y = y`
-
-`!x. x = x`
-
-# e (GEN_TAC);;
-val it : xgoalstack = 1 subgoal (3 total)
-
-`x = x`
-
-# e (REFL_TAC);;
-val it : xgoalstack = 1 subgoal (2 total)
-
-`!y. y = y`
-
-# e (GEN_TAC);;
-val it : xgoalstack = 1 subgoal (2 total)
-
-`y = y`
-
-# e (REFL_TAC);;
-val it : xgoalstack = 1 subgoal (1 total)
-
-`!z. z = z`
-
-# e (GEN_TAC);;
-val it : xgoalstack = 1 subgoal (1 total)
-
-`z = z`
-
-# e (REFL_TAC);;
-val it : xgoalstack = No subgoals
-
-# print_executed_proof ();;
-e (REPEAT CONJ_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-
-val it : unit = ()
-# print_flat_proof ();;
-e (CONJ_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (CONJ_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-e (GEN_TAC);;
-e (REFL_TAC);;
-
-val it : unit = ()
-# print_thenl_proof ();;
-e (CONJ_TAC THENL [GEN_TAC THEN REFL_TAC; CONJ_TAC THENL [GEN_TAC THEN
REFL_TAC; GEN_TAC THEN REFL_TAC]]);;
-
-val it : unit = ()
-# print_optimal_proof ();;
-e (REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);;
-val it : unit = ()
-#
\ No newline at end of file
diff --git a/hol-light/TacticRecording/examples2.ml
b/hol-light/TacticRecording/examples2.ml
deleted file mode 100644
index a53baa4..0000000
--- a/hol-light/TacticRecording/examples2.ml
+++ /dev/null
@@ -1,45 +0,0 @@
-#use "hol.ml";;
-needs "Examples/prime.ml";;
-
-#use "TacticRecording/main.ml";;
-
-
-let egcd = define
- `egcd(m,n) = if m = 0 then n
- else if n = 0 then m
- else if m <= n then egcd(m,n - m)
- else egcd(m - n,n)`;;
-
-let egcd = theorem_wrap "egcd" egcd;;
-let DIVIDES_0 = theorem_wrap "DIVIDES_0" DIVIDES_0;;
-let WF_INDUCT_TAC = term_tactic_wrap "WF_INDUCT_TAC" WF_INDUCT_TAC;;
-
-g `!m n d. d divides egcd(m,n) <=> d divides m /\ d divides n`;;
-e (GEN_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `m + n` THEN
- GEN_TAC THEN ONCE_REWRITE_TAC[egcd] THEN
- ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
- ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
- COND_CASES_TAC);;
-top_goal ();;
-
-print_executed_proof ();;
-print_flat_proof ();;
-print_thenl_proof ();;
-print_optimal_proof ();;
-is_empty [23];;
-not true or not true;;
-
-let EGCD_INVARIANT = prove
- (`!m n d. d divides egcd(m,n) <=> d divides m /\ d divides n`,
- GEN_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `m + n` THEN
- GEN_TAC THEN ONCE_REWRITE_TAC[egcd] THEN
- ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
- ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
- COND_CASES_TAC THEN
- (W(fun (asl,w) -> FIRST_X_ASSUM(fun th ->
- MP_TAC(PART_MATCH (lhs o snd o dest_forall o rand) th (lhand w)))) THEN
- ANTS_TAC THENL [REPEAT(POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC]) THEN
- ASM_MESON_TAC[DIVIDES_SUB; DIVIDES_ADD; SUB_ADD; LE_CASES]);;
-
-
-
diff --git a/hol-light/TacticRecording/examples3.ml
b/hol-light/TacticRecording/examples3.ml
deleted file mode 100644
index f78ace3..0000000
--- a/hol-light/TacticRecording/examples3.ml
+++ /dev/null
@@ -1,236 +0,0 @@
-#use"hol.ml";;
-needs "Library/products.ml";;
-
-#use "TacticRecording/main.ml";;
-
-prioritize_real();;
-
-AIM: CONT_COMPOSE (Library/analysis.ml)
-- used by John in his Proof Style paper
-
-
-(* ** LEMMA1 from HOL Light's 100/arithmetic_geometric_mean.ml ** *)
-
-let LEMMA_1 = prove
- (`!x n. x pow (n + 1) - (&n + &1) * x + &n =
- (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
- CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN INDUCT_TAC THEN
- REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL
- [REAL_ARITH_TAC; REWRITE_TAC[ARITH_RULE `1 <= SUC n`]] THEN
- SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN
- REWRITE_TAC[real_pow; REAL_MUL_RID] THEN
- REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN
- ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN
- REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC);;
-
-let LEMMA_1 = prove
- (`!x n. x pow (n + 1) - (&n + &1) * x + &n =
- (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
- CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN
- HILABEL "induction"
- (INDUCT_TAC THEN
- REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL
- [HILABEL "base case" REAL_ARITH_TAC; ALL_TAC] THEN
- HILABEL "step case" (REWRITE_TAC[ARITH_RULE `1 <= SUC n`] THEN
- SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN
- REWRITE_TAC[real_pow; REAL_MUL_RID] THEN
- REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN
- ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN
- REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC)));;
-
-let LEMMA_1 = theorem_wrap "LEMMA_1" LEMMA_1;;
-
-top_thm ();;
-print_executed_proof true;;
-print_flat_proof true;;
-print_packaged_proof ();;
-print_thenl_proof ();;
-print_gv_proof ();;
-
-let gtr = !the_goal_tree;;
-let h = gtree_to_hiproof gtr;;
-let h' = (trivsimp_hiproof o dethen_hiproof) h;;
-
-g `!x n. x pow (n + 1) - (&n + &1) * x + &n =
- (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`;;
-e (CONV_TAC (ONCE_DEPTH_CONV SYM_CONV));;
-e (GEN_TAC);;
-e (INDUCT_TAC);;
-(* *** Subgoal 1 *** *)
-e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
-e (REAL_ARITH_TAC);;
-(* *** Subgoal 2 *** *)
-e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
-e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
-e (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]);;
-e (REWRITE_TAC [real_pow;REAL_MUL_RID]);;
-e (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]);;
-e (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]);;
-e (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]);;
-e (REAL_ARITH_TAC);;
-
-print_executed_proof true;;
-print_packaged_proof ();;
-print_thenl_proof ();;
-
-(* LEMMA 2 *)
-
-let LEMMA_2 = prove
- (`!n x. &0 <= x ==> &0 <= x pow (n + 1) - (&n + &1) * x + &n`,
- REPEAT STRIP_TAC THEN REWRITE_TAC[LEMMA_1] THEN
- MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE] THEN
- MATCH_MP_TAC SUM_POS_LE_NUMSEG THEN
- ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_POW_LE]);;
-
-let LEMMA_2 = theorem_wrap "LEMMA_2" LEMMA_2;;
-
-print_executed_proof true;;
-print_flat_proof true;;
-print_packaged_proof ();;
-print_gv_proof ();;
-
-g `!n x. &0 <= x ==> &0 <= x pow (n + 1) - (&n + &1) * x + &n`;;
-
-(* LEMMA 3 *)
-
-let LEMMA_3 = prove
- (`!n x. 1 <= n /\ (!i. 1 <= i /\ i <= n + 1 ==> &0 <= x i)
- ==> x(n + 1) * (sum(1..n) x / &n) pow n
- <= (sum(1..n+1) x / (&n + &1)) pow (n + 1)`,
- REPEAT STRIP_TAC THEN
- ABBREV_TAC `a = sum(1..n+1) x / (&n + &1)` THEN
- ABBREV_TAC `b = sum(1..n) x / &n` THEN
- SUBGOAL_THEN `x(n + 1) = (&n + &1) * a - &n * b` SUBST1_TAC THENL
- [MAP_EVERY EXPAND_TAC ["a"; "b"] THEN
- ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; LE_1;
- REAL_ARITH `~(&n + &1 = &0)`] THEN
- SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`; SUM_SING_NUMSEG] THEN
- REAL_ARITH_TAC;
- ALL_TAC] THEN
- SUBGOAL_THEN `&0 <= a /\ &0 <= b` STRIP_ASSUME_TAC THENL
- [MAP_EVERY EXPAND_TAC ["a"; "b"] THEN CONJ_TAC THEN
- MATCH_MP_TAC REAL_LE_DIV THEN
- (CONJ_TAC THENL [MATCH_MP_TAC SUM_POS_LE_NUMSEG; REAL_ARITH_TAC]) THEN
- ASM_SIMP_TAC[ARITH_RULE `p <= n ==> p <= n + 1`];
- ALL_TAC] THEN
- ASM_CASES_TAC `b = &0` THEN
- ASM_SIMP_TAC[REAL_POW_ZERO; LE_1; REAL_MUL_RZERO; REAL_POW_LE] THEN
- MP_TAC(ISPECL [`n:num`; `a / b`] LEMMA_2) THEN ASM_SIMP_TAC[REAL_LE_DIV] THEN
- REWRITE_TAC[REAL_ARITH `&0 <= x - a + b <=> a - b <= x`; REAL_POW_DIV] THEN
- SUBGOAL_THEN `&0 < b` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
- ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_POW_LT] THEN
- MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
- REWRITE_TAC[REAL_POW_ADD] THEN UNDISCH_TAC `~(b = &0)` THEN
- CONV_TAC REAL_FIELD);;
-
-let LEMMA_3 = theorem_wrap "LEMMA_3" LEMMA_3;;
-
-print_executed_proof true;;
-print_flat_proof true;;
-print_thenl_proof ();;
-print_packaged_proof ();;
-print_gv_proof ();;
-
-g `!n x. 1 <= n /\ (!i. 1 <= i /\ i <= n + 1 ==> &0 <= x i)
- ==> x(n + 1) * (sum(1..n) x / &n) pow n
- <= (sum(1..n+1) x / (&n + &1)) pow (n + 1)`;;
-
-print_flat_proof true;;
-e (STRIP_TAC);;
-e (STRIP_TAC);;
-e (STRIP_TAC);;
-e (ABBREV_TAC `a = sum (1..n + 1) x / (&n + &1)`);;
-e (ABBREV_TAC `b = sum (1..n) x / &n`);;
-e (SUBGOAL_THEN `x (n + 1) = (&n + &1) * a - &n * b` SUBST1_TAC);;
-(* *** Subgoal 1 *** *)
-e (EXPAND_TAC "a");;
-e (EXPAND_TAC "b");;
-e (ASM_SIMP_TAC [REAL_DIV_LMUL; REAL_OF_NUM_EQ; LE_1; REAL_ARITH `~(&n + &1 =
&0)`]);;
-e (SIMP_TAC [SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`; SUM_SING_NUMSEG]);;
-e (REAL_ARITH_TAC);;
-(* *** Subgoal 2 *** *)
-e (SUBGOAL_THEN `&0 <= a /\ &0 <= b` STRIP_ASSUME_TAC);;
-(* *** Subgoal 2.1 *** *)
-e (EXPAND_TAC "a");;
-e (EXPAND_TAC "b");;
-e (CONJ_TAC);;
-(* *** Subgoal 2.1.1 *** *)
-e (MATCH_MP_TAC REAL_LE_DIV);;
-e (CONJ_TAC);;
-(* *** Subgoal 2.1.1.1 *** *)
-e (MATCH_MP_TAC SUM_POS_LE_NUMSEG);;
-e (ASM_SIMP_TAC [ARITH_RULE `p <= n ==> p <= n + 1`]);;
-(* *** Subgoal 2.1.1.2 *** *)
-e (REAL_ARITH_TAC);;
-(* *** Subgoal 2.1.2 *** *)
-e (MATCH_MP_TAC REAL_LE_DIV);;
-e (CONJ_TAC);;
-(* *** Subgoal 2.1.2.1 *** *)
-e (MATCH_MP_TAC SUM_POS_LE_NUMSEG);;
-e (ASM_SIMP_TAC [ARITH_RULE `p <= n ==> p <= n + 1`]);;
-(* *** Subgoal 2.1.2.2 *** *)
-e (REAL_ARITH_TAC);;
-(* *** Subgoal 2.2 *** *)
-e (ASM_CASES_TAC `b = &0`);;
-(* *** Subgoal 2.2.1 *** *)
-e (ASM_SIMP_TAC [REAL_POW_ZERO;LE_1;REAL_MUL_RZERO;REAL_POW_LE]);;
-(* *** Subgoal 2.2.2 *** *)
-e (ASM_SIMP_TAC [REAL_POW_ZERO;LE_1;REAL_MUL_RZERO;REAL_POW_LE]);;
-e (MP_TAC (ISPECL [`n`;`a / b`] LEMMA_2));;
-e (ASM_SIMP_TAC [REAL_LE_DIV]);;
-e (REWRITE_TAC [REAL_ARITH `&0 <= x - a + b <=> a - b <= x`; REAL_POW_DIV]);;
-e (SUBGOAL_THEN `&0 < b` ASSUME_TAC);;
-(* *** Subgoal 2.2.2.1 *** *)
-e (ASM_REAL_ARITH_TAC);;
-(* *** Subgoal 2.2.2.2 *** *)
-e (ASM_SIMP_TAC [REAL_LE_RDIV_EQ;REAL_POW_LT]);;
-e (MATCH_MP_TAC EQ_IMP);;
-e (AP_THM_TAC);;
-e (AP_TERM_TAC);;
-e (REWRITE_TAC [REAL_POW_ADD]);;
-e (UNDISCH_TAC `~(b = &0)`);;
-e (CONV_TAC REAL_FIELD);;
-
-(* AGM *)
-
-let AGM = prove
- (`!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
- ==> product(1..n) a <= (sum(1..n) a / &n) pow n`,
- INDUCT_TAC THEN REWRITE_TAC[ARITH; PRODUCT_CLAUSES_NUMSEG] THEN
- REWRITE_TAC[ARITH_RULE `1 <= SUC n`] THEN X_GEN_TAC `x:num->real` THEN
- ASM_CASES_TAC `n = 0` THENL
- [ASM_REWRITE_TAC[PRODUCT_CLAUSES_NUMSEG; ARITH; SUM_SING_NUMSEG] THEN
- REAL_ARITH_TAC;
- REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
- EXISTS_TAC `x(n + 1) * (sum(1..n) x / &n) pow n` THEN
- ASM_SIMP_TAC[LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1;
- ARITH_RULE `i <= n ==> i <= n + 1`] THEN
- GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LE_RMUL
THEN
- ASM_SIMP_TAC[LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]]);;
-
-g `!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
- ==> product(1..n) a <= (sum(1..n) a / &n) pow n`;;
-e (INDUCT_TAC);;
-(* *** Subgoal 1 *** *)
-e (REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG]);;
-(* *** Subgoal 2 *** *)
-e (REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG]);;
-e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
-e (X_GEN_TAC `x:num->real`);;
-e (ASM_CASES_TAC `n = 0`);;
-(* *** Subgoal 2.1 *** *)
-e (ASM_REWRITE_TAC [PRODUCT_CLAUSES_NUMSEG;ARITH;SUM_SING_NUMSEG]);;
-e (REAL_ARITH_TAC);;
-(* *** Subgoal 2.2 *** *)
-e (REWRITE_TAC [ADD1]);;
-e (STRIP_TAC);;
-e (MATCH_MP_TAC REAL_LE_TRANS);;
-e (EXISTS_TAC `x (n + 1) * (sum (1..n) x / &n) pow n`);;
-e (ASM_SIMP_TAC [LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1; ARITH_RULE `i <= n ==> i
<= n + 1`]);;
-e (GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM]);;
-e (MATCH_MP_TAC REAL_LE_RMUL);;
-e (ASM_SIMP_TAC [LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]);;
-
-g `!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
- ==> product(1..n) a <= (sum(1..n) a / &n) pow n`;;
-e (INDUCT_TAC THEN REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG] THEN REWRITE_TAC
[ARITH_RULE `1 <= SUC n`] THEN X_GEN_TAC `x:num->real` THEN ASM_CASES_TAC `n =
0` THENL [ASM_REWRITE_TAC [PRODUCT_CLAUSES_NUMSEG;ARITH;SUM_SING_NUMSEG] THEN
REAL_ARITH_TAC; REWRITE_TAC [ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN EXISTS_TAC `x (n + 1) * (sum (1..n) x / &n) pow n` THEN
ASM_SIMP_TAC [LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1; ARITH_RULE `i <= n ==> i <=
n + 1`] THEN GEN_REWRITE_TAC RAND_ [...]
diff --git a/hol-light/TacticRecording/examples3_LEMMA1.dot
b/hol-light/TacticRecording/examples3_LEMMA1.dot
deleted file mode 100644
index 69bc7c4..0000000
--- a/hol-light/TacticRecording/examples3_LEMMA1.dot
+++ /dev/null
@@ -1,24 +0,0 @@
-digraph G {
- subgraph cluster0 {
- label = "induction";
- 517->518;
- 517->519;
- }
- subgraph cluster1 {
- label = "base case";
- 528->528
- }
- subgraph cluster2 {
- label = "step case";
- 537->538;
- 538->540;
- 540->542;
- 542->544;
- 544->546;
- 546->548;
- }
- 512->513;
- 513->517;
- 518->528;
- 519->537;
-}
\ No newline at end of file
diff --git a/hol-light/TacticRecording/examples3_output.txt
b/hol-light/TacticRecording/examples3_output.txt
deleted file mode 100644
index 18d4901..0000000
--- a/hol-light/TacticRecording/examples3_output.txt
+++ /dev/null
@@ -1,36 +0,0 @@
-# let LEMMA_1 = prove
- (`!x n. x pow (n + 1) - (&n + &1) * x + &n =
- (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
- CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN INDUCT_TAC THEN
- REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL
- [REAL_ARITH_TAC; REWRITE_TAC[ARITH_RULE `1 <= SUC n`]] THEN
- SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN
- REWRITE_TAC[real_pow; REAL_MUL_RID] THEN
- REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN
- ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN
- REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC);;
-val ( LEMMA_1 ) : thm =
- |- !x n.
- x pow (n + 1) - (&n + &1) * x + &n =
- (x - &1) pow 2 * sum (1..n) (\k. &k * x pow (n - k))
-
-# print_executed_proof ();;
-e ((CONV_TAC (ONCE_DEPTH_CONV SYM_CONV)) THEN GEN_TAC THEN INDUCT_TAC THEN
(REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]) THENL [REAL_ARITH_TAC;
REWRITE_TAC [ARITH_RULE `1 <= SUC n`]] THEN (SIMP_TAC [ARITH_RULE `k <= n ==>
SUC n - k = SUC (n - k)`; SUB_REFL]) THEN (REWRITE_TAC [real_pow;REAL_MUL_RID])
THEN (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]) THEN
(ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]) THEN (REWRITE_TAC
[GSYM REAL_OF_NUM_SUC; RE [...]
-
-val it : unit = ()
-# print_flat_proof ();;
-e (CONV_TAC (ONCE_DEPTH_CONV SYM_CONV));;
-e (GEN_TAC);;
-e (INDUCT_TAC);;
-e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
-e (REAL_ARITH_TAC);;
-e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
-e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
-e (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]);;
-e (REWRITE_TAC [real_pow;REAL_MUL_RID]);;
-e (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]);;
-e (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]);;
-e (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]);;
-e (REAL_ARITH_TAC);;
-
-
diff --git a/hol-light/TacticRecording/examples4.ml
b/hol-light/TacticRecording/examples4.ml
deleted file mode 100644
index 3178f65..0000000
--- a/hol-light/TacticRecording/examples4.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-pg_mode_on ();;
-get_pg_mode ();;
-
-g `(?x:num. p(x) /\ q(x) /\ r(x)) ==> (?x. r(x) /\ p(x)) /\ (?x. p(x) /\ (q(x)
<=> r(x)))`;;
-e (STRIP_TAC);;
-e (STRIP_TAC);;
-e (X_META_EXISTS_TAC `n1:num` THEN CONJ_TAC);;
-e (FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n1:num`]));;
-e (ASM_REWRITE_TAC[]);;
-e (X_META_EXISTS_TAC `n2:num` THEN CONJ_TAC);;
-e (FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n2:num`]));;
-e (ASM_REWRITE_TAC[]);;
-let th = top_thm ();;
diff --git a/hol-light/TacticRecording/examples5.ml
b/hol-light/TacticRecording/examples5.ml
deleted file mode 100644
index 1ded99c..0000000
--- a/hol-light/TacticRecording/examples5.ml
+++ /dev/null
@@ -1,182 +0,0 @@
-(* Taken from Library/prime.ml *)
-
-prioritize_num();;
-
-(* ------------------------------------------------------------------------- *)
-(* HOL88 compatibility (since all this is a port of old HOL88 stuff). *)
-(* ------------------------------------------------------------------------- *)
-
-let MULT_MONO_EQ = prove
- (`!m i n. ((SUC n) * m = (SUC n) * i) <=> (m = i)`,
- REWRITE_TAC[EQ_MULT_LCANCEL; NOT_SUC]);;
-
-let LESS_ADD_1 = prove
- (`!m n. n < m ==> (?p. m = n + (p + 1))`,
- REWRITE_TAC[LT_EXISTS; ADD1; ADD_ASSOC]);;
-
-let LESS_ADD_SUC = ARITH_RULE `!m n. m < (m + (SUC n))`;;
-
-let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;;
-
-let LESS_MONO_ADD = ARITH_RULE `!m n p. m < n ==> (m + p) < (n + p)`;;
-
-let LESS_EQ_0 = prove
- (`!n. n <= 0 <=> (n = 0)`,
- REWRITE_TAC[LE]);;
-
-let LESS_LESS_CASES = ARITH_RULE `!m n. (m = n) \/ m < n \/ n < m`;;
-
-let LESS_ADD_NONZERO = ARITH_RULE `!m n. ~(n = 0) ==> m < (m + n)`;;
-
-let NOT_EXP_0 = prove
- (`!m n. ~((SUC n) EXP m = 0)`,
- REWRITE_TAC[EXP_EQ_0; NOT_SUC]);;
-
-let LESS_THM = ARITH_RULE `!m n. m < (SUC n) <=> (m = n) \/ m < n`;;
-
-let NOT_LESS_0 = ARITH_RULE `!n. ~(n < 0)`;;
-
-let ZERO_LESS_EXP = prove
- (`!m n. 0 < ((SUC n) EXP m)`,
- REWRITE_TAC[LT_NZ; NOT_EXP_0]);;
-
-(* ------------------------------------------------------------------------- *)
-(* General arithmetic lemmas. *)
-(* ------------------------------------------------------------------------- *)
-
-let MULT_FIX = prove(
- `!x y. (x * y = x) <=> (x = 0) \/ (y = 1)`,
- REPEAT GEN_TAC THEN
- STRUCT_CASES_TAC(SPEC `x:num` num_CASES) THEN
- REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN
- REWRITE_TAC[GSYM(el 4 (CONJUNCTS (SPEC_ALL MULT_CLAUSES)))] THEN
- GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) (* MMA: this is a problem !!!!)
- [GSYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
- MATCH_ACCEPT_TAC MULT_MONO_EQ);;
-
-let LESS_EQ_MULT = prove(
- `!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)`,
- REPEAT GEN_TAC THEN
- DISCH_THEN(STRIP_ASSUME_TAC o REWRITE_RULE[LE_EXISTS]) THEN
- ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB;
- GSYM ADD_ASSOC; LE_ADD]);;
-
-let LESS_MULT = prove(
- `!m n p q. m < n /\ p < q ==> (m * p) < (n * q)`,
- REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN
- ((CHOOSE_THEN SUBST_ALL_TAC) o MATCH_MP LESS_ADD_1)) THEN
- REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
- REWRITE_TAC[GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; GSYM ADD_ASSOC] THEN
- ONCE_REWRITE_TAC[GSYM (el 3 (CONJUNCTS ADD_CLAUSES))] THEN
- MATCH_ACCEPT_TAC LESS_ADD_SUC);;
-
-let MULT_LCANCEL = prove(
- `!a b c. ~(a = 0) /\ (a * b = a * c) ==> (b = c)`,
- REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC `a:num` num_CASES) THEN
- REWRITE_TAC[NOT_SUC; MULT_MONO_EQ]);;
-
-let LT_POW2_REFL = prove
- (`!n. n < 2 EXP n`,
- INDUCT_TAC THEN REWRITE_TAC[EXP] THEN TRY(POP_ASSUM MP_TAC) THEN ARITH_TAC);;
-
-(* ------------------------------------------------------------------------- *)
-(* Properties of the exponential function. *)
-(* ------------------------------------------------------------------------- *)
-
-let EXP_0 = prove
- (`!n. 0 EXP (SUC n) = 0`,
- REWRITE_TAC[EXP; MULT_CLAUSES]);;
-
-let EXP_MONO_LT_SUC = prove
- (`!n x y. (x EXP (SUC n)) < (y EXP (SUC n)) <=> (x < y)`,
- REWRITE_TAC[EXP_MONO_LT; NOT_SUC]);;
-
-let EXP_MONO_LE_SUC = prove
- (`!x y n. (x EXP (SUC n)) <= (y EXP (SUC n)) <=> x <= y`,
- REWRITE_TAC[EXP_MONO_LE; NOT_SUC]);;
-
-let EXP_MONO_EQ_SUC = prove
- (`!x y n. (x EXP (SUC n) = y EXP (SUC n)) <=> (x = y)`,
- REWRITE_TAC[EXP_MONO_EQ; NOT_SUC]);;
-
-let EXP_EXP = prove
- (`!x m n. (x EXP m) EXP n = x EXP (m * n)`,
- REWRITE_TAC[EXP_MULT]);;
-
-(* ------------------------------------------------------------------------- *)
-(* More ad-hoc arithmetic lemmas unlikely to be useful elsewhere. *)
-(* ------------------------------------------------------------------------- *)
-
-let DIFF_LEMMA = prove(
- `!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)`,
- REPEAT GEN_TAC THEN
- DISJ_CASES_TAC(SPEC `a:num` LESS_0_CASES) THEN ASM_REWRITE_TAC[] THEN
- DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN
- DISJ2_TAC THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
- GEN_REWRITE_TAC LAND_CONV [GSYM (CONJUNCT1 ADD_CLAUSES)] THEN
- REWRITE_TAC[ADD_ASSOC] THEN
- REPEAT(MATCH_MP_TAC LESS_MONO_ADD) THEN POP_ASSUM ACCEPT_TAC);;
-
-let NOT_EVEN_EQ_ODD = prove(
- `!m n. ~(2 * m = SUC(2 * n))`,
- REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
- REWRITE_TAC[EVEN; EVEN_MULT; ARITH]);;
-
-let CANCEL_TIMES2 = prove(
- `!x y. (2 * x = 2 * y) <=> (x = y)`,
- REWRITE_TAC[num_CONV `2`; MULT_MONO_EQ]);;
-
-let EVEN_SQUARE = prove(
- `!n. EVEN(n) ==> ?x. n EXP 2 = 4 * x`,
- GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN
- DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
- EXISTS_TAC `m * m` THEN REWRITE_TAC[EXP_2] THEN
- REWRITE_TAC[SYM(REWRITE_CONV[ARITH] `2 * 2`)] THEN
- REWRITE_TAC[MULT_AC]);;
-
-let ODD_SQUARE = prove(
- `!n. ODD(n) ==> ?x. n EXP 2 = (4 * x) + 1`,
- GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN
- DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
- ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
- REWRITE_TAC[GSYM ADD1; SUC_INJ] THEN
- EXISTS_TAC `(m * m) + m` THEN
- REWRITE_TAC(map num_CONV [`4`; `3`; `2`; `1`]) THEN
- REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
- REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
- REWRITE_TAC[ADD_AC]);;
-
-let DIFF_SQUARE = prove(
- `!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)`,
- REPEAT GEN_TAC THEN
- DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THENL
- [SUBGOAL_THEN `(x * x) <= (y * y)` MP_TAC THENL
- [MATCH_MP_TAC LESS_EQ_MULT THEN ASM_REWRITE_TAC[];
- POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM SUB_EQ_0] THEN
- REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES]];
- POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
- REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
- REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
- REWRITE_TAC[GSYM ADD_ASSOC; ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
- AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [ADD_SYM] THEN
- AP_TERM_TAC THEN MATCH_ACCEPT_TAC MULT_SYM]);;
-
-let ADD_IMP_SUB = prove(
- `!x y z. (x + y = z) ==> (x = z - y)`,
- REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
- REWRITE_TAC[ADD_SUB]);;
-
-let ADD_SUM_DIFF = prove(
- `!v w. v <= w ==> ((w + v) - (w - v) = 2 * v) /\
- ((w + v) + (w - v) = 2 * w)`,
- REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
- DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
- REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
- REWRITE_TAC[MULT_2; GSYM ADD_ASSOC] THEN
- ONCE_REWRITE_TAC[ADD_SYM] THEN
- REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB; GSYM ADD_ASSOC]);;
-
-let EXP_4 = prove(
- `!n. n EXP 4 = (n EXP 2) EXP 2`,
- GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN
- REWRITE_TAC[ARITH]);;
diff --git a/hol-light/TacticRecording/gvexport.ml
b/hol-light/TacticRecording/gvexport.ml
deleted file mode 100644
index 952b3ad..0000000
--- a/hol-light/TacticRecording/gvexport.ml
+++ /dev/null
@@ -1,47 +0,0 @@
-(* ==========================================================================
*)
-(* GRAPHVIZ EXPORT (HOL LIGHT)
*)
-(* - Exporting recorded tactics into a Dot file for GraphViz
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2012
*)
-(* ==========================================================================
*)
-
-
-let cluster_count = ref 0;;
-
-let rec print_gv_graphelem d ge =
- match ge with
- Box (l,ges)
- -> let () = (cluster_count := !cluster_count + 1) in
- (print_indent d; print_string "subgraph cluster";
- print_int !cluster_count; print_string " "; print_string "{\n";
- print_indent (d+2); print_string "label = "; print_label l;
- print_string ";\n";
- do_list (print_gv_graphelem (d+2)) ges;
- print_indent d; print_string "}\n")
- | Line (id1,id2)
- -> (print_indent d; print_goalid id1; print_string " -> ";
- print_goalid id2; print_string ";\n")
- | Single id
- -> (print_indent d; print_goalid id; print_string ";\n")
- | Name (id,x)
- -> (print_indent d; print_goalid id;
- print_string " [label = "; print_fstring x; print_string "];\n");;
-
-let print_gv_graph ges =
- let () = (cluster_count := 0) in
- (print_string "digraph G {\n";
- do_list (print_gv_graphelem 2) ges;
- print_string "}\n");;
-
-let print_hiproof_gv_graph h =
- let h' = (trivsimp_hiproof o rightgroup_hiproof o
- trivsimp_hiproof o dethen_hiproof) h in
- let ges = hiproof_graph h' in
- print_gv_graph ges;;
-
-let print_gtree_gv_proof gtr =
- let h = gtree_to_hiproof gtr in
- print_hiproof_gv_graph h;;
-
-let print_gv_proof () = print_gtree_gv_proof !the_goal_tree;;
diff --git a/hol-light/TacticRecording/hiproofs.ml
b/hol-light/TacticRecording/hiproofs.ml
deleted file mode 100644
index 310ba67..0000000
--- a/hol-light/TacticRecording/hiproofs.ml
+++ /dev/null
@@ -1,417 +0,0 @@
-(* ==========================================================================
*)
-(* HIPROOFS (HOL LIGHT)
*)
-(* - Hiproofs and refactoring operations
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2012
*)
-(* ==========================================================================
*)
-
-
-(* This file defines a hiproof [1] datatype and various operations on it.
*)
-(* The datatype closely resembles that proposed in [2], with the notable
*)
-(* difference that atomic steps carry their arity.
*)
-
-(* [1] "Hiproofs: A Hierarchical Notion of Proof Tree", Denney, Power &
*)
-(* Tourlas, 2006.
*)
-(* [2] "A Tactic Language for Hiproofs", Aspinall, Denney & Luth, 2008.
*)
-
-
-
-(* ** DATATYPE ** *)
-
-
-(* Hiproof datatype *)
-
-(* Note that atomic tactics are labelled with their arity, corresponding to
*)
-(* how many subgoals they result in. An arity of -1 indicates unknown, and 0
*)
-(* indicates a tactic that completes its goal.
*)
-
-type hiproof =
- Hactive of goalid (* Active subgoal *)
- | Hatomic of (goalid * int) (* Atomic tactic + arity *)
- | Hidentity of goalid (* Null, for wiring *)
- | Hlabelled of (label * hiproof) (* Box *)
- | Hsequence of (hiproof * hiproof) (* Serial application *)
- | Htensor of hiproof list (* Parallel application *)
- | Hempty;; (* Completed goal *)
-
-
-(* Constructors and destructors *)
-
-let hsequence (h1,h2) = Hsequence (h1,h2);;
-
-let dest_hsequence h =
- match h with
- Hsequence hh -> hh
- | _ -> failwith "Not a sequence hiproof";;
-
-let is_hsequence h = can dest_hsequence h;;
-
-let is_hidentity h = match h with Hidentity _ -> true | _ -> false;;
-
-let hiproof_id h =
- match h with
- Hactive id | Hatomic (id,_) | Hidentity id -> id
- | _ -> failwith "hiproof_id: Not a unit hiproof";;
-
-
-(* Arity *)
-
-let rec hiproof_arity h =
- match h with
- Hactive _ -> 1
- | Hatomic (_,n) -> n
- | Hidentity _ -> 1
- | Hlabelled (_,h0) -> hiproof_arity h0
- | Hsequence (h1,h2) -> hiproof_arity h2
- | Htensor hs -> sum (map hiproof_arity hs)
- | Hempty -> 0;;
-
-
-(* Hitrace *)
-
-type hitrace =
- Hicomment of int list
- | Hiproof of hiproof;;
-
-
-
-(* ** TRANSLATION OF GOAL TREE TO HIPROOF ** *)
-
-
-let rec gtree_to_hiproof gtr =
- let id = gtree_id gtr in
- let (_,gtrm) = gtr in
- match !gtrm with
- Gactive
- -> Hactive id
- | Gexit _
- -> Hidentity id
- | Gexecuted (gstp,gtrs)
- -> let h1 =
- match gstp with
- Gatom _ | Gbox (_,_,true)
- -> Hatomic (id, length gtrs)
- | Gbox (l,gtr,false)
- -> Hlabelled (l, gtree_to_hiproof gtr) in
- let h2 = Htensor (map gtree_to_hiproof gtrs) in
- Hsequence (h1,h2);;
-
-
-
-(* ** REFACTORING OPERATIONS ** *)
-
-
-(* Generic refactoring operation *)
-
-(* Applies a refactoring function 'foo' at every level of hiproof 'h', from
*)
-(* bottom up. If the 'r' flag is set then refactoring is repeated bottom up
*)
-(* whenever 'foo' makes a change. Note that if 'foo' makes no change then it
*)
-(* should just return its input hiproof (rather than raise an exception).
*)
-
-let rec refactor_hiproof r foo h =
- let h' =
- match h with
- Hlabelled (l,h0)
- -> let h0' = refactor_hiproof r foo h0 in
- Hlabelled (l,h0')
- | Hsequence (h1,h2)
- -> let h1' = refactor_hiproof r foo h1 in
- let h2' = refactor_hiproof r foo h2 in
- Hsequence (h1',h2')
- | Htensor hs
- -> let hs' = map (refactor_hiproof r foo) hs in
- Htensor hs'
- | _ -> h in
- let h'' = if (h' = h) then h else h' in
- let h''' = foo h'' in
- if r & not (h''' = h'')
- then refactor_hiproof r foo h'''
- else h''';;
-
-
-(* Trivial simplification *)
-
-(* Removes basic algebraic identities/zeros.
*)
-
-let collapse_tensor h hs =
- match h with
- Hempty -> hs
- | Htensor hs0 -> hs0 @ hs
- | _ -> h :: hs;;
-
-let trivsimp_hiproof h =
- let trivsimp h =
- match h with
- Hatomic (id,_) when (gtree_tactic (get_gtree id) = ("ALL_TAC",[]))
- -> Hidentity id
- | Hsequence (h1, Hempty) -> h1
- | Hsequence (h1, Hidentity _) -> h1
- | Hsequence (h1, Htensor hs2) -> if (forall is_hidentity hs2)
- then h1
- else h
- | Hsequence (Hidentity _, h2) -> h2
- | Hsequence (Htensor hs1, h2) -> if (forall is_hidentity hs1)
- then h2
- else h
- | Htensor [] -> Hempty
- | Htensor [h0] -> h0
- | Htensor hs0 -> Htensor (foldr collapse_tensor hs0 [])
- | _ -> h in
- refactor_hiproof true trivsimp h;;
-
-
-(* Matching up two tensored lists to create single tensored list *)
-
-let rec matchup_hiproofs0 hs1 hs2 =
- match hs1 with
- [] -> []
- | h1::hs01
- -> let n1 = hiproof_arity h1 in
- let (hs2a,hs2b) = try chop_list n1 hs2
- with Failure _ ->
- if (n1 = -1)
- then failwith "matchup_hiproofs: unknown arity"
- else failwith "matchup_hiproofs: Internal error - \
- inconsistent arities" in
- (h1,hs2a) :: (matchup_hiproofs0 hs01 hs2b);;
-
-let matchup_hiproofs hs1 hs2 =
- let hhs = matchup_hiproofs0 hs1 hs2 in
- map (fun (h1,hs2) -> Hsequence (h1, Htensor hs2)) hhs;;
-
-
-(* Separating out tensored list into head tensor and tail tensor *)
-
-let separate_hiproofs0 h (hs01,hs02) =
- match h with
- Hsequence (h1,h2)
- -> (h1::hs01, h2::hs02)
- | _ -> let n = hiproof_arity h in
- let h2 = Htensor (copy n (Hidentity (-1))) in
- (h::hs01, h2::hs02);;
-
-let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);;
-
-
-(* Delabelling *)
-
-(* Strips out any boxes from the proof. Note that some boxes, such as
*)
-(* 'SUBGOAL_THEN', cannot be stripped out without spoiling the proof, and so
*)
-(* are left alone.
*)
-
-let delabel_hiproof h =
- let delabel h =
- match h with
- Hlabelled (Tactical ("SUBGOAL_THEN",_), h0)
- -> h
- | Hlabelled (_,h0)
- -> h0
- | _ -> h in
- refactor_hiproof true delabel h;;
-
-let dethen_hiproof h =
- let dethen h =
- match h with
- Hlabelled (Tactical (("THEN" | "THENL"),_), h0)
- -> h0
- | _ -> h in
- refactor_hiproof true dethen h;;
-
-
-(* Right-grouping *)
-
-(* Expands the proof into a right-associative sequence, with tensor
*)
-(* compounding on the right. Leaves all boxes unchanged.
*)
-
-let rightgroup_hiproof h =
- let rightgroup h =
- match h with
- Hsequence (Hsequence (h1, Htensor hs2), Htensor hs3)
- -> Hsequence (h1, Htensor (matchup_hiproofs hs2 hs3))
- | Hsequence (Hsequence (h1, Htensor hs2), h3)
- -> Hsequence (h1, Htensor (matchup_hiproofs hs2 [h3]))
- | Hsequence (Hsequence (h1,h2), h3)
- -> Hsequence (h1, Hsequence (h2,h3))
- | _ -> h in
- refactor_hiproof true rightgroup h;;
-
-
-(* Left-grouping *)
-
-(* Expands the proof into a left-associative sequence.
*)
-
-let leftgroup_hiproof h =
- let leftgroup h =
- match h with
- Hsequence (h1, Hsequence (h2, h3))
- -> Hsequence (Hsequence (h1,h2), h3)
- | _ -> h in
- refactor_hiproof true leftgroup h;;
-
-
-(* THEN insertion *)
-
-(* Looks for opportunities to use 'THEN' tacticals. Note that assumes a
*)
-(* normal form where trivsimp has taken place.
*)
-
-let rec head_hiproof_equiv h1 h2 =
- match (h1,h2) with
- (Hatomic (id1,_), Hatomic (id2,_))
- -> (gtree_tactic o get_gtree) id1 = (gtree_tactic o get_gtree) id2
- | (Hidentity _, Hidentity _)
- -> true
- | (Hsequence (h1a,h1b), h2)
- -> head_hiproof_equiv h1a h2
- | (h1, Hsequence (h2a,h2b))
- -> head_hiproof_equiv h1 h2a
- | (Hempty, Hempty)
- -> true
- | _ -> false;;
-
-let thenise_hiproof h =
- let rec thenise h =
- match h with
- Hsequence (h1, Htensor (h2::h2s))
- -> if not (is_hidentity h2) & (forall (head_hiproof_equiv h2) h2s)
- then let (hs2a,hs2b) = separate_hiproofs (h2::h2s) in
- let h' = Hsequence
- (Hlabelled (Tactical ("THEN",[]),
- Hsequence (h1, Htensor hs2a)),
- Htensor hs2b) in
- thenise h'
- else h
- | _ -> h in
- refactor_hiproof false thenise h;;
-
-
-
-(* ** HIPROOF GRAPH ** *)
-
-
-(* Graph element datatype *)
-
-type graph_elem =
- Box of (label * graph_elem list)
- | Line of (goalid * goalid)
- | Single of goalid
- | Name of (goalid * string);;
-
-let is_box ge =
- match ge with Box _ -> true | _ -> false;;
-
-let mk_line id1 id2 = Line (id1,id2);;
-
-let rec graph_elem_nodes ge =
- match ge with
- Box (_,ges) -> graph_nodes ges
- | Line (id1,id2) -> [id1;id2]
- | Single id -> [id]
- | Name (id,x) -> [id]
-
-and graph_nodes ges =
- foldr (fun ge ids -> union (graph_elem_nodes ge) ids) ges [];;
-
-
-(* Utils *)
-
-let rec hiproof_ins h =
- match h with
- Hactive id -> [id]
- | Hatomic (id,n) -> [id]
- | Hidentity id -> [-1]
- | Hlabelled (l,h0) -> hiproof_ins h0
- | Hsequence (h1,h2) -> hiproof_ins h1
- | Htensor hs -> flat (map hiproof_ins hs)
- | Hempty -> [];;
-
-let rec hiproof_outs (h:hiproof) : goalid list =
- match h with
- Hactive id -> [id]
- | Hatomic (id,n) -> copy n id
- | Hidentity id -> [id]
- | Hlabelled (l,h0) -> hiproof_outs h0
- | Hsequence (h1, Htensor hs2)
- -> let nhs2 = enumerate hs2 in
- let ids1 = hiproof_outs h1 in
- let foo (n2,h2) =
- if (is_hidentity h2) then [el (n2-1) ids1]
- else hiproof_outs h2 in
- flat (map foo nhs2)
- | Hsequence (h1,h2) -> hiproof_outs h2
- | Htensor hs -> flat (map hiproof_outs hs)
- | Hempty -> [];;
-
-
-(* Graph production *)
-
-let rec hiproof_graph0 h =
- match h with
- Hactive _ -> []
- | Hatomic _ -> []
- | Hidentity _ -> []
- | Hlabelled (l,Hatomic (id,_))
- -> [Box (l, [Single id])]
- | Hlabelled (l,h0)
- -> [Box (l, hiproof_graph0 h0)]
- | Hsequence (h1,h2)
- -> let idids = zip (hiproof_outs h1) (hiproof_ins h2) in
- let idids' = filter (fun (_,id2) -> (id2 > 0)) idids in
- (hiproof_graph0 h1) @
- (map (fun idid -> Line idid) idids') @
- (hiproof_graph0 h2)
- | Htensor hs -> flat (map hiproof_graph0 hs)
- | Hempty -> [];;
-
-let hiproof_graph h =
- let ges = hiproof_graph0 h in
- let ids = graph_nodes ges in
- let tacname_of_id id = (fst o gtree_tactic1 o get_gtree) id in
- let ges' = map (fun id -> Name (id, tacname_of_id id)) ids in
- ges' @ ges;;
-
-
-
-(* ** OTHER OPERATIONS ** *)
-
-
-(* Tactic trace *)
-
-(* Gives a linear trace of the basic tactics used in the proof, ignoring how
*)
-(* they were combined by tacticals.
*)
-
-let rec hiproof_tactic_trace0 h =
- match h with
- Hactive _
- -> [active_info]
- | Hatomic (id, _)
- -> [gtree_tactic (get_gtree id)]
- | Hidentity _
- -> []
- | Hlabelled (_,h0)
- -> hiproof_tactic_trace0 h0
- | Hsequence (h1,h2)
- -> (hiproof_tactic_trace0 h1) @ (hiproof_tactic_trace0 h2)
- | Htensor hs
- -> flat (map hiproof_tactic_trace0 hs)
- | Hempty
- -> [];;
-
-let hiproof_tactic_trace h = (hiproof_tactic_trace0 o delabel_hiproof) h;;
-
-
-(* Block trace *)
-
-(* Gives a linear trace of the hiproofs used in the proof, stopping at boxes.
*)
-
-let rec hiproof_block_trace0 ns0 h =
- match h with
- | Hsequence (h1,h2)
- -> (hiproof_block_trace0 ns0 h1) @ (hiproof_block_trace0 ns0 h2)
- | Htensor hs
- -> let nss = map (fun n -> ns0 @ [n]) (1 -- length hs) in
- flat (map (fun (ns,h) -> (Hicomment ns) :: hiproof_block_trace0 ns h)
- (zip nss hs))
- | _ -> [Hiproof h];;
-
-let hiproof_block_trace h = hiproof_block_trace0 [] h;;
diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml
deleted file mode 100644
index 5de2833..0000000
--- a/hol-light/TacticRecording/lib.ml
+++ /dev/null
@@ -1,91 +0,0 @@
-
-let rec copy n x =
- if (n > 0) then x::(copy (n-1) x)
- else [];;
-
-
-let rec enumerate0 n xs =
- match xs with
- [] -> []
- | x::xs0 -> (n,x)::enumerate0 (n+1) xs0;;
-let enumerate xs = enumerate0 1 xs;;
-
-
-(* foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
*)
-
-let rec foldr f xs a =
- match xs with
- x1::xs2 -> f x1 (foldr f xs2 a)
- | [] -> a;;
-
-
-(* foldr1 : ('a -> 'a -> 'a) -> 'a list -> 'a
*)
-
-let rec foldr1 f xs =
- match xs with
- x::[] -> x
- | x1::xs2 -> f x1 (foldr1 f xs2)
- | [] -> failwith "foldr1: Empty list";;
-
-
-(* foldl : ('b -> 'a -> 'b) -> 'b -> 'a list -> 'b
*)
-
-let rec foldl f a xs =
- match xs with
- x1::xs2 -> foldl f (f a x1) xs2
- | [] -> a;;
-
-
-(* is_empty *)
-
-let is_empty xs =
- match xs with
- [] -> true
- | _ -> false;;
-
-
-(* front *)
-
-let rec front xs =
- match xs with
- _::[] -> []
- | x0::xs0 -> x0::(front xs0)
- | [] -> failwith "front: Empty list";;
-
-
-(* string_option *)
-
-let string_option x0 x_ =
- match x_ with
- Some x -> x
- | None -> x0;;
-
-
-(* print_option *)
-
-let print_option x0 x_ =
- match x_ with
- Some x -> print_string x
- | None -> print_string x0;;
-
-
-(* seplists *)
-
-let print_seplist p sep xs =
- if (xs = [])
- then ()
- else (p (hd xs);
- do_list (fun x -> print_string sep; p x) (tl xs));;
-
-let print_string_seplist sep xs =
- print_seplist print_string sep xs;;
-
-
-(* sum *)
-
-let sum ns = foldl (+) 0 ns;;
-
-
-(* snd_map *)
-
-let snd_map f xys = map (fun (x,y) -> (x, f y)) xys;;
diff --git a/hol-light/TacticRecording/main.ml
b/hol-light/TacticRecording/main.ml
deleted file mode 100644
index 57c8254..0000000
--- a/hol-light/TacticRecording/main.ml
+++ /dev/null
@@ -1,31 +0,0 @@
-(* Library stuff *)
-
-#use "TacticRecording/lib.ml";;
-#use "TacticRecording/dltree.mli";;
-#use "TacticRecording/dltree.ml";;
-
-(* Datatypes and recording mechanism *)
-
-#use "TacticRecording/mldata.ml";;
-#use "TacticRecording/xthm.ml";;
-#use "TacticRecording/xtactics.ml";;
-#use "TacticRecording/tacticrec.ml";;
-#use "TacticRecording/wrappers.ml";;
-
-(* Prooftree support *)
-
-#use "TacticRecording/prooftree.ml";;
-
-(* Hiproofs & refactoring *)
-
-#use "TacticRecording/hiproofs.ml";;
-
-(* Export *)
-
-#use "TacticRecording/printutils.ml";;
-#use "TacticRecording/gvexport.ml";;
-#use "TacticRecording/mlexport.ml";;
-
-(* Overwriting the existing HOL Light objects *)
-
-#use "TacticRecording/promote.ml";;
diff --git a/hol-light/TacticRecording/mldata.ml
b/hol-light/TacticRecording/mldata.ml
deleted file mode 100644
index b547a89..0000000
--- a/hol-light/TacticRecording/mldata.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-
-
-type mlarg =
- Mlint of int
- | Mlstring of string
- | Mlterm of term
- | Mltype of hol_type
- | Mlthm of mldata
- | Mlpair of mlarg * mlarg
- | Mllist of mlarg list
- | Mlfn of mldata
-
-and mldata = string * mlarg list;; (* ML object name and args *)
-
-
-type label =
- Tactical of mldata
- | Label of string;;
-
-
-(* Atomic tests *)
-
-let is_atomic_mlarg arg =
- match arg with
- Mlthm (_,(_::_)) | Mlpair _ | Mlfn (_, _::_) -> false
- | _ -> true;;
-
-let is_atomic_mldata ((x,args):mldata) = (is_empty args);;
-
-
-(* active_info *)
-
-let active_info = ("...",[]);;
diff --git a/hol-light/TacticRecording/mlexport.ml
b/hol-light/TacticRecording/mlexport.ml
deleted file mode 100644
index 9a9207d..0000000
--- a/hol-light/TacticRecording/mlexport.ml
+++ /dev/null
@@ -1,186 +0,0 @@
-(* ==========================================================================
*)
-(* ML EXPORT (HOL LIGHT)
*)
-(* - Exporting recorded tactics into a proof script
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2012
*)
-(* ==========================================================================
*)
-
-
-(* Routines for exporting an ML tactic proof script from the recorded tactic
*)
-(* proof tree, via a hiproof representation.
*)
-
-
-
-(* ** UTILS ** *)
-
-
-(* Printer for tactic is just the ML data printer *)
-
-let print_tactic br obj = print_mldata br obj;;
-
-
-(* Printer for subgoal comments *)
-
-let print_hicomment_line ns =
- (print_string "(* *** Subgoal ";
- print_int (hd ns);
- do_list (fun n -> print_string "."; print_int n) (tl ns);
- print_string " *** *)\n");;
-
-
-(* print_tactic_line *)
-
-let print_tactic_line_with pr arg =
- (print_string "e ("; pr false arg; print_string ");;\n");;
-
-let print_tactic_line obj =
- (print_tactic_line_with print_tactic obj);;
-
-let print_hitrace_line_with fl pr htr =
- match htr with
- Hicomment ns -> if fl then print_hicomment_line ns
- | Hiproof h -> print_tactic_line_with pr h;;
-
-
-(* print_hiproof0 *)
-
-(* This is a utility used in exporters, for basic cases not explicitly dealt
*)
-(* with in the exporter's special cases. Does not print tacticals, other
*)
-(* than 'THEN' (for single arity) and 'THENL' (for multi-arity). Argument
*)
-(* 'pr' is the printer to be used on subcases.
*)
-
-let print_hiproof0 pr br h =
- match h with
- Hactive _
- -> print_string "..."
- | Hatomic (id,_)
- -> print_tactic br (gtree_tactic (get_gtree id))
- | Hidentity _
- -> print_string "ALL_TAC"
- | Hlabelled (_,h0)
- -> pr br h0
- | Hsequence (h1, Htensor h2s)
- -> (print_string_if br "(";
- pr false h1;
- print_string " THENL [";
- print_seplist (pr false) "; " h2s;
- print_string "]";
- print_string_if br ")")
- | Hsequence (h1,Hempty)
- -> (pr br h1)
- | Hsequence (h1,h2)
- -> (print_string_if br "(";
- pr false h1;
- print_string " THEN ";
- pr true h2;
- print_string_if br ")")
- | Htensor _
- -> failwith "print_hiproof: Unexpected tensor"
- | Hempty
- -> failwith "print_hiproof: Unexpected empty";;
-
-
-(* A basic hiproof printer that just uses 'print_hiproof0'.
*)
-
-let rec print_hiproof1 br h = print_hiproof0 print_hiproof1 br h;;
-
-
-(* print_hiproof2 *)
-
-let rec print_hiproof2 br h =
- match h with
- Hlabelled (Tactical ("REPEAT", _), Hsequence (h1,h2)) (* if repeated *)
- -> (print_string_if br "(";
- print_string "REPEAT ";
- print_hiproof2 true h1;
- print_string_if br ")")
- | Hlabelled (Tactical ("THEN", _), (* if tac2 used *)
- Hsequence (h1, Htensor (h2::h2s)))
- -> (print_string_if br "(";
- print_hiproof2 false h1;
- print_string " THEN ";
- print_hiproof2 true h2;
- print_string_if br ")")
- | Hlabelled (Tactical (("SUBGOAL_THEN", (* special case *)
- (Mlterm tm)::[_]) as obj),
- _)
- -> (print_tactic br obj)
- | Hlabelled (Label x, h)
- -> (print_string_if br "(";
- print_string "HILABEL ";
- print_fstring x; print_string " ";
- print_hiproof2 true h;
- print_string_if br ")")
- | _ -> (print_hiproof0 print_hiproof2 br h);;
-
-
-
-(* ** PRINTERS ** *)
-
-
-(* Executed proof *)
-
-(* Prints proof according to how it was executed, i.e. using the original e-
*)
-(* steps and according to any user-supplied 'REPEAT' and 'THEN' tacticals,
*)
-(* but only those parts that actually execute and not according to any other
*)
-(* tacticals.
*)
-
-let print_hiproof_executed_proof fl h =
- let h' = trivsimp_hiproof h in
- let htrs' = hiproof_block_trace h' in
- do_list (print_hitrace_line_with fl print_hiproof2) htrs';;
-
-let print_gtree_executed_proof fl gtr =
- (print_hiproof_executed_proof fl o gtree_to_hiproof) gtr;;
-
-let print_executed_proof fl = print_gtree_executed_proof fl !the_goal_tree;;
-
-
-(* Packaged proof *)
-
-(* Prints proof as a monolithic step, spotting opportunities for 'REPEAT' and
*)
-(* multi-arity 'THEN' tacticals in addition to those already in proof.
*)
-(* ! 'REPEAT' not currently catered for.
*)
-
-let print_hiproof_packaged_proof h =
- let h' = (trivsimp_hiproof o thenise_hiproof o
- trivsimp_hiproof o leftgroup_hiproof) h in
- print_tactic_line_with print_hiproof2 h';;
-
-let print_gtree_packaged_proof gtr =
- (print_hiproof_packaged_proof o gtree_to_hiproof) gtr;;
-
-let print_packaged_proof () = print_gtree_packaged_proof !the_goal_tree;;
-
-
-(* THENL proof *)
-
-(* Prints proof as a naive monolithic step, using 'THEN' for single arity,
*)
-(* and 'THENL' for multi-arity (even if each subgoal has the same proof).
*)
-(* This gives the full structure of each tactic execution.
*)
-
-let print_hiproof_thenl_proof h =
- let h' = (trivsimp_hiproof o delabel_hiproof) h in
- print_tactic_line_with print_hiproof1 h';;
-
-let print_gtree_thenl_proof gtr =
- (print_hiproof_thenl_proof o gtree_to_hiproof) gtr;;
-
-let print_thenl_proof () = print_gtree_thenl_proof !the_goal_tree;;
-
-
-(* Flat proof *)
-
-(* This exports a proof as a flat series of e-steps, with no tacticals.
*)
-
-let print_hiproof_flat_proof fl h =
- let h' = (trivsimp_hiproof o rightgroup_hiproof o trivsimp_hiproof o
- delabel_hiproof) h in
- let htrs' = hiproof_block_trace h' in
- do_list (print_hitrace_line_with fl print_hiproof2) htrs';;
-
-let print_gtree_flat_proof fl gtr =
- (print_hiproof_flat_proof fl o gtree_to_hiproof) gtr;;
-
-let print_flat_proof fl = print_gtree_flat_proof fl !the_goal_tree;;
diff --git a/hol-light/TacticRecording/printutils.ml
b/hol-light/TacticRecording/printutils.ml
deleted file mode 100644
index aa74ee2..0000000
--- a/hol-light/TacticRecording/printutils.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-(* ==========================================================================
*)
-(* PRINTER UTILITIES (HOL LIGHT)
*)
-(* - Various basic utilities used in writing the exporters
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2012
*)
-(* ==========================================================================
*)
-
-
-(* Basics *)
-
-let print_string_if b x = if b then print_string x;;
-
-let print_fstring x = print_string ("\"" ^ String.escaped x ^ "\"");;
-
-let print_fterm tm = print_string ("`" ^ string_of_term tm ^ "`");;
-
-let print_ftype ty = print_string ("`" ^ string_of_type ty ^ "`");;
-
-let print_goalid id = print_int id;;
-
-let print_indent d = print_string (String.make d ' ');;
-
-
-(* Printer for 'mldata' *)
-
-let rec print_mlarg br arg =
- match arg with
- Mlint n -> print_int n
- | Mlstring x -> print_fstring x
- | Mlterm tm -> print_fterm tm
- | Mltype ty -> print_ftype ty
- | Mlthm prf -> print_mldata br prf
- | Mlpair (arg1,arg2)
- -> let sep =
- if (forall is_atomic_mlarg [arg1;arg2]) then "," else ", " in
- (print_string_if br "(";
- print_mlarg false arg1;
- print_string sep;
- print_mlarg false arg2;
- print_string_if br ")")
- | Mllist args
- -> let sep = if (forall is_atomic_mlarg args) then ";" else "; " in
- (print_string "[";
- print_seplist (print_mlarg false) sep args;
- print_string "]")
- | Mlfn f
- -> (print_mldata br f)
-
-and print_mldata br ((x,args):mldata) =
- (print_string_if (br & not (is_empty args)) "(";
- print_string x;
- do_list (fun arg -> print_string " "; print_mlarg true arg) args;
- print_string_if (br & not (is_empty args)) ")");;
-
-
-(* Printer for labels *)
-
-let print_label l =
- match l with
- Tactical (x,_) | Label x -> print_fstring x;;
diff --git a/hol-light/TacticRecording/promote.ml
b/hol-light/TacticRecording/promote.ml
deleted file mode 100644
index c19abb8..0000000
--- a/hol-light/TacticRecording/promote.ml
+++ /dev/null
@@ -1,327 +0,0 @@
-(* ==========================================================================
*)
-(* PROMOTTION (HOL LIGHT)
*)
-(* - Overwrites original HOL Light tactics/etc with xgoal/xthm versions
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2012
*)
-(* ==========================================================================
*)
-
-
-
-(* ** TACTICS.ML ** *)
-
-
-(* Tactics *)
-
-(* Atomic tactics can be automatically promoted to deal with xgoals and
*)
-(* recording.
*)
-
-let NO_TAC = tactic_wrap "NO_TAC" NO_TAC;;
-let ALL_TAC = tactic_wrap "ALL_TAC" ALL_TAC;;
-
-let LABEL_TAC = stringthm_tactic_wrap "LABEL_TAC" LABEL_TAC;;
-let ASSUME_TAC = thm_tactic_wrap "ASSUME_TAC" ASSUME_TAC;;
-
-let ACCEPT_TAC = thm_tactic_wrap "ACCEPT_TAC" ACCEPT_TAC;;
-
-let CONV_TAC = conv_tactic_wrap "CONV_TAC" CONV_TAC;;
-
-let REFL_TAC = tactic_wrap "REFL_TAC" REFL_TAC;;
-let ABS_TAC = tactic_wrap "ABS_TAC" ABS_TAC;;
-let MK_COMB_TAC = tactic_wrap "MK_COMB_TAC" MK_COMB_TAC;;
-let AP_TERM_TAC = tactic_wrap "AP_TERM_TAC" AP_TERM_TAC;;
-let AP_THM_TAC = tactic_wrap "AP_THM_TAC" AP_THM_TAC;;
-let BINOP_TAC = tactic_wrap "BINOP_TAC" BINOP_TAC;;
-let SUBST1_TAC = thm_tactic_wrap "SUBST1_TAC" SUBST1_TAC;;
-let SUBST_ALL_TAC = thm_tactic_wrap "SUBST_ALL_TAC" SUBST_ALL_TAC;;
-let BETA_TAC = tactic_wrap "BETA_TAC" BETA_TAC;;
-
-let SUBST_VAR_TAC = thm_tactic_wrap "SUBST_VAR_TAC" SUBST_VAR_TAC;;
-
-let DISCH_TAC = tactic_wrap "DISCH_TAC" DISCH_TAC;;
-let MP_TAC = thm_tactic_wrap "MP_TAC" MP_TAC;;
-let EQ_TAC = tactic_wrap "EQ_TAC" EQ_TAC;;
-let UNDISCH_TAC = term_tactic_wrap "UNDISCH_TAC" UNDISCH_TAC;;
-let SPEC_TAC = termpair_tactic_wrap "SPEC_TAC" SPEC_TAC;;
-let X_GEN_TAC = term_tactic_wrap "X_GEN_TAC" X_GEN_TAC;;
-let GEN_TAC = tactic_wrap "GEN_TAC" GEN_TAC;;
-let EXISTS_TAC = term_tactic_wrap "EXISTS_TAC" EXISTS_TAC;;
-let CHOOSE_TAC = thm_tactic_wrap "CHOOSE_TAC" CHOOSE_TAC;;
-let CONJ_TAC = tactic_wrap "CONJ_TAC" CONJ_TAC;;
-let DISJ1_TAC = tactic_wrap "DISJ1_TAC" DISJ1_TAC;;
-let DISJ2_TAC = tactic_wrap "DISJ2_TAC" DISJ2_TAC;;
-let DISJ_CASES_TAC = thm_tactic_wrap "DISJ_CASES_TAC" DISJ_CASES_TAC;;
-let CONTR_TAC = thm_tactic_wrap "CONTR_TAC" CONTR_TAC;;
-let MATCH_ACCEPT_TAC = thm_tactic_wrap "MATCH_ACCEPT_TAC" MATCH_ACCEPT_TAC;;
-let MATCH_MP_TAC = thm_tactic_wrap "MATCH_MP_TAC" MATCH_MP_TAC;;
-
-let STRIP_ASSUME_TAC = thm_tactic_wrap "STRIP_ASSUME_TAC" STRIP_ASSUME_TAC;;
-let STRUCT_CASES_TAC = thm_tactic_wrap "STRUCT_CASES_TAC" STRUCT_CASES_TAC;;
-let STRIP_TAC = tactic_wrap "STRIP_TAC" STRIP_TAC;;
-
-let X_META_EXISTS_TAC = term_tactic_wrap "X_META_EXISTS_TAC"
X_META_EXISTS_TAC;;
-let META_EXISTS_TAC = tactic_wrap "META_EXISTS_TAC" META_EXISTS_TAC;;
-
-let ANTS_TAC = tactic_wrap "ANTS_TAC" ANTS_TAC;;
-
-
-(* Special cases, already fully hand-promoted *)
-
-let SUBGOAL_THEN = xSUBGOAL_THEN;;
-
-
-(* Tacticals *)
-
-(* Tacticals need to be hand-promoted to deal with xgoals, but this is
*)
-(* trivial and is done in 'xtactics.ml'. They are further promoted here to
*)
-(* get recorded as boxes, using the tactical-wrap functions.
*)
-
-let (THEN) = btactical_wrap "THEN" (xTHEN);;
-let (THENL) = btactical_wrap "THENL" (xTHENL);;
-let (ORELSE) = btactical_wrap "ORELSE" (xORELSE);;
-let TRY = tactical_wrap "TRY" xTRY;;
-let REPEAT = tactical_wrap "REPEAT" xREPEAT;;
-let EVERY = tactical_wrap "EVERY" xEVERY;;
-let FIRST = tactical_wrap "FIRST" xFIRST;;
-let MAP_EVERY = list_tactical_wrap "MAP_EVERY" xMAP_EVERY;;
-let MAP_FIRST = list_tactical_wrap "MAP_FIRST" xMAP_FIRST;;
-let CHANGED_TAC = tactical_wrap "CHANGED_TAC" xCHANGED_TAC;;
-let REPLICATE_TAC = int_tactical_wrap "REPLICATE_TAC" xREPLICATE_TAC;;
-
-
-(* Subgoal commands *)
-
-let e = xe;;
-let r = xr;;
-let set_goal = xset_goal;;
-let g = xg;;
-let b = xb;;
-let p = xp;;
-let top_goal = xtop_goal;;
-let top_thm = xtop_thm;;
-
-let prove = xprove;;
-
-
-
-(* ** COMMON HOL API ** *)
-
-
-(* Rules *)
-
-let ADD_ASSUM = term_rule_wrap "ADD_ASSUM" ADD_ASSUM;;
-let ASSUME = conv_wrap "ASSUME" ASSUME;;
-let BETA_CONV = conv_wrap "BETA_CONV" BETA_CONV;;
-let CCONTR = term_rule_wrap "CCONTR" CCONTR;;
-let CHOOSE = termthmpair_rule_wrap "CHOOSE" CHOOSE;;
-let CONJ = drule_wrap "CONJ" CONJ;;
-let CONJUNCT1 = rule_wrap "CONJUNCT1" CONJUNCT1;;
-let CONJUNCT2 = rule_wrap "CONJUNCT2" CONJUNCT2;;
-let CONTR = term_rule_wrap "CONTR" CONTR;;
-let DEDUCT_ANTISYM_RULE = drule_wrap "DEDUCT_ANTISYM_RULE"
DEDUCT_ANTISYM_RULE;;
-let DISCH = term_rule_wrap "DISCH" DISCH;;
-let DISJ1 = thm_conv_wrap "DISJ1" DISJ1;;
-let DISJ2 = term_rule_wrap "DISJ2" DISJ2;;
-let DISJ_CASES = trule_wrap "DISJ_CASES" DISJ_CASES;;
-let EQ_MP = drule_wrap "EQ_MP" EQ_MP;;
-let EQF_INTRO = rule_wrap "EQF_INTRO" EQF_INTRO;;
-let EQF_ELIM = rule_wrap "EQF_ELIM" EQF_ELIM;;
-let EQT_INTRO = rule_wrap "EQT_INTRO" EQT_INTRO;;
-let EQT_ELIM = rule_wrap "EQT_ELIM" EQT_ELIM;;
-let ETA_CONV = conv_wrap "ETA_CONV" ETA_CONV;;
-let EXISTS = termpair_rule_wrap "EXISTS" EXISTS;;
-let GEN = term_rule_wrap "GEN" GEN;;
-let GENL = termlist_rule_wrap "GENL" GENL;;
-let IMP_ANTISYM_RULE = drule_wrap "IMP_ANTISYM_RULE" IMP_ANTISYM_RULE;;
-let IMP_TRANS = drule_wrap "IMP_TRANS" IMP_TRANS;;
-let INST = terminst_rule_wrap "INST" INST;;
-let INST_TYPE = typeinst_rule_wrap "INST_TYPE" INST_TYPE;;
-let MP = drule_wrap "MP" MP;;
-let NOT_ELIM = rule_wrap "NOT_ELIM" NOT_ELIM;;
-let NOT_INTRO = rule_wrap "NOT_INTRO" NOT_INTRO;;
-let PROVE_HYP = drule_wrap "PROVE_HYP" PROVE_HYP;;
-let REFL = conv_wrap "REFL" REFL;;
-let SELECT_RULE = rule_wrap "SELECT_RULE" SELECT_RULE;;
-let SPEC = term_rule_wrap "SPEC" SPEC;;
-let SPECL = termlist_rule_wrap "SPECL" SPECL;;
-let SUBS = thmlist_rule_wrap "SUBS" SUBS;;
-let SUBS_CONV = thmlist_conv_wrap "SUBS_CONV" SUBS_CONV;;
-let SYM = rule_wrap "SYM" SYM;;
-let SYM_CONV = conv_wrap "SYM_CONV" SYM_CONV;;
-let TRANS = drule_wrap "TRANS" TRANS;;
-let UNDISCH = rule_wrap "UNDISCH" UNDISCH;;
-
-let ABS = term_rule_wrap "ABS" ABS;;
-let MK_COMB = prule_wrap "MK_COMB" MK_COMB;;
-let AP_THM = thm_conv_wrap "AP_THM" AP_THM;;
-let AP_TERM = term_rule_wrap "AP_TERM" AP_TERM;;
-
-let NUM_SUC_CONV = conv_wrap "NUM_SUC_CONV" NUM_SUC_CONV;;
-let NUM_PRE_CONV = conv_wrap "NUM_PRE_CONV" NUM_PRE_CONV;;
-let NUM_ADD_CONV = conv_wrap "NUM_ADD_CONV" NUM_ADD_CONV;;
-let NUM_SUB_CONV = conv_wrap "NUM_SUB_CONV" NUM_SUB_CONV;;
-let NUM_MULT_CONV = conv_wrap "NUM_MULT_CONV" NUM_MULT_CONV;;
-let NUM_EXP_CONV = conv_wrap "NUM_EXP_CONV" NUM_EXP_CONV;;
-let NUM_EQ_CONV = conv_wrap "NUM_EQ_CONV" NUM_EQ_CONV;;
-let NUM_LT_CONV = conv_wrap "NUM_LT_CONV" NUM_LT_CONV;;
-let NUM_LE_CONV = conv_wrap "NUM_LE_CONV" NUM_LE_CONV;;
-let NUM_GT_CONV = conv_wrap "NUM_GT_CONV" NUM_GT_CONV;;
-let NUM_EVEN_CONV = conv_wrap "NUM_EVEN_CONV" NUM_EVEN_CONV;;
-let NUM_ODD_CONV = conv_wrap "NUM_ODD_CONV" NUM_ODD_CONV;;
-
-
-(* Theorems *)
-
-let ETA_AX = theorem_wrap "ETA_AX" ETA_AX;;
-let INFINITY_AX = theorem_wrap "INFINITY_AX" INFINITY_AX;;
-let BOOL_CASES_AX = theorem_wrap "BOOL_CASES_AX" BOOL_CASES_AX;;
-let SELECT_AX = theorem_wrap "SELECT_AX" SELECT_AX;;
-let TRUTH = theorem_wrap "TRUTH" TRUTH;;
-let EXCLUDED_MIDDLE = theorem_wrap "EXCLUDED_MIDDLE" EXCLUDED_MIDDLE;;
-
-let PAIR_EQ = theorem_wrap "PAIR_EQ" PAIR_EQ;;
-let PAIR_SURJECTIVE = theorem_wrap "PAIR_SURJECTIVE" PAIR_SURJECTIVE;;
-let FST = theorem_wrap "FST" FST;;
-let SND = theorem_wrap "SND" SND;;
-
-let IND_SUC_0 = theorem_wrap "IND_SUC_0" IND_SUC_0;;
-let IND_SUC_INJ = theorem_wrap "IND_SUC_INJ" IND_SUC_INJ;;
-
-let NOT_SUC = theorem_wrap "NOT_SUC" NOT_SUC;;
-let SUC_INJ = theorem_wrap "SUC_INJ" SUC_INJ;;
-let num_INDUCTION = theorem_wrap "num_INDUCTION" num_INDUCTION;;
-let num_CASES = theorem_wrap "num_CASES" num_CASES;;
-let num_RECURSION = theorem_wrap "num_RECURSION" num_RECURSION;;
-let PRE = theorem_wrap "PRE" PRE;;
-let ADD = theorem_wrap "ADD" ADD;;
-let SUB = theorem_wrap "SUB" SUB;;
-let MULT = theorem_wrap "MULT" MULT;;
-let EXP = theorem_wrap "EXP" EXP;;
-let LT = theorem_wrap "LT" LT;;
-let LE = theorem_wrap "LE" LE;;
-let GT = theorem_wrap "GT" GT;;
-let GE = theorem_wrap "GE" GE;;
-let EVEN = theorem_wrap "EVEN" EVEN;;
-let ODD = theorem_wrap "ODD" ODD;;
-
-
-
-(* ** OTHER HOL LIGHT ** *)
-
-
-(* More tactics *)
-
-let REWRITE_TAC = thmlist_tactic_wrap "REWRITE_TAC" REWRITE_TAC;;
-let PURE_REWRITE_TAC = thmlist_tactic_wrap "PURE_REWRITE_TAC"
PURE_REWRITE_TAC;;
-let ONCE_REWRITE_TAC = thmlist_tactic_wrap "ONCE_REWRITE_TAC"
ONCE_REWRITE_TAC;;
-let ASM_REWRITE_TAC = thmlist_tactic_wrap "ASM_REWRITE_TAC" ASM_REWRITE_TAC;;
-let PURE_ASM_REWRITE_TAC =
- thmlist_tactic_wrap "PURE_ASM_REWRITE_TAC" PURE_ASM_REWRITE_TAC;;
-let ONCE_ASM_REWRITE_TAC =
- thmlist_tactic_wrap "ONCE_ASM_REWRITE_TAC" ONCE_ASM_REWRITE_TAC;;
-let GEN_REWRITE_TAC =
- convconvthmlist_tactic_wrap "GEN_REWRITE_TAC" GEN_REWRITE_TAC;;
-let SIMP_TAC = thmlist_tactic_wrap "SIMP_TAC" SIMP_TAC;;
-let PURE_SIMP_TAC = thmlist_tactic_wrap "PURE_SIMP_TAC" PURE_SIMP_TAC;;
-let ONCE_SIMP_TAC = thmlist_tactic_wrap "ONCE_SIMP_TAC" ONCE_SIMP_TAC;;
-let ASM_SIMP_TAC = thmlist_tactic_wrap "ASM_SIMP_TAC" ASM_SIMP_TAC;;
-let PURE_ASM_SIMP_TAC =
- thmlist_tactic_wrap "PURE_ASM_SIMP_TAC" PURE_ASM_SIMP_TAC;;
-let ONCE_ASM_SIMP_TAC =
- thmlist_tactic_wrap "ONCE_ASM_SIMP_TAC" ONCE_ASM_SIMP_TAC;;
-let ABBREV_TAC = term_tactic_wrap "ABBREV_TAC" ABBREV_TAC;;
-let EXPAND_TAC = string_tactic_wrap "EXPAND_TAC" EXPAND_TAC;;
-
-let ASM_CASES_TAC = term_tactic_wrap "ASM_CASES_TAC" ASM_CASES_TAC;;
-let COND_CASES_TAC = tactic_wrap "COND_CASES_TAC" COND_CASES_TAC;;
-
-let ARITH_TAC = tactic_wrap "ARITH_TAC" ARITH_TAC;;
-let INDUCT_TAC = tactic_wrap "INDUCT_TAC" INDUCT_TAC;;
-
-let REAL_ARITH_TAC = tactic_wrap "REAL_ARITH_TAC" REAL_ARITH_TAC;;
-let ASM_REAL_ARITH_TAC = tactic_wrap "ASM_REAL_ARITH_TAC" ASM_REAL_ARITH_TAC;;
-
-
-(* More rules *)
-
-let RATOR_CONV = conv_conv_wrap "RATOR_CONV" RATOR_CONV;;
-let RAND_CONV = conv_conv_wrap "RAND_CONV" RAND_CONV;;
-let LAND_CONV = conv_conv_wrap "LAND_CONV" LAND_CONV;;
-let ABS_CONV = conv_conv_wrap "ABS_CONV" ABS_CONV;;
-let BINDER_CONV = conv_conv_wrap "BINDER_CONV" BINDER_CONV;;
-let SUB_CONV = conv_conv_wrap "SUB_CONV" SUB_CONV;;
-let BINOP_CONV = conv_conv_wrap "BINOP_CONV" BINOP_CONV;;
-let GSYM = rule_wrap "GSYM" GSYM;;
-let CONJUNCTS = multirule_wrap "CONJUNCTS" CONJUNCTS;;
-let SPEC_ALL = rule_wrap "SPEC_ALL" SPEC_ALL;;
-let ISPECL = termlist_rule_wrap "ISPECL" ISPECL;;
-let ALL_CONV = conv_wrap "ALL_CONV" ALL_CONV;;
-let (REPEATC) = conv_conv_wrap "REPEATC" REPEATC;;
-let ONCE_DEPTH_CONV = conv_conv_wrap "ONCE_DEPTH_CONV" ONCE_DEPTH_CONV;;
-
-let REWRITE_RULE = thmlist_rule_wrap "REWRITE_RULE" REWRITE_RULE;;
-
-let num_CONV = conv_wrap "num_CONV" num_CONV;;
-let ARITH_RULE = conv_wrap "ARITH_RULE" ARITH_RULE;;
-
-let REAL_ARITH = conv_wrap "REAL_ARITH" REAL_ARITH;;
-let REAL_FIELD = conv_wrap "REAL_FIELD" REAL_FIELD;;
-
-
-(* More theorems *)
-
-let CONJ_ASSOC = theorem_wrap "CONJ_ASSOC" CONJ_ASSOC;;
-let IMP_IMP = theorem_wrap "IMP_IMP" IMP_IMP;;
-let EQ_IMP = theorem_wrap "EQ_IMP" EQ_IMP;;
-
-let ARITH = theorem_wrap "ARITH" ARITH;;
-let ARITH_EQ = theorem_wrap "ARITH_EQ" ARITH_EQ;;
-let ADD_ASSOC = theorem_wrap "ADD_ASSOC" ADD_ASSOC;;
-let ADD_CLAUSES = theorem_wrap "ADD_CLAUSES" ADD_CLAUSES;;
-let LEFT_ADD_DISTRIB = theorem_wrap "LEFT_ADD_DISTRIB" LEFT_ADD_DISTRIB;;
-let RIGHT_ADD_DISTRIB = theorem_wrap "RIGHT_ADD_DISTRIB" RIGHT_ADD_DISTRIB;;
-let MULT_CLAUSES =theorem_wrap "MULT_CLAUSES" MULT_CLAUSES;;
-let SUB_REFL = theorem_wrap "SUB_REFL" SUB_REFL;;
-let ADD1 = theorem_wrap "ADD1" ADD1;;
-let EQ_MULT_LCANCEL = theorem_wrap "EQ_MULT_LCANCEL" EQ_MULT_LCANCEL;;
-let LE_EXISTS = theorem_wrap "LE_EXISTS" LE_EXISTS;;
-let LE_ADD = theorem_wrap "LE_ADD" LE_ADD;;
-let LE_1 = theorem_wrap "LE_1" LE_1;;
-let LE_REFL = theorem_wrap "LE_REFL" LE_REFL;;
-let LT_SUC = theorem_wrap "LT_SUC" LT_SUC;;
-let LT_EXISTS = theorem_wrap "LT_EXISTS" LT_EXISTS;;
-let LT_NZ = theorem_wrap "LT_NZ" LT_NZ;;
-let EXP_EQ_0 = theorem_wrap "EXP_EQ_0" EXP_EQ_0;;
-let FACT = theorem_wrap "FACT" FACT;;
-let = theorem_wrap "" ;;
-
-let REAL_ADD_LDISTRIB = theorem_wrap "REAL_ADD_LDISTRIB" REAL_ADD_LDISTRIB;;
-let REAL_OF_NUM_ADD = theorem_wrap "REAL_OF_NUM_ADD" REAL_OF_NUM_ADD;;
-let REAL_OF_NUM_EQ = theorem_wrap "REAL_OF_NUM_EQ" REAL_OF_NUM_EQ;;
-let REAL_OF_NUM_SUC = theorem_wrap "REAL_OF_NUM_SUC" REAL_OF_NUM_SUC;;
-let REAL_MUL_ASSOC = theorem_wrap "REAL_MUL_ASSOC" REAL_MUL_ASSOC;;
-let REAL_MUL_SYM = theorem_wrap "REAL_MUL_SYM" REAL_MUL_SYM;;
-let REAL_MUL_RID = theorem_wrap "REAL_MUL_RID" REAL_MUL_RID;;
-let REAL_MUL_RZERO = theorem_wrap "REAL_MUL_RZERO" REAL_MUL_RZERO;;
-let REAL_DIV_LMUL = theorem_wrap "REAL_DIV_LMUL" REAL_DIV_LMUL;;
-let REAL_POS = theorem_wrap "REAL_POS" REAL_POS;;
-let REAL_LE_TRANS = theorem_wrap "REAL_LE_TRANS" REAL_LE_TRANS;;
-let REAL_LE_MUL = theorem_wrap "REAL_LE_MUL" REAL_LE_MUL;;
-let REAL_LE_RMUL = theorem_wrap "REAL_LE_RMUL" REAL_LE_RMUL;;
-let REAL_LE_DIV = theorem_wrap "REAL_LE_DIV" REAL_LE_DIV;;
-let REAL_LE_SQUARE = theorem_wrap "REAL_LE_SQUARE" REAL_LE_SQUARE;;
-let REAL_LE_RDIV_EQ = theorem_wrap "REAL_LE_RDIV_EQ" REAL_LE_RDIV_EQ;;
-let real_pow = theorem_wrap "real_pow" real_pow;;
-let REAL_POW_2 = theorem_wrap "REAL_POW_2" REAL_POW_2;;
-let REAL_POW_ZERO = theorem_wrap "REAL_POW_ZERO" REAL_POW_ZERO;;
-let REAL_POW_ADD = theorem_wrap "REAL_POW_ADD" REAL_POW_ADD;;
-let REAL_POW_DIV = theorem_wrap "REAL_POW_DIV" REAL_POW_DIV;;
-let REAL_POW_LE = theorem_wrap "REAL_POW_LE" REAL_POW_LE;;
-let REAL_POW_LT = theorem_wrap "REAL_POW_LT" REAL_POW_LT;;
-let SUM_RMUL = theorem_wrap "SUM_RMUL" SUM_RMUL;;
-let SUM_ADD_SPLIT = theorem_wrap "SUM_ADD_SPLIT" SUM_ADD_SPLIT;;
-let SUM_POS_LE_NUMSEG = theorem_wrap "SUM_POS_LE_NUMSEG" SUM_POS_LE_NUMSEG;;
-let SUM_CLAUSES_NUMSEG = theorem_wrap "SUM_CLAUSES_NUMSEG" SUM_CLAUSES_NUMSEG;;
-let SUM_SING_NUMSEG = theorem_wrap "SUM_SING_NUMSEG" SUM_SING_NUMSEG;;
-let PRODUCT_CLAUSES_NUMSEG =
- theorem_wrap "PRODUCT_CLAUSES_NUMSEG" PRODUCT_CLAUSES_NUMSEG;;
\ No newline at end of file
diff --git a/hol-light/TacticRecording/prooftree.ml
b/hol-light/TacticRecording/prooftree.ml
deleted file mode 100644
index 877e738..0000000
--- a/hol-light/TacticRecording/prooftree.ml
+++ /dev/null
@@ -1,177 +0,0 @@
-(* ========================================================================= *)
-(* HOL Light subgoal package amended for Proof General's Prooftree. *)
-(* *)
-(* Mark Adams, School of Informatics, University of Edinburgh *)
-(* *)
-(* (c) Copyright, University of Edinburgh, 2012 *)
-(* ========================================================================= *)
-
-(* This file provides alternatives to HOL Light's subgoal package commands *)
-(* that output additional annotations specifically for Prooftree. These *)
-(* annotations get intercepted by Proof General, which removes them from the *)
-(* output displayed to the Proof General user. Annotation can be switched *)
-(* off completely with the 'pg_mode_off' command. *)
-
-(* Note that this assumes the existence of xgoals (see 'xtactics.ml'). *)
-
-(* ------------------------------------------------------------------------- *)
-(* Proof General mode, for providing extra annotations for Prooftree. *)
-(* ------------------------------------------------------------------------- *)
-
-let pg_mode = ref (false : bool);;
-
-let pg_mode_on () = (pg_mode := true);;
-let pg_mode_off () = (pg_mode := false);;
-
-let get_pg_mode () = !pg_mode;;
-
-(* ------------------------------------------------------------------------- *)
-(* The Prooftree global state is an ever increasing counter. *)
-(* ------------------------------------------------------------------------- *)
-
-let the_pt_global_state = ref 1;;
-
-let inc_pt_global_state () =
- (the_pt_global_state := !the_pt_global_state + 1);;
-
-let pt_global_state () = !the_pt_global_state;;
-
-(* ------------------------------------------------------------------------- *)
-(* The Prooftree proof state is the length of the goal stack. *)
-(* ------------------------------------------------------------------------- *)
-
-let pt_proof_state () = length !current_xgoalstack;;
-
-let pt_back_to_proof_state n : xgoalstack =
- let pst = pt_proof_state () in
- if (0 <= n) & (n <= pst)
- then (current_xgoalstack :=
- snd (chop_list (pst-n) !current_xgoalstack);
- !current_xgoalstack)
- else failwith "Not a valid Prooftree state number";;
-
-(* ------------------------------------------------------------------------- *)
-(* Subgoal package commands adjusted to update Prooftree global state. *)
-(* ------------------------------------------------------------------------- *)
-
-let the_tactic_flag = ref false;;
-
-let xe tac =
- let result = xe tac in
- (inc_pt_global_state ();
- the_tactic_flag := true; (* So that special info gets displayed *)
- result);;
-
-let xr n =
- let result = xr n in
- (inc_pt_global_state ();
- result);;
-
-let xset_goal (asl,w) =
- let result = xset_goal (asl,w) in
- (inc_pt_global_state ();
- result);;
-
-let xg t =
- let fvs = sort (<) (map (fst o dest_var) (frees t)) in
- (if fvs <> [] then
- let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
- warn true ("Free variables in goal: "^errmsg)
- else ());
- xset_goal([],t);;
-
-let xb () =
- let result = xb () in
- (inc_pt_global_state ();
- result);;
-
-(* ------------------------------------------------------------------------- *)
-(* Special Prooftree printers for xgoals and xgoalstacks. *)
-(* ------------------------------------------------------------------------- *)
-
-let the_new_goal_ids = ref ([] : goalid list);;
-
-let print_prooftree_xgoal ((g,id) : xgoal) : unit =
- ((if (!pg_mode)
- then (print_string ("[Goal ID " ^ string_of_goal_id id ^ "]");
- print_newline ()));
- print_goal g);;
-
-let (print_prooftree_xgoalstack:xgoalstack->unit) =
- let print_prooftree_xgoalstate k gs =
- let (_,gl,_) = gs in
- let n = length gl in
- let s = if n = 0 then "No subgoals" else
- (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
- ^" ("^(string_of_int n)^" total)" in
- print_string s; print_newline();
- if gl = [] then () else
- (do_list (print_prooftree_xgoal o C el gl) (rev(1--(k-1)));
- (if (!pg_mode) then print_string "[*]");
- print_prooftree_xgoal (el 0 gl)) in
- fun l ->
- ((if (!pg_mode) & (!the_tactic_flag)
- then let xs = map string_of_int (!the_new_goal_ids) in
- (the_tactic_flag := false;
- print_string "[New Goal IDs: ";
- print_string_seplist " " xs;
- print_string "]";
- print_newline ()));
- (if l = [] then print_string "Empty goalstack"
- else if tl l = [] then
- let (_,gl,_ as gs) = hd l in
- print_prooftree_xgoalstate 1 gs
- else
- let (_,gl,_ as gs) = hd l
- and (_,gl0,_) = hd(tl l) in
- let p = length gl - length gl0 in
- let p' = if p < 1 then 1 else p + 1 in
- print_prooftree_xgoalstate p' gs);
- (if (!pg_mode) then
- let (vs,theta) =
- if (l = []) then ([],[])
- else let ((vs,(_,theta,_)),_,_) = hd l in
- (vs,theta) in
- let foo v =
- let (x,_) = dest_var v in
- x ^ if (can (rev_assoc v) theta) then " using" else " open" in
- let xs = map foo vs in
- (print_newline();
- print_string "(dependent evars: ";
- print_string_seplist ", " xs;
- print_string ")";
- print_newline ())));;
-
-(* ------------------------------------------------------------------------- *)
-(* Adjust the OCaml prompt to carry information for Prooftree. *)
-(* ------------------------------------------------------------------------- *)
-
-let original_prompt_fn = !Toploop.read_interactive_input in
-Toploop.read_interactive_input :=
- fun prompt buffer len ->
- let basic_prompt = "<" in (* 'prompt' arg is ignored *)
- let prompt' =
- if (!pg_mode)
- then let pst = pt_proof_state () and gst = pt_global_state () in
- "<prompt> " ^ basic_prompt ^ " " ^
- string_of_int gst ^ " || " ^ string_of_int pst ^
- " " ^ basic_prompt ^ " </prompt>"
- else prompt in
- original_prompt_fn prompt' buffer len;;
-
-(* ------------------------------------------------------------------------- *)
-(* Printing the goal of a given Prooftree goal id. *)
-(* ------------------------------------------------------------------------- *)
-
-let xgoal_of_id (id:goalid) : xgoal =
- let gsts = !current_xgoalstack in
- let find_goal (_,xgs,_) = find (fun (g,id0) -> id0 = id) xgs in
- let xg = tryfind find_goal gsts in
- xg;;
-
-(* ------------------------------------------------------------------------- *)
-(* Install the new goal-related printers. *)
-(* ------------------------------------------------------------------------- *)
-
-#install_printer print_prooftree_xgoal;;
-#install_printer print_prooftree_xgoalstack;;
diff --git a/hol-light/TacticRecording/tacticrec.ml
b/hol-light/TacticRecording/tacticrec.ml
deleted file mode 100644
index c65ee71..0000000
--- a/hol-light/TacticRecording/tacticrec.ml
+++ /dev/null
@@ -1,383 +0,0 @@
-(* ==========================================================================
*)
-(* TACTIC RECORDING (HOL LIGHT)
*)
-(* - Mechanism to record tactic proofs at the user level
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2011-2012
*)
-(* ==========================================================================
*)
-
-
-(* This file implements a mechanism for recording tactic proofs at the level
*)
-(* of interactive proof steps. A recorded proof takes the form of a tree of
*)
-(* goals, and is capable of capturing both complete and incomplete proofs, as
*)
-(* well as hierarchy correspoding to tacticals.
*)
-
-(* The crucial mechanism by which goals in the subgoal package state are
*)
-(* linked to parts of the stored goal tree is based on unique goal id
*)
-(* numbers. Each goal in the subgoal package state is annotated with such an
*)
-(* id, and this is also stored at each level of the goal tree. As a tactic
*)
-(* is executed, the id from the goal in the subgoal package state that it
*)
-(* executes on is used to locate the corresponding part of the goal tree, and
*)
-(* the ids of the resulting subgoals are used to label the corresponding
*)
-(* subparts of the goal tree.
*)
-
-
-open Dltree;;
-
-
-
-(* ** MODES ** *)
-
-
-(* Store goal sequent flag *)
-
-(* Intermediate goal results are only stored if this flag is set. This can
*)
-(* be used to cut down on memory usage.
*)
-
-let store_goalsequent_flag = ref true;;
-
-
-
-(* ** GOAL TREE DATATYPES & STATE ** *)
-
-
-(* Goal tree datatype *)
-
-(* This is the datatype for recording tactic proofs as a tree of goals, with
*)
-(* structure corresponding to interactive proof steps. The structural aspect
*)
-(* is captured by 'gtree0':
*)
-(* Gactive - Leaf for an active goal in the proof;
*)
-(* Gexecuted - Node for a goal that has had a tactic successfully executed
*)
-(* on it. Carries a list of subtrees, one for each of the
*)
-(* resulting subgoals, where the list is empty for a tactic that
*)
-(* completes its goal;
*)
-(* Gexit - Wiring exiting a box, indicating destination goal.
*)
-
-type ginfo =
- (goalid * goalid) (* Goal id & Parent id *)
- * string option (* Goal name (optional) *)
- * goal option (* Goal sequent (optional) *)
- * unit option ref;; (* Formal proof (optional) *)
-
-type gstep =
- Gatom of mldata (* Atomic tactic *)
- | Gbox of (label * gtree * bool) (* Box for a tactical; flag for special *)
-
-and gtree0 =
- Gactive (* Active goal *)
- | Gexecuted of (gstep * (* Tactic structure *) (* Executed tactic *)
- gtree list) (* Resulting subgoals *)
- | Gexit of goalid (* Exit the box *)
-
-and gtree =
- ginfo (* Various info about goal *)
- * gtree0 ref;; (* Goal plumbing *)
-
-
-(* Example *)
-
-(* Figure 1(b) in Denny et al would be represented by the following:
*)
-(*
*)
-(* (_, ref
*)
-(* Gexecuted
*)
-(* (Gbox (Tactical ("T1",[])
*)
-(* (_, ref
*)
-(* Gexecuted
*)
-(* (Gatom ("T2",[]),
*)
-(* [ (_, ref Gexecuted (Gatom ("WF",[]), []));
*)
-(* (_, ref Gexit _) ])),
*)
-(* [ (_, ref
*)
-(* Gexecuted
*)
-(* (Gbox (Tactical ("DP",[]))
*)
-(* (_, ref
*)
-(* Gexecuted
*)
-(* (Gatom ("Normalise",[]),
*)
-(* [ (_, ref Gexecuted (Gatom ("Taut",[]), [])) ])),
*)
-(* [])) ]))
*)
-
-
-(* Destructors *)
-
-let ginfo_id (((id,_),_,_,_):ginfo) : goalid = id;;
-
-let ginfo_pid (((_,pid),_,_,_):ginfo) : goalid = pid;;
-
-let ginfo_name ((_,x_,_,_):ginfo) : string =
- match x_ with
- Some x -> x
- | None -> failwith "Goal not named";;
-
-let ginfo_sqt ((_,_,sqt_,_):ginfo) : goal =
- match sqt_ with
- Some sqt -> sqt
- | None -> failwith "Goal sequent not stored";;
-
-let ginfo_fproof ((_,_,_,prf_):ginfo) : unit =
- match !prf_ with
- Some prf -> prf
- | None -> failwith "Goal's formal proof not stored";;
-
-let gtree_id ((info,_):gtree) = ginfo_id info;;
-let gtree_pid ((info,_):gtree) = ginfo_pid info;;
-let gtree_name ((info,_):gtree) = ginfo_name info;;
-let gtree_sqt ((info,_):gtree) = ginfo_sqt info;;
-let gtree_fproof ((info,_):gtree) = ginfo_fproof info;;
-
-let gstep_tactic (gstp:gstep) =
- match gstp with
- Gatom obj | Gbox (Tactical obj, _, true) -> obj
- | Gbox _ -> failwith "gstep_tactic: Not an atomic tactic";;
-
-let gtree_proof ((_,gtrm):gtree) =
- match (!gtrm) with
- Gexecuted (gstp,_) -> gstp
- | _ -> failwith "gtree_proof: Not executed";;
-
-let gtree_tactic gtr =
- (gstep_tactic o gtree_proof) gtr;;
-
-let gtree_tactic1 ((_,gtrm) as gtr :gtree) =
- match !gtrm with
- Gactive -> active_info
- | _ -> gtree_tactic gtr;;
-
-
-(* Tests *)
-
-let is_active_gtree ((_,gtrm):gtree) =
- match !gtrm with
- Gactive -> true
- | _ -> false;;
-
-
-(* Dummy values *)
-
-let dummy_goal_info : ginfo = ((0,0), None, None, ref None);;
-
-let dummy_goal_tree : gtree = (dummy_goal_info, ref Gactive);;
-
-
-(* Goal tree database *)
-
-let the_goal_tree = ref dummy_goal_tree;;
-
-
-(* Location database *)
-
-(* This database is maintained in parallel with the goal tree, to enable fast
*)
-(* location of the subtree corresponding to a goal (as opposed to laboriously
*)
-(* traversing the tree to find the branch with the right id).
*)
-
-let the_gtree_locations = (dltree_empty () : (goalid, gtree ref) dltree);;
-
-let get_gtree id = !(dltree_lookup id the_gtree_locations);;
-
-let deregister_gtree gtr =
- (dltree_remove (gtree_id gtr) the_gtree_locations);;
-
-let register_gtree gtr =
- (dltree_insert (gtree_id gtr, ref gtr) the_gtree_locations);;
-
-
-(* Initialisation of the goal tree state *)
-
-let init_goal_tree g =
- let g_ = if (!store_goalsequent_flag) then Some g else None in
- let ginfo = ((!the_goal_id_counter,0), None, g_, ref None) in
- let gtr = (ginfo, ref Gactive) in
- (the_goal_tree := gtr;
- dltree_reempty the_gtree_locations;
- register_gtree gtr);;
-
-
-
-(* ** GTREE UTILITIES ** *)
-
-
-(* All children *)
-
-let rec gtree_all_children gtr =
- let (_,gtrm) = gtr in
- match (!gtrm) with
- Gexecuted (gstp,gtrs)
- -> (gstep_all_children gstp) @
- gtrs @
- flat (map gtree_all_children gtrs)
- | _ -> []
-
-and gstep_all_children gstp =
- match gstp with
- Gatom _ | Gbox (_,_,true) -> []
- | Gbox (_,gtr,false) -> gtr::(gtree_all_children gtr);;
-
-
-
-(* ** PLUMBING ** *)
-
-(* These utilities do the plumbing for tactic applications and tactical
*)
-(* applications, promoting operations from goals to xgoals and incorporating
*)
-(* the results into gtrees.
*)
-
-
-(* Creating a sub gtree *)
-
-(* This creates a new xgoal for a goal, giving it a fresh id and registering
*)
-(* it in the locations database. Used on all new subgoals.
*)
-
-let new_active_subgtree pid (g:goal) : goalid * gtree =
- let id = (inc_goal_id_counter (); !the_goal_id_counter) in
- let g_ = if (!store_goalsequent_flag) then Some g else None in
- let info = ((id,pid), None, g_, ref None) in
- let gtr = (info, ref Gactive) in
- (register_gtree gtr;
- (id,gtr));;
-
-
-(* Extension *)
-
-(* This extends a gtree with the subgoals resulting from applying a tactic.
*)
-
-let extend_gtree (pid:goalid) (gstp:gstep) (gs':goal list) : xgoal list =
- let gtr = get_gtree pid in
- let (_,gtrm) = gtr in
- let () = try assert (!gtrm = Gactive)
- with Assert_failure _ ->
- failwith "extend_gtree: Internal error - Not active" in
- let (ids',gtrs) = unzip (map (new_active_subgtree pid) gs') in
- let xgs' = zip gs' ids' in
- (gtrm := Gexecuted (gstp,gtrs);
- xgs');;
-
-
-(* Deletion *)
-
-(* This deletes from a gtree the result of applying a tactic to a given goal,
*)
-(* also deleting the resulting subgoals from the locations database.
*)
-
-let delete_step (id:goalid) =
- let gtr = get_gtree id in
- let (_,gtrm) = gtr in
- let () = match (!gtrm) with
- Gexecuted _ -> ()
- | _ -> failwith "delete_step: Internal error - Not executed" in
- let gtrs = gtree_all_children gtr in
- (gtrm := Gactive;
- do_list deregister_gtree gtrs);;
-
-
-(* Externalising *)
-
-(* This is used for turning a box's active subgoal to exit wiring.
*)
-
-let externalise_gtree ((id0,id):goalid*goalid) : unit =
- let (_,gtrm) = get_gtree id0 in
- match (!gtrm) with
- Gactive -> (gtrm := Gexit id)
- | _ -> failwith "externalise_gtree: Internal error - Not active";;
-
-
-
-(* ** SUBGOAL PACKAGE OPERATIONS FOR XGOALS ** *)
-
-(* A few of the xtactic subgoal package commands are adjusted here.
*)
-
-
-(* Starting/finishing a tactic proof *)
-
-(* For commands that start a tactic proof, 'mk_xgoalstate' is adjusted to
*)
-(* initialise the goal tree. Commands that return a tactic proof's resulting
*)
-(* theorem, the theorem is adjusted to be an 'xthm' that carries a reference
*)
-(* to the goal tree.
*)
-
-let mk_xgoalstate (g:goal) : xgoalstate =
- let result = mk_xgoalstate g in
- (init_goal_tree g;
- result);;
-
-let (xTAC_PROOF : goal * xtactic -> thm) =
- fun (g,tac) ->
- let gstate = mk_xgoalstate g in
- let _,sgs,just = xby tac gstate in
- if sgs = [] then just null_inst []
- else failwith "TAC_PROOF: Unsolved goals";;
-
-let xprove(t,tac) =
- let th = xTAC_PROOF(([],t),tac) in
- let t' = concl th in
- let th' =
- if t' = t then th else
- try EQ_MP (ALPHA t' t) th
- with Failure _ -> failwith "prove: justification generated wrong theorem"
in
- mk_xthm (th', ("<tactic-proof>",[]))
-
-let xset_goal(asl,w) =
- current_xgoalstack :=
- [mk_xgoalstate(map (fun t -> "",ASSUME t) asl,w)];
- !current_xgoalstack;;
-
-let xg t =
- let fvs = sort (<) (map (fst o dest_var) (frees t)) in
- (if fvs <> [] then
- let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
- warn true ("Free variables in goal: "^errmsg)
- else ());
- xset_goal([],t);;
-
-
-(* Undoing a tactic proof step *)
-
-(* 'xb' needs to be adjusted to delete the undone step in the goal tree.
*)
-
-let xb () =
- let result = xb () in
- let (_,xgs,_) = hd result in
- let (_,id) = hd xgs in
- (delete_step id;
- result);;
-
-
-
-(* ** GTREE OPERATIONS ** *)
-
-
-(* Goal id graph *)
-
-let rec gtree_graph0 gtr graph0 =
- let (info,gtrm) = gtr in
- let ((id,pid),_,g_,_) = info in
- match !gtrm with
- Gactive
- -> (pid,id)::graph0
- | Gexit id
- -> failwith "???"
- | Gexecuted (_,gtrs)
- -> (pid,id)::(foldr gtree_graph0 gtrs graph0);;
-
-let gtree_graph () =
- let nns = gtree_graph0 (!the_goal_tree) [] in
- tl nns;; (* remove (0,0) at head of dumped list *)
-
-
-(* Goal id trace *)
-
-let rec gtree_id_trace gtr =
- let (_,gtrm) = gtr in
- match !gtrm with
- Gactive
- -> [gtree_id gtr]
- | Gexit id
- -> let gtr1 = get_gtree id in
- gtree_id_trace gtr1
- | Gexecuted (gstp,gtrs1)
- -> (match gstp with
- Gatom _ | Gbox (_,_,true)
- -> (gtree_id gtr) :: flat (map gtree_id_trace gtrs1)
- | Gbox (_,gtr1,false)
- -> gtree_id_trace gtr1);;
-
-
-(* Tactic trace *)
-
-let rec gtree_tactic_trace gtr =
- map (gtree_tactic1 o get_gtree) (gtree_id_trace gtr);;
-
diff --git a/hol-light/TacticRecording/wrappers.ml
b/hol-light/TacticRecording/wrappers.ml
deleted file mode 100644
index 115163d..0000000
--- a/hol-light/TacticRecording/wrappers.ml
+++ /dev/null
@@ -1,359 +0,0 @@
-(* ==========================================================================
*)
-(* WRAPPER FUNCTIONS (HOL LIGHT)
*)
-(* - Functions for promoting thm/goal-related ML objects for xthm/xgoal
*)
-(*
*)
-(* By Mark Adams
*)
-(* Copyright (c) Univeristy of Edinburgh, 2011-2012
*)
-(* ==========================================================================
*)
-
-
-
-(* ** THEOREM-RELATED WRAPPER FUNCTIONS ** *)
-
-
-(* mldata_as_meta_arg *)
-
-let mldata_as_meta_arg (obj:mldata) =
- match obj with
- (x, ((_::_) as args))
- -> Mlfn (x, front args)
- | _ -> failwith "mldata_as_meta_arg: Unexpected empty rule arg list";;
-
-let mldata_as_meta2_arg (obj:mldata) =
- match obj with
- (x, ((_::_) as args))
- -> Mlfn (x, (front o front) args)
- | _ -> failwith "mldata_as_meta_arg: Unexpected empty rule arg list";;
-
-
-(* detect_rule_app *)
-
-(* Based on the assumption that the given meta function actually executes its
*)
-(* rule argument at some point, this utility detects such an execution during
*)
-(* the demotion of a given xrule argument to a rule. The meta function's
*)
-(* result is returned along with an 'farg' that captures the rule.
*)
-
-let detect_rule_app (mfunc:('a->thm)->'b) (xr:'a->xthm) : 'c =
- let temp = ref (Mlfn ("<rule>", []) : mlarg) in
- let r arg = let xth = xr arg in
- let (th,obj) = dest_xthm xth in
- (temp := mldata_as_meta_arg obj;
- th) in
- let th = mfunc r in
- (th,!temp);;
-
-let detect_metarule_app (mfunc:(('a->thm)->'b->thm)->'c)
- (xmr:('a->xthm)->'b->xthm) : 'd =
- let temp = ref (Mlfn ("<meta-rule>",[]) : mlarg) in
- let mr marg arg = let xmarg arg0 =
- let th = marg arg0 in
- let obj = ("<rule>", [Mlfn ("<arg>",[])]) in
- mk_xthm (th,obj) in
- let xth = xmr xmarg arg in
- let (th,obj) = dest_xthm xth in
- (temp := mldata_as_meta2_arg obj;
- th) in
- let th = mfunc mr in
- (th,!temp);;
-
-
-(* Theorem wrapper *)
-
-let theorem_wrap (x:string) (th:thm) : xthm =
- (th, (x,[]));;
-
-
-(* Rule wrappers *)
-
-(* Lots of rule wrappers are required because there are many different type
*)
-(* shapes for rules.
*)
-
-let rule_wrap0 obj (r:'a->thm) (arg:'a) : xthm =
- let th' = r arg in
- mk_xthm (th',obj);;
-
-let conv_wrap x (r:term->thm) (tm:term) : xthm =
- rule_wrap0 (x, [Mlterm tm]) r tm;;
-
-let thm_conv_wrap x (r:thm->term->thm) (xth:xthm) tm : xthm =
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x, [Mlthm prf; Mlterm tm]) (r th) tm;;
-
-let thmlist_conv_wrap x (r:thm list->term->thm) xths (tm:term) : xthm =
- let (ths,prfs) = unzip (map dest_xthm xths) in
- rule_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs); Mlterm tm])
- (r ths) tm;;
-
-let rule_wrap x (r:thm->thm) (xth:xthm) : xthm =
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x, [Mlthm prf]) r th;;
-
-let drule_wrap x (r:thm->thm->thm) (xth1:xthm) (xth2:xthm) : xthm =
- let (th1,prf1) = dest_xthm xth1 in
- let (th2,prf2) = dest_xthm xth2 in
- rule_wrap0 (x, [Mlthm prf1; Mlthm prf2]) (r th1) th2;;
-
-let prule_wrap x (r:thm*thm->thm) ((xth1:xthm),(xth2:xthm)) : xthm =
- let (th1,prf1) = dest_xthm xth1 in
- let (th2,prf2) = dest_xthm xth2 in
- rule_wrap0 (x, [Mlpair(Mlthm prf1, Mlthm prf2)]) r (th1,th2);;
-
-let trule_wrap x (r:thm->thm->thm->thm)
- (xth1:xthm) (xth2:xthm) (xth3:xthm) : xthm =
- let (th1,prf1) = dest_xthm xth1 in
- let (th2,prf2) = dest_xthm xth2 in
- let (th3,prf3) = dest_xthm xth3 in
- rule_wrap0 (x, [Mlthm prf1; Mlthm prf2; Mlthm prf3]) (r th1 th2) th3;;
-
-let term_rule_wrap x (r:term->thm->thm) tm (xth:xthm) : xthm =
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x, [Mlterm tm; Mlthm prf]) (r tm) th;;
-
-let termpair_rule_wrap x (r:term*term->thm->thm) (tm1,tm2) (xth:xthm) : xthm =
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x, [Mlpair(Mlterm tm1,Mlterm tm2); Mlthm prf]) (r (tm1,tm2)) th;;
-
-let termthmpair_rule_wrap x (r:term*thm->thm->thm) (tm,xth0) (xth:xthm) : xthm
=
- let (th0,prf0) = dest_xthm xth0 in
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x, [Mlpair(Mlterm tm, Mlthm prf0); Mlthm prf]) (r (tm,th0)) th;;
-
-let termlist_rule_wrap x (r:term list->thm->thm) tms (xth:xthm) : xthm =
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x, [Mllist (map (fun tm -> Mlterm tm) tms); Mlthm prf])
- (r tms) th;;
-
-let terminst_rule_wrap x (r:(term*term)list->thm->thm) theta (xth:xthm) : xthm
=
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x,
- [Mllist (map (fun (tm1,tm2) -> Mlpair(Mlterm tm1, Mlterm tm2))
- theta);
- Mlthm prf])
- (r theta) th;;
-
-let typeinst_rule_wrap x (r:(hol_type*hol_type)list->thm->thm)
- theta (xth:xthm) : xthm =
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x,
- [Mllist (map (fun (tm1,tm2) -> Mlpair(Mltype tm1, Mltype tm2))
- theta);
- Mlthm prf])
- (r theta) th;;
-
-let thmlist_rule_wrap x (r:thm list->thm->thm) xths (xth:xthm) : xthm =
- let (ths,prfs) = unzip (map dest_xthm xths) in
- let (th,prf) = dest_xthm xth in
- rule_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs); Mlthm prf])
- (r ths) th;;
-
-
-(* Multi-rule wrappers *)
-
-let multirule_wrap0 obj (r:'a->thm list) (arg:'a) : xthm list =
- let ths' = r arg in
- let n = length ths' in
- let infos' = map (fun i -> ("el", [Mlint i; Mlfn obj])) (0 -- (n-1)) in
- map mk_xthm (zip ths' infos');;
-
-let multirule_wrap x (r:thm->thm list) (xth:xthm) : xthm list =
- let (th,prf) = dest_xthm xth in
- multirule_wrap0 (x, [Mlthm prf]) r th;;
-
-
-(* Meta rule wrappers *)
-
-let meta_rule_wrap0 info0 (mr:('a->thm)->'b->thm)
- (xr:'a->xthm) (arg:'b) : xthm =
- let (th',f) = detect_rule_app (fun r -> mr r arg) xr in
- let (x,args0) = info0 in
- let obj' = (x, f::args0) in
- (th',obj');;
-
-let conv_conv_wrap x (mc:conv->conv) (xc:term->xthm) (tm:term) : xthm =
- meta_rule_wrap0 (x, [Mlterm tm]) mc xc tm;;
-
-
-
-(* ** TACTIC-RELATED WRAPPER FUNCTIONS ** *)
-
-(* These functions are for promoting existing tactics and tacticals.
*)
-
-
-(* Generic basic wrapper util *)
-
-(* Applies a tactic and incorproates the results into the goal tree. Takes
*)
-(* an "infotactic", i.e. like a normal tactic that works on 'goal' and
*)
-(* returns 'goalstate', but that also returns a 'gstep' summary of the
*)
-(* operation. This is used to promote every basic tactic-based function.
*)
-
-let infotactic_wrap (infotac:goal->goalstate*mldata) (xg:xgoal) : xgoalstate =
- let (g,id) = dest_xgoal xg in
- let ((meta,gs,just),obj) = infotac g in
- let xgs = extend_gtree id (Gatom obj) gs in
- (meta,xgs,just);;
-
-
-(* Generic box wrapper util *)
-
-(* Sets up a box to apply an xtactic within, applies the xtactic (which
*)
-(* incorporates itself into the goal tree) and wires up the resulting
*)
-(* subgoals to external subgoals of the box. Note that this is not quite
*)
-(* generic enough for 'SUBGOAL_THEN' (because there is not a total surjection
*)
-(* between internal and external goals).
*)
-
-let infobox_wrap (xinfotac:xgoal->xgoalstate*label) (xg:xgoal) : xgoalstate =
- let (g,id) = dest_xgoal xg in
- let (id0,gtr0) = new_active_subgtree id g in
- let xg0 = mk_xgoal (g,id0) in
- let ((meta,xgs0,just),l) = xinfotac xg0 in
- let (gs0,ids0) = unzip (map dest_xgoal xgs0) in
- let xgs = extend_gtree id (Gbox (l,gtr0,false)) gs0 in
- let ids = map xgoal_id xgs in
- (do_list externalise_gtree (zip ids0 ids);
- (meta,xgs,just));;
-
-
-(* Tactic wrapper *)
-
-(* This is for wrapping around a tactic, to promote it to work on xgoals and
*)
-(* incorporate the results into an existing gtree.
*)
-
-let tactic_wrap0 obj (tac:tactic) : xtactic =
- let infotac g = (tac g, obj) in
- infotactic_wrap infotac;;
-
-let tactic_wrap x tac =
- tactic_wrap0 (x, []) tac;;
-
-let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic =
- tactic_wrap0 (x, [Mlstring s]) (tac s);;
-
-let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic =
- tactic_wrap0 (x, [Mlterm tm]) (tac tm);;
-
-let termpair_tactic_wrap x (tac:term*term->tactic) (tm1,tm2) : xtactic =
- tactic_wrap0 (x, [Mlpair (Mlterm tm1, Mlterm tm2)]) (tac (tm1,tm2));;
-
-let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic =
- tactic_wrap0 (x, [Mllist (map (fun tm -> Mlterm tm) tms)]) (tac tms);;
-
-let thm_tactic_wrap x (tac:thm->tactic) (xth:xthm) : xtactic =
- let (th,prf) = dest_xthm xth in
- tactic_wrap0 (x, [Mlthm prf]) (tac th);;
-
-let thmlist_tactic_wrap x (tac:thm list->tactic) (xths:xthm list) : xtactic =
- let (ths,prfs) = unzip (map dest_xthm xths) in
- tactic_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs)]) (tac ths);;
-
-let stringthm_tactic_wrap x (tac:string->thm->tactic) s (xth:xthm) : xtactic =
- let (th,prf) = dest_xthm xth in
- tactic_wrap0 (x, [Mlstring s; Mlthm prf]) (tac s th);;
-
-
-(* Meta-tactic wrapper *)
-
-(* For tactics that take rule arguments.
*)
-
-let meta_tactic_wrap0 info0 (mtac:('a->thm)->tactic)
- (xr:'a->xthm) : xtactic =
- let infotac g =
- let (gst,f) = detect_rule_app (fun r -> mtac r g) xr in
- let (x,args0) = info0 in
- let obj = (x, f::args0) in
- (gst,obj) in
- infotactic_wrap infotac;;
-
-let conv_tactic_wrap x (mtac:conv->tactic) (xc:xconv) : xtactic =
- meta_tactic_wrap0 (x, []) mtac xc;;
-
-let metameta_tactic_wrap info0 (mmtac:(('a->thm)->'b->thm)->tactic)
- (xmr:('a->xthm)->'b->xthm) : xtactic =
- let infotac g =
- let (gst,f) = detect_metarule_app (fun mr -> mmtac mr g) xmr in
- let (x,args0) = info0 in
- let obj = (x, f::args0) in
- (gst,obj) in
- infotactic_wrap infotac;;
-
-let convconvthmlist_tactic_wrap x (mmtac:(conv->conv)->thm list->tactic)
- (xmc:xconv->xconv) (xths:xthm list) : xtactic
=
- let (ths,prfs) = unzip (map dest_xthm xths) in
- metameta_tactic_wrap (x, [Mllist (map (fun prf -> Mlthm prf) prfs)])
- (fun mc -> mmtac mc ths)
- xmc;;
-
-
-(* Tactical wrapper *)
-
-(* This is for wrapping around a tactical, to incorporate the results into a
*)
-(* box in an existing gtree, where the execution of the tactical's tactics is
*)
-(* captured inside the box, so that they can be stepped through and/or
*)
-(* refactored. Thus we cannot take the tactical as a black box; it must
*)
-(* already be promoted to work with xtactics and xgoals. This must done by
*)
-(* hand for each tactical by trivially adjusting its original source code.
*)
-
-let tactical_wrap0 obj (xttcl:'a->xtactic) (arg:'a) : xtactic =
- let xinfotac xg = (xttcl arg xg, Tactical obj) in
- infobox_wrap xinfotac;;
-
-let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic =
- tactical_wrap0 (x,[]) xttcl xtac;;
-
-let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic =
- tactical_wrap0 (x,[]) (xttcl xtac1) xtac2;;
-
-let int_tactical_wrap x (xttcl:int->'a->xtactic) (n:int) (xtac:'a) : xtactic =
- tactical_wrap0 (x, [Mlint n]) (xttcl n) xtac;;
-
-let list_tactical_wrap x (xttcl:('a->xtactic)->'a list->xtactic)
- (xtac:'a->xtactic) (l:'a list) : xtactic =
- tactical_wrap0 (x,[]) (xttcl xtac) l;;
-
-
-(* HILABEL *)
-
-(* Command for putting the result of a tactic into a box and giving the box a
*)
-(* label (distinct from a tactical label).
*)
-
-let HILABEL x (xtac:xtactic) : xtactic =
- let xinfotac xg = (xtac xg, Label x) in
- infobox_wrap xinfotac;;
-
-
-(* xSUBGOAL_THEN - seems to be a special case *)
-
-let xASSUME = conv_wrap "ASSUME" ASSUME;;
-
-let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (xg:xgoal) : xgoalstate =
- let arg = xASSUME tm in
-
- let (g,id) = dest_xgoal xg in
- let (id0,gtr0) = new_active_subgtree id g in
- let xg0 = mk_xgoal (g,id0) in
- let (meta,xgs0,just) = ttac arg xg0 in
-
- let (asl,_) = g in
- let g2 = (asl,tm) in
- let obj = ("SUBGOAL_THEN",
- [Mlterm tm; (mldata_as_meta_arg o gtree_tactic) gtr0]) in
-
- let (gs0,ids0) = unzip (map dest_xgoal xgs0) in
- let xgs = extend_gtree id (Gbox (Tactical obj, gtr0, true)) (g2::gs0) in
- let ids1 = map xgoal_id (tl xgs) in
- let just' = fun i l -> PROVE_HYP (hd l) (just i (tl l)) in
- (do_list externalise_gtree (zip ids0 ids1);
- (meta,xgs,just'));;
-
-
-(*
-let SUBGOAL_TAC s tm prfs =
- match prfs with
- p::ps -> (warn (ps <> []) "SUBGOAL_TAC: additional subproofs ignored";
- SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC])
- | [] -> failwith "SUBGOAL_TAC: no subproof given";;
-
-let (FREEZE_THEN :thm_tactical) =
- fun ttac th (asl,w) ->
- let meta,gl,just = ttac (ASSUME(concl th)) (asl,w) in
- meta,gl,fun i l -> PROVE_HYP th (just i l);;
-*)
diff --git a/hol-light/TacticRecording/xtactics.ml
b/hol-light/TacticRecording/xtactics.ml
deleted file mode 100644
index fb7028c..0000000
--- a/hol-light/TacticRecording/xtactics.ml
+++ /dev/null
@@ -1,451 +0,0 @@
-(* ========================================================================= *)
-(* HOL Light subgoal package amended for id-carrying goals. *)
-(* *)
-(* Mark Adams, School of Informatics, University of Edinburgh *)
-(* *)
-(* (c) Copyright, University of Edinburgh, 2012 *)
-(* ========================================================================= *)
-
-(* The 'xgoal' variant of the 'goal' datatype is defined here, to label *)
-(* goals with a unique goal id. This gives a basis for recording tactic *)
-(* proofs. Variants of all the datatypes depending on 'goal', such as *)
-(* 'xgoalstate' and 'xtactic', are also defined, along with a variant *)
-(* subgoal package. ML names are given an "x" prefix to keep them distinct *)
-(* from the originals for now (but originals are overwritten later, in *)
-(* 'install.ml'). *)
-
-(* The goal id counter is only adjusted in this file by being incremented in *)
-(* 'mk_xgoalstate', used when starting a new subgoal package proof. *)
-(* Xtactics are assumed to give their resulting xgoals id labels based on an *)
-(* appropriately updated goal id counter. *)
-
-(* After the implementation of xgoals themselves at the start of this file, *)
-(* the rest of the file is more-or-less copied verbatim from HOL Light's *)
-(* original 'tactics.ml', with just a few changes required. This enables an *)
-(* easy diff operation with the original if required to check that the *)
-(* changes are valid. *)
-
-(* ------------------------------------------------------------------------- *)
-(* Goal counter for providing goal ids. *)
-(* ------------------------------------------------------------------------- *)
-
-type goalid = int;;
-
-let string_of_goal_id (id:goalid) = string_of_int id;;
-
-let the_goal_id_counter = ref (0 : goalid);;
-
-let inc_goal_id_counter () =
- (the_goal_id_counter := !the_goal_id_counter + 1);;
-
-(* ------------------------------------------------------------------------- *)
-(* An xgoal extends a goal with an identity. *)
-(* ------------------------------------------------------------------------- *)
-
-type xgoal = goal * goalid;;
-
-let equals_xgoal (((a,w),_):xgoal) (((a',w'),_):xgoal) =
- forall2 (fun (s,th) (s',th') -> s = s' & equals_thm th th') a a' & w = w';;
-
-let mk_xgoal (gn:goal*goalid) : xgoal = gn;;
-
-let dest_xgoal (gn:xgoal) : goal*goalid = gn;;
-
-let xgoal_goal ((g,id):xgoal) : goal = g;;
-
-let xgoal_id ((g,id):xgoal) : goalid = id;;
-
-(* ------------------------------------------------------------------------- *)
-(* The xgoalstate is like goalstate but for xgoals instead of goals. *)
-(* ------------------------------------------------------------------------- *)
-
-type xgoalstate = (term list * instantiation) * xgoal list * justification;;
-
-(* ------------------------------------------------------------------------- *)
-(* A goalstack but for xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-type xgoalstack = xgoalstate list;;
-
-(* ------------------------------------------------------------------------- *)
-(* Refinements for xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-type xrefinement = xgoalstate -> xgoalstate;;
-
-(* ------------------------------------------------------------------------- *)
-(* Tactics for xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-type xtactic = xgoal -> xgoalstate;;
-
-type xthm_tactic = xthm -> xtactic;;
-
-type xthm_tactical = xthm_tactic -> xthm_tactic;;
-
-(* ------------------------------------------------------------------------- *)
-(* Instantiation of xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-let (inst_xgoal:instantiation->xgoal->xgoal) =
- fun p ((thms,w),id) ->
- (map (I F_F INSTANTIATE_ALL p) thms,instantiate p w),id;;
-
-(* ------------------------------------------------------------------------- *)
-(* Validity check for xtactics. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xVALID:xtactic->xtactic) =
- let fake_thm ((asl,w),id) =
- let asms = itlist (union o hyp o snd) asl [] in
- mk_fthm(asms,w)
- and false_tm = `_FALSITY_` in
- fun tac ((asl,w),id) ->
- let ((mvs,i),gls,just as res) = tac ((asl,w),id) in
- let ths = map fake_thm gls in
- let asl',w' = dest_thm(just null_inst ths) in
- let asl'',w'' = inst_goal i (asl,w) in
- let maxasms =
- itlist (fun (_,th) -> union (insert (concl th) (hyp th))) asl'' [] in
- if aconv w' w'' & forall (C mem maxasms) (subtract asl' [false_tm])
- then res else failwith "VALID: Invalid tactic";;
-
-(* ------------------------------------------------------------------------- *)
-(* Various simple combinators for tactics, identity tactic etc. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xTHEN),(xTHENL) =
- let propagate_empty i [] = []
- and propagate_thm th i [] = INSTANTIATE_ALL i th in
- let compose_justs n just1 just2 i ths =
- let ths1,ths2 = chop_list n ths in
- (just1 i ths1)::(just2 i ths2) in
- let rec seqapply l1 l2 = match (l1,l2) with
- ([],[]) -> null_meta,[],propagate_empty
- | ((tac:xtactic)::tacs),((goal:xgoal)::goals) ->
- let ((mvs1,insts1),gls1,just1 as gstate1) = tac goal in
- let goals' = map (inst_xgoal insts1) goals in
- let ((mvs2,insts2),gls2,just2 as gstate2) = seqapply tacs goals' in
- ((union mvs1 mvs2,compose_insts insts1 insts2),
- gls1@gls2,compose_justs (length gls1) just1 just2)
- | _,_ -> failwith "seqapply: Length mismatch" in
- let justsequence just1 just2 insts2 i ths =
- just1 (compose_insts insts2 i) (just2 i ths) in
- let tacsequence ((mvs1,insts1),gls1,just1 as gstate1) tacl =
- let ((mvs2,insts2),gls2,just2 as gstate2) = seqapply tacl gls1 in
- let jst = justsequence just1 just2 insts2 in
- let just = if gls2 = [] then propagate_thm (jst null_inst []) else jst in
- ((union mvs1 mvs2,compose_insts insts1 insts2),gls2,just) in
- let (then_: xtactic -> xtactic -> xtactic) =
- fun tac1 tac2 g ->
- let _,gls,_ as gstate = tac1 g in
- tacsequence gstate (replicate tac2 (length gls))
- and (thenl_: xtactic -> xtactic list -> xtactic) =
- fun tac1 tac2l g ->
- let _,gls,_ as gstate = tac1 g in
- if gls = [] then tacsequence gstate []
- else tacsequence gstate tac2l in
- then_,thenl_;;
-
-let ((xORELSE): xtactic -> xtactic -> xtactic) =
- fun tac1 tac2 g ->
- try tac1 g with Failure _ -> tac2 g;;
-
-let (xFAIL_TAC: string -> xtactic) =
- fun tok g -> failwith tok;;
-
-let (xALL_TAC:xtactic) =
- fun g -> null_meta,[g],fun _ [th] -> th;;
-
-let xTRY tac =
- xORELSE tac xALL_TAC;;
-
-let rec xREPEAT tac g =
- (xORELSE (xTHEN tac (xREPEAT tac)) xALL_TAC) g;;
-
-let xEVERY tacl =
- itlist (fun t1 t2 -> xTHEN t1 t2) tacl xALL_TAC;;
-
-let (xFIRST: xtactic list -> xtactic) =
- fun tacl g -> end_itlist (fun t1 t2 -> xORELSE t1 t2) tacl g;;
-
-let xMAP_EVERY tacf lst =
- xEVERY (map tacf lst);;
-
-let xMAP_FIRST tacf lst =
- xFIRST (map tacf lst);;
-
-let (xCHANGED_TAC: xtactic -> xtactic) =
- fun tac g ->
- let (meta,gl,_ as gstate) = tac g in
- if meta = null_meta & length gl = 1 & equals_xgoal (hd gl) g
- then failwith "CHANGED_TAC" else gstate;;
-
-let rec xREPLICATE_TAC n tac =
- if n <= 0 then xALL_TAC else xTHEN tac (xREPLICATE_TAC (n - 1) tac);;
-
-(* ------------------------------------------------------------------------- *)
-(* Combinators for theorem continuations adjusted for xthms and xtactics. *)
-(* ------------------------------------------------------------------------- *)
-
-let ((xTHEN_TCL): xthm_tactical -> xthm_tactical -> xthm_tactical) =
- fun ttcl1 ttcl2 ttac -> ttcl1 (ttcl2 ttac);;
-
-let ((xORELSE_TCL): xthm_tactical -> xthm_tactical -> xthm_tactical) =
- fun ttcl1 ttcl2 ttac th ->
- try ttcl1 ttac th with Failure _ -> ttcl2 ttac th;;
-
-let rec xREPEAT_TCL ttcl ttac th =
- (xORELSE_TCL (xTHEN_TCL ttcl (xREPEAT_TCL ttcl)) I) ttac th;;
-
-let (xREPEAT_GTCL: xthm_tactical -> xthm_tactical) =
- let rec xREPEAT_GTCL ttcl ttac th g =
- try ttcl (xREPEAT_GTCL ttcl ttac) th g with Failure _ -> ttac th g in
- xREPEAT_GTCL;;
-
-let (xALL_THEN: xthm_tactical) =
- I;;
-
-let (xNO_THEN: xthm_tactical) =
- fun ttac th -> failwith "NO_THEN";;
-
-let xEVERY_TCL ttcll =
- itlist (fun t1 t2 -> xTHEN_TCL t1 t2) ttcll xALL_THEN;;
-
-let xFIRST_TCL ttcll =
- end_itlist (fun t1 t2 -> xORELSE_TCL t1 t2) ttcll;;
-
-(* ------------------------------------------------------------------------- *)
-(* Tactics to augment assumption list. Note that to allow "ASSUME p" for *)
-(* any assumption "p", these add a PROVE_HYP in the justification function, *)
-(* just in case. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xLABEL_TAC: string -> xthm_tactic) =
- fun s thm ((asl,w),id) ->
- let thm' = xthm_thm thm in
- null_meta,[(((s,thm')::asl,w),id)],
- fun i [th] -> PROVE_HYP (INSTANTIATE_ALL i thm') th;;
-
-(* ------------------------------------------------------------------------- *)
-(* Manipulation of assumption list. *)
-(* ------------------------------------------------------------------------- *)
-
-let mk_asm_xthm th = mk_xthm0 "<asm>" th;;
-
-let (xFIND_ASSUM: xthm_tactic -> term -> xtactic) =
- fun ttac t (((asl,w),id) as g) ->
- ttac (mk_asm_xthm (snd(find (fun (_,th) -> concl th = t) asl))) g;;
-
-let (xPOP_ASSUM: xthm_tactic -> xtactic) =
- fun ttac ->
- function ((((_,th)::asl),w),id) -> ttac (mk_asm_xthm th) ((asl,w),id)
- | _ -> failwith "POP_ASSUM: No assumption to pop";;
-
-let (xASSUM_LIST: (xthm list -> xtactic) -> xtactic) =
- fun aslfun ((asl,w),id) -> aslfun (map (mk_asm_xthm o snd) asl)
- ((asl,w),id);;
-
-let (xPOP_ASSUM_LIST: (xthm list -> xtactic) -> xtactic) =
- fun asltac ((asl,w),id) -> asltac (map (mk_asm_xthm o snd) asl) (([],w),id);;
-
-let (xEVERY_ASSUM: xthm_tactic -> xtactic) =
- fun ttac -> xASSUM_LIST (xMAP_EVERY ttac);;
-
-let (xFIRST_ASSUM: xthm_tactic -> xtactic) =
- fun ttac (((asl,w),id) as g) ->
- tryfind (fun (_,th) -> ttac (mk_asm_xthm th) g) asl;;
-
-let (xRULE_ASSUM_TAC :(xthm->xthm)->xtactic) =
- fun rule ((asl,w),id) ->
- (xTHEN (xPOP_ASSUM_LIST(K xALL_TAC))
- (xMAP_EVERY
- (fun (s,th) -> xLABEL_TAC s (rule (mk_asm_xthm th)))
- (rev asl)))
- ((asl,w),id);;
-
-(* ------------------------------------------------------------------------- *)
-(* Operate on assumption identified by a label. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xUSE_THEN:string->xthm_tactic->xtactic) =
- fun s ttac (((asl,w),id) as gl) ->
- let th = try assoc s asl with Failure _ ->
- failwith("USE_TAC: didn't find assumption "^s) in
- ttac (mk_asm_xthm th) gl;;
-
-let (xREMOVE_THEN:string->xthm_tactic->xtactic) =
- fun s ttac ((asl,w),id) ->
- let th = try assoc s asl with Failure _ ->
- failwith("USE_TAC: didn't find assumption "^s) in
- let asl1,asl2 = chop_list(index s (map fst asl)) asl in
- let asl' = asl1 @ tl asl2 in
- ttac (mk_asm_xthm th) ((asl',w),id);;
-
-(* ------------------------------------------------------------------------- *)
-(* General tool to augment a required set of theorems with assumptions. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xASM :(xthm list -> xtactic)->(xthm list -> xtactic)) =
- fun tltac ths
- (((asl,w),id) as g) -> tltac (map (mk_asm_xthm o snd) asl @ ths) g;;
-
-(* ------------------------------------------------------------------------- *)
-(* A printer for xgoals etc. *)
-(* ------------------------------------------------------------------------- *)
-
-let print_xgoal ((g,x):xgoal) : unit =
- print_goal g;;
-
-let (print_xgoalstack:xgoalstack->unit) =
- let print_xgoalstate k gs =
- let (_,gl,_) = gs in
- let n = length gl in
- let s = if n = 0 then "No subgoals" else
- (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
- ^" ("^(string_of_int n)^" total)" in
- print_string s; print_newline();
- if gl = [] then () else
- do_list (print_xgoal o C el gl) (rev(0--(k-1))) in
- fun l ->
- if l = [] then print_string "Empty goalstack"
- else if tl l = [] then
- let (_,gl,_ as gs) = hd l in
- print_xgoalstate 1 gs
- else
- let (_,gl,_ as gs) = hd l
- and (_,gl0,_) = hd(tl l) in
- let p = length gl - length gl0 in
- let p' = if p < 1 then 1 else p + 1 in
- print_xgoalstate p' gs;;
-
-(* ------------------------------------------------------------------------- *)
-(* Convert an xtactic into an xrefinement. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xby:xtactic->xrefinement) =
- fun tac ((mvs,inst),gls,just) ->
- let g = hd gls
- and ogls = tl gls in
- let ((newmvs,newinst),subgls,subjust) = tac g in
- let n = length subgls in
- let mvs' = union newmvs mvs
- and inst' = compose_insts inst newinst
- and gls' = subgls @ map (inst_xgoal newinst) ogls in
- let just' i ths =
- let i' = compose_insts inst' i in
- let cths,oths = chop_list n ths in
- let sths = (subjust i cths) :: oths in
- just i' sths in
- (mvs',inst'),gls',just';;
-
-(* ------------------------------------------------------------------------- *)
-(* Rotate for xgoalstate. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xrotate:int->xrefinement) =
- let rotate_p (meta,sgs,just) =
- let sgs' = (tl sgs)@[hd sgs] in
- let just' i ths =
- let ths' = (last ths)::(butlast ths) in
- just i ths' in
- (meta,sgs',just')
- and rotate_n (meta,sgs,just) =
- let sgs' = (last sgs)::(butlast sgs) in
- let just' i ths =
- let ths' = (tl ths)@[hd ths] in
- just i ths' in
- (meta,sgs',just') in
- fun n -> if n > 0 then funpow n rotate_p
- else funpow (-n) rotate_n;;
-
-(* ------------------------------------------------------------------------- *)
-(* Refinement proof, tactic proof etc for xgoals/xtactics. *)
-(* ------------------------------------------------------------------------- *)
-
-let (mk_xgoalstate:goal->xgoalstate) =
- fun (asl,w) ->
- if type_of w = bool_ty then
- let id = (inc_goal_id_counter (); !the_goal_id_counter) in
- null_meta,[((asl,w),id)],
- (fun inst [th] -> INSTANTIATE_ALL inst th)
- else failwith "mk_goalstate: Non-boolean goal";;
-
-let (xTAC_PROOF : goal * xtactic -> thm) =
- fun (g,tac) ->
- let gstate = mk_xgoalstate g in
- let _,sgs,just = xby tac gstate in
- if sgs = [] then just null_inst []
- else failwith "TAC_PROOF: Unsolved goals";;
-
-let xprove(t,tac) =
- let th = xTAC_PROOF(([],t),tac) in
- let t' = concl th in
- let th' =
- if t' = t then th else
- try EQ_MP (ALPHA t' t) th
- with Failure _ -> failwith "prove: justification generated wrong theorem"
in
- mk_xthm (th', ("<tactic-proof>",[]))
-
-(* ------------------------------------------------------------------------- *)
-(* Subgoal package for xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-let current_xgoalstack = ref ([] :xgoalstack);;
-
-let (xrefine:xrefinement->xgoalstack) =
- fun r ->
- let l = !current_xgoalstack in
- let h = hd l in
- let res = r h :: l in
- current_xgoalstack := res;
- !current_xgoalstack;;
-
-let flush_xgoalstack() =
- let l = !current_xgoalstack in
- current_xgoalstack := [hd l];;
-
-let xe tac = xrefine(xby(xVALID tac));;
-
-let xr n = xrefine(xrotate n);;
-
-let xset_goal(asl,w) =
- current_xgoalstack :=
- [mk_xgoalstate(map (fun t -> "",ASSUME t) asl,w)];
- !current_xgoalstack;;
-
-let xg t =
- let fvs = sort (<) (map (fst o dest_var) (frees t)) in
- (if fvs <> [] then
- let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
- warn true ("Free variables in goal: "^errmsg)
- else ());
- xset_goal([],t);;
-
-let xb() =
- let l = !current_xgoalstack in
- if length l = 1 then failwith "Can't back up any more" else
- current_xgoalstack := tl l;
- !current_xgoalstack;;
-
-let xp() =
- !current_xgoalstack;;
-
-let xtop_realgoal() =
- let (_,(((asl,w),_)::_),_)::_ = !current_xgoalstack in
- asl,w;;
-
-let xtop_goal() =
- let asl,w = xtop_realgoal() in
- map (concl o snd) asl,w;;
-
-let xtop_thm() =
- let (_,[],f)::_ = !current_xgoalstack in
- mk_xthm (f null_inst [], ("<tactic-proof>",[]));;
-
-(* ------------------------------------------------------------------------- *)
-(* Install the goal-related printers. *)
-(* ------------------------------------------------------------------------- *)
-
-#install_printer print_xgoal;;
-#install_printer print_xgoalstack;;
diff --git a/hol-light/TacticRecording/xthm.ml
b/hol-light/TacticRecording/xthm.ml
deleted file mode 100644
index 97fcec5..0000000
--- a/hol-light/TacticRecording/xthm.ml
+++ /dev/null
@@ -1,40 +0,0 @@
-
-
-
-(* ** DATATYPE ** *)
-
-
-(* The 'xthm' datatype *)
-
-(* This couples a theorem with an 'mldata' representation of its proof. For
*)
-(* named ML objects, this 'mldata' will simply be the ML name of the theorem.
*)
-(* For rule applications, it will capture the rule and its arguments.
*)
-
-type xthm = thm * mldata;;
-
-type xconv = term -> xthm;;
-
-
-(* Constructors and destructors *)
-
-let mk_xthm (xth:thm*mldata) : xthm = xth;;
-
-let mk_xthm0 x th = mk_xthm (th, (x,[]));;
-
-let dest_xthm ((th,prf):xthm) : thm * mldata = (th,prf);;
-
-let xthm_thm ((th,_):xthm) = th;;
-
-let xthm_proof ((_,prf):xthm) = prf;;
-
-let name_xthm x ((th,_):xthm) : xthm = (th, (x,[]));;
-
-
-
-(* ** INSTALL PRINTERS ** *)
-
-
-let print_xthm ((th,_):xthm) = print_thm th;;
-
-#install_printer print_xthm;;
-
diff --git a/hol-light/example.ml b/hol-light/example.ml
deleted file mode 100644
index 7010fbc..0000000
--- a/hol-light/example.ml
+++ /dev/null
@@ -1,19 +0,0 @@
-(*
- Example proof script for HOL Proof General.
-
- $Id$
-*)
-
-g `A /\ B ==> B /\ A`;;
-e DISCH_TAC;;
-e CONJ_TAC;;
-e (ASM_SIMP_TAC[]);;
-e (ASM_SIMP_TAC[]);;
-let and_comms = top_thm();;
-
-g `A /\ B ==> B /\ A`;;
-e DISCH_TAC;;
-e CONJ_TAC;;
-e (ASM_SIMP_TAC[]);;
-e (ASM_SIMP_TAC[]);;
-let and_comms2 = top_thm();;
diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
deleted file mode 100644
index dab2c4c..0000000
--- a/hol-light/hol-light-autotest.el
+++ /dev/null
@@ -1,42 +0,0 @@
-;;; hol-light-autotest.el --- tests of HOL Light Proof General.
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014, 2018 Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017 Pierre Courtieu
-;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
-;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-
-;;; Commentary:
-;;
-;; You can run these by issuing "make test.hol-light" in PG home dir.
-;;
-
-;;; Code:
-
-(require 'proof-site)
-(proof-ready-for-assistant 'hol-light)
-
-(require 'pg-autotest)
-
-(unless (bound-and-true-p byte-compile-current-file)
-
- (pg-autotest start 'debug)
- (pg-autotest log ".autotest.log") ; convention
-
- (pg-autotest timestart 'total)
-
- (pg-autotest remark "Testing standard examples...")
-
- (pg-autotest script-wholefile "hol-light/example.ml")
-
- (proof-shell-wait)
-
-
- (pg-autotest remark "Complete.")
-
- (pg-autotest timetaken 'total)
-
- (pg-autotest exit))
diff --git a/hol-light/hol-light-unicode-tokens.el
b/hol-light/hol-light-unicode-tokens.el
deleted file mode 100644
index 7e24e4b..0000000
--- a/hol-light/hol-light-unicode-tokens.el
+++ /dev/null
@@ -1,252 +0,0 @@
-;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*-
coding: utf-8; -*-
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017 Pierre Courtieu
-;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
-;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-
-;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
-
-;;; Commentary:
-;;
-;; This file is loaded by `proof-unicode-tokens.el'.
-;;
-;; It sets the variables defined at the top of unicode-tokens.el,
-;; unicode-tokens-<foo> is set from hol-light-<foo>. See the corresponding
-;; variable for documentation.
-;;
-;; For HOL Light, there is no dedicated token syntax, we simply
-;; define replacements for common ASCII sequences.
-;;
-;; FIXME TODO:
-;; - only do it for quoted text
-;; - fix unicode tokens sorting so longs tokens handled first (broken?)
-;; <=> not <= >
-
-;;; Code:
-
-(require 'proof-unicode-tokens)
-
-(defconst hol-light-token-format "%s") ; plain tokens
-(defconst hol-light-token-match nil)
-(defconst hol-light-hexcode-match nil)
-
-(defun hol-light-unicode-tokens-set (sym val)
- "Change a Unicode Tokens configuration variable and restart."
- (set-default sym val)
- (when (featurep 'hol-light-unicode-tokens) ; not during loading
- (proof-unicode-tokens-configure)))
-
-(defcustom hol-light-token-symbol-map
- '(;; Greek letters
- ("alpha" "α")
- ("beta" "β")
- ("gamma" "γ")
- ("delta" "δ")
- ("epsilon" "ε")
- ("zeta" "ζ")
- ("eta" "η")
- ("theta" "θ")
- ("iota" "ι")
- ("kappa" "κ")
- ("lambda" "λ")
- ("mu" "μ")
- ("nu" "ν")
- ("xi" "ξ")
- ("pi" "π")
- ("rho" "ρ")
- ("sigma" "σ")
- ("tau" "τ")
- ("upsilon" "υ")
- ("phi" "ϕ")
- ("chi" "χ")
- ("psi" "ψ")
- ("omega" "ω")
- ("Gamma" "Γ")
- ("Delta" "Δ")
- ("Theta" "Θ")
- ("Lambda" "Λ")
- ("Xi" "Ξ")
- ("Pi" "Π")
- ("Sigma" "Σ")
- ("Upsilon" "Υ")
- ("Phi" "Φ")
- ("Psi" "Ψ")
- ("Omega" "Ω")
- ;; logic
- ("forall" "∀")
- ("exists" "∃")
- ("num" "ℕ" type) ;; ?
- ("complex" "ℂ" type)
- ("real" "ℝ" type)
- ("int" "ℤ" type)
- ("rat" "ℚ" type)
- ("bool" "B" underline type)
- ("false" "false" bold sans)
- ("true" "true" bold sans)
-
- ("lhd" "⊲")
- ("rhd" "⊳")
- ("<=" "≤")
- (">=" "≥")
- ("=>" "⇒")
- ("->" "→") ; or ⟶ or ⟹ if you prefer
- ("<-" "←") ; or ⟵ or ⟸
- ("<->" "↔") ; or ⟷ ...
- ("++" "⧺")
- ("<<" "《")
- (">>" "》")
-
- ;; Equivalence
- ("===" "≡") ; equiv
- ("=/=" "≢") ; complement equiv
- ("=~=" "≅") ; pequiv
- ("==b" "≡") ; NB: same presentation
- ("<>b" "≢") ; NB: same presentation
-
- ("-->" "⟹-") ; Morphisms
- ("++>" "⟹+") ;
- ("==>" "⟹") ;
-
- (":=" "≔")
- ("|-" "⊢")
- ("<>" "≠")
- ("-|" "⊣")
- ("\\/" "∨")
- ("/\\" "∧")
- ("~" "¬")
- )
- ;; an alist of token name, unicode char sequence
- "Table mapping Coq tokens to Unicode strings.
-
-You can adjust this table to add entries, or to change entries for
-glyphs that not are available in your Emacs or chosen font.
-
-When a file is visited, tokens are replaced by the strings
-in this table. When the file is saved, the reverse is done.
-The string mapping can be anything, but should be such that
-tokens can be uniquely recovered from a decoded text; otherwise
-results will be undefined when files are saved."
- :type 'unicode-tokens-token-symbol-map
- :set 'hol-light-unicode-tokens-set
- :group 'coq
- :tag "Coq Unicode Token Mapping")
-
-(defcustom hol-light-shortcut-alist
- '(; short cut, REAL unicode string
- ("<>" . "⋄")
- ("|>" . "⊳")
- ("\\/" . "∨")
- ("/\\" . "∧")
- ("+O" . "⊕")
- ("-O" . "⊖")
- ("xO" . "⊗")
- ("/O" . "⊘")
- (".O" . "⊙")
- ("|+" . "†")
- ("|++" . "‡")
- ("<=" . "≤")
- ("|-" . "⊢")
- (">=" . "≥")
- ("-|" . "⊣")
- ("||" . "∥")
- ("==" . "≡")
- ("~=" . "≃")
- ("~~~" . "≍")
- ("~~" . "≈")
- ("~==" . "≅")
- ("|<>|" . "⋈")
- ("|=" . "⊨")
- ("=." . "≐")
- ("_|_" . "⊥")
- ("</" . "≮")
- (">=/" . "≱")
- ("=/" . "≠")
- ("==/" . "≢")
- ("~/" . "≁")
- ("~=/" . "≄")
- ("~~/" . "≉")
- ("~==/" . "≇")
- ("<-" . "←")
- ("<=" . "⇐")
- ("->" . "→")
- ("=>" . "⇒")
- ("<->" . "↔")
- ("<=>" . "⇔")
- ("|->" . "↦")
- ("<--" . "⟵")
- ("<==" . "⟸")
- ("-->" . "⟶")
- ("==>" . "⟹")
- ("<==>" . "⟷")
- ("|-->" . "⟼")
- ("<--" . "←⎯")
- ("<-->" . "⟷")
- ("<<" . "⟪")
- ("[|" . "⟦")
- (">>" . "⟫")
- ("|]" . "⟧")
- ("``" . "”")
- ("''" . "“")
- ("--" . "–")
- ("---" . "—")
- ("''" . "″")
- ("'''" . "‴")
- ("''''" . "⁗")
- (":=" . "≔")
- ;; some word shortcuts, started with backslash otherwise
- ;; too annoying, perhaps.
- ("\\int" . "ℤ")
- ("\\rat" . "ℚ")
- ("\\complex" . "ℂ")
- ("\\euro" . "€")
- ("\\yen" . "¥")
- ("\\cent" . "¢"))
- "Shortcut key sequence table for Unicode strings.
-
-You can adjust this table to add more entries, or to change entries for
-glyphs that not are available in your Emacs or chosen font.
-
-These shortcuts are only used for input; no reverse conversion is
-performed. This means that the target strings need to have a defined
-meaning to be useful."
- :type '(repeat (cons (string :tag "Shortcut sequence")
- (string :tag "Unicode string")))
- :set 'hol-light-unicode-tokens-set
- :group 'coq
- :tag "Coq Unicode Input Shortcuts")
-
-
-;;
-;; Controls
-;;
-
-(defconst hol-light-control-char-format-regexp
- ;; FIXME: fix Coq identifier syntax below
- "\\(\s*%s\s*\\)\\([a-zA-Z0-9']+\\)")
-
-(defconst hol-light-control-char-format " %s ")
-
-(defconst hol-light-control-characters
- '(("Subscript" "__" sub)
- ("Superscript" "^^" sup)))
-
-(defconst hol-light-control-region-format-regexp
"\\(\s*%s\{\\)\\([^}]*\\)\\(\}\s*\\)")
-
-(defconst hol-light-control-regions
- '(("Subscript" "," "" sub)
- ("Superscript" "^" "" sup)
- ("Bold" "BOLD" "" bold)
- ("Italic" "ITALIC" "" italic)
- ("Script" "SCRIPT" "" script)
- ("Frakt" "FRACT" "" frakt)
- ("Roman" "ROMAN" "" serif)))
-
-
-(provide 'hol-light-unicode-tokens)
-
-;;; hol-light-unicode-tokens.el ends here
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
deleted file mode 100644
index 808e04a..0000000
--- a/hol-light/hol-light.el
+++ /dev/null
@@ -1,519 +0,0 @@
-;;; hol-light.el --- Basic Proof General instance for HOL Light
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017 Pierre Courtieu
-;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
-;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-
-;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
-;; Mark Adams <mark@proof-technologies.com>
-
-;;; Commentary:
-;;
-;; See the README file in this directory for information.
-;;
-
-;;; Code:
-
-(require 'proof-easy-config) ; easy configure mechanism
-(require 'proof-syntax) ; functions for making regexps
-
-(proof-try-require 'caml-font) ; use OCaml Emacs mode syntax
-
-(eval-when-compile
- (require 'proof-tree))
-
-(defcustom hol-light-home
- (or (getenv "HOLLIGHT_HOME")
- (concat (getenv "HOME") "/hol_light"))
- "*Directory holding the local installation of HOL Light."
- :type 'string
- :group 'hol-light)
-
-(defcustom hol-light-prog-name
- (or (getenv "HOLLIGHT_OCMAL")
- (getenv "OCAML")
- "ocaml")
- "*Name of the OCaml interpreter to launch HOL Light."
- :type 'string
- :group 'hol-light)
-
-(defcustom hol-light-use-custom-toplevel t
- "*If non-nil, we use a custom toplevel for Proof General.
-This configures extra annotations inside HOL Light to help
-recognise portions of output from the proof assistant.
-
-If this is incompatible with your usage of HOL Light for
-some reason, you can change this setting to run in a
-degraded (less robust) way which interfaces with the
-standard top level.
-
-You need to restart Emacs if you change this setting."
- :type 'boolean
- :group 'hol-light)
-
-(defconst hol-light-pre-sync-cmd
- (format "#use \"%shol-light/pg_prompt.ml\";; " proof-home-directory)
- "Command used to configure prompt annotations for Proof General.")
-
-(defcustom hol-light-init-cmd
- (append
- (list (format "#cd \"%s\"" hol-light-home)
- "#use \"hol.ml\"")
- (if hol-light-use-custom-toplevel
- (list (format "#use \"%shol-light/pg_tactics.ml\""
- proof-home-directory))
- (list
- "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f
(n-1));;"
- "let pg_undo n = (pg_repeat n (fun ()->let _ = b() in ()); p());;"
- "let pg_kill() = current_goalstack:=[];;"
- "let pg_forget id = ();;"
- "let pg_restart() = print_string \"*** Session restarted.\";;")))
- "*Commands used to start up a running HOL Light session."
- :type '(list string)
- :group 'hol-light)
-
-;;
-;; Regular expressions for matching output with
-;; standard or custom top levels
-;;
-
-(defconst hol-light-plain-start-goals-regexp
- (concat
- "^\\(val it : x?goalstack = \\)"
- "\\(?:.+\n\\)*"
- "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)")
- "Value for `proof-shell-start-goals-regexp' with standard top level.")
-
-(defconst hol-light-annotated-start-goals-regexp
- hol-light-plain-start-goals-regexp
- "Value for `proof-shell-start-goals-regexp' with custom top level.")
-
-(defconst hol-light-plain-interrupt-regexp
- "Interrupted"
- "Value for `proof-shell-interrupt-regexp' with standard top level.")
-
-(defconst hol-light-annotated-interrupt-regexp
- hol-light-plain-interrupt-regexp ;; TODO
- "Value for `proof-shell-interrupt-regexp' with custom top level.")
-
-(defconst hol-light-plain-prompt-regexp
- "\\(val it : unit = ()\n\\)?^# "
- "Value for `proof-shell-annotated-prompt-regexp' with standard top level.")
-
-(defconst hol-light-annotated-prompt-regexp
- "\\(val it : unit = ()\n\\)?<prompt>.*</prompt>"
- "Value for `proof-shell-annotated-prompt-regexp' with custom top level.")
-
-(defconst hol-light-plain-error-regexp
- (proof-regexp-alt "Characters [0-9]+-[0-9]+:"
- "^Exception: Failure"
- "^Parse error: "
- "^Cannot find file"
- "^Error: Unbound value"
- "^Error: Syntax error"
- ;; TODO: more here
- )
- "Value for `proof-shell-error-regexp' with standard top level.")
-
-(defconst hol-light-annotated-error-regexp
- ;; "<error>.+</error>" ;; unfortunately not enough, this is only for failwith
- hol-light-plain-error-regexp
- "Value for `proof-shell-error-regexp' with custom top level.")
-
-(defconst hol-light-plain-proof-completed-regexp
- "Initial goal proved"
- "Value for `proof-shell-proof-completed-regexp' with standard top level.")
-
-(defconst hol-light-annotated-proof-completed-regexp
- hol-light-plain-proof-completed-regexp ;; TODO
- "Value for `proof-shell-proof-completed-regexp' with standard top level.")
-
-(defconst hol-light-plain-message-start
- "^Warning \\|\\*\*\\*"
- "Value for `proof-shell-eager-annotation-start' with standard top level.")
-
-(defconst hol-light-annotated-message-start
- "^Warning \\|\\*\\*\\*" ;; TODO
- "Value for `proof-shell-eager-annotation-start' with custom top level.")
-
-(defconst hol-light-plain-message-end
- "\n" ;; TODO
- "Value for `proof-shell-eager-annotation-start' with standard top level.")
-
-(defconst hol-light-annotated-message-end
- "\n" ;; TODO
- "Value for `proof-shell-eager-annotation-start' with custom top level.")
-
-
-;;;
-;;; State
-;;;
-
-(defvar hol-light-keywords nil)
-(defvar hol-light-rules nil)
-(defvar hol-light-tactics nil)
-(defvar hol-light-tacticals nil)
-
-
-;;;
-;;; Main configuration
-;;;
-
-(proof-easy-config 'hol-light "HOL Light"
- proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/";
- proof-prog-name hol-light-prog-name
- proof-terminal-string ";;"
- proof-shell-pre-sync-init-cmd hol-light-pre-sync-cmd
- proof-shell-init-cmd hol-light-init-cmd
-
- ;; Regexps for matching tactic script inputs: all approximations, of course.
- proof-goal-command-regexp "^g[ `]"
- proof-save-command-regexp "top_thm()"
- proof-goal-with-hole-regexp "let \\(\\([^ \t=]*\\)\\)[ \t]*=[
\t]*prove"
- proof-save-with-hole-regexp "let \\(\\([^ \t=]*\\)\\)[ \t]*=[
\t]*top_thm()"
- proof-non-undoables-regexp "b()" ; and others..
- proof-goal-command "g `%s`;;"
- proof-save-command "val %s = top_thm();;"
- proof-kill-goal-command "pg_kill();;"
- proof-undo-n-times-cmd "pg_undo %s;;"
- proof-forget-id-command "pg_forget \"%s\";;"
- proof-shell-restart-cmd "pg_restart();;"
- proof-showproof-command "p();;"
- proof-auto-multiple-files t
- proof-shell-cd-cmd "#cd \"%s\";;"
- proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\""))
-
- proof-shell-annotated-prompt-regexp (if hol-light-use-custom-toplevel
- hol-light-annotated-prompt-regexp
- hol-light-plain-prompt-regexp)
-
- proof-shell-interrupt-regexp (if hol-light-use-custom-toplevel
- hol-light-annotated-interrupt-regexp
- hol-light-plain-interrupt-regexp)
-
- proof-shell-start-goals-regexp (if hol-light-use-custom-toplevel
- hol-light-annotated-start-goals-regexp
- hol-light-plain-start-goals-regexp)
-
- proof-shell-error-regexp (if hol-light-use-custom-toplevel
- hol-light-annotated-error-regexp
- hol-light-plain-error-regexp)
-
- proof-shell-proof-completed-regexp (if hol-light-use-custom-toplevel
-
hol-light-annotated-proof-completed-regexp
- hol-light-plain-proof-completed-regexp)
-
- proof-shell-eager-annotation-start (if hol-light-use-custom-toplevel
- hol-light-annotated-message-start
- hol-light-plain-message-start)
-
- proof-shell-eager-annotation-end (if hol-light-use-custom-toplevel
- hol-light-annotated-message-end
- hol-light-plain-message-end)
-
-
- ;; FIXME: add optional help topic parameter to help command.
- proof-info-command "help \"hol\""
-
- ;; FIXME: next one needs setting so that "urgent" messages are displayed
- ;; eagerly from HOL.
- ;; proof-shell-eager-annotation-start
- proof-find-theorems-command "DB.match [] (%s);;"
-
- ;;
- ;; Syntax and syntax table entries for proof scripts
- ;;
- proof-script-comment-start "(*"
- proof-script-comment-end "*)"
- proof-script-syntax-table-entries
- '(?\` "\""
- ?\$ "."
- ?\/ "."
- ?\\ "."
- ?+ "."
- ?- "."
- ?= "."
- ?% "."
- ?< "."
- ?> "."
- ?\& "."
- ?. "w"
- ?_ "w"
- ?\' "w"
- ?\| "."
- ?\* ". 23n"
- ?\( "()1"
- ?\) ")(4")
-
- ;;
- ;; A few of the vast variety of keywords, tactics, tacticals,
- ;; for decorating proof scripts.
- ;;
- ;; In the future, PG will use a mechanism for passing identifier
- ;; lists like this from the proof assistant, we don't really
- ;; want to duplicate all this information here!
- ;;
- hol-light-keywords '("g" "expand" "e" "store_thm" "top_thm" "by"
- "Define" "xDefine" "Hol_defn"
- "Induct" "Cases" "Cases_on" "Induct_on"
- "std_ss" "arith_ss" "list_ss"
- "define_type")
-
- hol-light-rules
- '("REFL" "TRANS" "MK_COMB" "ABS" "BETA" "BETA_CONV"
- "ASSUME" "EQ_MP" "DEDUCT_ANTISYM_RULE" "INST_TYPE" "INST"
- "TRUTH" "CONJ" "CONJUNCT1" "CONJUNCT2" "PINST" "PROVE_HYP"
- "T_DEF" "TRUTH" "EQT_ELIM" "EQT_INTRO" "AND_DEF" "CONJ"
- "CONJUNCT1" "CONJUNCT2" "CONJ_PAIR" "CONJUNCTS" "IMP_DEF" "MP"
- "DISCH" "DISCH_ALL" "UNDISCH" "UNDISCH_ALL" "IMP_ANTISYM_RULE" "ADD_ASSUM"
- "EQ_IMP_RULE" "IMP_TRANS" "FORALL_DEF" "SPEC" "SPECL" "SPEC_VAR"
- "SPEC_ALL" "ISPEC" "ISPECL" "GEN" "GENL" "GEN_ALL"
- "EXISTS_DEF" "EXISTS" "SIMPLE_EXISTS" "CHOOSE" "SIMPLE_CHOOSE" "OR_DEF"
- "DISJ1" "DISJ2" "DISJ_CASES" "SIMPLE_DISJ_CASES" "F_DEF" "NOT_DEF"
- "NOT_ELIM" "NOT_INTRO" "EQF_INTRO" "EQF_ELIM" "CONTR" "EXISTS_UNIQUE_DEF"
- "EXISTENCE"
- "EQ_REFL" "REFL_CLAUSE" "EQ_SYM" "EQ_SYM_EQ" "EQ_TRANS"
- "AC" "BETA_THM" "ABS_SIMP" "CONJ_ASSOC" "CONJ_SYM"
- "CONJ_ACI" "DISJ_ASSOC" "DISJ_SYM" "DISJ_ACI" "IMP_CONJ"
- "IMP_IMP" "IMP_CONJ_ALT" "LEFT_OR_DISTRIB" "RIGHT_OR_DISTRIB" "FORALL_SIMP"
- "EXISTS_SIMP" "EQ_IMP" "EQ_CLAUSES" "NOT_CLAUSES_WEAK" "AND_CLAUSES"
- "OR_CLAUSES" "IMP_CLAUSES" "IMP_EQ_CLAUSE" "EXISTS_UNIQUE_THM" "EXISTS_REFL"
- "EXISTS_UNIQUE_REFL" "UNWIND_THM1" "UNWIND_THM2" "FORALL_UNWIND_THM2"
"FORALL_UNWIND_THM1"
- "SWAP_FORALL_THM" "SWAP_EXISTS_THM" "FORALL_AND_THM" "AND_FORALL_THM"
"LEFT_AND_FORALL_THM"
- "RIGHT_AND_FORALL_THM" "EXISTS_OR_THM" "OR_EXISTS_THM" "LEFT_OR_EXISTS_THM"
"RIGHT_OR_EXISTS_THM"
- "LEFT_EXISTS_AND_THM" "RIGHT_EXISTS_AND_THM" "TRIV_EXISTS_AND_THM"
- "LEFT_AND_EXISTS_THM" "RIGHT_AND_EXISTS_THM"
- "TRIV_AND_EXISTS_THM" "TRIV_FORALL_OR_THM"
- "TRIV_OR_FORALL_THM" "RIGHT_IMP_FORALL_THM" "RIGHT_FORALL_IMP_THM"
- "LEFT_IMP_EXISTS_THM" "LEFT_FORALL_IMP_THM" "TRIV_FORALL_IMP_THM"
- "TRIV_EXISTS_IMP_THM" "EXISTS_UNIQUE_ALT" "EXISTS_UNIQUE")
-
- hol-light-tactics
- '("ABS_TAC" "ACCEPT_TAC" "ALL_TAC" "ANTS_TAC" "AP_TERM_TAC"
- "AP_THM_TAC" "ASSUME_TAC" "BETA_TAC" "BINOP_TAC" "CHANGED_TAC"
- "CHEAT_TAC" "CHOOSE_TAC" "CONJ_TAC" "CONTR_TAC" "CONV_TAC"
- "DISCARD_TAC" "DISCH_TAC" "DISJ1_TAC" "DISJ2_TAC" "DISJ_CASES_TAC"
- "EQ_TAC" "EXISTS_TAC" "FAIL_TAC" "GEN_TAC" "LABEL_TAC"
- "MATCH_ACCEPT_TAC" "MATCH_MP_TAC " "META_EXISTS_TAC" "META_SPEC_TAC"
"MK_COMB_TAC"
- "MP_TAC" "NO_TAC" "RECALL_ACCEPT_TAC" "REFL_TAC" "REPLICATE_TAC"
- "RULE_ASSUM_TAC " "SPEC_TAC" "STRIP_ASSUME_TAC" "STRIP_GOAL_THEN"
"STRIP_TAC"
- "STRUCT_CASES_TAC" "SUBGOAL_TAC" "SUBST1_TAC" "SUBST_ALL_TAC"
"SUBST_VAR_TAC"
- "UNDISCH_TAC" "X_CHOOSE_TAC" "X_GEN_TAC" "X_META_EXISTS_TAC")
-
- hol-light-tacticals
- '("ORELSE" "FIRST" "CHANGED_TAC" "THEN" "THENL"
- "EVERY" "REPEAT" "MAP_EVERY"
- "IMP_RES_THEN"
- "FIND_ASSUM" "POP_ASSUM" "ASSUM_LIST" "EVERY_ASSUM" "FIRST_ASSUM"
- "CONJUCTS_THEN" "DISJ_CASES_THEN" "DISCH_THEN" "X_CHOOSE_THEN" "MAP_EVERY"
- "CHOOSE_THEN" "STRIP_THM_THEN" "SUBGOAL_THEN" "FREEZE_THEN")
-
- proof-script-font-lock-keywords
- (append
- (bound-and-true-p caml-font-lock-keywords)
- (list
- (cons (proof-ids-to-regexp hol-light-keywords) 'font-lock-keyword-face)
- (cons (proof-ids-to-regexp hol-light-tactics) 'proof-tactics-name-face)
- (cons (proof-ids-to-regexp hol-light-rules) 'font-lock-keyword-face)
- (cons (proof-ids-to-regexp hol-light-tacticals)
'proof-tacticals-name-face)))
-
- ;;
- ;; Some decoration of the goals output [FIXME: not yet HOL Light]
- ;;
- proof-goals-font-lock-keywords
- (list
- (cons (proof-ids-to-regexp '("Proof manager status"
- "proof" "Incomplete"
- "Initial goal proved"
- "Initial goal"
- "There are currently no proofs"
- "OK"))
- 'font-lock-keyword-face)
- (cons (regexp-quote "------------------------------------")
- 'font-lock-comment-face)
- (cons ": GoalstackPure.goalstack" 'proof-boring-face)
- (cons ": GoalstackPure.proofs" 'proof-boring-face)
- (cons ": Thm.thm" 'proof-boring-face)
- (cons "val it =" 'proof-boring-face))
-
- ;;
- ;; Some decoration of the response output
- ;;
- proof-goals-font-lock-keywords
- (setq
- proof-goals-font-lock-keywords
- (list
- ;; Help system output
- (cons (proof-ids-to-regexp
- '("^----------[-]+$"
- "SYNOPSIS" "DESCRIPTION" "FAILURE CONDITIONS"
- "EXAMPLES" "SEE ALSO"))
- 'font-lock-keyword-face)
- (cons ": GoalstackPure.goalstack" 'proof-boring-face)
- (cons ": GoalstackPure.proofs" 'proof-boring-face)
- (cons ": Thm.thm" 'proof-boring-face)
- (cons "val it =" 'proof-boring-face)))
-
- ;; End of easy config.
- )
-
-
-;;;
-;;; Prooftree configuration (experimental, ongoing)
-;;;
-
-;; regexps for recognising additional markup in output
-
-(defvar hol-light-update-goal-regexp
- (concat "\\[Goal ID \\([0-9]+\\)\\]"
- "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)"))
-
-(defconst hol-light-current-goal-regexp
- ;; match final (focused) subgoal.
- (concat (regexp-quote "[*]")
- "\\[Goal ID \\([0-9]+\\)\\]"
- "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)"))
-
-(defconst hol-light-additional-subgoal-regexp
- "\\[New Goal IDs: \\([0-9 ]+\\)\\]"
- "HOL Light instance of `proof-tree-additional-subgoal-ID-regexp'.")
-
-(defconst hol-light-statenumber-regexp
- "<prompt>\\([0-9]+\\)|\\([0-9]+\\)</prompt>"
- "Regular expression to match prompt with state numbers.
-The first number is a global state counter which increases with
-processed steps. The second number is the number of steps within
-the currently open proof.")
-
-(defconst hol-light-existential-regexp "\\(\\?[0-9]+\\)"
- "Regexp for `proof-tree-existential-regexp'.")
-
-(defconst hol-light-existentials-state-start-regexp "^(dependent evars:"
- "HOL Light instance of `proof-tree-existentials-state-start-regexp'.")
-
-(defconst hol-light-existentials-state-end-regexp ")\n"
- "HOL Light instance of `proof-tree-existentials-state-end-regexp'.")
-
-
-(setq
- ;; These ones belong in script mode config
- proof-tree-configured t
- proof-tree-get-proof-info 'hol-light-get-proof-info
- proof-tree-find-begin-of-unfinished-proof
- 'hol-light-find-begin-of-unfinished-proof
- ;; These ones belong in shell mode
- proof-tree-branch-finished-regexp "No subgoals"
- proof-tree-show-sequent-command
- (lambda (id) (format "print_xgoal_of_id \"%s\";;" id))
-
- proof-tree-current-goal-regexp hol-light-current-goal-regexp
- proof-tree-additional-subgoal-ID-regexp hol-light-additional-subgoal-regexp
- proof-tree-update-goal-regexp hol-light-update-goal-regexp
- proof-tree-cheating-regexp "CHEAT_TAC" ;; others...
-
- proof-tree-existential-regexp hol-light-existential-regexp
- proof-tree-existentials-state-start-regexp
hol-light-existentials-state-start-regexp
- proof-tree-existentials-state-end-regexp
hol-light-existentials-state-end-regexp
- ) ;; end setq proof tree stuff
-
-
-
-;;; get proof info: uses last goals output
-;;; FIXME problem here: this is called BEFORE last goals output
-;;; is set. Can we move order without harming Coq?
-
-;; TEMP to fix compile. Will use Coq-stype annotated prompt for proof tree
now.
-(defvar proof-shell-delayed-output-start nil)
-(defvar proof-shell-delayed-output-end nil)
-(defvar proof-info nil)
-(defvar proof-action-list nil)
-(defun proof-shell-action-list-item (&rest args))
-
-(defconst hol-light-show-sequent-command "print_xgoal_of_id %s;;")
-
-(defun hol-light-get-proof-info ()
- "Return proof info for Prooftree for HOL Light.
-See `proof-tree-get-proof-info'."
- (let ((proof-state-number 0)
- (proof-name "Goal")) ; no named goals
-
- (when (and t ; (> proof-nesting-depth 0) ; inside a proof
- (string-match hol-light-statenumber-regexp
- proof-shell-last-prompt))
- (setq proof-state-number
- (string-to-number
- (match-string 1 proof-shell-last-prompt))))
- (list
- proof-state-number
- proof-name)))
-
-(defun hol-light-find-begin-of-unfinished-proof ()
- ;; Quick hack, we should use some internal proof script stuff here
- (save-excursion
- (re-search-backward "^g" nil t)))
-
-
-;;; FIXME: this is duplicated from coq.el. It might be kind of generic.
-;;; However, for HOL Light the default behaviour is actually to print out
-;;; exactly the new subgoals arising from a previous tactic allocation,
-;;; or the currently focused goal (top of stack).
-
-(defun hol-light-proof-tree-get-new-subgoals ()
- "Check for new subgoals and issue appropriate Show commands.
-This is a hook function for `proof-tree-urgent-action-hook'. This
-function examines the current goal output and searches for new
-unknown subgoals. Those subgoals have been generated by the last
-proof command and we must send their complete sequent text
-eventually to prooftree. Because subgoals may change with
-the next proof command, we must execute the additionally needed
-Show commands before the next real proof command.
-
-The ID's of the open goals are checked with
-`proof-tree-sequent-hash' in order to find out if they are new.
-For any new goal an appropriate Show Goal command with a
-'proof-tree-show-subgoal flag is inserted into
-`proof-action-list'. Then, in the normal delayed output
-processing, the sequent text is send to prooftree as a sequent
-update (see `proof-tree-update-sequent') and the ID of the
-sequent is registered as known in `proof-tree-sequent-hash'.
-
-The not yet delayed output is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
- ;; (message "CPTGNS start %s end %s"
- ;; proof-shell-delayed-output-start
- ;; proof-shell-delayed-output-end)
- (with-current-buffer proof-shell-buffer
- (let ((start proof-shell-delayed-output-start)
- (end proof-shell-delayed-output-end))
- (goto-char start)
- (while (proof-re-search-forward
- hol-light-update-goal-regexp end t)
- (let ((subgoal-id (match-string-no-properties 1)))
- (unless (gethash subgoal-id proof-tree-sequent-hash)
- (setq proof-action-list
- (cons (proof-shell-action-list-item
- (format hol-light-show-sequent-command subgoal-id)
- (proof-tree-make-show-goal-callback (car proof-info))
- '(no-goals-display
- no-response-display
- proof-tree-show-subgoal))
- proof-action-list))))))))
-
-(add-hook 'proof-tree-urgent-action-hook
'hol-light-proof-tree-get-new-subgoals)
-
-
-;;;
-;;; Menu commands
-;;;
-
-(proof-definvisible hol-light-dump-proof "dump_proof();;")
-
-(defpgdefault menu-entries
- '(["Dump refactored proof" hol-light-dump-proof t]))
-
-(provide 'hol-light)
diff --git a/hol-light/pg_prompt.ml b/hol-light/pg_prompt.ml
deleted file mode 100644
index b14c01c..0000000
--- a/hol-light/pg_prompt.ml
+++ /dev/null
@@ -1,59 +0,0 @@
-(* ========================================================================= *)
-(* HOL Light tweaks for Proof General. *)
-(* *)
-(* Mark Adams, David Aspinall. *)
-(* LFCS, School of Informatics, University of Edinburgh
*)
-(* *)
-(* (c) Copyright University of Edinburgh and authors, 2012. *)
-(* *)
-(* This file adjust the OCaml prompt to help Proof General synchronization. *)
-(* It is loaded before HOL Light. *)
-(* ========================================================================= *)
-
-
-(* ------------------------------------------------------------------------- *)
-(* Proof General mode, providing extra annotations in output *)
-(* ------------------------------------------------------------------------- *)
-
-let pg_mode = ref (true : bool);;
-
-let pg_mode_on () = (pg_mode := true);;
-let pg_mode_off () = (pg_mode := false);;
-
-let pg_prompt_info = ref (fun () -> "");;
-
-
-(* ------------------------------------------------------------------------- *)
-(* Adjust the OCaml prompt to carry information for Proof General *)
-(* ------------------------------------------------------------------------- *)
-
-let original_prompt_fn = !Toploop.read_interactive_input in
-(Toploop.read_interactive_input :=
- fun prompt buffer len ->
- let prompt' =
- if (!pg_mode)
- then "<prompt>" ^
- (!pg_prompt_info()) ^
- "</prompt>"
- else prompt in
- original_prompt_fn prompt' buffer len);;
-
-
-(* ------------------------------------------------------------------------- *)
-(* Adjust error printing to markup error messages *)
-(* ------------------------------------------------------------------------- *)
-
-(* Doesn't really work, as many errors are from OCaml top level and
- not printed in this way.
-
-let print_exn e =
- match e with
- Failure x -> Format.print_string
- (if (!pg_mode) then
- "<error>" ^ x ^ "</error>"
- else x)
- | _ -> Format.print_string (Printexc.to_string e);;
-
-#install_printer print_exn;;
-
-*)
diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml
deleted file mode 100644
index 2943f46..0000000
--- a/hol-light/pg_tactics.ml
+++ /dev/null
@@ -1,349 +0,0 @@
-(* ========================================================================= *)
-(* HOL Light subgoal package amended for Proof General and Prooftree. *)
-(* *)
-(* Mark Adams, David Aspinall. *)
-(* LFCS, School of Informatics, University of Edinburgh
*)
-(* *)
-(* (c) Copyright University of Edinburgh and authors, 2012. *)
-(* *)
-(* This file contains some functions that are modified from the
*)
-(* original HOL Light code, and is therefore subject to the HOL Light *)
-(* copyright, see the file LICENSE-HOL-LIGHT in this directory.
*)
-(* *)
-(* ========================================================================= *)
-(* *)
-(* This file overwrites HOL Light's subgoal package commands with variants *)
-(* that output additional annotations specifically for Prooftree. These get *)
-(* intercepted by Proof General, which removes them from the output *)
-(* displayed to the Proof General user.
*)
-
-(* TODO:
- 1. add urgent message annotations for errors and strings output during
- long-running tactics
- 2. fix on/off: don't turn off prompt annotation, support Prooftree on/off.
-*)
-
-(* ------------------------------------------------------------------------- *)
-(* Goal counter for providing goal ids. *)
-(* ------------------------------------------------------------------------- *)
-
-type goal_id = int;;
-
-let string_of_goal_id id = string_of_int id;;
-
-let the_goal_counter = ref (0 : goal_id);;
-
-let inc_goal_counter () =
- (the_goal_counter := !the_goal_counter + 1);;
-
-let reset_goal_counter () =
- (the_goal_counter := 0;
- !the_goal_counter);;
-
-(* ------------------------------------------------------------------------- *)
-(* An xgoal extends a goal with an identity. *)
-(* ------------------------------------------------------------------------- *)
-
-type xgoal = goal * goal_id;;
-
-let dest_xgoal (gx : xgoal) = gx;;
-
-(* ------------------------------------------------------------------------- *)
-(* The xgoalstate is like goalstate but for xgoals instead of goals. *)
-(* ------------------------------------------------------------------------- *)
-
-type xgoalstate = (term list * instantiation) * xgoal list * justification;;
-
-(* ------------------------------------------------------------------------- *)
-(* A goalstack but for xgoals. Overwrites original HL datatype. *)
-(* ------------------------------------------------------------------------- *)
-
-type goalstack = xgoalstate list;;
-
-(* ------------------------------------------------------------------------- *)
-(* A refinement but for xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-type xrefinement = xgoalstate -> xgoalstate;;
-
-(* ------------------------------------------------------------------------- *)
-(* Instantiation of xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-let (inst_xgoal:instantiation->xgoal->xgoal) =
- fun p ((thms,w),id) ->
- (map (I F_F INSTANTIATE_ALL p) thms,instantiate p w),id;;
-
-(* ------------------------------------------------------------------------- *)
-(* A printer for xgoals and xgoalstacks. *)
-(* ------------------------------------------------------------------------- *)
-
-let the_new_goal_ids = ref ([] : goal_id list);;
-
-let the_tactic_flag = ref false;;
-
-let print_string_seplist sep xs =
- if (xs = [])
- then ()
- else (print_string (hd xs);
- do_list (fun x -> print_string sep; print_string x) (tl xs));;
-
-let print_xgoal ((g,id) : xgoal) : unit =
- ((if (!pg_mode)
- then (print_string ("[Goal ID " ^ string_of_goal_id id ^ "]");
- print_newline ()));
- print_goal g);;
-
-let (print_xgoalstack:goalstack->unit) =
- let print_xgoalstate k gs =
- let (_,gl,_) = gs in
- let n = length gl in
- let s = if n = 0 then "No subgoals" else
- (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
- ^" ("^(string_of_int n)^" total)" in
- print_string s; print_newline();
- if gl = [] then () else
- (do_list (print_xgoal o C el gl) (rev(1--(k-1)));
- (if (!pg_mode) then print_string "[*]");
- print_xgoal (el 0 gl)) in
- fun l ->
- ((if (!pg_mode) & (!the_tactic_flag)
- then let xs = map string_of_int (!the_new_goal_ids) in
- (the_tactic_flag := false;
- print_string "[New Goal IDs: ";
- print_string_seplist " " xs;
- print_string "]";
- print_newline ()));
- (if l = [] then print_string "Empty goalstack"
- else if tl l = [] then
- let (_,gl,_ as gs) = hd l in
- print_xgoalstate 1 gs
- else
- let (_,gl,_ as gs) = hd l
- and (_,gl0,_) = hd(tl l) in
- let p = length gl - length gl0 in
- let p' = if p < 1 then 1 else p + 1 in
- print_xgoalstate p' gs);
- (if (!pg_mode) then
- let (vs,theta) =
- if (l = []) then ([],[])
- else let ((vs,(_,theta,_)),_,_) = hd l in
- (vs,theta) in
- let foo v =
- let (x,_) = dest_var v in
- "?" (* FIXME: Coq syntax for meta vars is expected by Prooftree *)
- ^ x ^ if (can (rev_assoc v) theta) then " using" else " open" in
- let xs = map foo vs in
- (print_newline();
- print_string "(dependent evars:";
- if xs != [] then
- (print_string " ";
- print_string_seplist ", " xs;
- print_string ",");
- print_string ")";
- print_newline ())));;
-
-(* ------------------------------------------------------------------------- *)
-(* Goal labelling, for fresh xgoals. *)
-(* ------------------------------------------------------------------------- *)
-
-let label_goals (gs : goal list) : xgoal list =
- let gxs = map (fun g -> inc_goal_counter (); (g, !the_goal_counter))
- gs in
- (the_new_goal_ids := map snd gxs;
- gxs);;
-
-(* ------------------------------------------------------------------------- *)
-(* Version of 'by' for xrefinements. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xby:tactic->xrefinement) =
- fun tac ((mvs,inst),glsx,just) ->
- let gx = hd glsx
- and oglsx = tl glsx in
- let (g,id) = dest_xgoal gx in
- let ((newmvs,newinst),subgls,subjust) = tac g in
- let subglsx = label_goals subgls in
- let n = length subglsx in
- let mvs' = union newmvs mvs
- and inst' = compose_insts inst newinst
- and glsx' = subglsx @ map (inst_xgoal newinst) oglsx in
- let just' i ths =
- let i' = compose_insts inst' i in
- let cths,oths = chop_list n ths in
- let sths = (subjust i cths) :: oths in
- just i' sths in
- (mvs',inst'),glsx',just';;
-
-(* ------------------------------------------------------------------------- *)
-(* Rotate but for xgoalstate. Only change is different ML datatype. *)
-(* ------------------------------------------------------------------------- *)
-
-let (xrotate:int->xrefinement) =
- let rotate_p (meta,sgs,just) =
- let sgs' = (tl sgs)@[hd sgs] in
- let just' i ths =
- let ths' = (last ths)::(butlast ths) in
- just i ths' in
- (meta,sgs',just')
- and rotate_n (meta,sgs,just) =
- let sgs' = (last sgs)::(butlast sgs) in
- let just' i ths =
- let ths' = (tl ths)@[hd ths] in
- just i ths' in
- (meta,sgs',just') in
- fun n -> if n > 0 then funpow n rotate_p
- else funpow (-n) rotate_n;;
-
-(* ------------------------------------------------------------------------- *)
-(* Perform refinement proof, tactic proof etc. *)
-(* ------------------------------------------------------------------------- *)
-
-let (mk_xgoalstate:goal->xgoalstate) =
- fun (asl,w) ->
- if type_of w = bool_ty then
- null_meta,[((asl,w), reset_goal_counter ())],
- (fun inst [th] -> INSTANTIATE_ALL inst th)
- else failwith "mk_goalstate: Non-boolean goal";;
-
-(* ------------------------------------------------------------------------- *)
-(* The global state counts the total number of proof steps taken. *)
-(* ------------------------------------------------------------------------- *)
-
-let the_pg_global_state = ref 1;;
-
-let inc_pg_global_state () =
- (the_pg_global_state := !the_pg_global_state + 1);;
-
-let dec_pg_global_state n =
- (the_pg_global_state := !the_pg_global_state - n);;
-
-let pg_global_state () = !the_pg_global_state;;
-
-(* ------------------------------------------------------------------------- *)
-(* The proof state number is the length of the current goal stack. *)
-(* ------------------------------------------------------------------------- *)
-
-let the_current_xgoalstack = ref ([] : goalstack);;
-
-let pg_proof_state () = length !the_current_xgoalstack;;
-
-(* ------------------------------------------------------------------------- *)
-(* Subgoal package for xgoals and with a constrained undo protocol for *)
-(* interacting with Proof General to track the state. These overwrite the *)
-(* existing commands and may cause breakage of interactive proofs. *)
-(* *)
-(* The restrictions are: *)
-(* - top_thm may only be called once and closes the currently open proof. *)
-(* - the back command b() is not allowed to appear in a file. *)
-(* *)
-(* ------------------------------------------------------------------------- *)
-
-let (xrefine:xrefinement->goalstack) =
- fun r ->
- let l = !the_current_xgoalstack in
- let h = hd l in
- let res = r h :: l in
- the_current_xgoalstack := res;
- !the_current_xgoalstack;;
-
-let flush_goalstack() =
- let l = !the_current_xgoalstack in
- the_current_xgoalstack := [hd l];;
-
-let e tac =
- let result = xrefine(xby(VALID tac)) in
- (inc_pg_global_state ();
- the_tactic_flag := true;
- result);;
-
-let r n =
- (inc_pg_global_state ();
- xrefine(xrotate n));;
-
-let set_goal(asl,w) =
- let aths = map ASSUME asl in
- (inc_pg_global_state ();
- the_current_xgoalstack :=
- [mk_xgoalstate(map (fun th -> "",th) aths,w)];
- !the_current_xgoalstack);;
-
-let g t =
- let fvs = sort (<) (map (fst o dest_var) (frees t)) in
- (if fvs <> [] then
- let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
- warn true ("Free variables in goal: "^errmsg)
- else ());
- set_goal([],t);;
-
-let p() = !the_current_xgoalstack;;
-
-let b() =
- failwith "Undo with b() is not available in Proof General top level";;
-
-let top_realgoal() =
- let (_,(((asl,w),id)::_),_)::_ = !the_current_xgoalstack in
- asl,w;;
-
-let top_goal() =
- let asl,w = top_realgoal() in
- map (concl o snd) asl,w;;
-
-let plain_top_thm() =
- let (_,[],f)::_ = !the_current_xgoalstack in
- f null_inst [];;
-
-let top_thm() =
- let t = plain_top_thm() in
- (inc_pg_global_state();
- the_current_xgoalstack := [];
- t);;
-
-(* ------------------------------------------------------------------------- *)
-(* Undo handling functions for Proof General *)
-(* ------------------------------------------------------------------------- *)
-
-let pg_undo n =
- let l = !the_current_xgoalstack in
- if length l < n then failwith "pg_undo: called with too many steps"
- else (dec_pg_global_state n;
- the_current_xgoalstack := snd (chop_list n l);
- p());;
-
-let pg_kill() =
- let n = length (!the_current_xgoalstack) in
- (dec_pg_global_state n;
- the_current_xgoalstack := [];
- print_string "*** Proof aborted.\n");;
-
-let pg_forget s =
- print_string ("*** Remove theorem "^s^"\n");;
-
-let pg_restart() =
- print_string "*** Session restarted.\n";;
-
-(* ------------------------------------------------------------------------- *)
-(* Configure the annotated prompt. *)
-(* ------------------------------------------------------------------------- *)
-
-pg_prompt_info :=
- fun () ->
- let pst = pg_proof_state () and gst = pg_global_state () in
- string_of_int gst ^ "|" ^ string_of_int pst;;
-
-(* ------------------------------------------------------------------------- *)
-(* Printing the goal of a given Prooftree goal id. *)
-(* ------------------------------------------------------------------------- *)
-
-let print_xgoal_of_id (id:goal_id) : unit =
- let gsts = !the_current_xgoalstack in
- let find_goal (_,xgs,_) = find (fun (g,id0) -> id0 = id) xgs in
- let xg = tryfind find_goal gsts in
- print_xgoal xg;;
-
-(* ------------------------------------------------------------------------- *)
-(* Install the new goal-related printers. *)
-(* ------------------------------------------------------------------------- *)
-
-#install_printer print_xgoal;;
-#install_printer print_xgoalstack;;
diff --git a/hol-light/temp-prooftree-configure.patch
b/hol-light/temp-prooftree-configure.patch
deleted file mode 100644
index 8716610..0000000
--- a/hol-light/temp-prooftree-configure.patch
+++ /dev/null
@@ -1,25 +0,0 @@
-Index: generic/proof-tree.el
-===================================================================
-RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-tree.el,v
-retrieving revision 12.3
-diff -c -r12.3 proof-tree.el
-*** generic/proof-tree.el 19 Jan 2012 13:23:56 -0000 12.3
---- generic/proof-tree.el 19 Jan 2012 13:25:30 -0000
-***************
-*** 492,498 ****
- "Send the configure message."
- (proof-tree-send-message
- (format "configure for \"%s\" and protocol version %02d"
-! proof-assistant
- proof-tree-protocol-version)
- ()))
-
---- 492,499 ----
- "Send the configure message."
- (proof-tree-send-message
- (format "configure for \"%s\" and protocol version %02d"
-! ;; temporarily pretend every proof assistant is Coq
-! "Coq" ;; was proof-assistant
- proof-tree-protocol-version)
- ()))
-
- [nongnu] elpa/proof-general updated (20412f1 -> 1b1083e), ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 1931c8c 01/13: Remove Twelf support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 48bd86b 02/13: Remove HOL98 support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 73571a5 03/13: Remove CCC support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 8b16d1d 04/13: Remove LEGO support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 23f7895 05/13: Remove Hol-Light support,
ELPA Syncer <=
- [nongnu] elpa/proof-general 6c9c995 12/13: Change the license to GPLv3+ (Fix #198), ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 511226f 09/13: Remove Isabelle/Isar support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 497709f 10/13: AUTHORS: Add notes about copyright status, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 0a295cd 07/13: Remove Plastic support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general e27b1ef 08/13: Remove Lambda-Clam support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general f99cdf2 11/13: Misc cosmetic tweaks that occurred during GPLv3+ license work, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general da5f073 06/13: Remove ACL2 support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 1b1083e 13/13: Merge pull request #627 from ProofGeneral/scratch-GPLv3, ELPA Syncer, 2021/11/25