src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 36029 a790b94e090c
parent 36022 c0fa8499e366
child 36032 dfd30b5b4e73
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:48 2010 +0200
     1.3 @@ -400,52 +400,13 @@
     1.4  
     1.5  (* split theorems of case expressions *)
     1.6  
     1.7 -(*
     1.8 -fun has_split_rule_cname @{const_name "nat_case"} = true
     1.9 -  | has_split_rule_cname @{const_name "list_case"} = true
    1.10 -  | has_split_rule_cname _ = false
    1.11 -  
    1.12 -fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true 
    1.13 -  | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true 
    1.14 -  | has_split_rule_term thy _ = false
    1.15 -
    1.16 -fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
    1.17 -  | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
    1.18 -  | has_split_rule_term' thy c = has_split_rule_term thy c
    1.19 -
    1.20 -*)
    1.21  fun prepare_split_thm ctxt split_thm =
    1.22      (split_thm RS @{thm iffD2})
    1.23      |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
    1.24        @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
    1.25  
    1.26 -fun find_split_thm thy (Const (name, typ)) =
    1.27 -  let
    1.28 -    fun split_name str =
    1.29 -      case first_field "." str
    1.30 -        of (SOME (field, rest)) => field :: split_name rest
    1.31 -         | NONE => [str]
    1.32 -    val splitted_name = split_name name
    1.33 -  in
    1.34 -    if length splitted_name > 0 andalso
    1.35 -       String.isSuffix "_case" (List.last splitted_name)
    1.36 -    then
    1.37 -      (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
    1.38 -      |> space_implode "."
    1.39 -      |> PureThy.get_thm thy
    1.40 -      |> SOME
    1.41 -      handle ERROR msg => NONE
    1.42 -    else NONE
    1.43 -  end
    1.44 -  | find_split_thm _ _ = NONE
    1.45 -
    1.46 -
    1.47 -(* TODO: split rules for let and if are different *)
    1.48 -fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
    1.49 -  | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
    1.50 -  | find_split_thm' thy c = find_split_thm thy c
    1.51 -
    1.52 -fun has_split_thm thy t = is_some (find_split_thm thy t)
    1.53 +fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
    1.54 +  | find_split_thm thy _ = NONE
    1.55  
    1.56  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
    1.57