Theory Sepref_Guide_General_Util

section ‹General Purpose Utilities›
theory Sepref_Guide_General_Util
imports "../IICF/IICF"
begin

text ‹This userguide documents some of the general purpose utilities that 
  come with the Sepref tool, but are useful in other contexts, too.›

subsection ‹Methods›
subsubsection ‹Resolve with Premises›
text ‹The @{method rprems} resolves the current subgoal with 
  one of its premises. It returns a sequence of possible resolvents.
  Optionally, the number of the premise to resolve with can be specified.
›

subsubsection ‹First-Order Resolution›
text ‹The @{method fo_rule} applies a rule with first-order matching.
  It is very useful to be used with theorems like @{thm arg_cong}.›

notepad begin
  have "card {x. 3<x ∧ x<(7::nat)} = card {x. 4≤x ∧ x≤(6::nat)}"
    apply (fo_rule arg_cong)
    apply auto
    done

  ― ‹While the first goal could also have been solved with 
    ‹rule arg_cong[where f=card]›, things would be much more 
    verbose for the following goal. (Such goals actually occur in practice!)›  

  fix f :: "nat set ⇒ nat set ⇒ bool"  
  have "⋀a. f {x. x*2 + a + 3 < 10} {x. 3<x ∧ x<(7::nat)} = f {x. x*2 + a ≤6} {x. 4≤x ∧ x≤(6::nat)}"
    apply (fo_rule arg_cong fun_cong cong)+
    apply auto
    done

end


subsubsection ‹Clarsimp all goals›
text ‹@{method clarsimp_all} is a ‹clarsimp› on all goals. 
  It takes the same arguments as ‹clarsimp›.›

subsubsection ‹VCG solver›
text ‹@{method vc_solve} clarsimps all subgoals. 
  Then, it tries to apply a rule specified in the ‹solve: › argument,
  and tries to solve the result by ‹auto›. If the goal cannot be solved this way, 
  it is not changed.

  This method is handy to be applied after verification condition generation.
  If ‹auto› shall be tried on all subgoals, specify ‹solve: asm_rl›.
›

subsection ‹Structured Apply Scripts (experimental)›
text ‹A few variants of the apply command, that document the
  subgoal structure of a proof. They are a lightweight alternative to 
  @{command subgoal}, and fully support schematic variables.
  
  @{command applyS} applies a method to the current subgoal, and fails if the
    subgoal is not solved.

  @{command apply1} applies a method to the current subgoal, and fails if
    the goal is solved or additional goals are created.

  @{command focus} selects the current subgoal, and optionally applies a method.

  @{command applyF} selects the current subgoal and applies a method.

  @{command solved} enforces no subgoals to be left in the current selection, and unselects.

  Note: The selection/unselection mechanism is a primitive version of focusing
    on a subgoal, realized by inserting protect-tags into the goal-state.

›

subsection ‹Extracting Definitions from Theorems›
text ‹
  The @{command concrete_definition} can be used to extract parts of a theorem
  as a constant. It is documented at the place where it is defined 
  (ctrl-click to jump there).
›



(* clarsimp_all, vc_solve *)

(*
  Methods
    rprems

  Structured Apply
  concrete_definition, prepare_code_thms

  CONSTRAINT
  PHASES'

*)

end