# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID bb8806eb5da7698bb896b7d7f9f5d9e7ec1e68a3 # Parent 2fef4f9429f79947870bd0f2c468d8050281e7f4 importing of polymorphic introduction rules with different schematic variable names diff -r 2fef4f9429f7 -r bb8806eb5da7 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 @@ -83,7 +83,7 @@ val intross4 = map (maps remove_pointless_clauses) intross3 val _ = print_intross options thy''' "After removing pointless clauses: " intross4 val intross5 = map (map (AxClass.overload thy''')) intross4 - val intross6 = burrow (map (expand_tuples thy''')) intross5 + val intross6 = map (map (expand_tuples thy''')) intross5 val _ = print_intross options thy''' "introduction rules before registering: " intross6 val _ = print_step options "Registering introduction rules..." val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' diff -r 2fef4f9429f7 -r bb8806eb5da7 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 @@ -256,7 +256,24 @@ (if null param_modes then "" else "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes)) -(* generation of case rules from user-given introduction rules *) +fun unify_consts thy cs intr_ts = + (let + val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I); + fun varify (t, (i, ts)) = + let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t)) + in (maxidx_of_term t', t'::ts) end; + val (i, cs') = foldr varify (~1, []) cs; + val (i', intr_ts') = foldr varify (i, []) intr_ts; + val rec_consts = fold add_term_consts_2 cs' []; + val intr_consts = fold add_term_consts_2 intr_ts' []; + fun unify (cname, cT) = + let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) + in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; + val (env, _) = fold unify rec_consts (Vartab.empty, i'); + val subst = map_types (Envir.norm_type env) + in (map subst cs', map subst intr_ts') + end) handle Type.TUNIFY => + (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); (* how to detect polymorphic type dependencies in mutual recursive inductive predicates? *) fun import_intros [] ctxt = ([], ctxt) @@ -289,9 +306,12 @@ (th' :: ths', ctxt1) end + +(* generation of case rules from user-given introduction rules *) + fun mk_casesrule ctxt nparams introrules = let - val ((_, intros_th), ctxt1) = Variable.import false introrules ctxt + val (intros_th, ctxt1) = import_intros introrules ctxt val intros = map prop_of intros_th val (pred, (params, args)) = strip_intro_concl nparams (hd intros) val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 @@ -2178,11 +2198,13 @@ fun prepare_intrs thy prednames intros = let - val ((_, intrs), _) = Variable.import false intros (ProofContext.init thy) - val intrs = map prop_of intrs + val intrs = map prop_of intros val nparams = nparams_of thy (hd prednames) + val preds = distinct (fn ((c1, _), (c2, _)) => c1 = c2) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs) + val (preds, intrs) = unify_consts thy (map Const preds) intrs + val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] (ProofContext.init thy) + val preds = map dest_Const preds val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) - val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs) val _ $ u = Logic.strip_imp_concl (hd intrs); val params = List.take (snd (strip_comb u), nparams); val param_vs = maps term_vs params diff -r 2fef4f9429f7 -r bb8806eb5da7 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 @@ -426,6 +426,8 @@ code_pred [inductify] replicate . code_pred [inductify] splice . code_pred [inductify] List.rev . +thm map.simps +code_pred [inductify, show_steps, show_intermediate_results] map . code_pred [inductify] foldr . code_pred [inductify] foldl . code_pred [inductify] filter .