# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 0f6e30b87cf19c0fd424e9ff50736dcf48dcc181 # Parent 6672184a736bdc645f3799015ddcb9f491cdcf6f processing of tuples in introduction rules diff -r 6672184a736b -r 0f6e30b87cf1 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ROOT.ML Sat Oct 24 16:55:42 2009 +0200 @@ -1,5 +1,6 @@ (* Classical Higher-order Logic -- batteries included *) +Toplevel.debug := true; use_thy "Complex_Main"; val HOL_proofs = ! Proofterm.proofs; diff -r 6672184a736b -r 0f6e30b87cf1 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200 @@ -73,8 +73,15 @@ (* fun map_atoms f intro = -fun fold_atoms f intro = *) +fun fold_atoms f intro s = + let + val (literals, head) = Logic.strip_horn intro + fun appl t s = (case t of + (@{term "Not"} $ t') => f t' s + | _ => f t s) + in fold appl (map HOLogic.dest_Trueprop literals) s end + fun fold_map_atoms f intro s = let val (literals, head) = Logic.strip_horn intro diff -r 6672184a736b -r 0f6e30b87cf1 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 @@ -17,7 +17,73 @@ val priority = tracing; +(* tuple processing *) + +fun expand_tuples thy intro = + let + fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) + | rewrite_args (arg::args) (pats, intro_t, ctxt) = + (case HOLogic.strip_tupleT (fastype_of arg) of + (Ts as _ :: _ :: _) => + let + fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) + (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) + | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = + let + val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt + val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) + (*val _ = tracing ("Rewriting term " ^ + (Syntax.string_of_term_global thy (fst pat)) ^ " to " ^ + (Syntax.string_of_term_global thy (snd pat)) ^ " in " ^ + (Syntax.string_of_term_global thy intro_t))*) + val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t + val args' = map (Pattern.rewrite_term thy [pat] []) args + in + rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) + end + | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) + val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) + (args, (pats, intro_t, ctxt)) + in + rewrite_args args' (pats, intro_t', ctxt') + end + | _ => rewrite_args args (pats, intro_t, ctxt)) + fun rewrite_prem atom = + let + val (_, args) = strip_comb atom + in rewrite_args args end + val ctxt = ProofContext.init thy + val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt + val intro_t = prop_of intro' + val concl = Logic.strip_imp_concl intro_t + val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) + val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) + val (pats', intro_t', ctxt3) = + fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) + (*val _ = Output.tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t')) + val _ = Output.tracing ("pats : " ^ (commas (map + (fn (t1, t2) => (Syntax.string_of_term_global thy t1) ^ " -> " ^ + Syntax.string_of_term_global thy t2) pats'))*) + fun rewrite_pat (ct1, ct2) = + (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) + val t_insts' = map rewrite_pat t_insts + (*val _ = Output.tracing ("t_insts':" ^ (commas (map + (fn (ct1, ct2) => (Syntax.string_of_term_global thy (term_of ct1) ^ " -> " ^ + Syntax.string_of_term_global thy (term_of ct2))) t_insts')))*) + val intro'' = Thm.instantiate (T_insts, t_insts') intro + (*val _ = Output.tracing ("intro'':" ^ (Display.string_of_thm_global thy intro''))*) + val [intro'''] = Variable.export ctxt3 ctxt [intro''] + (*val _ = Output.tracing ("intro''':" ^ (Display.string_of_thm_global thy intro'''))*) + in + intro''' + end + + (* eliminating fst/snd functions *) +val simplify_fst_snd = Simplifier.full_simplify + (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) + (* Some last processing *) + fun remove_pointless_clauses intro = if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then [] @@ -35,24 +101,25 @@ thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates (get_specs funnames) val _ = priority "Compiling predicates to flat introrules..." - val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess + val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess (get_specs prednames) thy') val _ = tracing ("Flattened introduction rules: " ^ - commas (map (Display.string_of_thm_global thy'') (flat intross))) + commas (map (Display.string_of_thm_global thy'') (flat intross1))) val _ = priority "Replacing functions in introrules..." (* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *) - val intross' = + val intross2 = if fail_safe_mode then - case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of - SOME intross' => intross' - | NONE => let val _ = warning "Function replacement failed!" in intross end - else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross + case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of + SOME intross => intross + | NONE => let val _ = warning "Function replacement failed!" in intross1 end + else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 val _ = tracing ("Introduction rules with replaced functions: " ^ - commas (map (Display.string_of_thm_global thy'') (flat intross'))) - val intross'' = burrow (maps remove_pointless_clauses) intross' - val intross'' = burrow (map (AxClass.overload thy'')) intross'' + commas (map (Display.string_of_thm_global thy'') (flat intross2))) + val intross3 = burrow (maps remove_pointless_clauses) intross2 + val intross4 = burrow (map (AxClass.overload thy'')) intross3 + val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4 val _ = priority "Registering intro rules..." - val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy'' + val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy'' in thy''' end; diff -r 6672184a736b -r 0f6e30b87cf1 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 @@ -108,6 +108,7 @@ val is_predT : typ -> bool val guess_nparams : typ -> int val cprods_subset : 'a list list -> 'a list list + val dest_prem : theory -> term list -> term -> indprem end; structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE = @@ -527,7 +528,7 @@ val bigeq = (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}]) (cterm_of thy elimrule'))) - val tac = (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy) + val tac = (fn _ => setmp quick_and_dirty true (SkipProof.cheat_tac thy)) val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac val _ = Output.tracing "Preprocessed elimination rule" in @@ -2205,54 +2206,7 @@ forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems end -fun expand_tuples thy intro = - let - fun rewrite_args [] (intro_t, names) = (intro_t, names) - | rewrite_args (arg::args) (intro_t, names) = - (case HOLogic.strip_tupleT (fastype_of arg) of - (Ts as _ :: _ :: _) => - let - fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) - (args, (intro_t, names)) = rewrite_arg' (t2, T2) (args, (intro_t, names)) - | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (intro_t, names)) = - let - val [x, y] = Name.variant_list names ["x", "y"] - val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) - val _ = tracing ("Rewriting term " ^ - (Syntax.string_of_term_global thy (fst pat)) ^ " to " ^ - (Syntax.string_of_term_global thy (snd pat)) ^ " in " ^ - (Syntax.string_of_term_global thy intro_t)) - val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t - val args' = map (Pattern.rewrite_term thy [pat] []) args - in - rewrite_arg' (Free (y, T2), T2) (args', (intro_t', x::y::names)) - end - | rewrite_arg' _ (args, (intro_t, names)) = (args, (intro_t, names)) - val (args', (intro_t', names')) = rewrite_arg' (arg, fastype_of arg) - (args, (intro_t, names)) - in - rewrite_args args' (intro_t', names') - end - | _ => rewrite_args args (intro_t, names)) - fun rewrite_prem (Prem (args, _)) = rewrite_args args - | rewrite_prem (Negprem (args, _)) = rewrite_args args - | rewrite_prem _ = I - val intro_t = Logic.unvarify (prop_of intro) - val frees = Term.add_free_names intro_t [] - val concl = Logic.strip_imp_concl intro_t - val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) - val params = List.take (args, nparams_of thy (fst (dest_Const p))) - val (intro_t', frees') = rewrite_args args (intro_t, frees) - val (intro_t', _) = - fold (rewrite_prem o dest_prem thy params o HOLogic.dest_Trueprop) - (Logic.strip_imp_prems intro_t') (intro_t', frees') - val _ = tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t')) - val tac = - (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy) - in - Goal.prove (ProofContext.init thy) (Term.add_free_names intro_t' []) [] - intro_t' tac - end + (** main function of predicate compiler **) @@ -2260,10 +2214,9 @@ let val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) - val intros' = map (expand_tuples thy) (maps (intros_of thy) prednames) - val _ = map (check_format_of_intro_rule thy) intros' + val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = - prepare_intrs thy prednames intros' + prepare_intrs thy prednames (maps (intros_of thy) prednames) val _ = Output.tracing "Infering modes..." val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses diff -r 6672184a736b -r 0f6e30b87cf1 src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Sat Oct 24 16:55:42 2009 +0200 @@ -25,7 +25,7 @@ "set xs x ==> set (x' # xs) x" unfolding mem_def[symmetric, of _ x] by auto - +(* code_pred set proof - case set @@ -38,6 +38,7 @@ apply auto done qed +*) section {* Alternative rules for list_all2 *} @@ -47,6 +48,7 @@ lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" by auto +(* code_pred list_all2 proof - case list_all2 @@ -59,5 +61,5 @@ apply auto done qed - +*) end \ No newline at end of file diff -r 6672184a736b -r 0f6e30b87cf1 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 @@ -55,7 +55,7 @@ | "[| ys = fst (xa, y); x # zs = snd (xa, y); tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)" -code_pred tupled_append' . +code_pred (inductify_all) tupled_append' . thm tupled_append'.equation (* TODO: Missing a few modes! *) @@ -64,7 +64,9 @@ "tupled_append'' ([], xs, xs)" | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, x # zs) \ tupled_append'' (x # xs, yszs)" -code_pred tupled_append'' . +thm tupled_append''.cases + +code_pred (inductify_all) tupled_append'' . thm tupled_append''.equation (* TODO: Missing a few modes *) @@ -73,10 +75,19 @@ "tupled_append''' ([], xs, xs)" | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" -code_pred tupled_append''' . +code_pred (inductify_all) tupled_append''' . thm tupled_append'''.equation (* TODO: Missing a few modes *) +thm fst_conv snd_conv +thm map_of.simps +term "map_of" +inductive map_ofP :: "('a \ 'b) list \ 'a \ 'b \ bool" +where + "map_ofP ((a, b)#xs) a b" +| "map_ofP xs a b \ map_ofP (x#xs) a b" +code_pred map_ofP . +thm map_ofP.equation section {* reverse *} inductive rev where @@ -420,13 +431,13 @@ "length [x \ w. x = a] = length [x \ w. x = b] ==> test w" ML {* @{term "[x \ w. x = a]"} *} code_pred (inductify_all) test . - +(* theorem S\<^isub>3_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3" (*quickcheck[generator=SML]*) quickcheck[generator=pred_compile, size=10, iterations=100] oops - +*) inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where "[] \ S\<^isub>4" | "w \ A\<^isub>4 \ b # w \ S\<^isub>4"