--- a/etc/isar-keywords-ZF.el Wed Apr 22 11:10:23 2009 +0200
+++ b/etc/isar-keywords-ZF.el Mon May 11 09:18:42 2009 +0200
@@ -18,7 +18,6 @@
"ML"
"ML_command"
"ML_prf"
- "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -46,18 +45,15 @@
"class_deps"
"classes"
"classrel"
- "codatatype"
"code_datatype"
"code_library"
"code_module"
- "coinductive"
"commit"
"constdefs"
"consts"
"consts_code"
"context"
"corollary"
- "datatype"
"declaration"
"declare"
"def"
@@ -87,8 +83,6 @@
"help"
"hence"
"hide"
- "inductive"
- "inductive_cases"
"init_toplevel"
"instance"
"instantiation"
@@ -124,7 +118,6 @@
"presume"
"pretty_setmargin"
"prf"
- "primrec"
"print_abbrevs"
"print_antiquotations"
"print_ast_translation"
@@ -147,7 +140,6 @@
"print_simpset"
"print_statement"
"print_syntax"
- "print_tcset"
"print_theorems"
"print_theory"
"print_trans_rules"
@@ -162,7 +154,6 @@
"realizability"
"realizers"
"remove_thy"
- "rep_datatype"
"sect"
"section"
"setup"
@@ -216,13 +207,9 @@
"attach"
"begin"
"binder"
- "case_eqns"
- "con_defs"
"constrains"
"contains"
"defines"
- "domains"
- "elimination"
"file"
"fixes"
"for"
@@ -230,23 +217,17 @@
"if"
"imports"
"in"
- "induction"
"infix"
"infixl"
"infixr"
- "intros"
"is"
- "monos"
"notes"
"obtains"
"open"
"output"
"overloaded"
- "recursor_eqns"
"shows"
"structure"
- "type_elims"
- "type_intros"
"unchecked"
"uses"
"where"))
@@ -314,7 +295,6 @@
"print_simpset"
"print_statement"
"print_syntax"
- "print_tcset"
"print_theorems"
"print_theory"
"print_trans_rules"
@@ -349,7 +329,6 @@
(defconst isar-keywords-theory-decl
'("ML"
- "ML_test"
"abbreviation"
"arities"
"attribute_setup"
@@ -359,16 +338,13 @@
"class"
"classes"
"classrel"
- "codatatype"
"code_datatype"
"code_library"
"code_module"
- "coinductive"
"constdefs"
"consts"
"consts_code"
"context"
- "datatype"
"declaration"
"declare"
"defaultsort"
@@ -379,7 +355,6 @@
"finalconsts"
"global"
"hide"
- "inductive"
"instantiation"
"judgment"
"lemmas"
@@ -396,13 +371,11 @@
"overloading"
"parse_ast_translation"
"parse_translation"
- "primrec"
"print_ast_translation"
"print_translation"
"quickcheck_params"
"realizability"
"realizers"
- "rep_datatype"
"setup"
"simproc_setup"
"syntax"
@@ -417,7 +390,7 @@
"use"))
(defconst isar-keywords-theory-script
- '("inductive_cases"))
+ '())
(defconst isar-keywords-theory-goal
'("corollary"
--- a/etc/isar-keywords.el Wed Apr 22 11:10:23 2009 +0200
+++ b/etc/isar-keywords.el Mon May 11 09:18:42 2009 +0200
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + HOL-ex.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -18,7 +18,6 @@
"ML"
"ML_command"
"ML_prf"
- "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -37,7 +36,6 @@
"atp_kill"
"atp_messages"
"attribute_setup"
- "automaton"
"ax_specification"
"axclass"
"axiomatization"
@@ -63,6 +61,7 @@
"code_module"
"code_modulename"
"code_monad"
+ "code_pred"
"code_reserved"
"code_thms"
"code_type"
@@ -74,7 +73,6 @@
"consts_code"
"context"
"corollary"
- "cpodef"
"datatype"
"declaration"
"declare"
@@ -86,7 +84,6 @@
"defs"
"disable_pr"
"display_drafts"
- "domain"
"done"
"enable_pr"
"end"
@@ -100,8 +97,6 @@
"find_consts"
"find_theorems"
"fix"
- "fixpat"
- "fixrec"
"from"
"full_prf"
"fun"
@@ -151,7 +146,6 @@
"overloading"
"parse_ast_translation"
"parse_translation"
- "pcpodef"
"pr"
"prefer"
"presume"
@@ -255,15 +249,13 @@
"}"))
(defconst isar-keywords-minor
- '("actions"
- "advanced"
+ '("advanced"
"and"
"assumes"
"attach"
"avoids"
"begin"
"binder"
- "compose"
"congs"
"constrains"
"contains"
@@ -271,7 +263,6 @@
"file"
"fixes"
"for"
- "hide_action"
"hints"
"identifier"
"if"
@@ -280,11 +271,7 @@
"infix"
"infixl"
"infixr"
- "initially"
- "inputs"
- "internals"
"is"
- "lazy"
"module_name"
"monos"
"morphisms"
@@ -292,20 +279,10 @@
"obtains"
"open"
"output"
- "outputs"
"overloaded"
"permissive"
- "post"
- "pre"
- "rename"
- "restrict"
"shows"
- "signature"
- "states"
"structure"
- "to"
- "transitions"
- "transrel"
"unchecked"
"uses"
"where"))
@@ -419,12 +396,10 @@
(defconst isar-keywords-theory-decl
'("ML"
- "ML_test"
"abbreviation"
"arities"
"atom_decl"
"attribute_setup"
- "automaton"
"axclass"
"axiomatization"
"axioms"
@@ -456,13 +431,10 @@
"defer_recdef"
"definition"
"defs"
- "domain"
"equivariance"
"extract"
"extract_type"
"finalconsts"
- "fixpat"
- "fixrec"
"fun"
"global"
"hide"
@@ -513,8 +485,8 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "code_pred"
"corollary"
- "cpodef"
"function"
"instance"
"interpretation"
@@ -522,7 +494,6 @@
"nominal_inductive"
"nominal_inductive2"
"nominal_primrec"
- "pcpodef"
"recdef_tc"
"rep_datatype"
"specification"
--- a/lib/jedit/isabelle.xml Wed Apr 22 11:10:23 2009 +0200
+++ b/lib/jedit/isabelle.xml Mon May 11 09:18:42 2009 +0200
@@ -45,10 +45,8 @@
<OPERATOR>ML</OPERATOR>
<LABEL>ML_command</LABEL>
<OPERATOR>ML_prf</OPERATOR>
- <OPERATOR>ML_test</OPERATOR>
<LABEL>ML_val</LABEL>
<OPERATOR>abbreviation</OPERATOR>
- <KEYWORD4>actions</KEYWORD4>
<KEYWORD4>advanced</KEYWORD4>
<OPERATOR>also</OPERATOR>
<KEYWORD4>and</KEYWORD4>
@@ -63,7 +61,6 @@
<LABEL>atp_messages</LABEL>
<KEYWORD4>attach</KEYWORD4>
<OPERATOR>attribute_setup</OPERATOR>
- <OPERATOR>automaton</OPERATOR>
<KEYWORD4>avoids</KEYWORD4>
<OPERATOR>ax_specification</OPERATOR>
<OPERATOR>axclass</OPERATOR>
@@ -75,14 +72,12 @@
<OPERATOR>by</OPERATOR>
<INVALID>cannot_undo</INVALID>
<KEYWORD2>case</KEYWORD2>
- <KEYWORD4>case_eqns</KEYWORD4>
<LABEL>cd</LABEL>
<OPERATOR>chapter</OPERATOR>
<OPERATOR>class</OPERATOR>
<LABEL>class_deps</LABEL>
<OPERATOR>classes</OPERATOR>
<OPERATOR>classrel</OPERATOR>
- <OPERATOR>codatatype</OPERATOR>
<OPERATOR>code_abort</OPERATOR>
<OPERATOR>code_class</OPERATOR>
<OPERATOR>code_const</OPERATOR>
@@ -100,8 +95,6 @@
<OPERATOR>coinductive</OPERATOR>
<OPERATOR>coinductive_set</OPERATOR>
<LABEL>commit</LABEL>
- <KEYWORD4>compose</KEYWORD4>
- <KEYWORD4>con_defs</KEYWORD4>
<KEYWORD4>congs</KEYWORD4>
<OPERATOR>constdefs</OPERATOR>
<KEYWORD4>constrains</KEYWORD4>
@@ -110,7 +103,6 @@
<KEYWORD4>contains</KEYWORD4>
<OPERATOR>context</OPERATOR>
<OPERATOR>corollary</OPERATOR>
- <OPERATOR>cpodef</OPERATOR>
<OPERATOR>datatype</OPERATOR>
<OPERATOR>declaration</OPERATOR>
<OPERATOR>declare</OPERATOR>
@@ -123,10 +115,7 @@
<OPERATOR>defs</OPERATOR>
<LABEL>disable_pr</LABEL>
<LABEL>display_drafts</LABEL>
- <OPERATOR>domain</OPERATOR>
- <KEYWORD4>domains</KEYWORD4>
<OPERATOR>done</OPERATOR>
- <KEYWORD4>elimination</KEYWORD4>
<LABEL>enable_pr</LABEL>
<KEYWORD3>end</KEYWORD3>
<OPERATOR>equivariance</OPERATOR>
@@ -141,8 +130,6 @@
<LABEL>find_theorems</LABEL>
<KEYWORD2>fix</KEYWORD2>
<KEYWORD4>fixes</KEYWORD4>
- <OPERATOR>fixpat</OPERATOR>
- <OPERATOR>fixrec</OPERATOR>
<KEYWORD4>for</KEYWORD4>
<OPERATOR>from</OPERATOR>
<LABEL>full_prf</LABEL>
@@ -155,13 +142,11 @@
<LABEL>help</LABEL>
<OPERATOR>hence</OPERATOR>
<OPERATOR>hide</OPERATOR>
- <KEYWORD4>hide_action</KEYWORD4>
<KEYWORD4>hints</KEYWORD4>
<KEYWORD4>identifier</KEYWORD4>
<KEYWORD4>if</KEYWORD4>
<KEYWORD4>imports</KEYWORD4>
<KEYWORD4>in</KEYWORD4>
- <KEYWORD4>induction</KEYWORD4>
<OPERATOR>inductive</OPERATOR>
<KEYWORD1>inductive_cases</KEYWORD1>
<OPERATOR>inductive_set</OPERATOR>
@@ -169,19 +154,14 @@
<KEYWORD4>infixl</KEYWORD4>
<KEYWORD4>infixr</KEYWORD4>
<INVALID>init_toplevel</INVALID>
- <KEYWORD4>initially</KEYWORD4>
- <KEYWORD4>inputs</KEYWORD4>
<OPERATOR>instance</OPERATOR>
<OPERATOR>instantiation</OPERATOR>
- <KEYWORD4>internals</KEYWORD4>
<OPERATOR>interpret</OPERATOR>
<OPERATOR>interpretation</OPERATOR>
- <KEYWORD4>intros</KEYWORD4>
<KEYWORD4>is</KEYWORD4>
<OPERATOR>judgment</OPERATOR>
<INVALID>kill</INVALID>
<LABEL>kill_thy</LABEL>
- <KEYWORD4>lazy</KEYWORD4>
<OPERATOR>lemma</OPERATOR>
<OPERATOR>lemmas</OPERATOR>
<OPERATOR>let</OPERATOR>
@@ -213,16 +193,12 @@
<KEYWORD4>open</KEYWORD4>
<OPERATOR>oracle</OPERATOR>
<KEYWORD4>output</KEYWORD4>
- <KEYWORD4>outputs</KEYWORD4>
<KEYWORD4>overloaded</KEYWORD4>
<OPERATOR>overloading</OPERATOR>
<OPERATOR>parse_ast_translation</OPERATOR>
<OPERATOR>parse_translation</OPERATOR>
- <OPERATOR>pcpodef</OPERATOR>
<KEYWORD4>permissive</KEYWORD4>
- <KEYWORD4>post</KEYWORD4>
<LABEL>pr</LABEL>
- <KEYWORD4>pre</KEYWORD4>
<KEYWORD1>prefer</KEYWORD1>
<KEYWORD2>presume</KEYWORD2>
<LABEL>pretty_setmargin</LABEL>
@@ -252,7 +228,6 @@
<LABEL>print_simpset</LABEL>
<LABEL>print_statement</LABEL>
<LABEL>print_syntax</LABEL>
- <LABEL>print_tcset</LABEL>
<LABEL>print_theorems</LABEL>
<LABEL>print_theory</LABEL>
<LABEL>print_trans_rules</LABEL>
@@ -269,24 +244,19 @@
<OPERATOR>recdef</OPERATOR>
<OPERATOR>recdef_tc</OPERATOR>
<OPERATOR>record</OPERATOR>
- <KEYWORD4>recursor_eqns</KEYWORD4>
<LABEL>refute</LABEL>
<OPERATOR>refute_params</OPERATOR>
<LABEL>remove_thy</LABEL>
- <KEYWORD4>rename</KEYWORD4>
<OPERATOR>rep_datatype</OPERATOR>
- <KEYWORD4>restrict</KEYWORD4>
<OPERATOR>sect</OPERATOR>
<OPERATOR>section</OPERATOR>
<OPERATOR>setup</OPERATOR>
<KEYWORD2>show</KEYWORD2>
<KEYWORD4>shows</KEYWORD4>
- <KEYWORD4>signature</KEYWORD4>
<OPERATOR>simproc_setup</OPERATOR>
<LABEL>sledgehammer</LABEL>
<OPERATOR>sorry</OPERATOR>
<OPERATOR>specification</OPERATOR>
- <KEYWORD4>states</KEYWORD4>
<OPERATOR>statespace</OPERATOR>
<KEYWORD4>structure</KEYWORD4>
<OPERATOR>subclass</OPERATOR>
@@ -308,16 +278,11 @@
<LABEL>thm_deps</LABEL>
<KEYWORD2>thus</KEYWORD2>
<LABEL>thy_deps</LABEL>
- <KEYWORD4>to</KEYWORD4>
<LABEL>touch_thy</LABEL>
- <KEYWORD4>transitions</KEYWORD4>
<OPERATOR>translations</OPERATOR>
- <KEYWORD4>transrel</KEYWORD4>
<OPERATOR>txt</OPERATOR>
<OPERATOR>txt_raw</OPERATOR>
<LABEL>typ</LABEL>
- <KEYWORD4>type_elims</KEYWORD4>
- <KEYWORD4>type_intros</KEYWORD4>
<OPERATOR>typed_print_translation</OPERATOR>
<OPERATOR>typedecl</OPERATOR>
<OPERATOR>typedef</OPERATOR>
--- a/src/HOL/Predicate.thy Wed Apr 22 11:10:23 2009 +0200
+++ b/src/HOL/Predicate.thy Mon May 11 09:18:42 2009 +0200
@@ -640,4 +640,12 @@
hide (open) const Pred eval single bind if_pred not_pred
Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
+text {* dummy setup for code_pred keyword *}
+
+ML {*
+OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
+ OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]])))
+*}
+
+
end
--- a/src/HOL/ex/Predicate_Compile.thy Wed Apr 22 11:10:23 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Mon May 11 09:18:42 2009 +0200
@@ -5,6 +5,11 @@
setup {* Predicate_Compile.setup *}
+ML {*
+ OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
+ OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd)
+*}
+
primrec "next" :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
\<Rightarrow> 'a Predicate.seq \<Rightarrow> ('a \<times> 'a Predicate.pred) option" where
"next yield Predicate.Empty = None"
@@ -34,4 +39,17 @@
end
*}
+section {* Example for user interface *}
+
+inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+ "append [] ys ys"
+| "append xs' ys zs' \<Longrightarrow> append (x#xs') ys (x#zs')"
+
+code_pred append
+ using assms by (rule append.cases)
+
+thm append_cases
+
+
end
\ No newline at end of file
--- a/src/HOL/ex/predicate_compile.ML Wed Apr 22 11:10:23 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Mon May 11 09:18:42 2009 +0200
@@ -14,8 +14,12 @@
val code_ind_intros_attrib : attribute
val code_ind_cases_attrib : attribute
val setup : theory -> theory
+ val code_pred : string -> Proof.context -> Proof.state
+ val code_pred_cmd : string -> Proof.context -> Proof.state
val print_alternative_rules : theory -> theory
val do_proofs: bool ref
+ val pred_intros : theory -> string -> thm list
+ val get_nparams : theory -> string -> int
end;
structure Predicate_Compile: PREDICATE_COMPILE =
@@ -1340,6 +1344,57 @@
Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
"adding alternative elimination rules for code generation of inductive predicates";
+(* generation of case rules from user-given introduction rules *)
+
+ fun mk_casesrule introrules nparams ctxt = let
+ val intros = map prop_of introrules
+ val (pred, (params, args)) = strip_intro_concl (hd intros) nparams
+ val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
+ val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
+ val (argnames, ctxt2) = Variable.variant_fixes
+ (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
+ val argvs = map Free (argnames ~~ (map fastype_of args))
+ fun mk_case intro = let
+ val (_, (_, args)) = strip_intro_concl intro nparams
+ val prems = Logic.strip_imp_prems intro
+ val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+ val frees = (fold o fold_aterms)
+ (fn t as Free _ =>
+ if member (op aconv) params t then I else insert (op aconv) t
+ | _ => I) (args @ prems) []
+ in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
+ val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
+ val cases = map mk_case intros
+ val (_, ctxt3) = ProofContext.add_assms_i Assumption.assume_export
+ [((Binding.name AutoBind.assmsN, []), map (fn t => (t, [])) (assm :: cases))]
+ ctxt2
+ in (pred, prop, ctxt3) end;
+
+(* setup for user interface *)
+
+ fun generic_code_pred prep_const raw_const lthy =
+ let
+ val thy = (ProofContext.theory_of lthy)
+ val const = prep_const thy raw_const
+ val nparams = get_nparams thy const
+ val intro_rules = pred_intros thy const
+ val (((tfrees, frees), fact), ctxt') =
+ Variable.import_thms true intro_rules lthy;
+ val (pred, prop, ctxt'') = mk_casesrule fact nparams ctxt'
+ val (predname, _) = dest_Const pred
+ fun after_qed [[th]] ctxt'' =
+ LocalTheory.note Thm.theoremK
+ ((Binding.name (Long_Name.base_name predname ^ "_cases"),
+ [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) ctxt''
+ |> snd
+ |> ProofContext.theory (create_def_equation predname)
+ in
+ Proof.theorem_i NONE after_qed [[(prop, [])]] ctxt''
+ end;
+
+ val code_pred = generic_code_pred (K I);
+ val code_pred_cmd = generic_code_pred Code_Unit.read_const
+
end;
fun pred_compile name thy = Predicate_Compile.create_def_equation