Re: [isabelle] Syntax issue: lost between HOL and Isar



On 8/1/2012 5:07 PM, Yannick Duchêne (Hibou57) wrote:

I got it, that's in “Synopsis.thy”, and modulo the indentation, that's the same, there is no quote too:

  notepad
  begin
    fix n :: nat
    have "P n"
    proof (induct n)
      case 0
      show ?case sorry
    next
      case (Suc n)
      from Suc.hyps show ?case sorry
    qed
  end

So, what's the expression type of “(Suc n)” at the line whose text is “case (Suc n)”? Isn't “(Suc n)” an HOL expression? It appears in the text as if it was an Isar expression, but I feel sure it's not. I'm lost with that point.

I don't know much more than you, so you should keep that in mind for the future.

"Suc" is the successor function, and it comes from "Isabelle2012/src/HOL/Nat.thy". This is where those "declare" commands come in handy. I attach "I.thy". It has all the declare and print commands I found that looked useful. Delete what you don't want, or don't use any of it. I keep it open in jEdit all the time, that's why it has a short name.

In particular, I used:

declare[[names_unique=true]]   declare[[show_consts=true]]

In the output panel, it shows me:

constants:
  prop :: (prop ⇒ prop)
  Nat.Suc :: (Nat.nat ⇒ Nat.nat)

Isar as a language is independent of HOL. Isar can be used in any logic, such as Isabelle/ZF.

HOL is one of the many logics in Isabelle2012/src, although it's the most popular one.

"Expression" is an ambiguous word that can be used in lots of different ways.

Isar, as I understand it, is a link between the "inner syntax" and the "outer syntax", where HOL expressions would be "inner syntax". This is covered in Chapter 3 of isar-ref.pdf, and on Page 5 of prog-prove.pdf. I think "outer syntax" is related to the meta-logic which comes from "src/Pure". Isar is tied into Pure, and Pure is the foundation for logics such as HOL.

Putting in extraneous information here, where I use the ambiguous term "expression", I'll go out on a limb and say, "A HOL expression is always an Isar expression, but an Isar expression is not always a HOL expression."

I attach a screen shot to show you the useful information you get from five of the declare commands being true.

Regards,
GB






Attachment: case_Suc_n.png
Description: PNG image

(*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






















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