# HG changeset patch
# User haftmann
# Date 1242064483 -7200
# Node ID ef8210e58ad72ec7b976864edddb0520be16c9a0
# Parent  ac8a12b0ed3cdc03655c06d7db77ab4f9bde3c64# Parent  54092b86ef8190bfe0cd9166a20eb392bae442df
merged

diff -r ac8a12b0ed3c -r ef8210e58ad7 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon May 11 19:51:21 2009 +0200
+++ b/etc/isar-keywords-ZF.el	Mon May 11 19:54:43 2009 +0200
@@ -18,7 +18,6 @@
     "ML"
     "ML_command"
     "ML_prf"
-    "ML_test"
     "ML_val"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
@@ -349,7 +348,6 @@
 
 (defconst isar-keywords-theory-decl
   '("ML"
-    "ML_test"
     "abbreviation"
     "arities"
     "attribute_setup"
diff -r ac8a12b0ed3c -r ef8210e58ad7 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon May 11 19:51:21 2009 +0200
+++ b/etc/isar-keywords.el	Mon May 11 19:54:43 2009 +0200
@@ -18,7 +18,6 @@
     "ML"
     "ML_command"
     "ML_prf"
-    "ML_test"
     "ML_val"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
@@ -64,6 +63,7 @@
     "code_module"
     "code_modulename"
     "code_monad"
+    "code_pred"
     "code_reserved"
     "code_thms"
     "code_type"
@@ -421,7 +421,6 @@
 
 (defconst isar-keywords-theory-decl
   '("ML"
-    "ML_test"
     "abbreviation"
     "arities"
     "atom_decl"
@@ -515,6 +514,7 @@
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
+    "code_pred"
     "corollary"
     "cpodef"
     "function"
diff -r ac8a12b0ed3c -r ef8210e58ad7 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Mon May 11 19:51:21 2009 +0200
+++ b/lib/jedit/isabelle.xml	Mon May 11 19:54:43 2009 +0200
@@ -45,7 +45,6 @@
       <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>
@@ -95,6 +94,7 @@
       <OPERATOR>code_module</OPERATOR>
       <OPERATOR>code_modulename</OPERATOR>
       <OPERATOR>code_monad</OPERATOR>
+      <OPERATOR>code_pred</OPERATOR>
       <OPERATOR>code_reserved</OPERATOR>
       <LABEL>code_thms</LABEL>
       <OPERATOR>code_type</OPERATOR>
diff -r ac8a12b0ed3c -r ef8210e58ad7 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon May 11 19:51:21 2009 +0200
+++ b/src/HOL/Predicate.thy	Mon May 11 19:54:43 2009 +0200
@@ -622,7 +622,10 @@
   "pred_rec f P = f (eval P)"
   by (cases P) simp
 
-text {* for evaluation of predicate enumerations *}
+inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
+
+lemma eq_is_eq: "eq x y \<equiv> (x = y)"
+  by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
 
 ML {*
 signature PREDICATE =
@@ -666,6 +669,12 @@
 code_const Seq and Empty and Insert and Join
   (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
 
+text {* dummy setup for @{text 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) [[]])))
+*}
 
 no_notation
   inf (infixl "\<sqinter>" 70) and
@@ -678,6 +687,6 @@
 
 hide (open) type pred seq
 hide (open) const Pred eval single bind if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
 
 end
diff -r ac8a12b0ed3c -r ef8210e58ad7 src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Mon May 11 19:51:21 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Mon May 11 19:54:43 2009 +0200
@@ -7,6 +7,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)
+*}
+
 
 text {* Experimental code *}
 
@@ -83,4 +88,18 @@
 
 ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *}
 
+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_codegen
+thm append_cases
+
+
 end
\ No newline at end of file
diff -r ac8a12b0ed3c -r ef8210e58ad7 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon May 11 19:51:21 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Mon May 11 19:54:43 2009 +0200
@@ -18,7 +18,12 @@
   val modename_of: theory -> string -> mode -> string
   val modes_of: theory -> string -> mode list
   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 =
@@ -739,15 +744,15 @@
     Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
   | _ => error "Trueprop_conv"
 
-fun preprocess_intro thy rule = Thm.transfer thy rule (*FIXME preprocessor
+fun preprocess_intro thy rule =
   Conv.fconv_rule
     (imp_prems_conv
-      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @ {thm Predicate.eq_is_eq})))))
-    (Thm.transfer thy rule) *)
+      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
+    (Thm.transfer thy rule)
 
-fun preprocess_elim thy nargs elimrule = (*FIXME preprocessor -- let
+fun preprocess_elim thy nargs elimrule = let
    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
-      HOLogic.mk_Trueprop (Const (@ {const_name Predicate.eq}, T) $ lhs $ rhs)
+      HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
     | replace_eqs t = t
    fun preprocess_case t = let
      val params = Logic.strip_params t
@@ -759,10 +764,10 @@
    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
  in
    Thm.equal_elim
-     (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@ {thm eq_is_eq}])
+     (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
         (cterm_of thy elimrule')))
      elimrule
- end*) elimrule;
+ end;
 
 
 (* returns true if t is an application of an datatype constructor *)
@@ -1354,6 +1359,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), lthy') =
+        Variable.import_thms true intro_rules lthy;
+      val (pred, prop, lthy'') = mk_casesrule fact nparams lthy'
+      val (predname, _) = dest_Const pred
+      fun after_qed [[th]] lthy'' =
+        LocalTheory.note Thm.theoremK
+          ((Binding.name (Long_Name.base_name predname ^ "_cases"), (* FIXME: other suffix *)
+            [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) lthy''
+        |> snd
+        |> LocalTheory.theory (create_def_equation predname)
+    in
+      Proof.theorem_i NONE after_qed [[(prop, [])]] lthy''
+    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