# HG changeset patch
# User bulwahn
# Date 1253715613 -7200
# Node ID d5db9cf8540145ae4843bcb2a72bc10c2dfb132c
# Parent  90f3ce5d27ae85d65e6aa12200c51f3824040aad
replaced sorry by oops; removed old debug functions in predicate compiler

diff -r 90f3ce5d27ae -r d5db9cf85401 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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 *)
diff -r 90f3ce5d27ae -r d5db9cf85401 src/HOL/ex/Predicate_Compile_ex.thy
--- 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"