1.1 --- a/etc/isar-keywords-ZF.el	Wed Apr 22 11:10:23 2009 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon May 11 09:18:42 2009 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4      "ML"
     1.5      "ML_command"
     1.6      "ML_prf"
     1.7 -    "ML_test"
     1.8      "ML_val"
     1.9      "ProofGeneral\\.inform_file_processed"
    1.10      "ProofGeneral\\.inform_file_retracted"
    1.11 @@ -46,18 +45,15 @@
    1.12      "class_deps"
    1.13      "classes"
    1.14      "classrel"
    1.15 -    "codatatype"
    1.16      "code_datatype"
    1.17      "code_library"
    1.18      "code_module"
    1.19 -    "coinductive"
    1.20      "commit"
    1.21      "constdefs"
    1.22      "consts"
    1.23      "consts_code"
    1.24      "context"
    1.25      "corollary"
    1.26 -    "datatype"
    1.27      "declaration"
    1.28      "declare"
    1.29      "def"
    1.30 @@ -87,8 +83,6 @@
    1.31      "help"
    1.32      "hence"
    1.33      "hide"
    1.34 -    "inductive"
    1.35 -    "inductive_cases"
    1.36      "init_toplevel"
    1.37      "instance"
    1.38      "instantiation"
    1.39 @@ -124,7 +118,6 @@
    1.40      "presume"
    1.41      "pretty_setmargin"
    1.42      "prf"
    1.43 -    "primrec"
    1.44      "print_abbrevs"
    1.45      "print_antiquotations"
    1.46      "print_ast_translation"
    1.47 @@ -147,7 +140,6 @@
    1.48      "print_simpset"
    1.49      "print_statement"
    1.50      "print_syntax"
    1.51 -    "print_tcset"
    1.52      "print_theorems"
    1.53      "print_theory"
    1.54      "print_trans_rules"
    1.55 @@ -162,7 +154,6 @@
    1.56      "realizability"
    1.57      "realizers"
    1.58      "remove_thy"
    1.59 -    "rep_datatype"
    1.60      "sect"
    1.61      "section"
    1.62      "setup"
    1.63 @@ -216,13 +207,9 @@
    1.64      "attach"
    1.65      "begin"
    1.66      "binder"
    1.67 -    "case_eqns"
    1.68 -    "con_defs"
    1.69      "constrains"
    1.70      "contains"
    1.71      "defines"
    1.72 -    "domains"
    1.73 -    "elimination"
    1.74      "file"
    1.75      "fixes"
    1.76      "for"
    1.77 @@ -230,23 +217,17 @@
    1.78      "if"
    1.79      "imports"
    1.80      "in"
    1.81 -    "induction"
    1.82      "infix"
    1.83      "infixl"
    1.84      "infixr"
    1.85 -    "intros"
    1.86      "is"
    1.87 -    "monos"
    1.88      "notes"
    1.89      "obtains"
    1.90      "open"
    1.91      "output"
    1.92      "overloaded"
    1.93 -    "recursor_eqns"
    1.94      "shows"
    1.95      "structure"
    1.96 -    "type_elims"
    1.97 -    "type_intros"
    1.98      "unchecked"
    1.99      "uses"
   1.100      "where"))
   1.101 @@ -314,7 +295,6 @@
   1.102      "print_simpset"
   1.103      "print_statement"
   1.104      "print_syntax"
   1.105 -    "print_tcset"
   1.106      "print_theorems"
   1.107      "print_theory"
   1.108      "print_trans_rules"
   1.109 @@ -349,7 +329,6 @@
   1.110  
   1.111  (defconst isar-keywords-theory-decl
   1.112    '("ML"
   1.113 -    "ML_test"
   1.114      "abbreviation"
   1.115      "arities"
   1.116      "attribute_setup"
   1.117 @@ -359,16 +338,13 @@
   1.118      "class"
   1.119      "classes"
   1.120      "classrel"
   1.121 -    "codatatype"
   1.122      "code_datatype"
   1.123      "code_library"
   1.124      "code_module"
   1.125 -    "coinductive"
   1.126      "constdefs"
   1.127      "consts"
   1.128      "consts_code"
   1.129      "context"
   1.130 -    "datatype"
   1.131      "declaration"
   1.132      "declare"
   1.133      "defaultsort"
   1.134 @@ -379,7 +355,6 @@
   1.135      "finalconsts"
   1.136      "global"
   1.137      "hide"
   1.138 -    "inductive"
   1.139      "instantiation"
   1.140      "judgment"
   1.141      "lemmas"
   1.142 @@ -396,13 +371,11 @@
   1.143      "overloading"
   1.144      "parse_ast_translation"
   1.145      "parse_translation"
   1.146 -    "primrec"
   1.147      "print_ast_translation"
   1.148      "print_translation"
   1.149      "quickcheck_params"
   1.150      "realizability"
   1.151      "realizers"
   1.152 -    "rep_datatype"
   1.153      "setup"
   1.154      "simproc_setup"
   1.155      "syntax"
   1.156 @@ -417,7 +390,7 @@
   1.157      "use"))
   1.158  
   1.159  (defconst isar-keywords-theory-script
   1.160 -  '("inductive_cases"))
   1.161 +  '())
   1.162  
   1.163  (defconst isar-keywords-theory-goal
   1.164    '("corollary"

     2.1 --- a/etc/isar-keywords.el	Wed Apr 22 11:10:23 2009 +0200
     2.2 +++ b/etc/isar-keywords.el	Mon May 11 09:18:42 2009 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  ;;
     2.5  ;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
     2.7 +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + HOL-ex.
     2.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  
    2.11 @@ -18,7 +18,6 @@
    2.12      "ML"
    2.13      "ML_command"
    2.14      "ML_prf"
    2.15 -    "ML_test"
    2.16      "ML_val"
    2.17      "ProofGeneral\\.inform_file_processed"
    2.18      "ProofGeneral\\.inform_file_retracted"
    2.19 @@ -37,7 +36,6 @@
    2.20      "atp_kill"
    2.21      "atp_messages"
    2.22      "attribute_setup"
    2.23 -    "automaton"
    2.24      "ax_specification"
    2.25      "axclass"
    2.26      "axiomatization"
    2.27 @@ -63,6 +61,7 @@
    2.28      "code_module"
    2.29      "code_modulename"
    2.30      "code_monad"
    2.31 +    "code_pred"
    2.32      "code_reserved"
    2.33      "code_thms"
    2.34      "code_type"
    2.35 @@ -74,7 +73,6 @@
    2.36      "consts_code"
    2.37      "context"
    2.38      "corollary"
    2.39 -    "cpodef"
    2.40      "datatype"
    2.41      "declaration"
    2.42      "declare"
    2.43 @@ -86,7 +84,6 @@
    2.44      "defs"
    2.45      "disable_pr"
    2.46      "display_drafts"
    2.47 -    "domain"
    2.48      "done"
    2.49      "enable_pr"
    2.50      "end"
    2.51 @@ -100,8 +97,6 @@
    2.52      "find_consts"
    2.53      "find_theorems"
    2.54      "fix"
    2.55 -    "fixpat"
    2.56 -    "fixrec"
    2.57      "from"
    2.58      "full_prf"
    2.59      "fun"
    2.60 @@ -151,7 +146,6 @@
    2.61      "overloading"
    2.62      "parse_ast_translation"
    2.63      "parse_translation"
    2.64 -    "pcpodef"
    2.65      "pr"
    2.66      "prefer"
    2.67      "presume"
    2.68 @@ -255,15 +249,13 @@
    2.69      "}"))
    2.70  
    2.71  (defconst isar-keywords-minor
    2.72 -  '("actions"
    2.73 -    "advanced"
    2.74 +  '("advanced"
    2.75      "and"
    2.76      "assumes"
    2.77      "attach"
    2.78      "avoids"
    2.79      "begin"
    2.80      "binder"
    2.81 -    "compose"
    2.82      "congs"
    2.83      "constrains"
    2.84      "contains"
    2.85 @@ -271,7 +263,6 @@
    2.86      "file"
    2.87      "fixes"
    2.88      "for"
    2.89 -    "hide_action"
    2.90      "hints"
    2.91      "identifier"
    2.92      "if"
    2.93 @@ -280,11 +271,7 @@
    2.94      "infix"
    2.95      "infixl"
    2.96      "infixr"
    2.97 -    "initially"
    2.98 -    "inputs"
    2.99 -    "internals"
   2.100      "is"
   2.101 -    "lazy"
   2.102      "module_name"
   2.103      "monos"
   2.104      "morphisms"
   2.105 @@ -292,20 +279,10 @@
   2.106      "obtains"
   2.107      "open"
   2.108      "output"
   2.109 -    "outputs"
   2.110      "overloaded"
   2.111      "permissive"
   2.112 -    "post"
   2.113 -    "pre"
   2.114 -    "rename"
   2.115 -    "restrict"
   2.116      "shows"
   2.117 -    "signature"
   2.118 -    "states"
   2.119      "structure"
   2.120 -    "to"
   2.121 -    "transitions"
   2.122 -    "transrel"
   2.123      "unchecked"
   2.124      "uses"
   2.125      "where"))
   2.126 @@ -419,12 +396,10 @@
   2.127  
   2.128  (defconst isar-keywords-theory-decl
   2.129    '("ML"
   2.130 -    "ML_test"
   2.131      "abbreviation"
   2.132      "arities"
   2.133      "atom_decl"
   2.134      "attribute_setup"
   2.135 -    "automaton"
   2.136      "axclass"
   2.137      "axiomatization"
   2.138      "axioms"
   2.139 @@ -456,13 +431,10 @@
   2.140      "defer_recdef"
   2.141      "definition"
   2.142      "defs"
   2.143 -    "domain"
   2.144      "equivariance"
   2.145      "extract"
   2.146      "extract_type"
   2.147      "finalconsts"
   2.148 -    "fixpat"
   2.149 -    "fixrec"
   2.150      "fun"
   2.151      "global"
   2.152      "hide"
   2.153 @@ -513,8 +485,8 @@
   2.154  
   2.155  (defconst isar-keywords-theory-goal
   2.156    '("ax_specification"
   2.157 +    "code_pred"
   2.158      "corollary"
   2.159 -    "cpodef"
   2.160      "function"
   2.161      "instance"
   2.162      "interpretation"
   2.163 @@ -522,7 +494,6 @@
   2.164      "nominal_inductive"
   2.165      "nominal_inductive2"
   2.166      "nominal_primrec"
   2.167 -    "pcpodef"
   2.168      "recdef_tc"
   2.169      "rep_datatype"
   2.170      "specification"

     3.1 --- a/lib/jedit/isabelle.xml	Wed Apr 22 11:10:23 2009 +0200
     3.2 +++ b/lib/jedit/isabelle.xml	Mon May 11 09:18:42 2009 +0200
     3.3 @@ -45,10 +45,8 @@
     3.4        <OPERATOR>ML</OPERATOR>
     3.5        <LABEL>ML_command</LABEL>
     3.6        <OPERATOR>ML_prf</OPERATOR>
     3.7 -      <OPERATOR>ML_test</OPERATOR>
     3.8        <LABEL>ML_val</LABEL>
     3.9        <OPERATOR>abbreviation</OPERATOR>
    3.10 -      <KEYWORD4>actions</KEYWORD4>
    3.11        <KEYWORD4>advanced</KEYWORD4>
    3.12        <OPERATOR>also</OPERATOR>
    3.13        <KEYWORD4>and</KEYWORD4>
    3.14 @@ -63,7 +61,6 @@
    3.15        <LABEL>atp_messages</LABEL>
    3.16        <KEYWORD4>attach</KEYWORD4>
    3.17        <OPERATOR>attribute_setup</OPERATOR>
    3.18 -      <OPERATOR>automaton</OPERATOR>
    3.19        <KEYWORD4>avoids</KEYWORD4>
    3.20        <OPERATOR>ax_specification</OPERATOR>
    3.21        <OPERATOR>axclass</OPERATOR>
    3.22 @@ -75,14 +72,12 @@
    3.23        <OPERATOR>by</OPERATOR>
    3.24        <INVALID>cannot_undo</INVALID>
    3.25        <KEYWORD2>case</KEYWORD2>
    3.26 -      <KEYWORD4>case_eqns</KEYWORD4>
    3.27        <LABEL>cd</LABEL>
    3.28        <OPERATOR>chapter</OPERATOR>
    3.29        <OPERATOR>class</OPERATOR>
    3.30        <LABEL>class_deps</LABEL>
    3.31        <OPERATOR>classes</OPERATOR>
    3.32        <OPERATOR>classrel</OPERATOR>
    3.33 -      <OPERATOR>codatatype</OPERATOR>
    3.34        <OPERATOR>code_abort</OPERATOR>
    3.35        <OPERATOR>code_class</OPERATOR>
    3.36        <OPERATOR>code_const</OPERATOR>
    3.37 @@ -100,8 +95,6 @@
    3.38        <OPERATOR>coinductive</OPERATOR>
    3.39        <OPERATOR>coinductive_set</OPERATOR>
    3.40        <LABEL>commit</LABEL>
    3.41 -      <KEYWORD4>compose</KEYWORD4>
    3.42 -      <KEYWORD4>con_defs</KEYWORD4>
    3.43        <KEYWORD4>congs</KEYWORD4>
    3.44        <OPERATOR>constdefs</OPERATOR>
    3.45        <KEYWORD4>constrains</KEYWORD4>
    3.46 @@ -110,7 +103,6 @@
    3.47        <KEYWORD4>contains</KEYWORD4>
    3.48        <OPERATOR>context</OPERATOR>
    3.49        <OPERATOR>corollary</OPERATOR>
    3.50 -      <OPERATOR>cpodef</OPERATOR>
    3.51        <OPERATOR>datatype</OPERATOR>
    3.52        <OPERATOR>declaration</OPERATOR>
    3.53        <OPERATOR>declare</OPERATOR>
    3.54 @@ -123,10 +115,7 @@
    3.55        <OPERATOR>defs</OPERATOR>
    3.56        <LABEL>disable_pr</LABEL>
    3.57        <LABEL>display_drafts</LABEL>
    3.58 -      <OPERATOR>domain</OPERATOR>
    3.59 -      <KEYWORD4>domains</KEYWORD4>
    3.60        <OPERATOR>done</OPERATOR>
    3.61 -      <KEYWORD4>elimination</KEYWORD4>
    3.62        <LABEL>enable_pr</LABEL>
    3.63        <KEYWORD3>end</KEYWORD3>
    3.64        <OPERATOR>equivariance</OPERATOR>
    3.65 @@ -141,8 +130,6 @@
    3.66        <LABEL>find_theorems</LABEL>
    3.67        <KEYWORD2>fix</KEYWORD2>
    3.68        <KEYWORD4>fixes</KEYWORD4>
    3.69 -      <OPERATOR>fixpat</OPERATOR>
    3.70 -      <OPERATOR>fixrec</OPERATOR>
    3.71        <KEYWORD4>for</KEYWORD4>
    3.72        <OPERATOR>from</OPERATOR>
    3.73        <LABEL>full_prf</LABEL>
    3.74 @@ -155,13 +142,11 @@
    3.75        <LABEL>help</LABEL>
    3.76        <OPERATOR>hence</OPERATOR>
    3.77        <OPERATOR>hide</OPERATOR>
    3.78 -      <KEYWORD4>hide_action</KEYWORD4>
    3.79        <KEYWORD4>hints</KEYWORD4>
    3.80        <KEYWORD4>identifier</KEYWORD4>
    3.81        <KEYWORD4>if</KEYWORD4>
    3.82        <KEYWORD4>imports</KEYWORD4>
    3.83        <KEYWORD4>in</KEYWORD4>
    3.84 -      <KEYWORD4>induction</KEYWORD4>
    3.85        <OPERATOR>inductive</OPERATOR>
    3.86        <KEYWORD1>inductive_cases</KEYWORD1>
    3.87        <OPERATOR>inductive_set</OPERATOR>
    3.88 @@ -169,19 +154,14 @@
    3.89        <KEYWORD4>infixl</KEYWORD4>
    3.90        <KEYWORD4>infixr</KEYWORD4>
    3.91        <INVALID>init_toplevel</INVALID>
    3.92 -      <KEYWORD4>initially</KEYWORD4>
    3.93 -      <KEYWORD4>inputs</KEYWORD4>
    3.94        <OPERATOR>instance</OPERATOR>
    3.95        <OPERATOR>instantiation</OPERATOR>
    3.96 -      <KEYWORD4>internals</KEYWORD4>
    3.97        <OPERATOR>interpret</OPERATOR>
    3.98        <OPERATOR>interpretation</OPERATOR>
    3.99 -      <KEYWORD4>intros</KEYWORD4>
   3.100        <KEYWORD4>is</KEYWORD4>
   3.101        <OPERATOR>judgment</OPERATOR>
   3.102        <INVALID>kill</INVALID>
   3.103        <LABEL>kill_thy</LABEL>
   3.104 -      <KEYWORD4>lazy</KEYWORD4>
   3.105        <OPERATOR>lemma</OPERATOR>
   3.106        <OPERATOR>lemmas</OPERATOR>
   3.107        <OPERATOR>let</OPERATOR>
   3.108 @@ -213,16 +193,12 @@
   3.109        <KEYWORD4>open</KEYWORD4>
   3.110        <OPERATOR>oracle</OPERATOR>
   3.111        <KEYWORD4>output</KEYWORD4>
   3.112 -      <KEYWORD4>outputs</KEYWORD4>
   3.113        <KEYWORD4>overloaded</KEYWORD4>
   3.114        <OPERATOR>overloading</OPERATOR>
   3.115        <OPERATOR>parse_ast_translation</OPERATOR>
   3.116        <OPERATOR>parse_translation</OPERATOR>
   3.117 -      <OPERATOR>pcpodef</OPERATOR>
   3.118        <KEYWORD4>permissive</KEYWORD4>
   3.119 -      <KEYWORD4>post</KEYWORD4>
   3.120        <LABEL>pr</LABEL>
   3.121 -      <KEYWORD4>pre</KEYWORD4>
   3.122        <KEYWORD1>prefer</KEYWORD1>
   3.123        <KEYWORD2>presume</KEYWORD2>
   3.124        <LABEL>pretty_setmargin</LABEL>
   3.125 @@ -252,7 +228,6 @@
   3.126        <LABEL>print_simpset</LABEL>
   3.127        <LABEL>print_statement</LABEL>
   3.128        <LABEL>print_syntax</LABEL>
   3.129 -      <LABEL>print_tcset</LABEL>
   3.130        <LABEL>print_theorems</LABEL>
   3.131        <LABEL>print_theory</LABEL>
   3.132        <LABEL>print_trans_rules</LABEL>
   3.133 @@ -269,24 +244,19 @@
   3.134        <OPERATOR>recdef</OPERATOR>
   3.135        <OPERATOR>recdef_tc</OPERATOR>
   3.136        <OPERATOR>record</OPERATOR>
   3.137 -      <KEYWORD4>recursor_eqns</KEYWORD4>
   3.138        <LABEL>refute</LABEL>
   3.139        <OPERATOR>refute_params</OPERATOR>
   3.140        <LABEL>remove_thy</LABEL>
   3.141 -      <KEYWORD4>rename</KEYWORD4>
   3.142        <OPERATOR>rep_datatype</OPERATOR>
   3.143 -      <KEYWORD4>restrict</KEYWORD4>
   3.144        <OPERATOR>sect</OPERATOR>
   3.145        <OPERATOR>section</OPERATOR>
   3.146        <OPERATOR>setup</OPERATOR>
   3.147        <KEYWORD2>show</KEYWORD2>
   3.148        <KEYWORD4>shows</KEYWORD4>
   3.149 -      <KEYWORD4>signature</KEYWORD4>
   3.150        <OPERATOR>simproc_setup</OPERATOR>
   3.151        <LABEL>sledgehammer</LABEL>
   3.152        <OPERATOR>sorry</OPERATOR>
   3.153        <OPERATOR>specification</OPERATOR>
   3.154 -      <KEYWORD4>states</KEYWORD4>
   3.155        <OPERATOR>statespace</OPERATOR>
   3.156        <KEYWORD4>structure</KEYWORD4>
   3.157        <OPERATOR>subclass</OPERATOR>
   3.158 @@ -308,16 +278,11 @@
   3.159        <LABEL>thm_deps</LABEL>
   3.160        <KEYWORD2>thus</KEYWORD2>
   3.161        <LABEL>thy_deps</LABEL>
   3.162 -      <KEYWORD4>to</KEYWORD4>
   3.163        <LABEL>touch_thy</LABEL>
   3.164 -      <KEYWORD4>transitions</KEYWORD4>
   3.165        <OPERATOR>translations</OPERATOR>
   3.166 -      <KEYWORD4>transrel</KEYWORD4>
   3.167        <OPERATOR>txt</OPERATOR>
   3.168        <OPERATOR>txt_raw</OPERATOR>
   3.169        <LABEL>typ</LABEL>
   3.170 -      <KEYWORD4>type_elims</KEYWORD4>
   3.171 -      <KEYWORD4>type_intros</KEYWORD4>
   3.172        <OPERATOR>typed_print_translation</OPERATOR>
   3.173        <OPERATOR>typedecl</OPERATOR>
   3.174        <OPERATOR>typedef</OPERATOR>

     4.1 --- a/src/HOL/Predicate.thy	Wed Apr 22 11:10:23 2009 +0200
     4.2 +++ b/src/HOL/Predicate.thy	Mon May 11 09:18:42 2009 +0200
     4.3 @@ -640,4 +640,12 @@
     4.4  hide (open) const Pred eval single bind if_pred not_pred
     4.5    Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
     4.6  
     4.7 +text {* dummy setup for code_pred keyword *}
     4.8 +
     4.9 +ML {*
    4.10 +OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
    4.11 +  OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]])))
    4.12 +*}
    4.13 +
    4.14 +
    4.15  end

     5.1 --- a/src/HOL/ex/Predicate_Compile.thy	Wed Apr 22 11:10:23 2009 +0200
     5.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Mon May 11 09:18:42 2009 +0200
     5.3 @@ -5,6 +5,11 @@
     5.4  
     5.5  setup {* Predicate_Compile.setup *}
     5.6  
     5.7 +ML {*
     5.8 +  OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
     5.9 +  OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd)
    5.10 +*}
    5.11 +
    5.12  primrec "next" :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
    5.13    \<Rightarrow> 'a Predicate.seq \<Rightarrow> ('a \<times> 'a Predicate.pred) option" where
    5.14      "next yield Predicate.Empty = None"
    5.15 @@ -34,4 +39,17 @@
    5.16  end
    5.17  *}
    5.18  
    5.19 +section {* Example for user interface *}
    5.20 +
    5.21 +inductive append ::  "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    5.22 +where
    5.23 +  "append [] ys ys"
    5.24 +| "append xs' ys zs' \<Longrightarrow> append (x#xs') ys (x#zs')"
    5.25 +
    5.26 +code_pred append
    5.27 +  using assms by (rule append.cases)
    5.28 +
    5.29 +thm append_cases
    5.30 +
    5.31 +
    5.32  end
    5.33 \ No newline at end of file

     6.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Apr 22 11:10:23 2009 +0200
     6.2 +++ b/src/HOL/ex/predicate_compile.ML	Mon May 11 09:18:42 2009 +0200
     6.3 @@ -14,8 +14,12 @@
     6.4    val code_ind_intros_attrib : attribute
     6.5    val code_ind_cases_attrib : attribute
     6.6    val setup : theory -> theory
     6.7 +  val code_pred : string -> Proof.context -> Proof.state
     6.8 +  val code_pred_cmd : string -> Proof.context -> Proof.state
     6.9    val print_alternative_rules : theory -> theory
    6.10    val do_proofs: bool ref
    6.11 +  val pred_intros : theory -> string -> thm list
    6.12 +  val get_nparams : theory -> string -> int
    6.13  end;
    6.14  
    6.15  structure Predicate_Compile: PREDICATE_COMPILE =
    6.16 @@ -1340,6 +1344,57 @@
    6.17    Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
    6.18      "adding alternative elimination rules for code generation of inductive predicates";
    6.19  
    6.20 +(* generation of case rules from user-given introduction rules *)
    6.21 +
    6.22 +   fun mk_casesrule introrules nparams ctxt = let
    6.23 +    val intros = map prop_of introrules
    6.24 +    val (pred, (params, args)) = strip_intro_concl (hd intros) nparams
    6.25 +    val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
    6.26 +    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
    6.27 +    val (argnames, ctxt2) = Variable.variant_fixes
    6.28 +      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
    6.29 +    val argvs = map Free (argnames ~~ (map fastype_of args))
    6.30 +    fun mk_case intro = let
    6.31 +        val (_, (_, args)) = strip_intro_concl intro nparams
    6.32 +        val prems = Logic.strip_imp_prems intro
    6.33 +        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
    6.34 +        val frees = (fold o fold_aterms)
    6.35 +          (fn t as Free _ =>
    6.36 +              if member (op aconv) params t then I else insert (op aconv) t
    6.37 +           | _ => I) (args @ prems) []
    6.38 +        in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
    6.39 +    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
    6.40 +    val cases = map mk_case intros
    6.41 +    val (_, ctxt3) = ProofContext.add_assms_i Assumption.assume_export
    6.42 +              [((Binding.name AutoBind.assmsN, []), map (fn t => (t, [])) (assm :: cases))]
    6.43 +              ctxt2
    6.44 +  in (pred, prop, ctxt3) end;
    6.45 +
    6.46 +(* setup for user interface *)
    6.47 +
    6.48 +  fun generic_code_pred prep_const raw_const lthy =
    6.49 +    let
    6.50 +      val thy = (ProofContext.theory_of lthy)
    6.51 +      val const = prep_const thy raw_const
    6.52 +      val nparams = get_nparams thy const
    6.53 +      val intro_rules = pred_intros thy const
    6.54 +      val (((tfrees, frees), fact), ctxt') =
    6.55 +        Variable.import_thms true intro_rules lthy;
    6.56 +      val (pred, prop, ctxt'') = mk_casesrule fact nparams ctxt'
    6.57 +      val (predname, _) = dest_Const pred
    6.58 +      fun after_qed [[th]] ctxt'' =
    6.59 +        LocalTheory.note Thm.theoremK
    6.60 +          ((Binding.name (Long_Name.base_name predname ^ "_cases"),
    6.61 +            [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) ctxt''
    6.62 +        |> snd
    6.63 +        |> ProofContext.theory (create_def_equation predname)
    6.64 +    in
    6.65 +      Proof.theorem_i NONE after_qed [[(prop, [])]] ctxt''
    6.66 +    end;
    6.67 +
    6.68 +  val code_pred = generic_code_pred (K I);
    6.69 +  val code_pred_cmd = generic_code_pred Code_Unit.read_const
    6.70 +
    6.71  end;
    6.72  
    6.73  fun pred_compile name thy = Predicate_Compile.create_def_equation