--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 29 11:02:24 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 29 11:36:16 2010 +0200
@@ -1511,6 +1511,32 @@
thm test_uninterpreted_relation.equation
+inductive list_ex'
+where
+ "P x ==> list_ex' P (x#xs)"
+| "list_ex' P xs ==> list_ex' P (x#xs)"
+
+code_pred list_ex' .
+
+inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
+where
+ "list_ex r xs ==> test_uninterpreted_relation2 r xs"
+| "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
+
+text {* Proof procedure cannot handle this situation yet. *}
+
+code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
+
+thm test_uninterpreted_relation2.equation
+
+
+text {* Trivial predicate *}
+
+inductive implies_itself :: "'a => bool"
+where
+ "implies_itself x ==> implies_itself x"
+
+code_pred implies_itself .
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 29 11:02:24 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 29 11:36:16 2010 +0200
@@ -145,6 +145,7 @@
(* conversions *)
val imp_prems_conv : conv -> conv
(* simple transformations *)
+ val split_conjuncts_in_assms : Proof.context -> thm -> thm
val expand_tuples : theory -> thm -> thm
val eta_contract_ho_arguments : theory -> thm -> thm
val remove_equalities : theory -> thm -> thm
@@ -821,6 +822,19 @@
val (_, args) = strip_comb atom
in rewrite_args args end
+fun split_conjuncts_in_assms ctxt th =
+ let
+ val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt
+ fun split_conjs i nprems th =
+ if i > nprems then th
+ else
+ case try Drule.RSN (@{thm conjI}, (i, th)) of
+ SOME th' => split_conjs i (nprems+1) th'
+ | NONE => split_conjs (i+1) nprems th
+ in
+ singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
+ end
+
fun expand_tuples thy intro =
let
val ctxt = ProofContext.init_global thy
@@ -840,9 +854,7 @@
(HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
intro'''
(* splitting conjunctions introduced by Pair_eq*)
- fun split_conj prem =
- map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
- val intro''''' = map_term thy (maps_premises split_conj) intro''''
+ val intro''''' = split_conjuncts_in_assms ctxt intro''''
in
intro'''''
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 29 11:02:24 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 29 11:36:16 2010 +0200
@@ -1696,7 +1696,13 @@
ctxt name mode,
Comp_Mod.funT_of compilation_modifiers mode T)))
| (Free (s, T), Context m) =>
- SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+ (case (AList.lookup (op =) param_modes s) of
+ SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+ | NONE =>
+ let
+ val bs = map (pair "x") (binder_types (fastype_of t))
+ val bounds = map Bound (rev (0 upto (length bs) - 1))
+ in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end)
| (t, Context m) =>
let
val bs = map (pair "x") (binder_types (fastype_of t))
@@ -2556,15 +2562,17 @@
THEN (etac @{thm singleE} 1)
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac HOL_basic_ss' 1)
- THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
- THEN (asm_full_simp_tac HOL_basic_ss' 1)
- THEN SOLVED (print_tac options "state before applying intro rule:"
- THEN (rtac pred_intro_rule
- (* How to handle equality correctly? *)
- THEN_ALL_NEW (K (print_tac options "state before assumption matching")
- THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
- THEN' (K (print_tac options "state after pre-simplification:"))
- THEN' (K (print_tac options "state after assumption matching:")))) 1)
+ THEN TRY (
+ (REPEAT_DETERM (etac @{thm Pair_inject} 1))
+ THEN (asm_full_simp_tac HOL_basic_ss' 1)
+
+ THEN SOLVED (print_tac options "state before applying intro rule:"
+ THEN (rtac pred_intro_rule
+ (* How to handle equality correctly? *)
+ THEN_ALL_NEW (K (print_tac options "state before assumption matching")
+ THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
+ THEN' (K (print_tac options "state after pre-simplification:"))
+ THEN' (K (print_tac options "state after assumption matching:")))) 1))
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
val mode = head_mode_of deriv
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Sep 29 11:02:24 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Sep 29 11:36:16 2010 +0200
@@ -256,34 +256,18 @@
#> Conv.fconv_rule nnf_conv
#> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
-fun split_conjs thy t =
- let
- fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
- (split_conjunctions t1) @ (split_conjunctions t2)
- | split_conjunctions t = [t]
- in
- map HOLogic.mk_Trueprop (split_conjunctions (HOLogic.dest_Trueprop t))
- end
-
fun rewrite_intros thy =
Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
#> Simplifier.full_simplify
(HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
- #> map_term thy (maps_premises (split_conjs thy))
+ #> split_conjuncts_in_assms (ProofContext.init_global thy)
fun print_specs options thy msg ths =
if show_intermediate_results options then
(tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
else
()
-(*
-fun split_cases thy th =
- let
-
- in
- map_term thy th
- end
-*)
+
fun preprocess options (constname, specs) thy =
(* case Predicate_Compile_Data.processed_specs thy constname of
SOME specss => (specss, thy)
@@ -292,7 +276,7 @@
val ctxt = ProofContext.init_global thy
val intros =
if forall is_pred_equation specs then
- map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
+ map (split_conjuncts_in_assms ctxt) (introrulify thy (map rewrite specs))
else if forall (is_intro constname) specs then
map (rewrite_intros thy) specs
else