(*DOC*)theory I(*DOC*)
imports Main
begin

section{* Jv Favorites *}
(*
--"DECLARE====================================================================="
  --{*notation Trueprop("Tr")    notation "prop"("Pr")*}
  declare[[show_brackets=true]]  declare[[show_types=true]]
  declare[[names_long=false]]    declare[[show_sorts=false]]
  declare[[names_unique=true]]   declare[[show_consts=true]]

*)

section{* Misc Help Commands *}
(*help*)                         (*Lists the available commands.*)
help

section{* Show *}
declare[[show_brackets=true]] (*sub-exprs will be parenthesized*)
declare[[show_sorts=false]]   (*show type & sort constraints for term vars*)
declare[[show_types=true]]    (*show type constraints for term vars*)
declare[[names_long=false]]   (*names_long, names_short*)
declare[[names_unique=true]]  (*names_unique*)
declare[[show_consts=true]]   (*show constants when displaying a goal state*)

declare[[show_main_goal=true]](*main result to be proven is displayed*)
declare[[show_abbrevs=true]]  (*controls folding of constant abbreviations*)
declare[[eta_contract=false]] (*Isa performs eta-contractions before printing*)
declare[[goals_limit=100]]    (*max subgoals to be shown*)
declare[[show_hyps=true]]     (*show implicit hypotheses of local facts*)
declare[[show_tags=true]]     (*extra annotations within theorems*)
declare[[show_question_marks=true]](*question marks for schematic vars*)

(*From ~~/NEWS
syntax_ast_trace
syntax_ast_stat
syntax_ambiguity_level

rule_trace

thy_output_display
thy_output_quotes
thy_output_indent
thy_output_source
thy_output_break
*)

section{* Notation Tricks To Show Hidden Trueprop and prop *}
(*notation Trueprop  ("Tr")*)    (*Will display the hidden Trueprop function globally.*)
(*notation "prop" ("Pr")*)       (*Will  display the hidden prop function globally.*)
(*write Trueprop  ("Tr")*)       (*Use like "notation", but in notepad.*)

section{* Print Modes *}
(*isabelle jedit -m brackets     Start jEdit with print mode set to brackets*)
  (*
  brackets,                      Doesn't convert [|A;B|] ==> C|] in the goals.
  no_brackets,
  type_brackets,                 Control output of nested => (types)
  no_type_brackets
  iff                            Shows boolean equality as a double arrow.
  *)
(*ISABELLE_JEDIT_OPTIONS         In etc/settings gives default command line options.*)
(*ML{*print_mode_value();*}      List of currently active print mode names.*)


section{* Inspecting The Current Context *}
(*print_abbrevs     prints all constant abbreviations of the current context*)
(*print_attributes  all attributes available in the current theory context*)
(*print_binds       term abbreviations present in the context*)
(*print_bundles     prints the named bundles that are available in the current context*)
(*print_cases       prints all local contexts of the current state*)
(*print_claset      prints the collection of rules declared to the Classical Reasoner*)
(*print_classes     prints all classes in the current theory.*)
(*print_commands    outer theory syntax, including keywords and command*)
(*print_configs     prints available config options, with names, types, and current values*)
(*print_dependencies <expr> lists all locale instances for which interpretations would be added to the current context*)
(*print_facts       local facts of the current context, both named and unnamed*)
(*print_induct_rules      prints cases and induct rules for predicates (or sets) and types*)
(*print_interps <locale>  lists all interpretations of locale in the current theory or proof context*)
(*print_locale <locale>   prints the contents of the named locale; use ! to include notes*)
(*print_locales     prints the names of all locales of the current theory*)
(*print_methods     all proof methods available in the current theory context*)
(*print_simpset     prints the collection of rules declared to the Simplifier*)
(*print_statement <a> prints facts from the current theory or proof context in long statement form*)
(*print_syntax      prints the inner syntax of the current context*)
(*print_theorems !  theorems resulting from the last command; ! for verbosity*)
(*print_theory !    main logical content of theory context; ! for verbosity*)

section{* Find Commands *}
(*find_theorems <criteria>   facts from the theory or proof context matching criteria*)
(*find_consts <criteria>     all constants whose type meets all of the given criteria
  Example: find_consts  name: listT.Cons*)
(*thm_deps <a1...an>; visualizes dependencies of facts, using Isabelle's graph browser tool*)
(*unused_thms <A1...Am - B1...Bn> displays all unused theorems in theories B1...Bn or their parents, but not in A1...Am or their parents.*)

section{* Nitpick SATs *}
(*
  nitpick[sat_solver=Lingeling_JNI] nitpick[sat_solver=CryptoMiniSat_JNI]
  nitpick[sat_solver=MiniSat_JNI]   nitpick[sat_solver=SAT4J]
  nitpick[sat_solver=SAT4J_Light]

  Jasmin: SAT4J is very slow, but the others are roughly equivalent, with
  Lingeling slightly better than CryptoMiniSat, and CryptoMiniSat slightly
  better than vanilla MiniSat.
*)

section{* Sledgehammer and Nitpick parameters*}

nitpick_params[timeout=172800,sat_solver=MiniSat_JNI,verbose,user_axioms]
sledgehammer_params[timeout=172800,verbose,debug=false,isar_proof,provers="
  e spass_new remote_vampire remote_e_sine remote_iprover_eq
  vampire z3_tptp spass metis remote_e_tofof remote_iprover remote_snark
  z3 yices cvc3 smt alt_ergo remote_waldmeister
  "]

section{* Sledgehammer *}
subsection{* Groupings of the provers *}
  (*1 e spass_new remote_vampire remote_e_sine remote_iprover_eq*)
  (*2 vampire z3_tptp spass metis remote_e_tofof remote_iprover remote_snark*)
  (*3 z3 yices cvc3 smt alt_ergo remote_waldmeister*)
  (*4 satallax leo2*)
  (*5 remote_leo2 remote_satallax remote_e remote_z3_tptp remote_cvc3 remote_z3*)
(*
  WORKING PROVERS THAT AREN'T DUPLICATES
    metis smt alt_ergo dummy_thf e leo2 satallax spass spass_new spass_old
    vampire z3_tptp cvc3 yices z3 remote_e_sine remote_e_tofof remote_iprover
    remote_iprover_eq remote_snark remote_vampire remote_waldmeister
  NOT INSTALLED OR DUPLICATES
    remote_e remote_leo2 remote_satallax remote_z3_tptp remote_cvc3 remote_z3

  sledgehammer supported_provers
  metis smt alt_ergo dummy_thf e leo2 satallax spass spass_new spass_old
  vampire z3_tptp cvc3 yices z3 remote_e remote_e_sine remote_e_tofof
  remote_iprover remote_iprover_eq remote_leo2 remote_satallax remote_snark
  remote_vampire remote_waldmeister remote_z3_tptp remote_cvc3 remote_z3
*)

subsection{* Provers that found eeA, exA, upA, emS_is_empty inconsistency  *}
(*See E:\E_main\02-p\pi\piJv\sTs\120721__sTs_ASCII*)
(*
e
metis
spass
spass_new
z3_tptp
remote_e_sine
remote_iprover
remote_iprover_eq
remote_leo2
remote_satallax
remote_vampire
*)

subsection{* Site locations for prover downloads *}
(*
  alt_ergo...http://alt-ergo.lri.fr/
             http://why3.lri.fr/
             Norton deleted alt-ergo-0.94-mingw.exe installer.
  iprover....http://www.cs.man.ac.uk/~korovink/iprover/
  iprover_eq.http://www.cs.man.ac.uk/~korovink/iprover/
  leo2.......http://www.ags.uni-sb.de/~leo/, but need compiled with OCaml
  satallax...http://www.ps.uni-saarland.de/~cebrown/satallax/, needs make
  vampire....http://www.vprover.org/
  yices......http://yices.csl.sri.com/download.shtml
*)


end