text_formalization/general/tactics.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: General Tactics                                                     *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-07-16                                                           *)
   7 (* ========================================================================== *)
   8
   9 module Tactics = struct
  10
  11 (* ASSUMPTION LISTS *)
  12
  13 let ASM_STRIP_TAC =
  14    FIRST[FIRST_X_ASSUM CHOOSE_TAC;
  15    FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC);
  16         ];;
  17
  18 let FIRST_RULE_ASSUM rule ttc = FIRST_ASSUM (ttc o rule );;
  19
  20 let FIRST_RULE_X_ASSUM rule ttc = FIRST_X_ASSUM (ttc o rule );;
  21
  22 (* INDUCTION *)
  23
  24 let INDUCT_SPEC_TAC vn =
  25   let v = mk_var (vn,`:nat`) in
  26   SPEC_TAC (v,v) THEN INDUCT_TAC;;
  27
  28
  29 (* ------------------------------------------------------------------ *)
  30 (* SELECT ELIMINATION.
  31    SELECT_TAC should work whenever there is a single predicate selected.
  32    Something more sophisticated might be needed when there
  33    is (@)A and (@)B
  34    in the same formula.
  35    Useful for proving statements such as  `1 + (@x. (x=3)) = 4` *)
  36 (* ------------------------------------------------------------------ *)
  37
  38 (* spec form of SELECT_AX *)
  39 let select_thm select_fn select_exist =
  40   BETA_RULE (ISPECL [select_fn;select_exist]
  41              SELECT_AX);;
  42
  43 (* example *)
  44 select_thm
  45     `\m. (X:num->bool) m /\ (!n. X n ==> m <= n)` `n:num`;;
  46
  47 let SELECT_EXIST = prove_by_refinement(
  48   `!(P:A->bool) Q. (?y. P y) /\ (!t. (P t ==> Q t)) ==> Q ((@) P)`,
  49   (* {{{ proof *)
  50
  51   [
  52   REPEAT STRIP_TAC;
  53   ASSUME_TAC (ISPECL[`P:(A->bool)`;`y:A`] SELECT_AX);
  54   ASM_MESON_TAC[];
  55   ]);;
  56
  57   (* }}} *)
  58
  59 let SELECT_THM = MESON[SELECT_EXIST]
  60   `!(P:A->bool) Q. (((?y. P y) ==> (!t. (P t ==> Q t))) /\ ((~(?y. P y)) ==>
  61      (!t. Q t))) ==> Q ((@) P)`;;
  62
  63 let SELECT_TAC  =
  64   let unbeta = prove(
  65   `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,MESON_TAC[]) in
  66   let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in
  67   unbeta_tac THEN (MATCH_MP_TAC SELECT_THM) THEN BETA_TAC THEN
  68   REPEAT STRIP_TAC;;
  69
  70 (* PATTERNS *)
  71
  72 let (PAT_MATCH:term list -> (string*thm) -> bool) = fun pat sth ->
  73   not(search_thml (term_match[]) pat [sth] = []);;
  74
  75 let (PAT_TAC2:tactic -> tactic -> term list -> (string * thm) -> tactic)  = fun tac1 tac2 pat sth -> if PAT_MATCH pat sth then tac1 else tac2;;
  76
  77 let (PAT_TAC:term list -> (string * thm) -> tactic)  =
  78   PAT_TAC2 ALL_TAC NO_TAC;;
  79
  80 let (FIRST_PAT_ASSUM: term list -> thm_tactic -> tactic) =
  81   fun pat ttac gl -> tryfind (fun sth -> (PAT_TAC pat sth THEN ttac (snd sth)) gl) (goal_asms gl);;
  82
  83 let (FIRST_PAT_X_ASSUM:term list -> thm_tactic -> tactic) =
  84   fun pat ttac ->
  85     FIRST_PAT_ASSUM pat (fun th -> UNDISCH_THEN (concl th) ttac);;
  86
  87 let (EVERY_PAT_ASSUM:term list -> thm_tactic -> tactic) =
  88   fun pat ttac gl ->
  89     let rl = map snd (filter (PAT_MATCH pat) (goal_asms gl)) in
  90     let tacl = map ttac rl in
  91       EVERY tacl gl;;
  92
  93 (* Well defined functions *)
  94
  95 (* Harrison's lemma *)
  96 let WELLDEFINED_FUNCTION_1 = prove
  97  (`(?f:B->C. !x:A. f(s x) = t x) <=> (!x x'. s x = s x' ==> t x = t x')`,
  98   MATCH_MP_TAC EQ_TRANS THEN
  99   EXISTS_TAC `?f:B->C. !y. !x:A. s x = y ==> f y = t x` THEN
 100   CONJ_TAC THENL
 101    [MESON_TAC[]; REWRITE_TAC[GSYM SKOLEM_THM] THEN
 102   MESON_TAC[]]);;
 103
 104
 105 let WELLDEFINED_FUNCTION_2b = prove_by_refinement(
 106 `(?f:C->D. (!x:A y:B. P x y ==> f(s x y) = t x y)) <=>
 107    (!x x' y y'. (P x y /\ P x' y' /\ (s x y = s x' y')) ==> t x y = t x' y')`,
 108 [
 109   MATCH_MP_TAC EQ_TRANS ;
 110   EXISTS_TAC  `?f:C->D. !z. !x:A y:B. ((P x y) /\ (s x y = z)) ==> f z = t x y`;
 111   CONJ_TAC;
 112   MESON_TAC[];
 113   REWRITE_TAC[GSYM SKOLEM_THM];
 114   MESON_TAC[];
 115 ]);;
 116
 117
 118  end;;