--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Sep 27 12:01:04 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Sep 27 13:28:54 2010 +0200
@@ -102,7 +102,7 @@
{ensure_groundness = true,
limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
- (["accepts", "acceptsaux", "acceptsauxauxa", "acceptsauxaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
+ (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
replacing =
[(("repP", "limited_repP"), "lim_repIntPa"),
(("subP", "limited_subP"), "repIntP"),
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 27 12:01:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 27 13:28:54 2010 +0200
@@ -315,8 +315,9 @@
val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
in clause end
- val res = (map translate_intro intros', constant_table')
- in res end
+ in
+ (map translate_intro intros', constant_table')
+ end
fun depending_preds_of (key, intros) =
fold Term.add_const_names (map Thm.prop_of intros) []
@@ -669,7 +670,9 @@
|> (if #ensure_groundness options then
add_ground_predicates ctxt (#limited_types options)
else I)
+ |> tap (fn _ => tracing "Adding limited predicates...")
|> add_limited_predicates (#limited_predicates options)
+ |> tap (fn _ => tracing "Replacing predicates...")
|> apfst (fold replace (#replacing options))
|> apfst (reorder_manually (#manual_reorder options))
|> apfst rename_vars_program
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 27 12:01:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 27 13:28:54 2010 +0200
@@ -94,6 +94,56 @@
error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false
+fun try_destruct_case thy names atom =
+ case find_split_thm thy (fst (strip_comb atom)) of
+ NONE => NONE
+ | SOME raw_split_thm =>
+ let
+ val case_name = fst (dest_Const (fst (strip_comb atom)))
+ val split_thm = prepare_split_thm (ProofContext.init_global 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_global thy)*)
+ 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 case_name
+ val ths = maps (instantiated_case_rewrites thy) Tcons
+ val atom' = MetaSimplifier.rewrite_term thy
+ (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
+ val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
+ val names' = Term.add_free_names atom' names
+ fun mk_subst_rhs assm =
+ let
+ val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
+ val var_names = Name.variant_list names' (map fst vTs)
+ val vars = map Free (var_names ~~ (map snd vTs))
+ val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
+ fun partition_prem_subst prem =
+ case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
+ (Free (x, T), r) => (NONE, SOME ((x, T), r))
+ | _ => (SOME prem, NONE)
+ fun partition f xs =
+ let
+ fun partition' acc1 acc2 [] = (rev acc1, rev acc2)
+ | partition' acc1 acc2 (x :: xs) =
+ let
+ val (y, z) = f x
+ val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1
+ val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2
+ in partition' acc1' acc2' xs end
+ in partition' [] [] xs end
+ val (prems'', subst) = partition partition_prem_subst prems'
+ val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
+ val pre_rhs =
+ fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t
+ val rhs = Envir.expand_term_frees subst pre_rhs
+ in
+ case try_destruct_case thy (var_names @ names') rhs of
+ NONE => [(subst, rhs)]
+ | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs
+ end
+ in SOME (atom', maps mk_subst_rhs assms) end
+
fun flatten constname atom (defs, thy) =
if is_compound atom then
let
@@ -124,62 +174,20 @@
flatten constname atom' (defs, thy)
end
| _ =>
- case find_split_thm thy (fst (strip_comb atom)) of
+ case try_destruct_case thy [] 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_global 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_global thy)*)
- 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
- val atom = MetaSimplifier.rewrite_term thy
- (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
- val (f, args) = strip_comb atom
- val subst = Pattern.match thy (split_t, atom) (Vartab.empty, Vartab.empty)
- val (_, split_args) = strip_comb split_t
- val match = split_args ~~ args
- val names = Term.add_free_names atom []
- val frees = map Free (Term.add_frees atom [])
+ | SOME (atom', srs) =>
+ let
+ val frees = map Free (Term.add_frees atom' [])
val constname = Name.variant (map (Long_Name.base_name o fst) defs)
- ((Long_Name.base_name constname) ^ "_aux")
+ ((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
val constT = map fastype_of frees ---> HOLogic.boolT
val lhs = list_comb (Const (full_constname, constT), frees)
- fun new_def assm =
- let
- val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
- val var_names = Name.variant_list names (map fst vTs)
- val vars = map Free (var_names ~~ (map snd vTs))
- val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
- fun partition_prem_subst prem =
- case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
- (Free (x, T), r) => (NONE, SOME ((x, T), r))
- | _ => (SOME prem, NONE)
- fun partition f xs =
- let
- fun partition' acc1 acc2 [] = (rev acc1, rev acc2)
- | partition' acc1 acc2 (x :: xs) =
- let
- val (y, z) = f x
- val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1
- val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2
- in partition' acc1' acc2' xs end
- in partition' [] [] xs end
- val (prems'', subst) = partition partition_prem_subst prems'
- val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
- val pre_def = Logic.mk_equals (lhs,
- fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t)
- val def = Envir.expand_term_frees subst pre_def
- in
- def
- end
- val new_defs = map new_def assms
- val (definition, thy') = thy
+ fun mk_def (subst, rhs) =
+ Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
+ val new_defs = map mk_def srs
+ val (definition, thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
|> fold_map Specification.axiom (map_index
(fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)