# HG changeset patch
# User bulwahn
# Date 1242026322 -7200
# Node ID 9a1178204dc0b9f7465cf29ae7ae2904f87cf366
# Parent  95f66b234086d32a18656b417ca592d32c5db19b
Added pred_code command

diff -r 95f66b234086 -r 9a1178204dc0 etc/isar-keywords-ZF.el
--- 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"
diff -r 95f66b234086 -r 9a1178204dc0 etc/isar-keywords.el
--- 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"
diff -r 95f66b234086 -r 9a1178204dc0 lib/jedit/isabelle.xml
--- 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>
diff -r 95f66b234086 -r 9a1178204dc0 src/HOL/Predicate.thy
--- 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
diff -r 95f66b234086 -r 9a1178204dc0 src/HOL/ex/Predicate_Compile.thy
--- 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
diff -r 95f66b234086 -r 9a1178204dc0 src/HOL/ex/predicate_compile.ML
--- 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