(* This file is in severe need of a rewrite! *)

unambiguous_interface();;
prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* A printer that reverses the assumption list *)
(* ------------------------------------------------------------------------- *)

(*

   Objective version of HOL-light uses (rev asl) in the method print_goal.
   This means that the numbers printed next to the assumptions
   are the reverse of the numbering in the list.

   I want it the opposite way.
   This reverses the numbering on the assumption list,
   so that the printed numbers match the list order.

   To use, type
   #install_printer print_rev_goal;;
   #install_printer print_rev_goalstack;;

   To restore HOL-light defaults, type
   #install_printer print_goal;;
   #install_printer print_goalstack;;

*)

let (print_rev_goal:goal->unit) =
  fun (asl,w) ->
    print_newline();
    if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
    print_qterm w; print_newline();;

let (print_rev_goalstate:int->goalstate->unit) =
  fun 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_rev_goal o C el gl) (rev(0--(k-1)));;

let (print_rev_goalstack:goalstack->unit) =
  fun l ->
    if l = [] then print_string "Empty goalstack"
    else if tl l = [] then
      let (_,gl,_ as gs) = hd l in
      print_rev_goalstate 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_rev_goalstate p' gs;;

#install_printer print_rev_goal;;
#install_printer print_rev_goalstack;;




(* ------------------------------------------------------------------ *)
(* SOME EASY TACTICS *)
(* ------------------------------------------------------------------ *)

let TAUT_TAC t = (MATCH_MP_TAC (TAUT t));;

let REP_GEN_TAC = REPEAT GEN_TAC;;

let SUBGOAL_TAC t = SUBGOAL_THEN t MP_TAC;;

let DISCH_ALL_TAC = REP_GEN_TAC THEN
  let tac = TAUT_TAC `(b ==> a==> c) ==> (a /\ b ==> c)` in
  (REPEAT ((REPEAT tac) THEN DISCH_TAC)) THEN LABEL_ALL_TAC;;

(* ------------------------------------------------------------------ *)
(* TACTICS BY NUMBER. These are probably best avoided.
   NB:
   The numbering is that in the asm list -- not the printed numbers!  *)
(* ------------------------------------------------------------------ *)

let (UNDISCH_EL_TAC:int -> tactic) =
 fun i (asl,w) ->
   try let sthm,asl' = (el i asl),(drop i asl) in
        let tm = concl (snd (el i asl)) in
       let thm = snd sthm in
       null_meta,[asl',mk_imp(tm,w)],
       fun i [th] -> MP th (INSTANTIATE_ALL i thm)
   with Failure _ -> failwith "UNDISCH_EL_TAC";;

(* remove hypotheses by number *)
let rec (POPL_TAC:int list ->tactic) =
  let (POP_TAC:int->tactic) =
    fun i -> (UNDISCH_EL_TAC i) THEN (TAUT_TAC `B ==> (A==>B)`) in
  let renumber i =
    map(fun j -> if j<=i then j else (j-1)) in
  function [] -> ALL_TAC |
      (i::b) -> (POP_TAC i) THEN (POPL_TAC (renumber i b));;

let rec (UNDISCH_LIST:int list -> tactic) =
  let renumber i =
    map(fun j -> if j<=i then j else (j-1)) in
  function [] -> ALL_TAC |
      (i::b) -> (UNDISCH_EL_TAC i) THEN (UNDISCH_LIST (renumber i b));;

(* ------------------------------------------------------------------ *)
(*   Transformations of Hypothesis List by LABELS                     *)
(* ------------------------------------------------------------------ *)

type goalthm = goal -> thm;;

let (HYP_INT:int->goalthm) =
     fun i->
     fun ((asl,_):goal) ->
     snd (el i asl);;

let (HYP:string->goalthm) =
  fun s (asl,w) ->
    try assoc s asl
      with Failure _ -> assoc ("Z-"^s) asl;;

let (THM:thm->goalthm) =
     fun thm ->
     fun (_:goal) -> thm;;

let (H_RULER: (thm list->thm->thm)->(goalthm list)-> goalthm -> tactic) =
     fun rule gthl gthm ->
     fun ((asl,w) as g:goal) ->
     let thl =  map (fun x-> (x g)) gthl in
     let th = rule thl  (gthm g) in
     ASSUME_TAC th g;;

(* The next few term rules into goal_rules *)
(* H_type (x:type) should return an object
   similar to x but with thms made into goalthms *)

let (H_RULE_LIST: (thm list->thm->thm)->(goalthm list)-> goalthm -> goalthm) =
     fun rule gthl gthm g ->
     let thl =  map (fun x-> (x g)) gthl in
     rule thl  (gthm g);;

let H_RULE2 (rule:thm->thm->thm) =
  fun gthm1 gthm2 -> H_RULE_LIST (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;

let H_RULE (rule:thm->thm) =  fun gthm -> H_RULE_LIST (fun _ th -> rule th) [] gthm;;

let (H_TTAC : thm_tactic -> goalthm -> tactic ) =
  fun ttac gthm g -> (ttac (gthm g) g);;

let H_ASSUME_TAC = H_TTAC ASSUME_TAC;;
let INPUT = fun gth -> (H_ASSUME_TAC gth) THEN LABEL_ALL_TAC;;

let H_VAL2 (rule:thm->thm->thm) =
  fun gthm1 gthm2 -> H_RULER (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;

let H_CONJ = H_VAL2(CONJ);;
let H_MATCH_MP = H_VAL2(MATCH_MP);;

let H_REWRITE_RULE gthml gth = H_RULER REWRITE_RULE gthml gth;;
let H_ONCE_REWRITE_RULE gthml gth = H_RULER ONCE_REWRITE_RULE gthml gth;;
let H_SIMP_RULE = H_RULER SIMP_RULE;;

let H_VAL (rule:thm->thm) = fun gthm -> H_RULER (fun _ th -> rule th) [] gthm;;
let H = H_VAL;;

let H_CONJUNCT1 = H_VAL CONJUNCT1;;
let H_CONJUNCT2 = H_VAL CONJUNCT2;;
let H_EQT_INTRO = H_VAL EQT_INTRO;;
let H_EQT_ELIM  = H_VAL EQT_ELIM;;
let H_SPEC = fun t -> H_VAL(SPEC t);;
let H_GEN = fun t -> H_VAL(GEN t);;
let H_DISJ1 = C (fun t -> H_VAL ((C DISJ1) t));;
let H_DISJ2 =  (fun t -> H_VAL (( DISJ2) t));;
  (* beware! One is inverted here. *)
let H_NOT_ELIM = H_VAL (NOT_ELIM);;
let H_NOT_INTRO = H_VAL (NOT_INTRO);;
let H_EQF_ELIM = H_VAL (EQF_ELIM);;
let H_EQF_INTRO = H_VAL (EQF_INTRO);;
let (&&&) = H_RULE2 CONJ;;

let (H_UNDISCH_TAC:goalthm -> tactic) =
  fun gthm g ->
    let tm = concl(gthm g) in
    UNDISCH_TAC tm g;;



(* let upgs tac gs = by tac gs;; *)

let (thm_op:goalthm->goalthm->goalthm) =
  fun gt1 gt2 g ->
    if (is_eq (snd (strip_forall (concl (gt1 g)))))
    then REWRITE_RULE[gt1 g] (gt2 g) else
    MATCH_MP (gt1 g) (gt2 g);;

let (COMBO:goalthm list-> goalthm) =
  fun gthl -> end_itlist thm_op gthl;;

let INPUT_COMBO = INPUT o COMBO;;