Jordan/tactics_ext.ml

   1 (* This file is in severe need of a rewrite! *)
   2
   3 unambiguous_interface();;
   4 prioritize_real();;
   5
   6 (* ------------------------------------------------------------------------- *)
   7 (* A printer that reverses the assumption list *)
   8 (* ------------------------------------------------------------------------- *)
   9
  10 (*
  11
  12    Objective version of HOL-light uses (rev asl) in the method print_goal.
  13    This means that the numbers printed next to the assumptions
  14    are the reverse of the numbering in the list.
  15
  16    I want it the opposite way.
  17    This reverses the numbering on the assumption list,
  18    so that the printed numbers match the list order.
  19
  20    To use, type
  21    #install_printer print_rev_goal;;
  22    #install_printer print_rev_goalstack;;
  23
  24    To restore HOL-light defaults, type
  25    #install_printer print_goal;;
  26    #install_printer print_goalstack;;
  27
  28 *)
  29
  30 let (print_rev_goal:goal->unit) =
  31   fun (asl,w) ->
  32     print_newline();
  33     if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
  34     print_qterm w; print_newline();;
  35
  36 let (print_rev_goalstate:int->goalstate->unit) =
  37   fun k gs -> let (_,gl,_) = gs in
  38               let n = length gl in
  39               let s = if n = 0 then "No subgoals" else
  40                         (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
  41                      ^" ("^(string_of_int n)^" total)" in
  42               print_string s; print_newline();
  43               if gl = [] then () else
  44               do_list (print_rev_goal o C el gl) (rev(0--(k-1)));;
  45
  46 let (print_rev_goalstack:goalstack->unit) =
  47   fun l ->
  48     if l = [] then print_string "Empty goalstack"
  49     else if tl l = [] then
  50       let (_,gl,_ as gs) = hd l in
  51       print_rev_goalstate 1 gs
  52     else
  53       let (_,gl,_ as gs) = hd l
  54       and (_,gl0,_) = hd(tl l) in
  55       let p = length gl - length gl0 in
  56       let p' = if p < 1 then 1 else p + 1 in
  57       print_rev_goalstate p' gs;;
  58
  59 #install_printer print_rev_goal;;
  60 #install_printer print_rev_goalstack;;
  61
  62
  63
  64
  65 (* ------------------------------------------------------------------ *)
  66 (* SOME EASY TACTICS *)
  67 (* ------------------------------------------------------------------ *)
  68
  69 let TAUT_TAC t = (MATCH_MP_TAC (TAUT t));;
  70
  71 let REP_GEN_TAC = REPEAT GEN_TAC;;
  72
  73 let SUBGOAL_TAC t = SUBGOAL_THEN t MP_TAC;;
  74
  75 let DISCH_ALL_TAC = REP_GEN_TAC THEN
  76   let tac = TAUT_TAC `(b ==> a==> c) ==> (a /\ b ==> c)` in
  77   (REPEAT ((REPEAT tac) THEN DISCH_TAC)) THEN LABEL_ALL_TAC;;
  78
  79 (* ------------------------------------------------------------------ *)
  80 (* TACTICS BY NUMBER. These are probably best avoided.
  81    NB:
  82    The numbering is that in the asm list -- not the printed numbers!  *)
  83 (* ------------------------------------------------------------------ *)
  84
  85 let (UNDISCH_EL_TAC:int -> tactic) =
  86  fun i (asl,w) ->
  87    try let sthm,asl' = (el i asl),(drop i asl) in
  88         let tm = concl (snd (el i asl)) in
  89        let thm = snd sthm in
  90        null_meta,[asl',mk_imp(tm,w)],
  91        fun i [th] -> MP th (INSTANTIATE_ALL i thm)
  92    with Failure _ -> failwith "UNDISCH_EL_TAC";;
  93
  94 (* remove hypotheses by number *)
  95 let rec (POPL_TAC:int list ->tactic) =
  96   let (POP_TAC:int->tactic) =
  97     fun i -> (UNDISCH_EL_TAC i) THEN (TAUT_TAC `B ==> (A==>B)`) in
  98   let renumber i =
  99     map(fun j -> if j<=i then j else (j-1)) in
 100   function [] -> ALL_TAC |
 101       (i::b) -> (POP_TAC i) THEN (POPL_TAC (renumber i b));;
 102
 103 let rec (UNDISCH_LIST:int list -> tactic) =
 104   let renumber i =
 105     map(fun j -> if j<=i then j else (j-1)) in
 106   function [] -> ALL_TAC |
 107       (i::b) -> (UNDISCH_EL_TAC i) THEN (UNDISCH_LIST (renumber i b));;
 108
 109 (* ------------------------------------------------------------------ *)
 110 (*   Transformations of Hypothesis List by LABELS                     *)
 111 (* ------------------------------------------------------------------ *)
 112
 113 type goalthm = goal -> thm;;
 114
 115 let (HYP_INT:int->goalthm) =
 116      fun i->
 117      fun ((asl,_):goal) ->
 118      snd (el i asl);;
 119
 120 let (HYP:string->goalthm) =
 121   fun s (asl,w) ->
 122     try assoc s asl
 123       with Failure _ -> assoc ("Z-"^s) asl;;
 124
 125 let (THM:thm->goalthm) =
 126      fun thm ->
 127      fun (_:goal) -> thm;;
 128
 129 let (H_RULER: (thm list->thm->thm)->(goalthm list)-> goalthm -> tactic) =
 130      fun rule gthl gthm ->
 131      fun ((asl,w) as g:goal) ->
 132      let thl =  map (fun x-> (x g)) gthl in
 133      let th = rule thl  (gthm g) in
 134      ASSUME_TAC th g;;
 135
 136 (* The next few term rules into goal_rules *)
 137 (* H_type (x:type) should return an object
 138    similar to x but with thms made into goalthms *)
 139
 140 let (H_RULE_LIST: (thm list->thm->thm)->(goalthm list)-> goalthm -> goalthm) =
 141      fun rule gthl gthm g ->
 142      let thl =  map (fun x-> (x g)) gthl in
 143      rule thl  (gthm g);;
 144
 145 let H_RULE2 (rule:thm->thm->thm) =
 146   fun gthm1 gthm2 -> H_RULE_LIST (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
 147
 148 let H_RULE (rule:thm->thm) =  fun gthm -> H_RULE_LIST (fun _ th -> rule th) [] gthm;;
 149
 150 let (H_TTAC : thm_tactic -> goalthm -> tactic ) =
 151   fun ttac gthm g -> (ttac (gthm g) g);;
 152
 153 let H_ASSUME_TAC = H_TTAC ASSUME_TAC;;
 154 let INPUT = fun gth -> (H_ASSUME_TAC gth) THEN LABEL_ALL_TAC;;
 155
 156 let H_VAL2 (rule:thm->thm->thm) =
 157   fun gthm1 gthm2 -> H_RULER (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
 158
 159 let H_CONJ = H_VAL2(CONJ);;
 160 let H_MATCH_MP = H_VAL2(MATCH_MP);;
 161
 162 let H_REWRITE_RULE gthml gth = H_RULER REWRITE_RULE gthml gth;;
 163 let H_ONCE_REWRITE_RULE gthml gth = H_RULER ONCE_REWRITE_RULE gthml gth;;
 164 let H_SIMP_RULE = H_RULER SIMP_RULE;;
 165
 166 let H_VAL (rule:thm->thm) = fun gthm -> H_RULER (fun _ th -> rule th) [] gthm;;
 167 let H = H_VAL;;
 168
 169 let H_CONJUNCT1 = H_VAL CONJUNCT1;;
 170 let H_CONJUNCT2 = H_VAL CONJUNCT2;;
 171 let H_EQT_INTRO = H_VAL EQT_INTRO;;
 172 let H_EQT_ELIM  = H_VAL EQT_ELIM;;
 173 let H_SPEC = fun t -> H_VAL(SPEC t);;
 174 let H_GEN = fun t -> H_VAL(GEN t);;
 175 let H_DISJ1 = C (fun t -> H_VAL ((C DISJ1) t));;
 176 let H_DISJ2 =  (fun t -> H_VAL (( DISJ2) t));;
 177   (* beware! One is inverted here. *)
 178 let H_NOT_ELIM = H_VAL (NOT_ELIM);;
 179 let H_NOT_INTRO = H_VAL (NOT_INTRO);;
 180 let H_EQF_ELIM = H_VAL (EQF_ELIM);;
 181 let H_EQF_INTRO = H_VAL (EQF_INTRO);;
 182 let (&&&) = H_RULE2 CONJ;;
 183
 184 let (H_UNDISCH_TAC:goalthm -> tactic) =
 185   fun gthm g ->
 186     let tm = concl(gthm g) in
 187     UNDISCH_TAC tm g;;
 188
 189
 190
 191 (* let upgs tac gs = by tac gs;; *)
 192
 193 let (thm_op:goalthm->goalthm->goalthm) =
 194   fun gt1 gt2 g ->
 195     if (is_eq (snd (strip_forall (concl (gt1 g)))))
 196     then REWRITE_RULE[gt1 g] (gt2 g) else
 197     MATCH_MP (gt1 g) (gt2 g);;
 198
 199 let (COMBO:goalthm list-> goalthm) =
 200   fun gthl -> end_itlist thm_op gthl;;
 201
 202 let INPUT_COMBO = INPUT o COMBO;;
 203