# HG changeset patch
# User bulwahn
# Date 1269876648 -7200
# Node ID a790b94e090c225a699e593ab212b1c6aa78ff11
# Parent  3837493fe4ab724ae4cd5198dede052c56682885
removing fishing for split thm in the predicate compiler

diff -r 3837493fe4ab -r a790b94e090c src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:46 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:48 2010 +0200
@@ -400,52 +400,13 @@
 
 (* split theorems of case expressions *)
 
-(*
-fun has_split_rule_cname @{const_name "nat_case"} = true
-  | has_split_rule_cname @{const_name "list_case"} = true
-  | has_split_rule_cname _ = false
-  
-fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true 
-  | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true 
-  | has_split_rule_term thy _ = false
-
-fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
-  | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
-  | has_split_rule_term' thy c = has_split_rule_term thy c
-
-*)
 fun prepare_split_thm ctxt split_thm =
     (split_thm RS @{thm iffD2})
     |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
       @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
 
-fun find_split_thm thy (Const (name, typ)) =
-  let
-    fun split_name str =
-      case first_field "." str
-        of (SOME (field, rest)) => field :: split_name rest
-         | NONE => [str]
-    val splitted_name = split_name name
-  in
-    if length splitted_name > 0 andalso
-       String.isSuffix "_case" (List.last splitted_name)
-    then
-      (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
-      |> space_implode "."
-      |> PureThy.get_thm thy
-      |> SOME
-      handle ERROR msg => NONE
-    else NONE
-  end
-  | find_split_thm _ _ = NONE
-
-
-(* TODO: split rules for let and if are different *)
-fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
-  | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
-  | find_split_thm' thy c = find_split_thm thy c
-
-fun has_split_thm thy t = is_some (find_split_thm thy t)
+fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
+  | find_split_thm thy _ = NONE
 
 fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
 
diff -r 3837493fe4ab -r a790b94e090c src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 29 17:30:46 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 29 17:30:48 2010 +0200
@@ -202,11 +202,12 @@
               HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
             end)
         | _ =>
-        if has_split_thm thy (fst (strip_comb t)) then
+        case find_split_thm thy (fst (strip_comb t)) of
+          SOME raw_split_thm =>
           let
             val (f, args) = strip_comb t
-            val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
-            val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+            val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
+            val (assms, concl) = Logic.strip_horn (prop_of split_thm)
             val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
             val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
             val (_, split_args) = strip_comb split_t
@@ -231,7 +232,7 @@
           in
             maps flatten_of_assm assms
           end
-        else
+      | NONE =>
           let
             val (f, args) = strip_comb t
             val args = map (Pattern.eta_long []) args
diff -r 3837493fe4ab -r a790b94e090c src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Mar 29 17:30:46 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Mar 29 17:30:48 2010 +0200
@@ -113,7 +113,7 @@
       (lhs, ((full_constname, [definition]) :: defs, thy'))
     end
   else
-    (case (fst (strip_comb atom)) of
+    case (fst (strip_comb atom)) of
       (Const (@{const_name If}, _)) => let
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
           val atom' = MetaSimplifier.rewrite_term thy
@@ -122,14 +122,16 @@
         in
           flatten constname atom' (defs, thy)
         end
-    | _ =>  
-      if (has_split_thm thy (fst (strip_comb atom))) then
+    | _ =>
+      case find_split_thm thy (fst (strip_comb atom)) of
+        NONE => (atom, (defs, thy))
+      | SOME raw_split_thm =>
         let
           val (f, args) = strip_comb atom
-          val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
+          val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
           (* TODO: contextify things - this line is to unvarify the split_thm *)
           (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
-          val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+          val (assms, concl) = Logic.strip_horn (prop_of split_thm)
           val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
           val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
           val ths = maps (instantiated_case_rewrites thy) Tcons
@@ -182,8 +184,7 @@
         in
           (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
         end
-      else
-        (atom, (defs, thy)))
+
 
 fun flatten_intros constname intros thy =
   let