development/thales/chaff/tactic.hl

   1 (*
   2 places:
   3   goal, assumption list, input box with prompts, proof text, search results
   4
   5
   6 *)
   7
   8 (*
   9 theorem searching -n NAME, -o omit, -r rewrite format, -s sort by length, -
  10 save search history and selected results.,
  11
  12 *)
  13
  14 (* Jordan from:
  15     eventually merge...  *)
  16
  17 let rec type_set: (string*term) list  -> (term list*term) -> (term list*term)=
  18   fun tinfo (acclist,utm) -> match acclist with
  19     | [] -> (acclist,utm)
  20     | (Var(s,_) as a)::rest ->
  21          let a' = (assocd s tinfo a) in
  22            if (a = a') then type_set tinfo (rest,utm)
  23            else let inst = instantiate (term_match [] a a') in
  24              type_set tinfo ((map inst rest),inst utm)
  25     | _ -> failwith "type_set: variable expected"
  26   ;;
  27
  28 let has_stv t =
  29   let typ = (type_vars_in_term t) in
  30   can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
  31
  32 let typeinfo (asl,w) =
  33   let freel = itlist (union o frees o concl o snd) asl (frees w) in
  34   let pairup  = (function
  35                    |Var(s,_) as t -> (s,t)
  36                    | _ -> failwith "typeinfo: unreachable state" ) in
  37   map pairup freel;;
  38
  39 let set_types_from_goal (asl,w)  =
  40   let set_types tinfo t = snd (type_set tinfo ((frees t),t)) in
  41     set_types (typeinfo(asl,w));;
  42
  43 let TYPE_THEN: term  -> (term -> tactic) -> tactic =
  44   fun t tac (asl,w) ->
  45   let t' = set_types_from_goal(asl,w) t in
  46     (warn ((has_stv t')) "TYPE_THEN: unresolved type variables");
  47     tac t' (asl,w);;
  48
  49 let TYPEL_THEN: term list -> (term list -> tactic) -> tactic =
  50   fun t tac (asl,w) ->
  51   let t' = map (set_types_from_goal(asl,w)) t in
  52     (warn ((can (find has_stv) t')) "TYPEL_THEN: unresolved type vars");
  53      tac t' (asl,w);;
  54
  55 help "ABBREV_TAC";;
  56 (* hightlight term, typeover abbrev *)
  57 let MK_ABBREV_TAC: term -> string -> goal -> goalstate =
  58   fun oldtext abbrev (asl,w) ->
  59     let text = set_types_from_goal (asl,w) oldtext in
  60   let abbrev' = mk_var(abbrev,(type_of text)) in
  61    ABBREV_TAC (mk_eq (abbrev', text)) (asl,w);;
  62
  63 help "ABS_TAC";;
  64 (* delete the lambda, or the bound variable *)
  65
  66 help "ACCEPT_TAC";; (* ignore for now *)
  67
  68 help "ALL_TAC";; (* ignore for now *)
  69
  70 help "ANTE_RES_THEN";; (* ignore for now *)
  71
  72 help "ANTS_TAC";;  (* delete ant of ant, subgoal button *)
  73
  74 help "AP_TERM_TAC";;  (* delete f in f x = f y, either first or second instance *)
  75
  76 help "AP_THM_TAC";;  (* delete x in f x = g x, either first or second *)
  77
  78 help "ARITH_TAC";;  (* terminator, try if it is an arithmetic expression. *)
  79
  80 help "ASM_CASES_TAC";;  (* needs a term u to split *)
  81
  82 help "ASM_FOL_TAC";; (* ignore forever *)
  83
  84 help "ASM_MESON_TAC";; (* terminator , option -a on MESON_TAC *)
  85
  86 help "ASM_REWRITE_TAC";; (* option -a on REWRITE_TAC *)
  87
  88 help "ASM_SIMP_TAC";; (* option -a on SIMP_TAC *)
  89
  90 help "ASSUME_TAC";; (* needs theorem *)
  91
  92 help "BETA_TAC";; (* delete lambda *)
  93
  94
  95
  96
  97