--- 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)
--- 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
--- 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