HOL cheat sheet

HOL cheat sheet

synonyms:
   >>
   \\
   THEN
   ( means ";" in Isar )
  meaning:
    tac1 \\ tac2
    means apply tac1 to the current proof state
    then apply tac2 to all the resulting subgoals

  synonyms:
    >-
    THEN1
    ( something like "," then solved in Isar )
  meaning:
    tac1 >- tac2
    means apply tac1 to the current proof state
    then apply tac2 to the first subgoal (there must be at least one),
      which must solve the whole subgoal
  example:
    tac (* produces 5 subgoals *)
    >- tac1 (* solves the first one *)
    >- tac2 (* solves the second one *)
    >- tac3 (* solves the third one *)
    \\ rest_tac (* solves the last subgoals *)
    
  simplification tactics:

  simp [...]
    - operates on the goal
  fs [...]
    - operates on the goal and the assumptions
  rfs [...]
    - same as fs, but does the assumptions in the opposite order
  rw [thm1, thm2, ...]
    - operates on the goal
    - also clears out some simple useless assumptions
    - also strips off stuff from the goal (can produce new subgoals)

  (* these use srw_ss + some extra stuff for lists and numbers etc. *)

  srw_tac [simpset1, simpset2, ...] [thm1, thm2, ...]
    - like rw, but with srw_ss()++simpset1++simpset2 ...

  srw_ss()
  std_ss
  bool_ss
  pure_ss

  simp_tac simpset [thm1, thm2, ...]
  asm_simp_tac simpset [...]
  full_simp_tac simpset [...]

  (* just rewriting, no conditional rewriting *)
  rewrite_tac [...]
  asm_rewrite_tac [..]
  PURE_REWRITE_TAC [...]
  
  finding theorems:
DB.find "FLOOKUP"
DB.find_in "SUBMAP" (DB.match [] ``_ IN FDOM _``)
synonyms: print_find print_match


finding help:
help "rw"
web index of this: HOL/help/HOLIndex.html

  grabbing assumptions:
  first_x_assum continuation
  semantics:
    loop over each assumption th and try
      continuation th
    and stop looping if that tactic succeeds
    or you run out of assumptions (then this fails)
    also, remove the assumption
  first_assum - same thing, but don't remove the assumption
  last_x_assum
  last_assum - same thing but in the opposite order

  qpat_x_assum pattern continuation
    - grab the first assumption that matches pattern
      then apply the continuation
  qpat_assum

  pop_assum
    - grab the top assumption
ask on the CakeML channel

You have a bad character in the DB.find_in line