Merge pull request #207 from ptroja/master

HO_MATCH_MP_TAC documentation (and other minor fixes)

help/Docfiles/Arith.is_prenex.doc

@@ -15,11 +15,11 @@ Never fails.
 
 \EXAMPLE
 {
-#is_prenex "!x. ?y. x \/ y";;
-true : bool
+- is_prenex ``!x. ?y. x \/ y``;
+> val it = true : bool
 
-#is_prenex "!x. x ==> (?y. x /\ y)";;
-false : bool
+- is_prenex ``!x. x ==> (?y. x /\ y)``;
+> val it = false : bool
 }
 \USES
 Useful for determining whether it is necessary to apply a prenex normaliser to

help/Docfiles/Arith.is_presburger.doc

@@ -24,17 +24,17 @@ Never fails.
 
 \EXAMPLE
 {
-#is_presburger "!m n p. m < (2 * n) /\ (n + n) <= p ==> m < SUC p";;
-true : bool
+- is_presburger ``!m n p. m < (2 * n) /\ (n + n) <= p ==> m < SUC p``;
+> val it = true : bool
 
-#is_presburger "!m n p q. m < (n * p) /\ (n * p) < q ==> m < q";;
-false : bool
+- is_presburger ``!m n p q. m < (n * p) /\ (n * p) < q ==> m < q``;
+> val it = false : bool
 
-#is_presburger "(m <= n) ==> !p. (m < SUC(n + p))";;
-true : bool
+- is_presburger ``(m <= n) ==> !p. (m < SUC(n + p))``;
+> val it = true : bool
 
-#is_presburger "(m + n) - m = n";;
-true : bool
+- is_presburger ``(m + n) - m = n``;
+> val it = true : bool
 }
 \USES
 Useful for determining whether a decision procedure for Presburger arithmetic

help/Docfiles/Parse.add_rule.doc

@@ -226,7 +226,7 @@ because the {block_style} is {INCONSISTENT}.
 The pretty-printer prefers later rules over earlier rules by
 default (though this choice can be changed with {prefer_form_with_tok}
 (q.v.)), so conditional expressions print using the {if-then-else}
-syntax rather than the {_ => _  | _} syntax.
+syntax rather than the {_ => _ | _} syntax.
 
 \USES
 For making pretty concrete syntax possible.

help/Docfiles/Tactic.HO_MATCH_MP_TAC.doc

@@ -0,0 +1,54 @@
+\DOC HO_MATCH_MP_TAC
+
+\TYPE {HO_MATCH_MP_TAC : thm_tactic}
+
+\SYNOPSIS
+Reduces the goal using a supplied implication, with higher-order matching.
+
+\KEYWORDS
+tactic, modus ponens, implication.
+
+\DESCRIBE
+When applied to a theorem of the form
+{
+   A' |- !x1...xn. s ==> t
+}
+{HO_MATCH_MP_TAC} produces a tactic that reduces a goal whose conclusion
+{t'} is a substitution and/or type instance of {t} to the corresponding
+instance of {s}. Any variables free in {s} but not in {t} will be existentially
+quantified in the resulting subgoal:
+{
+     A ?- t'
+  ======================  MATCH_MP_TAC (A' |- !x1...xn. s ==> t)
+     A ?- ?z1...zp. s'
+}
+where {z1}, ..., {zp} are (type instances of) those variables among
+{x1}, ..., {xn} that do not occur free in {t}. Note that this is not a valid
+tactic unless {A'} is a subset of {A}.
+
+\EXAMPLE
+The following goal might be solved by case analysis:
+{
+  > g `!n:num. n <= n * n`;
+}
+We can ``manually'' perform induction by using the following theorem:
+{
+  > numTheory.INDUCTION;
+  - val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)
+}
+which is useful with {HO_MATCH_MP_TAC} because of higher-order matching:
+{
+  > e(HO_MATCH_MP_TAC numTheory.INDUCTION);
+  - val it : goalstack = 1 subgoal (1 total)
+
+  `0 <= 0 * 0 /\ (!n. n <= n * n ==> SUC n <= SUC n * SUC n)`
+}
+The goal can be finished with {SIMP_TAC arith_ss []}.
+
+\FAILURE
+Fails unless the theorem is an (optionally universally quantified) implication
+whose consequent can be instantiated to match the goal.
+
+\SEEALSO
+Tactic.MATCH_MP_TAC, bossLib.Induct_on, Thm.EQ_MP, Drule.MATCH_MP, Thm.MP, Tactic.MP_TAC, ConseqConv.CONSEQ_CONV_TAC.
+\ENDDOC

help/Docfiles/Tactic.MATCH_MP_TAC.doc

@@ -19,7 +19,7 @@ instance of {s}. Any variables free in {s} but not in {t} will be existentially
 quantified in the resulting subgoal:
 {
      A ?- !v1...vi. t'
-  ======================  MATCH_MP_TAC (A' |- !x1...xn. s ==> !y1...tm. t)
+  ======================  MATCH_MP_TAC (A' |- !x1...xn. s ==> !y1...ym. t)
      A ?- ?z1...zp. s'
 }
 where {z1}, ..., {zp} are (type instances of) those variables among

help/Docfiles/Theory.new_type.doc

@@ -19,17 +19,17 @@ the current theory.
 A non-definitional version of ZF set theory might declare a new type {set} and 
 start using it as follows:
 {
-   - new_theory"ZF";
+   - new_theory "ZF";
    <<HOL message: Created theory "ZF">>
    > val it = () : unit
 
-   - new_type("set", 0);;
+   - new_type ("set", 0);
    > val it = () : unit
 
    - new_constant ("mem", Type`:set->set->bool`);
    > val it = () : unit
 
-   - new_axiom("EXT", Term`(!z. mem z x = mem z y) ==> (x = y)`);
+   - new_axiom ("EXT", Term`(!z. mem z x = mem z y) ==> (x = y)`);
    > val it = |- (!z. mem z x = mem z y) ==> (x = y) : thm
 }
 

help/Docfiles/Thm.mk_oracle_thm.doc

@@ -54,7 +54,7 @@ of inference.
    - val SimonThm = mk_oracle_thm tag;
    > val SimonThm = fn : term list * term -> thm
 
-   - val th = SimonThm ([], Term `!x. x`);;
+   - val th = SimonThm ([], Term `!x. x`);
    > val th = |- !x. x : thm
 
    - val th1 = SPEC F th;
@@ -75,7 +75,6 @@ Tags accumulate in a manner similar to logical hypotheses.
    > val it = [oracles: Serena, SimonSays] [axioms: ] [] |- F /\ T : thm
 }
 
-
 \COMMENTS
 It is impossible to detach a tag from a theorem.
 

help/Docfiles/boolSyntax.new_binder.doc

@@ -24,10 +24,10 @@ Fails if the type does not correspond to the above pattern.
 \EXAMPLE
 {
    - new_theory "anorak";
-   () : unit
+   > val it = () : unit
 
-   - new_binder ("!!", (bool-->bool)-->bool);;
-   () : unit
+   - new_binder ("!!", (bool-->bool)-->bool);
+   > val it = () : unit
 
    - Term `!!x. T`;
    > val it = `!! x. T` : term

help/Docfiles/holCheckLib.get_results.doc

@@ -1,6 +1,6 @@
 \DOC get_results
 
-\TYPE {get_results : model ->  (term_bdd * thm option * term list option) list option}
+\TYPE {get_results : model -> (term_bdd * thm option * term list option) list option}
 
 \SYNOPSIS
 Returns the results of model checking the HolCheck model, if the model has been checked. 

help/Docfiles/numLib.ARITH_CONV.doc

@@ -58,34 +58,34 @@ A simple example containing a free variable:
 A more complex example with subtraction and universal quantifiers, and
 which is not initially in prenex normal form:
 {
-   #ARITH_CONV
-   # "!m p. p < m ==> !q r. (m < (p + q) + r) ==> ((m - p) < q + r)";;
-   |- (!m p. p < m ==> (!q r. m < ((p + q) + r) ==> (m - p) < (q + r))) = T
+   - ARITH_CONV
+     ``!m p. p < m ==> !q r. (m < (p + q) + r) ==> ((m - p) < q + r)``;
+   > val it = |- (!m p. p < m ==> (!q r. m < ((p + q) + r) ==> (m - p) < (q + r))) = T
 }
 Two examples with existential quantifiers:
 {
-   #ARITH_CONV "?m n. m < n";;
-   |- (?m n. m < n) = T
+   - ARITH_CONV ``?m n. m < n``;
+   > val it = |- (?m n. m < n) = T
 
-   #ARITH_CONV "?m n. (2 * m) + (3 * n) = 10";;
-   |- (?m n. (2 * m) + (3 * n) = 10) = T
+   - ARITH_CONV ``?m n. (2 * m) + (3 * n) = 10``;
+   > val it = |- (?m n. (2 * m) + (3 * n) = 10) = T
 }
 An instance of a universally quantified formula involving a conditional
 statement and subtraction:
 {
-   #ARITH_CONV
-   # "((p + 3) <= n) ==> (!m. ((m EXP 2 = 0) => (n - 1) | (n - 2)) > p)";;
-   |- (p + 3) <= n ==> (!m. ((m EXP 2 = 0) => n - 1 | n - 2) > p) = T
+   - ARITH_CONV
+     ``((p + 3) <= n) ==> (!m. ((m EXP 2 = 0) => (n - 1) | (n - 2)) > p)``;
+   > val it = |- (p + 3) <= n ==> (!m. ((m EXP 2 = 0) => n - 1 | n - 2) > p) = T
 }
 Failure due to mixing quantifiers:
 {
-   #ARITH_CONV "!m. ?n. m < n";;
+   - ARITH_CONV ``!m. ?n. m < n``;
    evaluation failed     ARITH_CONV -- formula not in the allowed subset
 }
 Failure because the truth of the formula relies on the fact that the
 variables cannot have fractional values:
 {
-   #ARITH_CONV "!m n. ~(SUC (2 * m) = 2 * n)";;
+   - ARITH_CONV ``!m n. ~(SUC (2 * m) = 2 * n)``;
    evaluation failed     ARITH_CONV -- cannot prove formula
 }
 \SEEALSO

src/1/Tactic.sml

@@ -909,7 +909,7 @@ fun HO_MATCH_MP_TAC th =
          in
             MP (DISCH tm (GEN_ALL (DISCH tm3 (UNDISCH th3)))) th
          end
-         handle HOL_ERR _ => raise ERR "MATCH_MP_TAC" "Bad theorem"
+         handle HOL_ERR _ => raise ERR "HO_MATCH_MP_TAC" "Bad theorem"
       val match_fun = HO_PART_MATCH (snd o dest_imp_only) sth
    in
       fn (asl, w) =>

src/parse/HOLtokens.sig

@@ -10,6 +10,6 @@ sig
 
   val ANDNOT : charclass * charclass -> charclass
   val OR : charclass * charclass -> charclass
-   val ITEMS : string -> charclass
+  val ITEMS : string -> charclass
   val ITEM : char -> charclass
 end