Unity/aux_definitions.ml

   1 (*
   2   File:        aux_definitions.ml
   3
   4   Description: This file defines a few useful functions
   5
   6   Author:       (c) Copyright 1989-2008 by Flemming Andersen
   7   Date:         October 23, 1989
   8   Last Update:  December 30, 2007
   9 *)
  10
  11 let prove_thm ((thm_name:string), thm_term, thm_tactic) =
  12     prove (thm_term, thm_tactic);;
  13
  14 (* Uniform error facility *)
  15 let UNITY_ERR (func,mesg) = ( failwith func, Failure mesg );;
  16
  17 (*----------------------------------------------------------------------*)
  18 (* Auxilliary definitions                                               *)
  19 (*----------------------------------------------------------------------*)
  20
  21 let UNDISCH_ALL_TAC =
  22     let th_tac (th:thm) (tac:tactic) = (MP_TAC th) THEN tac  in
  23     let u_asml (thml:thm list) = itlist  th_tac thml ALL_TAC in
  24         POP_ASSUM_LIST u_asml
  25     ;;
  26
  27 let UNDISCH_ONE_TAC =
  28     let th_tac (th:thm) (tac:tactic) = (UNDISCH_TAC (concl th)) THEN tac in
  29     let u_asm  (th:thm) = itlist  th_tac [th] ALL_TAC in
  30         FIRST_ASSUM u_asm
  31     ;;
  32
  33 let LIST_INDUCT = list_INDUCT;;
  34
  35 let CONTRAPOS =
  36   let a = `a:bool` and b = `b:bool` in
  37   let pth = ITAUT `(a ==> b) ==> (~b ==> ~a)` in
  38   fun th ->
  39     try let P,Q = dest_imp(concl th) in
  40         MP (INST [P,a; Q,b] pth) th
  41     with Failure _ -> failwith "CONTRAPOS";;
  42
  43
  44 let OP_FIX = 200;;
  45
  46 let new_infix_definition (define_name, name_org, define_term, fixity) =
  47 (
  48   let defined_thm            = new_definition define_term           in
  49   let (infix_num, assoc_str) = get_infix_status name_org            in
  50   let defined_infix          =
  51    ( parse_as_infix ( define_name, (infix_num + fixity, assoc_str) ) ) in
  52     (fst (defined_thm, defined_infix))
  53 );;
  54
  55 (*
  56 get_infix_status
  57 infixes();;
  58
  59 get_prefix_status
  60
  61 prefixes();;
  62
  63 *)
  64
  65 let new_binder_definition def_term def_binder =
  66 (
  67   let def_thm  = ( new_definition  def_term )   in
  68   let def_bind = ( parse_as_binder def_binder ) in
  69     (fst (def_thm, def_bind))
  70 );;