--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:40 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:42 2009 +0200
@@ -210,7 +210,7 @@
let
fun mk_prems' (t as Const (name, T)) (names, prems) =
if is_constr thy name orelse (is_none (try lookup_pred t)) then
- [(t ,(names, prems))]
+ [(t, (names, prems))]
else [(lookup_pred t, (names, prems))]
| mk_prems' (t as Free (f, T)) (names, prems) =
[(lookup_pred t, (names, prems))]
@@ -243,7 +243,8 @@
maps mk_prems_of_assm assms
end
else
- let
+ let
+ val _ = tracing ("Flattening term " ^ (Syntax.string_of_term_global thy t))
val (f, args) = strip_comb t
val resname = Name.variant names "res"
val resvar = Free (resname, body_type (fastype_of t))
@@ -281,7 +282,15 @@
val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
in (names', prem :: prems') end)
end
- | mk_prems'' t = error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
+ | mk_prems'' t =
+ let
+ val _ = tracing ("must define new constant for "
+ ^ (Syntax.string_of_term_global thy t))
+ in
+ (*if is_predT (fastype_of t) then
+ else*)
+ error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
+ end
in
map (pair resvar) (mk_prems'' f)
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:40 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200
@@ -10,6 +10,9 @@
structure Predicate_Compile : PREDICATE_COMPILE =
struct
+(* options *)
+val fail_safe_mode = false
+
open Predicate_Compile_Aux;
val priority = tracing;
@@ -39,9 +42,11 @@
val _ = priority "Replacing functions in introrules..."
(* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *)
val intross' =
- 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
+ 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
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'
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:40 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200
@@ -120,11 +120,18 @@
fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
-fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
+fun print_tac s = Seq.single;
fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
val do_proofs = Unsynchronized.ref true;
+datatype assertion = Max_number_of_subgoals of int
+fun assert_tac (Max_number_of_subgoals i) st =
+ if (nprems_of st <= i) then Seq.single st
+ else error ("assert_tac: Numbers of subgoals mismatch at goal state :"
+ ^ "\n" ^ Pretty.string_of (Pretty.chunks
+ (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
+
(* reference to preprocessing of InductiveSet package *)
val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*)
@@ -1433,7 +1440,7 @@
(u, rest)
end
in
- compile_match thy compfuns constr_vs' eqs out_ts''
+ compile_match thy compfuns constr_vs' eqs out_ts''
(mk_bind compfuns (compiled_clause, rest))
end
val prem_t = compile_prems in_ts' param_vs all_vs' moded_ps;
@@ -1914,10 +1921,15 @@
| _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
val (_, ts) = strip_comb t
in
- (Splitter.split_asm_tac split_rules 1)
-(* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
- THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *)
+ (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^
+ "splitting with rules \n" ^
+ commas (map (Display.string_of_thm_global thy) split_rules)))
+ THEN (Splitter.split_asm_tac split_rules 1)
+ THEN (print_tac "after splitting with split_asm rules")
+ (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
+ THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))
+ THEN (assert_tac (Max_number_of_subgoals 2))
THEN (EVERY (map split_term_tac ts))
end
else all_tac
@@ -2241,9 +2253,11 @@
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' (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy)
+ intro_t' tac
end
(** main function of predicate compiler **)
--- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:40 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
@@ -333,7 +333,7 @@
code_pred (inductify_all) S\<^isub>1p .
thm S\<^isub>1p.equation
-
+(*
theorem S\<^isub>1_sound:
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[generator=pred_compile]
@@ -375,6 +375,12 @@
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
quickcheck[size=10, generator = pred_compile]
oops
+*)
+inductive test
+where
+ "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] ==> test w"
+ML {* @{term "[x \<leftarrow> w. x = a]"} *}
+code_pred (inductify_all) test .
theorem S\<^isub>3_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"