--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 23 16:20:13 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 23 16:20:13 2009 +0200
@@ -125,12 +125,6 @@
val do_proofs = ref true;
-fun mycheat_tac thy i st =
- (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
-
-fun remove_last_goal thy st =
- (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
-
(* reference to preprocessing of InductiveSet package *)
val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*)
@@ -2119,7 +2113,7 @@
THEN print_tac "proved one direction"
THEN prove_other_direction thy modes pred mode moded_clauses
THEN print_tac "proved other direction")
- else (fn _ => mycheat_tac thy 1))
+ else (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy))
end;
(* composition of mode inference, definition, compilation and proof *)
--- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:13 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:13 2009 +0200
@@ -317,7 +317,6 @@
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
-ML {* reset Predicate_Compile_Core.do_proofs *}
(*
code_pred (inductify_all) S\<^isub>3 .
*)
@@ -348,19 +347,19 @@
theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[generator = pred_compile, size=2, iterations=1]
-sorry
+oops
theorem S\<^isub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
quickcheck[generator = pred_compile, size=5, iterations=1]
-sorry
+oops
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
(*quickcheck[generator = pred_compile, size=5, iterations=1]*)
-sorry
+oops
section {* Lambda *}
@@ -432,8 +431,6 @@
thm test.equation
*)
-ML {*set Toplevel.debug *}
-
lemma filter_eq_ConsD:
"filter P ys = x#xs \<Longrightarrow>
\<exists>us vs. ys = ts @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"