diff options
| author |  mark <> | 2012-02-16 17:09:21 +0000 |
|---|---|---|
| committer | mark <> | 2012-02-16 17:09:21 +0000 |
| commit | af9234996fb53a4e7c0ec404d8dd275df17f1ccd (patch) | |
| tree | f82922967f145b50480494b041178b82e36c5e1c /hol-light | |
| parent | e4438b2984cadf3e60935cb1e37be55e63f063a0 (diff) | |
First version of HOL Light tactic recording.
See INSTRUCTIONS and LIMITATIONS files for more details.
Currently works for flattening "packaged-up" tactic proofs into g/e commands.
Won't work for most proofs because most tactics/thms haven't been promoted.
Support for exporting proof graph as a series of goal pairs.
Support for displaying extra information to be intercepter by PG for Prooftree.
Diffstat (limited to 'hol-light')
21 files changed, 2979 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/INSTRUCTIONS b/hol-light/TacticRecording/INSTRUCTIONS new file mode 100644 index 00000000..86380b93 --- /dev/null +++ b/hol-light/TacticRecording/INSTRUCTIONS @@ -0,0 +1,36 @@ +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 new file mode 100644 index 00000000..56537d47 --- /dev/null +++ b/hol-light/TacticRecording/LIMITATIONS @@ -0,0 +1,18 @@ +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 new file mode 100644 index 00000000..0de31198 --- /dev/null +++ b/hol-light/TacticRecording/biolayout.ml @@ -0,0 +1,30 @@ +(* ========================================================================== *) +(* 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 new file mode 100644 index 00000000..e97ecd0b --- /dev/null +++ b/hol-light/TacticRecording/dltree.ml @@ -0,0 +1,268 @@ +(* ========================================================================== *) +(* 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 new file mode 100644 index 00000000..2f570490 --- /dev/null +++ b/hol-light/TacticRecording/dltree.mli @@ -0,0 +1,22 @@ +(* ========================================================================== *) +(* 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/examples1.ml b/hol-light/TacticRecording/examples1.ml new file mode 100644 index 00000000..b587c18f --- /dev/null +++ b/hol-light/TacticRecording/examples1.ml @@ -0,0 +1,65 @@ +#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 ();; + +#use"TacticRecording/mlexport.ml";; + +print_executed_proof ();; +print_flat_proof ();; +print_thenl_proof ();; +print_optimal_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 new file mode 100644 index 00000000..85f58add --- /dev/null +++ b/hol-light/TacticRecording/examples1_output.txt @@ -0,0 +1,72 @@ +# 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 new file mode 100644 index 00000000..a53baa40 --- /dev/null +++ b/hol-light/TacticRecording/examples2.ml @@ -0,0 +1,45 @@ +#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 new file mode 100644 index 00000000..a8fcdb16 --- /dev/null +++ b/hol-light/TacticRecording/examples3.ml @@ -0,0 +1,110 @@ +#use"hol.ml";; +needs "Library/products.ml";; + +#use "TacticRecording/main.ml";; + +prioritize_real();; + + +(* ** 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 = theorem_wrap "LEMMA_1" LEMMA_1;; + +top_thm ();; +print_executed_proof true;; +print_flat_proof true;; +print_packaged_proof ();; + +g `!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 ();; + +(* 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 ();; + +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 ();; + +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)`;; + +(* 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`]]);; diff --git a/hol-light/TacticRecording/examples3_output.txt b/hol-light/TacticRecording/examples3_output.txt new file mode 100644 index 00000000..18d4901f --- /dev/null +++ b/hol-light/TacticRecording/examples3_output.txt @@ -0,0 +1,36 @@ +# 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; REAL_POW_ADD]) THEN REAL_ARITH_TAC);; + +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 new file mode 100644 index 00000000..3178f656 --- /dev/null +++ b/hol-light/TacticRecording/examples4.ml @@ -0,0 +1,13 @@ +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/graveyard.ml b/hol-light/TacticRecording/graveyard.ml new file mode 100644 index 00000000..db5c733d --- /dev/null +++ b/hol-light/TacticRecording/graveyard.ml @@ -0,0 +1,12 @@ + + +(* Utility for applying tactic and incorproating results into goal tree. *) +(* Takes an "infotactic", i.e. like a normal tactic that works on 'goal' and *) +(* returns 'goalstate', but that also returns 'finfo' which summarises the *) +(* operation. These are easily formed by tagging normal tactics. *) + +let infotactic_wrap0 (infotac:goal->(goalstate*finfo)) (gx:xgoal) : xgoalstate = + let (g,id) = dest_xgoal gx in + let ((meta,gs,just),gst) = infotac g in + let gxs = extend_gtree id gst gs in + (meta,gxs,just);; diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml new file mode 100644 index 00000000..b48dd2da --- /dev/null +++ b/hol-light/TacticRecording/hiproofs.ml @@ -0,0 +1,279 @@ +(* ========================================================================== *) +(* 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 (* Active subgoal *) + | Hatomic of (finfo * int) (* Atomic tactic + arity *) + | Hidentity (* Null, for wiring *) + | Hlabelled of (finfo * 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 dest_atomic_hiproof h = + match h with + Hatomic (info,n) -> (info,n) + | _ -> failwith "dest_atomic_hiproof: Not an atomic 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;; + + + +(* ** 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 (info,h0) + -> let h0' = refactor_hiproof r foo h0 in + Hlabelled (info,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 ((Some"ALL_TAC",[]), _) -> Hidentity + | Hsequence (h1, Hempty) -> h1 + | Hsequence (h1, Hidentity) -> h1 + | Hsequence (Hidentity, h2) -> h2 + | Htensor [] -> Hempty + | Htensor [h0] -> h0 + | Htensor hs0 -> if (forall (fun h0 -> h0 = Hidentity) hs0) + then Hidentity + else Htensor (foldr collapse_tensor hs0 []) + | _ -> h in + refactor_hiproof true trivsimp h;; + + +(* Matching up lists of hiproofs *) + +let rec matchup_hiproofs 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 + Hsequence (h1, Htensor hs2a) :: (matchup_hiproofs hs01 hs2b);; + + +(* Separating out lists of hiproofs *) + +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) 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 ((Some "SUBGOAL_THEN",_),h0) + -> h + | Hlabelled (_,h0) + -> h0 + | _ -> h in + refactor_hiproof true delabel 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])) + | _ -> 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) +(* | Hsequence (h1, Htensor hs2) + -> if (exists is_hsequence hs2) + then let (hs2a,hs2b) = separate_hiproofs hs2 in + Hsequence (Hsequence (h1, Htensor hs2a), Htensor hs2b) + else h *) + | _ -> h in + refactor_hiproof true leftgroup h;; + + +(* THEN insertion *) + +(* Looks for opportunities to use 'THEN' tacticals. Note that this disrupts *) +(* arity consistency. *) + +let thenise_hiproof h = + let thenise h = + match h with + Hsequence (h1, Htensor (h2::h2s)) + -> if (forall (fun h0 -> h0 = h2) h2s) + then Hlabelled ((Some "THEN", []), h) + else h + | Hsequence (h1, Hsequence (Htensor (h2::h2s), h3)) + -> if (forall (fun h0 -> h0 = h2) h2s) + then Hsequence + (Hlabelled ((Some "THEN", []), + Hsequence (h1, Htensor (h2::h2s))), h3) + else h + | _ -> h in + refactor_hiproof false thenise h;; + + + +(* ** OTHER OPERATIONS ** *) + + +(* Tactic trace *) + +(* Gives a 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 (info, _) + -> [info] + | Hidentity + -> [] + | Hlabelled (info,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 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 new file mode 100644 index 00000000..ae66892e --- /dev/null +++ b/hol-light/TacticRecording/lib.ml @@ -0,0 +1,75 @@ + +let rec copy n x = + if (n > 0) then x::(copy (n-1) x) + else [];; + + +(* 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;; + + +(* 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 new file mode 100644 index 00000000..2dd6e6ef --- /dev/null +++ b/hol-light/TacticRecording/main.ml @@ -0,0 +1,14 @@ + +#use "TacticRecording/lib.ml";; +#use "TacticRecording/dltree.mli";; +#use "TacticRecording/dltree.ml";; + +#use "TacticRecording/xthm.ml";; +#use "TacticRecording/xtactics.ml";; +#use "TacticRecording/tacticrec.ml";; +#use "TacticRecording/prooftree.ml";; + +#use "TacticRecording/hiproofs.ml";; +#use "TacticRecording/mlexport.ml";; + +#use "TacticRecording/promote.ml";; diff --git a/hol-light/TacticRecording/mlexport.ml b/hol-light/TacticRecording/mlexport.ml new file mode 100644 index 00000000..ba26034a --- /dev/null +++ b/hol-light/TacticRecording/mlexport.ml @@ -0,0 +1,241 @@ +(* ========================================================================== *) +(* 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. *) + + + +(* Translation to hiproof *) + +let rec gtree_to_hiproof gtr = + let (_,gtrm) = gtr in + match !gtrm with + Gactive + -> Hactive + | Gexit id + -> Hidentity + | Gexecuted (gstp,gtrs) + -> let h1 = + match gstp with + Gatom info | Gbox (info,_,true) + -> Hatomic (info, length gtrs) + | Gbox (info,gtr,false) + -> Hlabelled (info, gtree_to_hiproof gtr) in + let h2 = Htensor (map gtree_to_hiproof gtrs) in + Hsequence (h1,h2);; + + + +(* ** PRINT UTILITIES ** *) + + +(* 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 ^ "`");; + + +(* Printer for 'finfo' *) + +let rec print_farg x0 br arg = + match arg with + Fint n -> print_int n + | Fstring x -> print_fstring x + | Fterm tm -> print_fterm tm + | Ftype ty -> print_ftype ty + | Fthm prf -> print_finfo "<rule>" br prf + | Fpair (arg1,arg2) + -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in + (print_string_if br "("; + print_farg x0 false arg1; + print_string sep; + print_farg x0 false arg2; + print_string_if br ")") + | Flist args + -> let sep = if (forall is_atomic_farg args) then ";" else "; " in + (print_string "["; + print_seplist (print_farg x0 false) sep args; + print_string "]") + | Ffn f + -> (print_finfo x0 br f) + +and print_finfo x0 br ((x_,args):finfo) = + (print_string_if (br & not (is_empty args)) "("; + print_option x0 x_; + do_list (fun arg -> print_string " "; print_farg x0 true arg) args; + print_string_if (br & not (is_empty args)) ")");; + + +(* Printer for tactic 'finfo' *) + +let print_tactic br ((x_,args):finfo) = + print_finfo "<tactic>" br ((x_,args):finfo);; + + +(* 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 info = + (print_tactic_line_with print_tactic info);; + +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 (info,_) + -> print_tactic br info + | Hidentity + -> print_string "ALL_TAC" + | Hlabelled (info,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 ((Some "REPEAT", _), Hsequence (h1,h2)) (* only if repeats *) + -> (print_string_if br "("; + print_string "REPEAT "; + print_hiproof2 true h1; + print_string_if br ")") + | Hlabelled ((Some "THEN", _), + Hsequence (h1, Htensor (h2::h2s))) (* only if tac2 used *) + -> (print_string_if br "("; + print_hiproof2 false h1; + print_string " THEN "; + print_hiproof2 true h2; + print_string_if br ")") + | Hlabelled (((Some "SUBGOAL_THEN", (Fterm tm)::[farg]) as info), _) + -> (print_tactic br info) + | _ -> (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' = (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/promote.ml b/hol-light/TacticRecording/promote.ml new file mode 100644 index 00000000..0b40b5f9 --- /dev/null +++ b/hol-light/TacticRecording/promote.ml @@ -0,0 +1,297 @@ +(* ========================================================================== *) +(* 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 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 CONV_TAC = xCONV_TAC;; +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 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 GSYM = rule_wrap "GSYM" GSYM;; +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 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_CLAUSES = theorem_wrap "ADD_CLAUSES" ADD_CLAUSES;; +let SUB_REFL = theorem_wrap "SUB_REFL" SUB_REFL;; +let ADD1 = theorem_wrap "ADD1" ADD1;; +let LE_1 = theorem_wrap "LE_1" LE_1;; + +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 new file mode 100644 index 00000000..877e738c --- /dev/null +++ b/hol-light/TacticRecording/prooftree.ml @@ -0,0 +1,177 @@ +(* ========================================================================= *) +(* 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 new file mode 100644 index 00000000..0836f87c --- /dev/null +++ b/hol-light/TacticRecording/tacticrec.ml @@ -0,0 +1,527 @@ +(* ========================================================================== *) +(* 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 finfo (* Atomic tactic *) + | Gbox of (finfo * 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 (Some "T1") *) +(* (_, ref *) +(* Gexecuted *) +(* (Gatom (Some "T2"), *) +(* [ (_, ref Gexecuted (Gatom (Some "WF"), [])); *) +(* (_, ref Gexit _) ])), *) +(* [ (_, ref *) +(* Gexecuted *) +(* (Gbox (Some "DP") *) +(* (_, ref *) +(* Gexecuted *) +(* (Gatom (Some "Normalise"), *) +(* [ (_, ref Gexecuted (Gatom (Some "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 info | Gbox (info,_,_) -> info;; + +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 + Gbox (_,gtr,false) -> gtr::(gtree_all_children gtr) + | Gatom _ | Gbox _ -> [];; + + + +(* ** 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 gxs' = zip gs' ids' in + (gtrm := Gexecuted (gstp,gtrs); + gxs');; + + +(* 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";; + + + +(* ** WRAPPER FUNCTIONS ** *) + +(* These functions are for promoting existing tactics and tacticals. *) + + +(* 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 finfo (tac:tactic) (gx:xgoal) : xgoalstate = + let (g,id) = dest_xgoal gx in + let (meta,gs',just) = tac g in + let gxs' = extend_gtree id (Gatom finfo) gs' in + (meta,gxs',just);; + +let tactic_wrap x tac = + tactic_wrap0 (Some x, []) tac;; + +let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic = + tactic_wrap0 (Some x, [Fstring s]) (tac s);; + +let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic = + tactic_wrap0 (Some x, [Fterm tm]) (tac tm);; + +let termpair_tactic_wrap x (tac:term*term->tactic) (tm1,tm2) : xtactic = + tactic_wrap0 (Some x, [Fpair (Fterm tm1, Fterm tm2)]) (tac (tm1,tm2));; + +let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic = + tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms)]) (tac tms);; + +let thm_tactic_wrap x (tac:thm->tactic) (xth:xthm) : xtactic = + let (th,prf) = dest_xthm xth in + tactic_wrap0 (Some x, [Fthm 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 (Some x, [Flist (map (fun prf -> Fthm 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 (Some x, [Fstring s; Fthm prf]) (tac s th);; + + +(* xCONV_TAC - a special case I think; not a tactical *) + +let t_tm = `T`;; + +let xCONV_TAC (cx:xconv) (gx:xgoal) : xgoalstate = + let (g,id) = dest_xgoal gx in + + let (asl,w) = g in + let thx = cx w in + let (th,proof) = dest_xthm thx in + let tm = concl th in + let finfo = (Some "CONV_TAC", [finfo_as_meta_arg proof]) in + + let tac g = + if (aconv tm w) + then (null_meta, [], fun i [] -> INSTANTIATE_ALL i th) + else let l,r = dest_eq tm in + if not (aconv l w) + then failwith "CONV_TAC: bad equation" + else if (r = t_tm) + then (null_meta, [], fun i [] -> INSTANTIATE_ALL i (EQT_ELIM th)) + else (null_meta, [(asl,r)], + fun i [th0] -> EQ_MP (INSTANTIATE_ALL i (SYM th)) th0) in + + let (meta,gs,just) = tac g in + let gxs = extend_gtree id (Gatom finfo) gs in + (meta,gxs,just);; + + +(* 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 finfo (xttcl:'a->xtactic) (arg:'a) (gx:xgoal) : xgoalstate = + let (g,id) = dest_xgoal gx in + let (id0,gtr0) = new_active_subgtree id g in + let gx0 = mk_xgoal (g,id0) in + let (meta,gxs0,just) = xttcl arg gx0 in + let (gs0,ids0) = unzip (map dest_xgoal gxs0) in + let gxs = extend_gtree id (Gbox (finfo,gtr0,false)) gs0 in + let ids = map xgoal_id gxs in + (do_list externalise_gtree (zip ids0 ids); + (meta,gxs,just));; + +let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic = + tactical_wrap0 (Some x, []) xttcl xtac;; + +let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic = + tactical_wrap0 (Some x, []) (xttcl xtac1) xtac2;; + +let int_tactical_wrap x (xttcl:int->'a->xtactic) (n:int) (xtac:'a) : xtactic = + tactical_wrap0 (Some x, [Fint n]) (xttcl n) xtac;; + +let list_tactical_wrap x (xttcl:('a->xtactic)->'a list->xtactic) + (xtac:'a->xtactic) (l:'a list) : xtactic = + tactical_wrap0 (Some x, []) (xttcl xtac) l;; + + +(* xSUBGOAL_THEN - seems to be another special case *) + +let xASSUME = conv_wrap "ASSUME" ASSUME;; + +let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (gx:xgoal) : xgoalstate = + let arg = xASSUME tm in + + let (g,id) = dest_xgoal gx in + let (id0,gtr0) = new_active_subgtree id g in + let gx0 = mk_xgoal (g,id0) in + let (meta,gxs0,just) = ttac arg gx0 in + let (gs0,ids0) = unzip (map dest_xgoal gxs0) in + + let (asl,_) = g in + let g2 = (asl,tm) in + let finfo = (Some "SUBGOAL_THEN", + [Fterm tm; (finfo_as_meta_arg o gtree_tactic) gtr0]) in + + let gxs = extend_gtree id (Gbox (finfo,gtr0,true)) (g2::gs0) in + let ids1 = map xgoal_id (tl gxs) in + let just' = fun i l -> PROVE_HYP (hd l) (just i (tl l)) in + (do_list externalise_gtree (zip ids0 ids1); + (meta,gxs,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);; +*) + + + +(* ** 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 + if t' = t then th else + try EQ_MP (ALPHA t' t) th + with Failure _ -> failwith "prove: justification generated wrong theorem";; + +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 deleted the undone step in the goal tree. *) + +let xb () = + let result = xb () in + let (_,gxs,_) = hd result in + let (_,id) = hd gxs 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/xtactics.ml b/hol-light/TacticRecording/xtactics.ml new file mode 100644 index 00000000..79b81648 --- /dev/null +++ b/hol-light/TacticRecording/xtactics.ml @@ -0,0 +1,449 @@ +(* ========================================================================= *) +(* 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 + if t' = t then th else + try EQ_MP (ALPHA t' t) th + with Failure _ -> failwith "prove: justification generated wrong theorem";; + +(* ------------------------------------------------------------------------- *) +(* 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 + f null_inst [];; + +(* ------------------------------------------------------------------------- *) +(* 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 new file mode 100644 index 00000000..210530fa --- /dev/null +++ b/hol-light/TacticRecording/xthm.ml @@ -0,0 +1,193 @@ + + + +(* ** DATATYPES ** *) + + +type farg = + Fint of int + | Fstring of string + | Fterm of term + | Ftype of hol_type + | Fthm of finfo + | Fpair of farg * farg + | Flist of farg list + | Ffn of finfo + +and finfo = + string option (* Function's name *) + * farg list;; (* Function's args *) + + +(* finfo_as_meta_arg *) + +let finfo_as_meta_arg (info:finfo) = + match info with + (x_, ((_::_) as args)) + -> Ffn (x_, front args) + | _ -> failwith "finfo_as_meta_arg: Unexpected empty rule arg list";; + + +(* Atomic tests *) + +let is_atomic_farg arg = + match arg with + Fthm (_,(_::_)) | Fpair _ -> false + | _ -> true;; + +let is_atomic_finfo ((x_,args):finfo) = (is_empty args);; + + +(* active_info *) + +let active_info = (Some "...", []);; + + +(* The 'xthm' datatype *) + +(* This couples a theorem with an 'finfo' representation of its proof. For *) +(* named ML objects, this 'finfo' will simply be the ML name of the theorem. *) +(* For rule applications, it will capture the rule and its arguments. *) + +type xthm = thm * finfo;; + +type xconv = term -> xthm;; + + +(* Constructors and destructors *) + +let mk_xthm (xth:thm*finfo) : xthm = xth;; + +let mk_xthm0 x th = mk_xthm (th, (Some x, []));; + +let dest_xthm ((th,x):xthm) : thm * finfo = (th,x);; + +let xthm_thm ((th,_):xthm) = th;; + +let xthm_proof ((_,prf):xthm) = prf;; + + + +(* ** WRAPPER FUNCTIONS ** *) + + +(* Theorem wrapper *) + +let theorem_wrap (x:string) (th:thm) : xthm = + (th, (Some x, []));; + + +(* Rule wrappers *) + +(* Lots of rule wrappers are required because there are many different type *) +(* shapes for rules. *) + +let rule_wrap0 finfo (r:'a->thm) (arg:'a) : xthm = + let th' = r arg in + mk_xthm (th',finfo);; + +let conv_wrap x (r:term->thm) (tm:term) : xthm = + rule_wrap0 (Some x, [Fterm tm]) r tm;; + +let thm_conv_wrap x (r:thm->term->thm) (thx:xthm) tm : xthm = + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, [Fthm prf; Fterm tm]) (r th) tm;; + +let thmlist_conv_wrap x (r:thm list->term->thm) thxs (tm:term) : xthm = + let (ths,prfs) = unzip (map dest_xthm thxs) in + rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fterm tm]) + (r ths) tm;; + +let rule_wrap x (r:thm->thm) (thx:xthm) : xthm = + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, [Fthm prf]) r th;; + +let drule_wrap x (r:thm->thm->thm) (thx1:xthm) (thx2:xthm) : xthm = + let (th1,prf1) = dest_xthm thx1 in + let (th2,prf2) = dest_xthm thx2 in + rule_wrap0 (Some x, [Fthm prf1; Fthm prf2]) (r th1) th2;; + +let prule_wrap x (r:thm*thm->thm) ((thx1:xthm),(thx2:xthm)) : xthm = + let (th1,prf1) = dest_xthm thx1 in + let (th2,prf2) = dest_xthm thx2 in + rule_wrap0 (Some x, [Fpair(Fthm prf1, Fthm prf2)]) r (th1,th2);; + +let trule_wrap x (r:thm->thm->thm->thm) + (thx1:xthm) (thx2:xthm) (thx3:xthm) : xthm = + let (th1,prf1) = dest_xthm thx1 in + let (th2,prf2) = dest_xthm thx2 in + let (th3,prf3) = dest_xthm thx3 in + rule_wrap0 (Some x, [Fthm prf1; Fthm prf2; Fthm prf3]) (r th1 th2) th3;; + +let term_rule_wrap x (r:term->thm->thm) tm (thx:xthm) : xthm = + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, [Fterm tm; Fthm prf]) (r tm) th;; + +let termpair_rule_wrap x (r:term*term->thm->thm) (tm1,tm2) (thx:xthm) : xthm = + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, [Fpair(Fterm tm1,Fterm tm2); Fthm prf]) (r (tm1,tm2)) th;; + +let termthmpair_rule_wrap x (r:term*thm->thm->thm) (tm,thx0) (thx:xthm) : xthm = + let (th0,prf0) = dest_xthm thx0 in + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, [Fpair(Fterm tm, Fthm prf0); Fthm prf]) (r (tm,th0)) th;; + +let termlist_rule_wrap x (r:term list->thm->thm) tms (thx:xthm) : xthm = + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms); Fthm prf]) + (r tms) th;; + +let terminst_rule_wrap x (r:(term*term)list->thm->thm) theta (thx:xthm) : xthm = + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, + [Flist (map (fun (tm1,tm2) -> Fpair(Fterm tm1, Fterm tm2)) theta); + Fthm prf]) + (r theta) th;; + +let typeinst_rule_wrap x (r:(hol_type*hol_type)list->thm->thm) + theta (thx:xthm) : xthm = + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, + [Flist (map (fun (tm1,tm2) -> Fpair(Ftype tm1, Ftype tm2)) theta); + Fthm prf]) + (r theta) th;; + +let thmlist_rule_wrap x (r:thm list->thm->thm) thxs (thx:xthm) : xthm = + let (ths,prfs) = unzip (map dest_xthm thxs) in + let (th,prf) = dest_xthm thx in + rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fthm prf]) + (r ths) th;; + + +(* Meta rule wrappers *) + +(* This works by ... *) +(* Fails to give a meta argument if it never gets executed. *) + +let meta_rule_wrap0 finfo0 (mr:('a->thm)->'b->thm) + (xr:'a->xthm) (arg:'b) : xthm = + let temp = ref ((Some "???", []) : finfo) in + let r arg0 = let thx = xr arg0 in + let (th,finfo) = dest_xthm thx in + ((match finfo with + (x_, (_::_ as args)) + -> (temp := (x_, front args)) + | _ -> ()); + th) in + let th' = mr r arg in + let (x_,args0) = finfo0 in + let finfo' = (x_, (Ffn !temp)::args0) in + (th',finfo');; + +let conv_conv_wrap x (mc:conv->conv) (c:term->xthm) (tm:term) : xthm = + meta_rule_wrap0 (Some x, [Fterm tm]) mc c tm;; + + + +(* ** INSTALL PRINTERS ** *) + + +let print_xthm ((th,info):xthm) = print_thm th;; + +#install_printer print_xthm;; + |