# HG changeset patch # User Christian Urban # Date 1280128768 -7200 # Node ID 83f1b16486ee91a1de6d18ff2a7a3dfcffd3710a # Parent e8b9c0ebf5dd2c2279f314bdf81d231359a1851d small cleaning diff -r e8b9c0ebf5dd -r 83f1b16486ee Attic/isar-keywords-quot.el --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/isar-keywords-quot.el Mon Jul 26 09:19:28 2010 +0200 @@ -0,0 +1,616 @@ +;; +;; Keyword classification tables for Isabelle/Isar. +;; Generated from HOL-Nominal-Quot + HOL-Nominal + HOL + Pure-ProofGeneral + Pure. +;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** +;; + +(defconst isar-keywords-major + '("\\." + "\\.\\." + "Isabelle\\.command" + "Isar\\.begin_document" + "Isar\\.define_command" + "Isar\\.edit_document" + "Isar\\.end_document" + "ML" + "ML_command" + "ML_prf" + "ML_val" + "ProofGeneral\\.inform_file_processed" + "ProofGeneral\\.inform_file_retracted" + "ProofGeneral\\.kill_proof" + "ProofGeneral\\.pr" + "ProofGeneral\\.process_pgip" + "ProofGeneral\\.restart" + "ProofGeneral\\.undo" + "abbreviation" + "also" + "apply" + "apply_end" + "arities" + "assume" + "atom_decl" + "atp_info" + "atp_kill" + "atp_messages" + "atp_minimize" + "attribute_setup" + "ax_specification" + "axclass" + "axiomatization" + "axioms" + "back" + "by" + "cannot_undo" + "case" + "cd" + "chapter" + "class" + "class_deps" + "classes" + "classrel" + "code_abort" + "code_class" + "code_const" + "code_datatype" + "code_deps" + "code_include" + "code_instance" + "code_library" + "code_module" + "code_modulename" + "code_monad" + "code_pred" + "code_reflect" + "code_reserved" + "code_thms" + "code_type" + "coinductive" + "coinductive_set" + "commit" + "constdefs" + "consts" + "consts_code" + "context" + "corollary" + "datatype" + "declaration" + "declare" + "def" + "default_sort" + "defer" + "defer_recdef" + "definition" + "defs" + "disable_pr" + "display_drafts" + "done" + "enable_pr" + "end" + "equivariance" + "exit" + "export_code" + "extract" + "extract_type" + "finalconsts" + "finally" + "find_consts" + "find_theorems" + "fix" + "from" + "full_prf" + "fun" + "function" + "global" + "guess" + "have" + "header" + "help" + "hence" + "hide_class" + "hide_const" + "hide_fact" + "hide_type" + "inductive" + "inductive_cases" + "inductive_set" + "init_toplevel" + "instance" + "instantiation" + "interpret" + "interpretation" + "judgment" + "kill" + "kill_thy" + "lemma" + "lemmas" + "let" + "linear_undo" + "local" + "local_setup" + "locale" + "method_setup" + "moreover" + "next" + "nitpick" + "nitpick_params" + "no_notation" + "no_syntax" + "no_translations" + "nominal_datatype" + "nominal_inductive" + "nominal_inductive2" + "nominal_primrec" + "nonterminals" + "normal_form" + "notation" + "note" + "obtain" + "oops" + "oracle" + "overloading" + "parse_ast_translation" + "parse_translation" + "pr" + "prefer" + "presume" + "pretty_setmargin" + "prf" + "primrec" + "print_abbrevs" + "print_antiquotations" + "print_ast_translation" + "print_atps" + "print_attributes" + "print_binds" + "print_cases" + "print_claset" + "print_classes" + "print_codeproc" + "print_codesetup" + "print_commands" + "print_configs" + "print_context" + "print_drafts" + "print_facts" + "print_induct_rules" + "print_interps" + "print_locale" + "print_locales" + "print_maps" + "print_methods" + "print_orders" + "print_quotconsts" + "print_quotients" + "print_rules" + "print_simpset" + "print_statement" + "print_syntax" + "print_theorems" + "print_theory" + "print_trans_rules" + "print_translation" + "proof" + "prop" + "prove" + "pwd" + "qed" + "quickcheck" + "quickcheck_params" + "quit" + "quotient_definition" + "quotient_type" + "realizability" + "realizers" + "recdef" + "recdef_tc" + "record" + "refute" + "refute_params" + "remove_thy" + "rep_datatype" + "repdef" + "schematic_corollary" + "schematic_lemma" + "schematic_theorem" + "sect" + "section" + "setup" + "show" + "simproc_setup" + "sledgehammer" + "sledgehammer_params" + "smt_status" + "sorry" + "specification" + "subclass" + "sublocale" + "subsect" + "subsection" + "subsubsect" + "subsubsection" + "syntax" + "term" + "termination" + "text" + "text_raw" + "then" + "theorem" + "theorems" + "theory" + "thm" + "thm_deps" + "thus" + "thy_deps" + "touch_thy" + "translations" + "txt" + "txt_raw" + "typ" + "typed_print_translation" + "typedecl" + "typedef" + "types" + "types_code" + "ultimately" + "undo" + "undos_proof" + "unfolding" + "unused_thms" + "use" + "use_thy" + "using" + "value" + "values" + "welcome" + "with" + "{" + "}")) + +(defconst isar-keywords-minor + '("advanced" + "and" + "as" + "assumes" + "attach" + "avoids" + "begin" + "binder" + "congs" + "constrains" + "contains" + "defines" + "file" + "fixes" + "for" + "hints" + "identifier" + "if" + "imports" + "in" + "infix" + "infixl" + "infixr" + "is" + "module_name" + "monos" + "morphisms" + "notes" + "obtains" + "open" + "output" + "overloaded" + "permissive" + "pervasive" + "shows" + "structure" + "unchecked" + "uses" + "where")) + +(defconst isar-keywords-control + '("Isabelle\\.command" + "Isar\\.begin_document" + "Isar\\.define_command" + "Isar\\.edit_document" + "Isar\\.end_document" + "ProofGeneral\\.inform_file_processed" + "ProofGeneral\\.inform_file_retracted" + "ProofGeneral\\.kill_proof" + "ProofGeneral\\.process_pgip" + "ProofGeneral\\.restart" + "ProofGeneral\\.undo" + "cannot_undo" + "exit" + "init_toplevel" + "kill" + "linear_undo" + "quit" + "undo" + "undos_proof")) + +(defconst isar-keywords-diag + '("ML_command" + "ML_val" + "ProofGeneral\\.pr" + "atp_info" + "atp_kill" + "atp_messages" + "atp_minimize" + "cd" + "class_deps" + "code_deps" + "code_thms" + "commit" + "disable_pr" + "display_drafts" + "enable_pr" + "export_code" + "find_consts" + "find_theorems" + "full_prf" + "header" + "help" + "kill_thy" + "nitpick" + "normal_form" + "pr" + "pretty_setmargin" + "prf" + "print_abbrevs" + "print_antiquotations" + "print_atps" + "print_attributes" + "print_binds" + "print_cases" + "print_claset" + "print_classes" + "print_codeproc" + "print_codesetup" + "print_commands" + "print_configs" + "print_context" + "print_drafts" + "print_facts" + "print_induct_rules" + "print_interps" + "print_locale" + "print_locales" + "print_maps" + "print_methods" + "print_orders" + "print_quotconsts" + "print_quotients" + "print_rules" + "print_simpset" + "print_statement" + "print_syntax" + "print_theorems" + "print_theory" + "print_trans_rules" + "prop" + "pwd" + "quickcheck" + "refute" + "remove_thy" + "sledgehammer" + "term" + "thm" + "thm_deps" + "thy_deps" + "touch_thy" + "typ" + "unused_thms" + "use_thy" + "value" + "values" + "welcome")) + +(defconst isar-keywords-theory-begin + '("theory")) + +(defconst isar-keywords-theory-switch + '()) + +(defconst isar-keywords-theory-end + '("end")) + +(defconst isar-keywords-theory-heading + '("chapter" + "section" + "subsection" + "subsubsection")) + +(defconst isar-keywords-theory-decl + '("ML" + "abbreviation" + "arities" + "atom_decl" + "attribute_setup" + "axclass" + "axiomatization" + "axioms" + "class" + "classes" + "classrel" + "code_abort" + "code_class" + "code_const" + "code_datatype" + "code_include" + "code_instance" + "code_library" + "code_module" + "code_modulename" + "code_monad" + "code_reflect" + "code_reserved" + "code_type" + "coinductive" + "coinductive_set" + "constdefs" + "consts" + "consts_code" + "context" + "datatype" + "declaration" + "declare" + "defaultsort" + "defer_recdef" + "definition" + "defs" + "equivariance" + "extract" + "extract_type" + "finalconsts" + "fun" + "global" + "hide_class" + "hide_const" + "hide_fact" + "hide_type" + "inductive" + "inductive_set" + "instantiation" + "judgment" + "lemmas" + "local" + "local_setup" + "locale" + "method_setup" + "nitpick_params" + "no_notation" + "no_syntax" + "no_translations" + "nominal_datatype" + "nonterminals" + "notation" + "oracle" + "overloading" + "parse_ast_translation" + "parse_translation" + "primrec" + "print_ast_translation" + "print_translation" + "quickcheck_params" + "quotient_definition" + "realizability" + "realizers" + "recdef" + "record" + "refute_params" + "setup" + "simproc_setup" + "sledgehammer_params" + "statespace" + "syntax" + "text" + "text_raw" + "theorems" + "translations" + "typed_print_translation" + "typedecl" + "types" + "types_code" + "use")) + +(defconst isar-keywords-theory-script + '("inductive_cases")) + +(defconst isar-keywords-theory-goal + '("ax_specification" + "code_pred" + "corollary" + "function" + "instance" + "interpretation" + "lemma" + "nominal_inductive" + "nominal_inductive2" + "nominal_primrec" + "prove" + "quotient_type" + "recdef_tc" + "rep_datatype" + "schematic_corollary" + "schematic_lemma" + "schematic_theorem" + "specification" + "subclass" + "sublocale" + "termination" + "theorem" + "typedef")) + +(defconst isar-keywords-qed + '("\\." + "\\.\\." + "by" + "done" + "sorry")) + +(defconst isar-keywords-qed-block + '("qed")) + +(defconst isar-keywords-qed-global + '("oops")) + +(defconst isar-keywords-proof-heading + '("sect" + "subsect" + "subsubsect")) + +(defconst isar-keywords-proof-goal + '("have" + "hence" + "interpret")) + +(defconst isar-keywords-proof-block + '("next" + "proof")) + +(defconst isar-keywords-proof-open + '("{")) + +(defconst isar-keywords-proof-close + '("}")) + +(defconst isar-keywords-proof-chain + '("finally" + "from" + "then" + "ultimately" + "with")) + +(defconst isar-keywords-proof-decl + '("ML_prf" + "also" + "let" + "moreover" + "note" + "txt" + "txt_raw" + "unfolding" + "using")) + +(defconst isar-keywords-proof-asm + '("assume" + "case" + "def" + "fix" + "presume")) + +(defconst isar-keywords-proof-asm-goal + '("guess" + "obtain" + "show" + "thus")) + +(defconst isar-keywords-proof-script + '("apply" + "apply_end" + "back" + "defer" + "prefer")) + +(provide 'isar-keywords) diff -r e8b9c0ebf5dd -r 83f1b16486ee TODO --- a/TODO Sun Jul 25 22:42:21 2010 +0200 +++ b/TODO Mon Jul 26 09:19:28 2010 +0200 @@ -35,30 +35,6 @@ - Parser adds syntax for raw datatype, but should add for lifted datatype. -- the alpha equivalence for - - Let as::assn t::trm bind "bn as" in t - - creates as premise - - EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t') - - but I think it should be - - as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t') - - (both are equivalent, but the second seems to be closer to - the fv-function) - -- when there are more than one shallow binder, then alpha - equivalence creates more than one permutation. According - to the paper, this is incorrect. - - Example in Classical.thy. - -- check whether weirdo example in TestMorePerm works - with shallow binders - - nested recursion, like types "trm list" in a constructor - define permute_bn automatically and prove properties of it diff -r e8b9c0ebf5dd -r 83f1b16486ee isar-keywords-quot.el --- a/isar-keywords-quot.el Sun Jul 25 22:42:21 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,616 +0,0 @@ -;; -;; Keyword classification tables for Isabelle/Isar. -;; Generated from HOL-Nominal-Quot + HOL-Nominal + HOL + Pure-ProofGeneral + Pure. -;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -;; - -(defconst isar-keywords-major - '("\\." - "\\.\\." - "Isabelle\\.command" - "Isar\\.begin_document" - "Isar\\.define_command" - "Isar\\.edit_document" - "Isar\\.end_document" - "ML" - "ML_command" - "ML_prf" - "ML_val" - "ProofGeneral\\.inform_file_processed" - "ProofGeneral\\.inform_file_retracted" - "ProofGeneral\\.kill_proof" - "ProofGeneral\\.pr" - "ProofGeneral\\.process_pgip" - "ProofGeneral\\.restart" - "ProofGeneral\\.undo" - "abbreviation" - "also" - "apply" - "apply_end" - "arities" - "assume" - "atom_decl" - "atp_info" - "atp_kill" - "atp_messages" - "atp_minimize" - "attribute_setup" - "ax_specification" - "axclass" - "axiomatization" - "axioms" - "back" - "by" - "cannot_undo" - "case" - "cd" - "chapter" - "class" - "class_deps" - "classes" - "classrel" - "code_abort" - "code_class" - "code_const" - "code_datatype" - "code_deps" - "code_include" - "code_instance" - "code_library" - "code_module" - "code_modulename" - "code_monad" - "code_pred" - "code_reflect" - "code_reserved" - "code_thms" - "code_type" - "coinductive" - "coinductive_set" - "commit" - "constdefs" - "consts" - "consts_code" - "context" - "corollary" - "datatype" - "declaration" - "declare" - "def" - "default_sort" - "defer" - "defer_recdef" - "definition" - "defs" - "disable_pr" - "display_drafts" - "done" - "enable_pr" - "end" - "equivariance" - "exit" - "export_code" - "extract" - "extract_type" - "finalconsts" - "finally" - "find_consts" - "find_theorems" - "fix" - "from" - "full_prf" - "fun" - "function" - "global" - "guess" - "have" - "header" - "help" - "hence" - "hide_class" - "hide_const" - "hide_fact" - "hide_type" - "inductive" - "inductive_cases" - "inductive_set" - "init_toplevel" - "instance" - "instantiation" - "interpret" - "interpretation" - "judgment" - "kill" - "kill_thy" - "lemma" - "lemmas" - "let" - "linear_undo" - "local" - "local_setup" - "locale" - "method_setup" - "moreover" - "next" - "nitpick" - "nitpick_params" - "no_notation" - "no_syntax" - "no_translations" - "nominal_datatype" - "nominal_inductive" - "nominal_inductive2" - "nominal_primrec" - "nonterminals" - "normal_form" - "notation" - "note" - "obtain" - "oops" - "oracle" - "overloading" - "parse_ast_translation" - "parse_translation" - "pr" - "prefer" - "presume" - "pretty_setmargin" - "prf" - "primrec" - "print_abbrevs" - "print_antiquotations" - "print_ast_translation" - "print_atps" - "print_attributes" - "print_binds" - "print_cases" - "print_claset" - "print_classes" - "print_codeproc" - "print_codesetup" - "print_commands" - "print_configs" - "print_context" - "print_drafts" - "print_facts" - "print_induct_rules" - "print_interps" - "print_locale" - "print_locales" - "print_maps" - "print_methods" - "print_orders" - "print_quotconsts" - "print_quotients" - "print_rules" - "print_simpset" - "print_statement" - "print_syntax" - "print_theorems" - "print_theory" - "print_trans_rules" - "print_translation" - "proof" - "prop" - "prove" - "pwd" - "qed" - "quickcheck" - "quickcheck_params" - "quit" - "quotient_definition" - "quotient_type" - "realizability" - "realizers" - "recdef" - "recdef_tc" - "record" - "refute" - "refute_params" - "remove_thy" - "rep_datatype" - "repdef" - "schematic_corollary" - "schematic_lemma" - "schematic_theorem" - "sect" - "section" - "setup" - "show" - "simproc_setup" - "sledgehammer" - "sledgehammer_params" - "smt_status" - "sorry" - "specification" - "subclass" - "sublocale" - "subsect" - "subsection" - "subsubsect" - "subsubsection" - "syntax" - "term" - "termination" - "text" - "text_raw" - "then" - "theorem" - "theorems" - "theory" - "thm" - "thm_deps" - "thus" - "thy_deps" - "touch_thy" - "translations" - "txt" - "txt_raw" - "typ" - "typed_print_translation" - "typedecl" - "typedef" - "types" - "types_code" - "ultimately" - "undo" - "undos_proof" - "unfolding" - "unused_thms" - "use" - "use_thy" - "using" - "value" - "values" - "welcome" - "with" - "{" - "}")) - -(defconst isar-keywords-minor - '("advanced" - "and" - "as" - "assumes" - "attach" - "avoids" - "begin" - "binder" - "congs" - "constrains" - "contains" - "defines" - "file" - "fixes" - "for" - "hints" - "identifier" - "if" - "imports" - "in" - "infix" - "infixl" - "infixr" - "is" - "module_name" - "monos" - "morphisms" - "notes" - "obtains" - "open" - "output" - "overloaded" - "permissive" - "pervasive" - "shows" - "structure" - "unchecked" - "uses" - "where")) - -(defconst isar-keywords-control - '("Isabelle\\.command" - "Isar\\.begin_document" - "Isar\\.define_command" - "Isar\\.edit_document" - "Isar\\.end_document" - "ProofGeneral\\.inform_file_processed" - "ProofGeneral\\.inform_file_retracted" - "ProofGeneral\\.kill_proof" - "ProofGeneral\\.process_pgip" - "ProofGeneral\\.restart" - "ProofGeneral\\.undo" - "cannot_undo" - "exit" - "init_toplevel" - "kill" - "linear_undo" - "quit" - "undo" - "undos_proof")) - -(defconst isar-keywords-diag - '("ML_command" - "ML_val" - "ProofGeneral\\.pr" - "atp_info" - "atp_kill" - "atp_messages" - "atp_minimize" - "cd" - "class_deps" - "code_deps" - "code_thms" - "commit" - "disable_pr" - "display_drafts" - "enable_pr" - "export_code" - "find_consts" - "find_theorems" - "full_prf" - "header" - "help" - "kill_thy" - "nitpick" - "normal_form" - "pr" - "pretty_setmargin" - "prf" - "print_abbrevs" - "print_antiquotations" - "print_atps" - "print_attributes" - "print_binds" - "print_cases" - "print_claset" - "print_classes" - "print_codeproc" - "print_codesetup" - "print_commands" - "print_configs" - "print_context" - "print_drafts" - "print_facts" - "print_induct_rules" - "print_interps" - "print_locale" - "print_locales" - "print_maps" - "print_methods" - "print_orders" - "print_quotconsts" - "print_quotients" - "print_rules" - "print_simpset" - "print_statement" - "print_syntax" - "print_theorems" - "print_theory" - "print_trans_rules" - "prop" - "pwd" - "quickcheck" - "refute" - "remove_thy" - "sledgehammer" - "term" - "thm" - "thm_deps" - "thy_deps" - "touch_thy" - "typ" - "unused_thms" - "use_thy" - "value" - "values" - "welcome")) - -(defconst isar-keywords-theory-begin - '("theory")) - -(defconst isar-keywords-theory-switch - '()) - -(defconst isar-keywords-theory-end - '("end")) - -(defconst isar-keywords-theory-heading - '("chapter" - "section" - "subsection" - "subsubsection")) - -(defconst isar-keywords-theory-decl - '("ML" - "abbreviation" - "arities" - "atom_decl" - "attribute_setup" - "axclass" - "axiomatization" - "axioms" - "class" - "classes" - "classrel" - "code_abort" - "code_class" - "code_const" - "code_datatype" - "code_include" - "code_instance" - "code_library" - "code_module" - "code_modulename" - "code_monad" - "code_reflect" - "code_reserved" - "code_type" - "coinductive" - "coinductive_set" - "constdefs" - "consts" - "consts_code" - "context" - "datatype" - "declaration" - "declare" - "defaultsort" - "defer_recdef" - "definition" - "defs" - "equivariance" - "extract" - "extract_type" - "finalconsts" - "fun" - "global" - "hide_class" - "hide_const" - "hide_fact" - "hide_type" - "inductive" - "inductive_set" - "instantiation" - "judgment" - "lemmas" - "local" - "local_setup" - "locale" - "method_setup" - "nitpick_params" - "no_notation" - "no_syntax" - "no_translations" - "nominal_datatype" - "nonterminals" - "notation" - "oracle" - "overloading" - "parse_ast_translation" - "parse_translation" - "primrec" - "print_ast_translation" - "print_translation" - "quickcheck_params" - "quotient_definition" - "realizability" - "realizers" - "recdef" - "record" - "refute_params" - "setup" - "simproc_setup" - "sledgehammer_params" - "statespace" - "syntax" - "text" - "text_raw" - "theorems" - "translations" - "typed_print_translation" - "typedecl" - "types" - "types_code" - "use")) - -(defconst isar-keywords-theory-script - '("inductive_cases")) - -(defconst isar-keywords-theory-goal - '("ax_specification" - "code_pred" - "corollary" - "function" - "instance" - "interpretation" - "lemma" - "nominal_inductive" - "nominal_inductive2" - "nominal_primrec" - "prove" - "quotient_type" - "recdef_tc" - "rep_datatype" - "schematic_corollary" - "schematic_lemma" - "schematic_theorem" - "specification" - "subclass" - "sublocale" - "termination" - "theorem" - "typedef")) - -(defconst isar-keywords-qed - '("\\." - "\\.\\." - "by" - "done" - "sorry")) - -(defconst isar-keywords-qed-block - '("qed")) - -(defconst isar-keywords-qed-global - '("oops")) - -(defconst isar-keywords-proof-heading - '("sect" - "subsect" - "subsubsect")) - -(defconst isar-keywords-proof-goal - '("have" - "hence" - "interpret")) - -(defconst isar-keywords-proof-block - '("next" - "proof")) - -(defconst isar-keywords-proof-open - '("{")) - -(defconst isar-keywords-proof-close - '("}")) - -(defconst isar-keywords-proof-chain - '("finally" - "from" - "then" - "ultimately" - "with")) - -(defconst isar-keywords-proof-decl - '("ML_prf" - "also" - "let" - "moreover" - "note" - "txt" - "txt_raw" - "unfolding" - "using")) - -(defconst isar-keywords-proof-asm - '("assume" - "case" - "def" - "fix" - "presume")) - -(defconst isar-keywords-proof-asm-goal - '("guess" - "obtain" - "show" - "thus")) - -(defconst isar-keywords-proof-script - '("apply" - "apply_end" - "back" - "defer" - "prefer")) - -(provide 'isar-keywords)