FloverTactics.sml 6.29 KB
Newer Older
1 2 3 4
(*
  Some tactics which ease proving goals
*)

Heiko Becker's avatar
Heiko Becker committed
5
structure FloverTactics =
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
struct

local open intLib wordsLib in end;
open set_relationTheory;
open BasicProvers Defn HolKernel Parse Tactic monadsyntax
     alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib
     combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs
     listTheory llistTheory markerLib miscTheory
     optionTheory pairLib pairTheory pred_setTheory
     quantHeuristicsLib relationTheory res_quanTheory rich_listTheory
     sortingTheory sptreeTheory stringTheory sumTheory wordsTheory;

fun elim_conj thm =
  let val (hypl, concl) = dest_thm thm in
      if is_conj concl
      then
          let val (thm1, thm2) = CONJ_PAIR thm in
              elim_conj thm1 \\ elim_conj thm2
          end
      else
          ASSUME_TAC thm
  end;

fun elim_exist1 thm =
  let val (hypl, concl) = dest_thm thm in
      if is_exists concl
      then
              CHOOSE_THEN elim_exist thm
      else
          elim_conj thm
  end
and elim_exist thm =
  let val (hypl, concl) = dest_thm thm in
      if is_exists concl
      then
              CHOOSE_THEN elim_exist1 thm
      else
          elim_conj thm
  end;

fun inversion pattern cases_thm =
  qpat_x_assum pattern
Heiko Becker's avatar
Heiko Becker committed
48
    (fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm));
49 50

fun qexistsl_tac termlist =
51 52 53
  case termlist of
      [] => ALL_TAC
    | t::tel => qexists_tac t \\ qexistsl_tac tel;
54

55 56 57 58 59 60 61 62 63 64
fun specialize pat_hyp pat_thm =
  qpat_x_assum pat_hyp
    (fn hyp =>
      (qspec_then pat_thm ASSUME_TAC hyp) ORELSE
      (qpat_assum pat_thm
         (fn asm => ASSUME_TAC (MP hyp asm))));

fun rw_asm pat_asm =
  qpat_x_assum pat_asm
    (fn asm =>
Heiko Becker's avatar
Heiko Becker committed
65 66 67 68 69 70
      (once_rewrite_tac [asm] \\ ASSUME_TAC asm));

fun rw_asm_star pat_asm =
  qpat_x_assum pat_asm
    (fn asm =>
        fs [Once asm] \\ ASSUME_TAC asm);
71 72 73 74

fun rw_sym_asm pat_asm =
  qpat_x_assum pat_asm
    (fn asm =>
Heiko Becker's avatar
Heiko Becker committed
75
      (once_rewrite_tac [GSYM asm] \\ ASSUME_TAC asm));
76 77 78 79 80 81

fun rw_thm_asm pat_asm thm =
  qpat_x_assum pat_asm
    (fn asm =>
      (ASSUME_TAC (ONCE_REWRITE_RULE[thm] asm)));

82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97

(* Destruct like tactic, by Michael Norrish, see HOL-info **)

(* Given theorem

  P x y z ==> ?w. Q w

  introduce P x y z as a subgoal and Q w for some w as hypothesis *)

fun destruct th =
  let
      val hyp_to_prove = lhand (concl th)
  in
      SUBGOAL_THEN hyp_to_prove (fn thm => STRIP_ASSUME_TAC (MP th thm))
  end

98 99 100 101 102 103 104
fun impl_subgoal_tac th =
  let
      val hyp_to_prove = lhand (concl th)
  in
      SUBGOAL_THEN hyp_to_prove (fn thm => assume_tac (MP th thm))
  end

Heiko Becker's avatar
Heiko Becker committed
105
val flover_eval_tac :tactic=
106 107 108
  let val _ =  computeLib.del_funs([sptreeTheory.lookup_def])
      val _ = computeLib.add_funs([sptreeTheory.lookup_compute]) in
    computeLib.EVAL_TAC
Heiko Becker's avatar
Heiko Becker committed
109 110 111
    \\ fs[sptreeTheory.lookup_def]
    \\ rpt strip_tac
    \\ fs[sptreeTheory.lookup_def]
112
    \\ EVAL_TAC
Heiko Becker's avatar
Heiko Becker committed
113 114
end;

Heiko Becker's avatar
Heiko Becker committed
115
(* Flover Compute Tactic as in Coq dev to simplify goals involving computations *)
116 117 118 119
fun iter n s f =
  if n = 0 then s
  else iter (n - 1) (f s) f;

Heiko Becker's avatar
Heiko Becker committed
120 121 122 123 124 125 126 127 128 129
fun getArgTypeList t num lst =
let val (name, list) = dest_type t in
    case name of
     "fun" =>
       let
           val (hdty, tylist) = (hd list, tl list) in
           getArgTypeList (hd tylist) (num + 1) (hdty :: lst)
       end
     | _ => (num, rev lst)
end
130

Heiko Becker's avatar
Heiko Becker committed
131
fun getPatTerm t =
Heiko Becker's avatar
Heiko Becker committed
132
  let
133
      val decl_list = decls (term_to_string t);
Heiko Becker's avatar
Heiko Becker committed
134 135
      val argTypes_list = map (fn t => getArgTypeList (#Ty (dest_thy_const t)) 0 []) decl_list in
      if length decl_list = 1
136
      then
Heiko Becker's avatar
Heiko Becker committed
137 138 139 140 141 142 143 144 145 146
          let
              val (cnt, tyList) = hd argTypes_list
          in
              iter cnt (hd decl_list, tyList)
                   (fn (t,tyList) =>
                       let
                           val var = mk_var ("_",hd tyList) in
                           (* val _ = print_term var; *)
                           (* val _ = print_term t in *)
                           (mk_comb (t, var), tl tyList)
147 148 149
                       end)
          end
      else raise ERR "Too many constants" ""
Heiko Becker's avatar
Heiko Becker committed
150
end;
151

Heiko Becker's avatar
Heiko Becker committed
152 153 154
(* This variable is supposed to hold all defined functions *)
val eval_funs:term list ref = ref [];

155 156 157 158 159 160 161 162
(* open TextIO; *)
(* val t = TextIO.openIn("/home/hbecker/Downloads/test.txt"); *)
(* inputLine(t); *)
(*  closeIn(t); *)
(*  val t2 = openIn("./test.txt"); *)
(*  inputLine(t2); *)
(*  output(t2, "ABC\n"); *)
(*  closeOut(t2); *)
Heiko Becker's avatar
Heiko Becker committed
163

Heiko Becker's avatar
Heiko Becker committed
164
fun add_unevaluated_function (t:term) :unit =
165
  let
Heiko Becker's avatar
Heiko Becker committed
166
      val add_t = "val _ = FloverTactics.eval_funs :=``" ^ term_to_string t ^ "`` :: (!FloverTactics.eval_funs);"
167
      val _ = adjoin_to_theory
168
                  { sig_ps = NONE,
169
                    struct_ps =
170
                    SOME (fn _ => PP.add_string add_t)};
171 172 173
  in
  eval_funs := t :: (!eval_funs)
  end;
Heiko Becker's avatar
Heiko Becker committed
174

Heiko Becker's avatar
Heiko Becker committed
175
fun Flover_compute t =
Heiko Becker's avatar
Heiko Becker committed
176
    let
Heiko Becker's avatar
Heiko Becker committed
177
        val eval_thm = fst (snd (hd (DB.find ((term_to_string t)^"_def"))));
Heiko Becker's avatar
Heiko Becker committed
178 179 180 181 182 183 184 185 186 187 188 189
        val (pat,_) = getPatTerm t in
        TRY (
            Tactical.PAT_X_ASSUM
                pat
                (fn thm =>
                    let
                        val rwthm = ONCE_REWRITE_RULE [eval_thm] thm;
                        val compute_thm = computeLib.RESTR_EVAL_RULE (!eval_funs) rwthm in
                        assume_tac compute_thm end)
        \\ fs[]
        \\ TRY (
            REPEAT (
190
              ((qpat_assum `option_CASE _ _ _`
Heiko Becker's avatar
Heiko Becker committed
191 192 193
                (fn thm =>
                    let
                        val (t,t2,_) = optionSyntax.dest_option_case (concl thm) in
194 195 196
                        Cases_on `^t2` \\ fs[] end))
              ORELSE
              (split_pair_case_tac)) \\ fs[])))
Heiko Becker's avatar
Heiko Becker committed
197 198
    end;

199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
fun iter_exists_tac ind n =
  fn tm =>
    if ind < n
    then
      (part_match_exists_tac
        (fn concl => List.nth (strip_conj concl, ind)) tm)
        ORELSE (iter_exists_tac (ind+1) n tm)
    else
      FAIL_TAC (concat ["No matching clause found for ", term_to_string tm]) ;

val try_all:term -> tactic =
  fn tm =>
    fn (asl, g) =>
      let
        val len = length (strip_conj (snd (dest_exists g))) in
        iter_exists_tac 0 len tm (asl, g)
     end;

val find_exists_tac =
  first_assum (try_all o concl);

Heiko Becker's avatar
Heiko Becker committed
220
(* val Flover_compute:tactic = *)
Heiko Becker's avatar
Heiko Becker committed
221 222 223 224 225 226
(*     fn (g:goal) => *)
(*        let *)
(*            val terms_to_eval = !eval_funs in *)
(*            if (length terms_to_eval = 0) *)
(*            then let val _ = print "Nothing to evaluate" in ALL_TAC g end *)
(*            else *)
Heiko Becker's avatar
Heiko Becker committed
227
(*                Flover_compute_steps terms_to_eval g *)
Heiko Becker's avatar
Heiko Becker committed
228
(*   end; *)
Heiko Becker's avatar
Heiko Becker committed
229

230

231
end