(*
  File:        aux_definitions.ml

  Description: This file defines a few useful functions

  Author:       (c) Copyright 1989-2008 by Flemming Andersen
  Date:         October 23, 1989
  Last Update:  December 30, 2007
*)

let prove_thm ((thm_name:string), thm_term, thm_tactic) =
    prove (thm_term, thm_tactic);;

(* Uniform error facility *)
let UNITY_ERR (func,mesg) = ( failwith func, Failure mesg );;

(*----------------------------------------------------------------------*)
(* Auxilliary definitions                                               *)
(*----------------------------------------------------------------------*)

let UNDISCH_ALL_TAC =
    let th_tac (th:thm) (tac:tactic) = (MP_TAC th) THEN tac  in
    let u_asml (thml:thm list) = itlist  th_tac thml ALL_TAC in
        POP_ASSUM_LIST u_asml
    ;;

let UNDISCH_ONE_TAC =
    let th_tac (th:thm) (tac:tactic) = (UNDISCH_TAC (concl th)) THEN tac in
    let u_asm  (th:thm) = itlist  th_tac [th] ALL_TAC in
        FIRST_ASSUM u_asm
    ;;

let LIST_INDUCT = list_INDUCT;;

let CONTRAPOS =
  let a = `a:bool` and b = `b:bool` in
  let pth = ITAUT `(a ==> b) ==> (~b ==> ~a)` in
  fun th ->
    try let P,Q = dest_imp(concl th) in
        MP (INST [P,a; Q,b] pth) th
    with Failure _ -> failwith "CONTRAPOS";;


let OP_FIX = 200;;

let new_infix_definition (define_name, name_org, define_term, fixity) =
(
  
let defined_thm            = new_definition define_term           in
  let (infix_num, assoc_str) = get_infix_status name_org            in
  let defined_infix          =
   ( parse_as_infix ( define_name, (infix_num + fixity, assoc_str) ) ) in
    (fst (defined_thm, defined_infix))
);;
(*
get_infix_status
infixes();;

get_prefix_status

prefixes();;

*)

let new_binder_definition def_term def_binder =
(
  let def_thm  = ( new_definition  def_term )   in
  let def_bind = ( parse_as_binder def_binder ) in
    (fst (def_thm, def_bind))
);;