# HG changeset patch
# User bulwahn
# Date 1284967580 -7200
# Node ID 631cf48c78940581a00d0d75573016181bc1fbdc
# Parent  3a07bbc264b27bd8733ef91d6b7dc6ff4fb3f2d6
code_pred_intro can be used to name facts for the code_pred command

diff -r 3a07bbc264b2 -r 631cf48c7894 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Mon Sep 20 09:26:19 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Mon Sep 20 09:26:20 2010 +0200
@@ -216,6 +216,37 @@
   qed
 qed
 
+subsection {* Named alternative rules *}
+
+inductive appending
+where
+  nil: "appending [] ys ys"
+| cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
+
+lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
+by (auto intro: appending.intros)
+
+lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
+by (auto intro: appending.intros)
+
+text {* With code_pred_intro, we can give fact names to the alternative rules,
+  which are used for the code_pred command. *}
+
+declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
+ 
+code_pred appending
+proof -
+  case appending
+  from prems show thesis
+  proof(cases)
+    case nil
+    from alt_nil nil show thesis by auto
+  next
+    case cons
+    from alt_cons cons show thesis by fastsimp
+  qed
+qed
+
 subsection {* Preprocessor Inlining  *}
 
 definition "equals == (op =)"
diff -r 3a07bbc264b2 -r 631cf48c7894 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 20 09:26:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 20 09:26:20 2010 +0200
@@ -28,7 +28,7 @@
   val all_random_modes_of : Proof.context -> (string * mode list) list
   val intros_of : Proof.context -> string -> thm list
   val intros_graph_of : Proof.context -> thm list Graph.T
-  val add_intro : thm -> theory -> theory
+  val add_intro : string option * thm -> theory -> theory
   val set_elim : thm -> theory -> theory
   val register_alternative_function : string -> mode -> string -> theory -> theory
   val alternative_compilation_of_global : theory -> string -> mode ->
@@ -216,7 +216,7 @@
   PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
 
 datatype pred_data = PredData of {
-  intros : thm list,
+  intros : (string option * thm) list,
   elim : thm option,
   function_names : (compilation * (mode * string) list) list,
   predfun_data : (mode * predfun_data) list,
@@ -237,7 +237,7 @@
   | eq_option eq _ = false
 
 fun eq_pred_data (PredData d1, PredData d2) = 
-  eq_list Thm.eq_thm (#intros d1, #intros d2) andalso
+  eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
   eq_option Thm.eq_thm (#elim d1, #elim d2)
 
 structure PredData = Theory_Data
@@ -261,7 +261,9 @@
 
 val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
 
-val intros_of = #intros oo the_pred_data
+val intros_of = map snd o #intros oo the_pred_data
+
+val names_of = map fst o #intros oo the_pred_data
 
 fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
  of NONE => error ("No elimination rule for predicate " ^ quote name)
@@ -316,7 +318,7 @@
 val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
 
 val intros_graph_of =
-  Graph.map (K (#intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
+  Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
 
 (* diagnostic display functions *)
 
@@ -654,7 +656,7 @@
         val elim =
           prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
       in
-        mk_pred_data ((intros, SOME elim), no_compilation)
+        mk_pred_data ((map (pair NONE) intros, SOME elim), no_compilation)
       end
   | NONE => error ("No such predicate: " ^ quote name)
 
@@ -668,21 +670,21 @@
 
 fun depending_preds_of ctxt (key, value) =
   let
-    val intros = (#intros o rep_pred_data) value
+    val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
   in
-    fold Term.add_const_names (map Thm.prop_of intros) []
+    fold Term.add_const_names intros []
       |> filter (fn c => (not (c = key)) andalso
         (is_inductive_predicate ctxt c orelse is_registered ctxt c))
   end;
 
-fun add_intro thm thy =
+fun add_intro (opt_case_name, thm) thy =
   let
     val (name, T) = dest_Const (fst (strip_intro_concl thm))
     fun cons_intro gr =
      case try (Graph.get_node gr) name of
        SOME pred_data => Graph.map_node name (map_pred_data
-         (apfst (fn (intros, elim) => (intros @ [thm], elim)))) gr
-     | NONE => Graph.new_node (name, mk_pred_data (([thm], NONE), no_compilation)) gr
+         (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))) gr
+     | NONE => Graph.new_node (name, mk_pred_data (([(opt_case_name, thm)], NONE), no_compilation)) gr
   in PredData.map cons_intro thy end
 
 fun set_elim thm =
@@ -694,7 +696,7 @@
 
 fun register_predicate (constname, pre_intros, pre_elim) thy =
   let
-    val intros = map (preprocess_intro thy) pre_intros
+    val intros = map (pair NONE o preprocess_intro thy) pre_intros
     val elim = preprocess_elim (ProofContext.init_global thy) pre_elim
   in
     if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
@@ -3042,9 +3044,10 @@
 
 (* code_pred_intro attribute *)
 
-fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+fun attrib' f opt_case_name =
+  Thm.declaration_attribute (fn thm => Context.mapping (f (opt_case_name, thm)) I);
 
-val code_pred_intro_attrib = attrib add_intro;
+val code_pred_intro_attrib = attrib' add_intro NONE;
 
 
 (*FIXME
@@ -3052,7 +3055,7 @@
 *)
 
 val setup = PredData.put (Graph.empty) #>
-  Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro))
+  Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
     "adding alternative introduction rules for code generation of inductive predicates"
 
 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
@@ -3075,12 +3078,14 @@
       in mk_casesrule lthy' pred intros end  
     val cases_rules = map mk_cases preds
     val cases =
-      map (fn case_rule => Rule_Cases.Case {fixes = [],
-        assumes = [("", Logic.strip_imp_prems case_rule)],
-        binds = [], cases = []}) cases_rules
+      map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
+        assumes = ("", Logic.strip_imp_prems case_rule)
+          :: (map_filter (fn (fact_name, fact) => Option.map (rpair [fact]) fact_name)
+            ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule)),
+        binds = [], cases = []}) preds cases_rules
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     val lthy'' = lthy'
-      |> fold Variable.auto_fixes cases_rules 
+      |> fold Variable.auto_fixes cases_rules
       |> ProofContext.add_cases true case_env
     fun after_qed thms goal_ctxt =
       let