src/HOL/ex/predicate_compile.ML

 signature PREDICATE_COMPILE =
 sig
   type mode = int list option list * int list
   val add_equations_of: string list -> theory -> theory
   val register_predicate : (thm list * thm * int) -> theory -> theory
+  val fetch_pred_data : theory -> string -> (thm list * thm * int)  
   val predfun_intro_of: theory -> string -> mode -> thm
   val predfun_elim_of: theory -> string -> mode -> thm
   val strip_intro_concl: int -> term -> term * (term list * term list)
   val predfun_name_of: theory -> string -> mode -> string
   val all_preds_of : theory -> string list
   val modes_of: theory -> string -> mode list
   val intros_of: theory -> string -> thm list
   val nparams_of: theory -> string -> int
+  val add_intro: thm -> theory -> theory
+  val set_elim: thm -> theory -> theory
   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 (*FIXME diagnostic command?*) *)
+  val print_stored_rules: theory -> unit
   val do_proofs: bool ref
+  val mk_casesrule : Proof.context -> int -> thm list -> term
   val analyze_compr: theory -> term -> term
   val eval_ref: (unit -> term Predicate.pred) option ref
   val add_equations : string -> theory -> theory
+  val code_pred_intros_attrib : attribute
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
 struct
 

 
 val predfun_intro_of = #intro ooo the_predfun_data
 
 val predfun_elim_of = #elim ooo the_predfun_data
 
-
-(* replaces print_alternative_rules *)
-(* TODO:
-fun print_alternative_rules thy = let
-    val d = IndCodegenData.get thy
-    val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
-    val _ = tracing ("preds: " ^ (makestring preds))
-    fun print pred = let
-      val _ = tracing ("predicate: " ^ pred)
-      val _ = tracing ("introrules: ")
-      val _ = fold (fn thm => fn u => tracing (makestring thm))
-        (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
-      val _ = tracing ("casesrule: ")
-      val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
-    in () end
-    val _ = map print preds
- in thy end;
-*)
-
+fun print_stored_rules thy =
+  let
+    val preds = (Graph.keys o PredData.get) thy
+    fun print pred () = let
+      val _ = writeln ("predicate: " ^ pred)
+      val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
+      val _ = writeln ("introrules: ")
+      val _ = fold (fn thm => fn u =>  writeln (Display.string_of_thm thm))
+        (rev (intros_of thy pred)) ()
+    in
+      if (has_elim thy pred) then
+        writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
+      else
+        writeln ("no elimrule defined")
+    end
+  in
+    fold print preds ()
+  end;
+
+(** preprocessing rules **)  
 
 fun imp_prems_conv cv ct =
   case Thm.term_of ct of
     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   | _ => Conv.all_conv ct

 
 fun add_predfun name mode data = let
     val add = apsnd (cons (mode, mk_predfun_data data))
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
+fun is_inductive_predicate thy name =
+  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
+
+fun depending_preds_of thy intros = fold Term.add_consts (map Thm.prop_of intros) [] |> map fst
+    |> filter (fn c => is_inductive_predicate thy c orelse is_pred thy c)
+
+(* code dependency graph *)    
+fun dependencies_of thy name =
+  let
+    val (intros, elim, nparams) = fetch_pred_data thy name 
+    val data = mk_pred_data ((intros, SOME elim, nparams), [])
+    val keys = depending_preds_of thy intros
+  in
+    (data, keys)
+  end;
+
+(* TODO: add_edges - by analysing dependencies *)
 fun add_intro thm thy = let
    val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
    fun cons_intro gr =
      case try (Graph.get_node gr) name of
        SOME pred_data => Graph.map_node name (map_pred_data

 
 fun set_nparams name nparams = let
     fun set (intros, elim, _ ) = (intros, elim, nparams) 
   in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
 
-fun register_predicate (intros, elim, nparams) = let
+fun register_predicate (intros, elim, nparams) thy = let
     val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros))))
     fun set _ = (intros, SOME elim, nparams)
-  in PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))) end
+  in
+    PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))
+      #> fold Graph.add_edge (map (pair name) (depending_preds_of thy intros))) thy
+  end
 
   
 (* Mode analysis *)
 
 (*** check if a term contains only constructor functions ***)

        THEN print_tac "after prove_match2:"
        THEN rest_tac
     end;
   val prems_tac = prove_prems2 in_ts' param_vs ps 
 in
-  print_tac "starting prove_clause2"
+  new_print_tac "starting prove_clause2"
   THEN etac @{thm bindE} 1
   THEN (etac @{thm singleE'} 1)
   THEN (TRY (etac @{thm Pair_inject} 1))
   THEN print_tac "after singleE':"
   THEN prems_tac

     THEN (prove_clause2 thy all_vs param_vs modes mode clause pred i)
 in
   (DETERM (TRY (rtac @{thm unit.induct} 1)))
    THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
    THEN (rtac (predfun_intro_of thy pred mode) 1)
+   THEN (REPEAT_DETERM (rtac @{thm refl} 2))
    THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses)))))
 end;
 
 fun prove_pred thy all_vs param_vs modes clauses (((pred, T), mode), t) = let
   val ctxt = ProofContext.init thy

         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
   in Logic.list_implies (assm :: cases, prop) end;
 
-(* code dependency graph *)
-
-fun dependencies_of thy name =
-  let
-    fun is_inductive_predicate thy name =
-      is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
-    val (intro, elim, nparams) = fetch_pred_data thy name 
-    val data = mk_pred_data ((intro, SOME elim, nparams), [])
-    val intros = map Thm.prop_of (#intros (rep_pred_data data))
-    val keys = fold Term.add_consts intros [] |> map fst
-    |> filter (is_inductive_predicate thy)
-  in
-    (data, keys)
-  end;
-
 fun add_equations name thy =
   let
     val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy |> Theory.checkpoint;
     (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *)
     fun strong_conn_of gr keys =

       (fn preds => fn thy =>
         if forall (null o modes_of thy) preds then add_equations_of preds thy else thy)
       scc thy' |> Theory.checkpoint
   in thy'' end
 
+  
+fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+
+val code_pred_intros_attrib = attrib add_intro;
+
 (** user interface **)
 
 local
-
-fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-
-(*
-val add_elim_attrib = attrib set_elim;
-*)
-
 
 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
 (* TODO: must create state to prove multiple cases *)
 fun generic_code_pred prep_const raw_const lthy =
   let