Re: [isabelle] I want to print axiom info (sledgeH error at end)



Here's a template I created to look at how Isabelle decides to type and parenthesize a formula in axiomatizations and definitions:

theorem show_info:
 "(True) =
  (True)"
  by(auto)
  thm show_info

Replace True with your formula. If you haven't imported "auto", then replace "by(auto)" and "thm" with "oops". You might want these more useful info commands above your working code to create different levels of information overload:

--"INFO BEGIN=================================================================="
  --{*notation Trueprop("Tr")    notation "prop"("Pr")*}
  declare[[show_brackets=true]]  declare[[show_sorts=false]]
  declare[[names_long=false]]    declare[[show_types=true]]
  declare[[names_unique=true]]   declare[[show_consts=true]]
--"INFO END--------------------------------------------------------------------"

Giving advice is free, so I just go ahead attach iI.thy to this email. I import it into my theories. It contains my default settings for the full set of "declare" commands. Commented out are print and find commands, so I don't have to look at isar-ref.pdf to remember what they are. There are the jEdit command line options that control some printing modes.

There are also my default sledgehammer settings. I do this, and I get all the provers:

     sledgehammer supported_provers

I went back and briefly experimented with all the remote provers. I eventually settled on these options:

sledgehammer_params [provers = "
  e cvc3 metis smt spass z3 z3_tptp remote_e_sine remote_vampire
", slice=true, verbose=true, isar_proof=true, timeout=120]

The 120 second timeout solved the problem of not finding structured proofs that I mentioned in another email.

Also, provers I wasn't using at the time of that email were "smt" and "remote_e_sine". "smt" finds proofs just like "metis".

Following the instructions in the sledgehammer manual, I've used "apply(auto)" prior to using sledgehammer. When I do that, proofs will be found to finish the simplified goal by "smt" and "metis", along with a structured proof to only finish the simplified goal.

"remote_e_sine" finds a short, structured proof that uses only the necessary axioms. If I have the theorem after unnecessary axioms, another structured proof is found which uses an unnecessary axiom, but even after the unnecessary axioms, "remote_e_sine" finds the proof using only the two necessary axioms.

I also figured out the simple fact (maybe from reading the sledgehammer manual) that I can click on any of the highlighted text in the output window, and it'll replace "sledgehammer" with that proof.

If I choose a "smt" or "metis" proof that's offered, it does indeed finish the proof. If I choose a structured proof, it complains about an unbound schematic variable, as shown in the attached screen shot.

Regards,
GB


Attachment: unbound_sch_var_error.png
Description: PNG image

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

section{* Jv Favorites *}
(*                     
--"INFO BEGIN=================================================================="
  --{*notation Trueprop("Tr")    notation "prop"("Pr")*}
  declare[[show_brackets=true]]  declare[[show_sorts=false]]
  declare[[names_long=false]]    declare[[show_types=true]]
  declare[[names_unique=true]]   declare[[show_consts=true]]
--"INFO END--------------------------------------------------------------------"
theorem show_info:
 "(True) =
  (True)"
  by(auto) 
  thm show_info
*)

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{* Sledgehammer *}
sledgehammer_params [provers = "
  e cvc3 metis smt spass z3 z3_tptp remote_e_sine remote_vampire   
", slice=true, verbose=true, isar_proof=true, timeout=120]

(*remote_e_tofof remote_leo2 remote_satallax remote_snark remote_waldmeister*)

(*
sledgehammer supported_provers

metis  smt  alt_ergo  dummy_thf  e  leo2  satallax  spass  spass_new  spass_old
vampire  z3_tptp  cvc3  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
*)


end























This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.