DaisyTactics.sml 3.44 KB
Newer Older
1 2 3 4 5 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
(*
  Some tactics which ease proving goals
*)

structure DaisyTactics =
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 106 107 108 109 110 111 112
fun daisy_eval_tac t :tactic=
  let
    val result_thm = computeLib.EVAL_CONV t
  in
    rewrite_tac [result_thm]
    \\ fs[sptreeTheory.lookup_def]
    \\ rpt strip_tac
    \\ fs[sptreeTheory.lookup_def]
Heiko Becker's avatar
Heiko Becker committed
113 114
end;

Heiko Becker's avatar
Heiko Becker committed
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
fun case_destruct_tac thm =
let
  val conclusion = concl thm;
  val caseTerm = find_term TypeBase.is_case conclusion;
  val (_, caseOn, _) = TypeBase.dest_case caseTerm
  val _ = print ("Case analysis on ")
  val _ = print_term caseOn in
    BasicProvers.Cases_on `^caseOn`
end;

fun case_compute_tac pat =
  qpat_x_assum pat
               (fn thm => REPEAT (case_destruct_tac thm \\ fs[]));

fun const_type_length cst =
let
    val holObj = dest_thy_const cst;
    val t = #Ty holObj;
    val (_, typeParamsList) = dest_type t in
    length typeParamsList
end

fun foo t =
  let
      val as_str = term_to_string t in
      map const_type_length (decls as_str)
end;
mk_comb (``typeCheck``,``_:real exp``)
dest_term ``typeCheck _``

145
end