# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 6672184a736bdc645f3799015ddcb9f491cdcf6f # Parent db5af7b86a2fcaa0a78b3f363f13eab084388298 added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions diff -r db5af7b86a2f -r 6672184a736b src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200 @@ -209,9 +209,11 @@ let fun is_nondefining_constname c = member (op =) logic_operator_names c val is_defining_constname = member (op =) (Symtab.keys table) + fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c) fun defiants_of specs = fold (Term.add_const_names o prop_of) specs [] |> filter is_defining_constname + |> filter_out has_code_pred_intros |> filter_out (case_consts thy) |> filter_out special_cases fun extend constname = diff -r db5af7b86a2f -r 6672184a736b src/HOL/Tools/Predicate_Compile/pred_compile_set.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Sat Oct 24 16:55:42 2009 +0200 @@ -15,7 +15,7 @@ structure Pred_Compile_Set : PRED_COMPILE_SET = struct (*FIXME: unfolding Ball in pretty adhoc here *) -val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}] +val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}, @{thm Bex_def}] val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas diff -r db5af7b86a2f -r 6672184a736b 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 @@ -993,7 +993,7 @@ (modes_of_term modes t handle Option => error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) | Negprem (us, t) => find_first (fn Mode (_, is, _) => - length us = length is andalso + is = map (rpair NONE) (1 upto length us) andalso terms_vs us subset vs andalso term_vs t subset vs) (modes_of_term modes t handle Option => @@ -2135,8 +2135,8 @@ fun prepare_intrs thy prednames intros = let - val intrs = intros - |> map (Logic.unvarify o prop_of) + val ((_, intrs), _) = Variable.import false intros (ProofContext.init thy) + val intrs = map prop_of intrs val nparams = nparams_of thy (hd prednames) 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) diff -r db5af7b86a2f -r 6672184a736b 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 @@ -14,4 +14,50 @@ setup {* Predicate_Compile.setup *} setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *} +section {* Alternative rules for set *} + +lemma set_ConsI1 [code_pred_intros]: + "set (x # xs) x" +unfolding mem_def[symmetric, of _ x] +by auto + +lemma set_ConsI2 [code_pred_intros]: + "set xs x ==> set (x' # xs) x" +unfolding mem_def[symmetric, of _ x] +by auto + +code_pred set +proof - + case set + from this show thesis + apply (case_tac a1) + apply auto + unfolding mem_def[symmetric, of _ a2] + apply auto + unfolding mem_def + apply auto + done +qed + +section {* Alternative rules for list_all2 *} + +lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []" +by auto + +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 + from this show thesis + apply - + apply (case_tac a1) + apply (case_tac a2) + apply auto + apply (case_tac a2) + apply auto + done +qed + end \ No newline at end of file diff -r db5af7b86a2f -r 6672184a736b 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 @@ -34,6 +34,8 @@ value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (append_3 ([]::int list))" +subsection {* Tricky cases with tuples *} + inductive tupled_append :: "'a list \ 'a list \ 'a list \ bool" where "tupled_append ([], xs, xs)" @@ -43,8 +45,40 @@ thm tupled_append.equation (* +TODO: values with tupled modes values "{xs. tupled_append ([1,2,3], [4,5], xs)}" *) + +inductive tupled_append' +where +"tupled_append' ([], xs, xs)" +| "[| 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' . +thm tupled_append'.equation +(* TODO: Missing a few modes! *) + +inductive tupled_append'' :: "'a list \ 'a list \ 'a list \ bool" +where + "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''.equation +(* TODO: Missing a few modes *) + +inductive tupled_append''' :: "'a list \ 'a list \ 'a list \ bool" +where + "tupled_append''' ([], xs, xs)" +| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" + +code_pred tupled_append''' . +thm tupled_append'''.equation +(* TODO: Missing a few modes *) + +section {* reverse *} + inductive rev where "rev [] []" | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" @@ -142,6 +176,8 @@ values 20 "{(n, m). tranclp succ n m}" *) +subsection{* *} + subsection{* IMP *} types