# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID bf18c8174571b6244f2e8236927c168d2ca5bbe3 # Parent 973d18ad2a738f3400eecb6ff9d57ac01fd9c4d0 added theory with alternative definitions for the predicate compiler; cleaned up examples diff -r 973d18ad2a73 -r bf18c8174571 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 @@ -129,8 +129,10 @@ fun store_thm_in_table ignore_consts thy th= let - val th = AxClass.unoverload thy th + val th = th |> inline_equations thy + |> Pred_Compile_Set.unfold_set_notation + |> AxClass.unoverload thy val (const, th) = if is_equationlike th then let @@ -139,9 +141,7 @@ in (defining_const_of_equation eq, eq) end - else if (is_introlike th) then - let val th = Pred_Compile_Set.unfold_set_notation th - in (defining_const_of_introrule th, th) end + else if (is_introlike th) then (defining_const_of_introrule th, th) else error "store_thm: unexpected definition format" in if not (member (op =) ignore_consts const) then @@ -191,7 +191,9 @@ val logic_operator_names = [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "op &"}] -val special_cases = member (op =) [@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat}, +val special_cases = member (op =) [ + @{const_name "False"}, + @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat}, @{const_name Nat.one_nat_inst.one_nat}, @{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"}, @{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus}, diff -r 973d18ad2a73 -r bf18c8174571 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,8 @@ 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}, @{thm Bex_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 973d18ad2a73 -r bf18c8174571 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,52 +14,4 @@ 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 973d18ad2a73 -r bf18c8174571 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 @@ -54,7 +54,8 @@ value [code] "Predicate.the (append_3 ([]::int list))" subsection {* Tricky case with alternative rules *} - +text {* This cannot be handled correctly yet *} +(* inductive append2 where "append2 [] xs xs" @@ -70,7 +71,7 @@ case append2 from append2.cases[OF append2(1)] append2(2-3) show thesis by blast qed - +*) subsection {* Tricky cases with tuples *} inductive tupled_append :: "'a list \ 'a list \ 'a list \ bool" @@ -370,10 +371,10 @@ code_pred (inductify_all) avl . thm avl.equation - +(* lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\(y::'a::type). False)" unfolding bot_fun_inst.bot_fun[symmetric] bot_bool_eq[symmetric] bot_fun_eq by simp - +*) fun set_of where "set_of ET = {}" @@ -384,9 +385,31 @@ "is_ord ET = True" | "is_ord (MKT n l r h) = ((\n' \ set_of l. n' < n) \ (\n' \ set_of r. n < n') \ is_ord l \ is_ord r)" +(* +lemma empty_set[code_pred_def]: "{} = (\x. False)" unfolding empty_def by simp +thm set_of.simps[unfolded empty_set Un_def] +*) +(* +declare empty_def[code_pred_def] +*) +ML {* prop_of (@{thm set_of.simps(1)}) *} +thm Un_def +thm eq_refl +declare eq_reflection[OF empty_def, code_pred_inline] +thm Un_def +definition Un' where "Un' A B == A Un B" -declare Un_def[code_pred_def] +lemma [code_pred_intros]: "A x ==> Un' A B x" +and [code_pred_intros] : "B x ==> Un' A B x" +sorry + +code_pred Un' sorry +lemmas a = Un'_def[symmetric] +declare a[code_pred_inline] +declare set_of.simps +ML {* prop_of @{thm Un_def} *} +ML {* tap *} code_pred (inductify_all) set_of . thm set_of.equation (* FIXME *) @@ -429,6 +452,8 @@ code_pred (inductify_all) List.rev . thm revP.equation +section {* Handling set operations *} + section {* Context Free Grammar *}